From: cristianrosa <cristianrosa@48e7efb5-ca39-0410-a469-dd3cf9ba447f>
Date: Mon, 17 May 2010 14:29:54 +0000 (+0000)
Subject: Initial FAQ section for using the model-checking mode.
X-Git-Tag: v3_5~1055
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/e5ada3ddb334e4c38537badb9beb35e16cdbd630

Initial FAQ section for using the model-checking mode.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/simgrid/simgrid/trunk@7753 48e7efb5-ca39-0410-a469-dd3cf9ba447f
---

diff --git a/doc/FAQ.doc b/doc/FAQ.doc
index 5f82438241..0014620cd6 100644
--- a/doc/FAQ.doc
+++ b/doc/FAQ.doc
@@ -2073,6 +2073,18 @@ $ defaults write Triva 'bcompute Color' '1 0 0'
 \endverbatim
 Where the three numbers in each line are the RGB color with values from 0 to 1.
 
+\subsection faq_modelchecking Model-Checking
+\subsubsection faq_modelchecking_howto How to use it
+To enable the experimental SimGrid model-checking support the program should
+be executed with the command line argument 
+\verbatim
+--cfg=model-check:1 
+\endverbatim
+Properties are expressed as assertions using the function
+\verbatim
+void MC_assert(int prop);
+\endverbatim
+
 \section faq_troubleshooting Troubleshooting
 
 \subsection faq_trouble_lib_compil SimGrid compilation and installation problems