From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Mon, 30 Sep 2013 15:40:08 +0000 (+0200)
Subject: model-checker : update Changelog
X-Git-Tag: v3_9_90~60^2~11
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/1f041a309f67456d9f3e473030dbbd02ef8af33d

model-checker : update Changelog
---

diff --git a/ChangeLog b/ChangeLog
index 0c9a927659..5a9de9e9f1 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -40,6 +40,15 @@ SimGrid (3.10) NOT RELEASED; urgency=low
  * Add all missing Fortran bindings, SMPI should work with Fortran 90
    (no privatization of global variables yet)
 
+ Model-Checking;
+ * Verification of liveness properties is now available
+    for SMPI applications (in addition to MSG applications)
+ * Bugged examples using SMPI in examples/smpi/mc/
+ * Add --cfg=model-check/visited option. Allows the verification of
+    infinite programs. Detection of loops in the execution thanks to the system
+    state comparison and reduction of the state space to explore. Can
+    be combined with DPOR for safety properties. 	
+
  SimDag:
  * Allow to change SimGrid configuration (see --help) within the code
    thanks to SD_config() as it can be done in MSG.