model-checker : new tesh for snapshot comparison tests

diff --git a/buildtools/Cmake/AddTests.cmake b/buildtools/Cmake/AddTests.cmake
index 224e0dc..8a820de 100644 (file)
--- a/buildtools/Cmake/AddTests.cmake
+++ b/buildtools/Cmake/AddTests.cmake
@@ -524,6 +524,11 @@ if(NOT enable_memcheck)
       ADD_TEST(mc-centralized-ucontext          ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc centralized.tesh)
       ADD_TEST(mc-bugged1-liveness-ucontext     ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc bugged1_liveness.tesh)
       ADD_TEST(mc-chord-neverjoin-ucontext      ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc/chord --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc/chord chord_neverjoin.tesh)
+      ADD_TEST(mc-test-snapshot-comparison1     ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc/test --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc/test snapshot_comparison1.tesh)
+      ADD_TEST(mc-test-snapshot-comparison2     ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc/test --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc/test snapshot-comparison2.tesh)
+      ADD_TEST(mc-test-snapshot-comparison3     ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc/test --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc/test snapshot_comparison3.tesh)
+      ADD_TEST(mc-test-snapshot-comparison4     ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc/test --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc/test snapshot_comparison4.tesh)
+      ADD_TEST(mc-test-snapshot-comparison5     ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc/test --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc/test snapshot_comparison5.tesh)
     endif()
     if(HAVE_RAWCTX)
       ADD_TEST(mc-bugged1-raw                   ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:raw --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc bugged1.tesh)

diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt
index 7f08a4c..9a246b7 100644 (file)
--- a/examples/msg/mc/CMakeLists.txt
+++ b/examples/msg/mc/CMakeLists.txt
@@ -14,11 +14,11 @@ if(HAVE_MC)
   add_executable(bugged1_liveness bugged1_liveness.c)
   add_executable(bugged2_liveness bugged2_liveness.c)
   add_executable(chord/chord_liveness chord/chord_liveness.c)
-  add_executable(test/snapshot_comparison_liveness1 test/snapshot_comparison_liveness1.c)
-  add_executable(test/snapshot_comparison_liveness2 test/snapshot_comparison_liveness2.c)
-  add_executable(test/snapshot_comparison_liveness3 test/snapshot_comparison_liveness3.c)
-  add_executable(test/snapshot_comparison_liveness4 test/snapshot_comparison_liveness4.c)
-  add_executable(test/snapshot_comparison_liveness5 test/snapshot_comparison_liveness5.c)
+  add_executable(test/snapshot_comparison1 test/snapshot_comparison1.c)
+  add_executable(test/snapshot_comparison2 test/snapshot_comparison2.c)
+  add_executable(test/snapshot_comparison3 test/snapshot_comparison3.c)
+  add_executable(test/snapshot_comparison4 test/snapshot_comparison4.c)
+  add_executable(test/snapshot_comparison5 test/snapshot_comparison5.c)
 
   target_link_libraries(centralized simgrid m )
   target_link_libraries(bugged1     simgrid m )
@@ -28,11 +28,11 @@ if(HAVE_MC)
   target_link_libraries(bugged1_liveness     simgrid m )
   target_link_libraries(bugged2_liveness     simgrid m )
   target_link_libraries(chord/chord_liveness     simgrid m )
-  target_link_libraries(test/snapshot_comparison_liveness1     simgrid m )
-  target_link_libraries(test/snapshot_comparison_liveness2     simgrid m )
-  target_link_libraries(test/snapshot_comparison_liveness3     simgrid m )
-  target_link_libraries(test/snapshot_comparison_liveness4     simgrid m )
-  target_link_libraries(test/snapshot_comparison_liveness5     simgrid m )
+  target_link_libraries(test/snapshot_comparison1     simgrid m )
+  target_link_libraries(test/snapshot_comparison2     simgrid m )
+  target_link_libraries(test/snapshot_comparison3     simgrid m )
+  target_link_libraries(test/snapshot_comparison4     simgrid m )
+  target_link_libraries(test/snapshot_comparison5     simgrid m )
 
 endif()
 
@@ -70,11 +70,11 @@ set(examples_src
   ${CMAKE_CURRENT_SOURCE_DIR}/bugged2_liveness.h
   ${CMAKE_CURRENT_SOURCE_DIR}/chord/chord_liveness.c
   ${CMAKE_CURRENT_SOURCE_DIR}/chord/chord_liveness.h
-  ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness1.c
-  ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness2.c
-  ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness3.c
-  ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness4.c
-  ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness5.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison1.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison2.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison3.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison4.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison5.c
   PARENT_SCOPE
   )
 set(bin_files

diff --git a/examples/msg/mc/test/snapshot_comparison_liveness1.c b/examples/msg/mc/test/snapshot_comparison1.c
similarity index 91%
rename from examples/msg/mc/test/snapshot_comparison_liveness1.c
rename to examples/msg/mc/test/snapshot_comparison1.c
index 5341091..982b146 100644 (file)
--- a/examples/msg/mc/test/snapshot_comparison_liveness1.c
+++ b/examples/msg/mc/test/snapshot_comparison1.c
@@ -21,15 +21,17 @@ int test(int argc, char **argv){
 
   void *snap1 = MC_snapshot();
 
+  XBT_INFO("First snapshot");
+
   MSG_process_sleep(1);
   
   void *snap2 = MC_snapshot();
 
   MSG_process_sleep(1);
-  
-  int res = MC_compare_snapshots(snap1, snap2);
 
-  XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", res);
+  XBT_INFO("Second snapshot");
+
+  XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
   
   XBT_INFO("**** End test ****");
 

diff --git a/examples/msg/mc/test/snapshot_comparison1.tesh b/examples/msg/mc/test/snapshot_comparison1.tesh
new file mode 100644 (file)
index 0000000..a2f0e01
--- /dev/null
+++ b/examples/msg/mc/test/snapshot_comparison1.tesh
@@ -0,0 +1,26 @@
+#! ./tesh
+
+! expect signal SIGABRT
+! timeout 60
+$ ${bindir:=.}/snapshot_comparison1 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
+> [  0.000000] (0:@) Configuration change: Set 'model-check' to '1'
+> [  0.000000] (0:@) type in variable = 2
+> [  0.000000] (0:@) Check the liveness property promela
+> [  1.000000] (1:test@HostA) **** Start test ****
+> [  1.000000] (1:test@HostA) Take two successive snapshots (No modification)
+> [  1.000000] (1:test@HostA) First snapshot
+> [  3.000000] (1:test@HostA) Second snapshot
+> [  3.000000] (1:test@HostA) Test result : 0 (0 = state equality, 1 = different states)
+> [  3.000000] (1:test@HostA) **** End test ****
+> [  0.000000] (0:@) Next pair (depth = 5) already reached !
+> [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
+> [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [  0.000000] (0:@) Counter-example that violates formula :
+> [  0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [  0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [  0.000000] (0:@) [(1)test] MC_COMPARE_SNAPSHOTS ((null))
+> [  0.000000] (0:@) End of system requests but evolution in Büchi automaton
+> [  0.000000] (0:@) Expanded pairs = 5
+> [  0.000000] (0:@) Visited pairs = 4
+> [  0.000000] (0:@) Expanded / Visited = 0.800000

diff --git a/examples/msg/mc/test/snapshot_comparison_liveness2.c b/examples/msg/mc/test/snapshot_comparison2.c
similarity index 87%
rename from examples/msg/mc/test/snapshot_comparison_liveness2.c
rename to examples/msg/mc/test/snapshot_comparison2.c
index e81f3f8..e3b04b0 100644 (file)
--- a/examples/msg/mc/test/snapshot_comparison_liveness2.c
+++ b/examples/msg/mc/test/snapshot_comparison2.c
@@ -8,7 +8,7 @@
 #include <simgrid/modelchecker.h>
 #include "mc/mc.h"
 
-XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness2, "Debug information for snasphot comparison liveness1 test example");
+XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness2, "Debug information for snasphot comparison liveness2 test example");
 
 int test(int argc, char **argv);
 
@@ -23,6 +23,8 @@ int test(int argc, char **argv){
 
   MSG_process_sleep(1);
 
+  XBT_INFO("First snapshot");
+
   char *toto = xbt_malloc(5);
   XBT_INFO("Toto allocated");
 
@@ -30,9 +32,9 @@ int test(int argc, char **argv){
 
   MSG_process_sleep(1);
 
-  int res = MC_compare_snapshots(snap1, snap2);
+  XBT_INFO("Second snapshot");
 
-  XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", res);
+  XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
   
   XBT_INFO("**** End test ****");
 

diff --git a/examples/msg/mc/test/snapshot_comparison2.tesh b/examples/msg/mc/test/snapshot_comparison2.tesh
new file mode 100644 (file)
index 0000000..b1e8aab
--- /dev/null
+++ b/examples/msg/mc/test/snapshot_comparison2.tesh
@@ -0,0 +1,27 @@
+#! ./tesh
+
+! expect signal SIGABRT
+! timeout 60
+$ ${bindir:=.}/snapshot_comparison2 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
+> [  0.000000] (0:@) Configuration change: Set 'model-check' to '1'
+> [  0.000000] (0:@) type in variable = 2
+> [  0.000000] (0:@) Check the liveness property promela
+> [  1.000000] (1:test@HostA) **** Start test ****
+> [  1.000000] (1:test@HostA) Malloc after first snapshot
+> [  2.000000] (1:test@HostA) First snapshot
+> [  2.000000] (1:test@HostA) Toto allocated
+> [  3.000000] (1:test@HostA) Second snapshot
+> [  3.000000] (1:test@HostA) Test result : 1 (0 = state equality, 1 = different states)
+> [  3.000000] (1:test@HostA) **** End test ****
+> [  0.000000] (0:@) Next pair (depth = 5) already reached !
+> [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
+> [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [  0.000000] (0:@) Counter-example that violates formula :
+> [  0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [  0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [  0.000000] (0:@) [(1)test] MC_COMPARE_SNAPSHOTS ((null))
+> [  0.000000] (0:@) End of system requests but evolution in Büchi automaton
+> [  0.000000] (0:@) Expanded pairs = 5
+> [  0.000000] (0:@) Visited pairs = 4
+> [  0.000000] (0:@) Expanded / Visited = 0.800000

diff --git a/examples/msg/mc/test/snapshot_comparison_liveness3.c b/examples/msg/mc/test/snapshot_comparison3.c
similarity index 91%
rename from examples/msg/mc/test/snapshot_comparison_liveness3.c
rename to examples/msg/mc/test/snapshot_comparison3.c
index 27703a7..8c3efd3 100644 (file)
--- a/examples/msg/mc/test/snapshot_comparison_liveness3.c
+++ b/examples/msg/mc/test/snapshot_comparison3.c
@@ -8,7 +8,7 @@
 #include <simgrid/modelchecker.h>
 #include "mc/mc.h"
 
-XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness3, "Debug information for snasphot comparison liveness1 test example");
+XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness3, "Debug information for snasphot comparison liveness3 test example");
 
 int test(int argc, char **argv);
 
@@ -25,6 +25,8 @@ int test(int argc, char **argv){
 
   MSG_process_sleep(1);
 
+  XBT_INFO("First snapshot");
+
   toto = xbt_malloc(5);
   XBT_INFO("Toto allocated");
   xbt_free(toto);
@@ -35,6 +37,8 @@ int test(int argc, char **argv){
 
   void *snap2 = MC_snapshot();
 
+  XBT_INFO("Second snapshot");
+
   MC_ignore_stack("snap2", "test");   
   MC_ignore_stack("snap1", "test");
 

diff --git a/examples/msg/mc/test/snapshot_comparison3.tesh b/examples/msg/mc/test/snapshot_comparison3.tesh
new file mode 100644 (file)
index 0000000..224e513
--- /dev/null
+++ b/examples/msg/mc/test/snapshot_comparison3.tesh
@@ -0,0 +1,28 @@
+#! ./tesh
+
+! expect signal SIGABRT
+! timeout 60
+$ ${bindir:=.}/snapshot_comparison3 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
+> [  0.000000] (0:@) Configuration change: Set 'model-check' to '1'
+> [  0.000000] (0:@) type in variable = 2
+> [  0.000000] (0:@) Check the liveness property promela
+> [  1.000000] (1:test@HostA) **** Start test ****
+> [  1.000000] (1:test@HostA) Malloc and free after first snapshot
+> [  2.000000] (1:test@HostA) First snapshot
+> [  2.000000] (1:test@HostA) Toto allocated
+> [  2.000000] (1:test@HostA) Toto free
+> [  3.000000] (1:test@HostA) Second snapshot
+> [  3.000000] (1:test@HostA) Test result : 0 (0 = state equality, 1 = different states)
+> [  3.000000] (1:test@HostA) **** End test ****
+> [  0.000000] (0:@) Next pair (depth = 5) already reached !
+> [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
+> [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [  0.000000] (0:@) Counter-example that violates formula :
+> [  0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [  0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [  0.000000] (0:@) [(1)test] MC_COMPARE_SNAPSHOTS ((null))
+> [  0.000000] (0:@) End of system requests but evolution in Büchi automaton
+> [  0.000000] (0:@) Expanded pairs = 5
+> [  0.000000] (0:@) Visited pairs = 4
+> [  0.000000] (0:@) Expanded / Visited = 0.800000

diff --git a/examples/msg/mc/test/snapshot_comparison_liveness4.c b/examples/msg/mc/test/snapshot_comparison4.c
similarity index 91%
rename from examples/msg/mc/test/snapshot_comparison_liveness4.c
rename to examples/msg/mc/test/snapshot_comparison4.c
index 9c38d30..e87c65c 100644 (file)
--- a/examples/msg/mc/test/snapshot_comparison_liveness4.c
+++ b/examples/msg/mc/test/snapshot_comparison4.c
@@ -8,7 +8,7 @@
 #include <simgrid/modelchecker.h>
 #include "mc/mc.h"
 
-XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness4, "Debug information for snasphot comparison liveness1 test example");
+XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness4, "Debug information for snasphot comparison liveness4 test example");
 
 int test(int argc, char **argv);
 
@@ -26,11 +26,15 @@ int test(int argc, char **argv){
 
   MSG_process_sleep(1);
 
+  XBT_INFO("First snapshot");
+
   xbt_free(toto);
   XBT_INFO("Toto free");
 
   void *snap2 = MC_snapshot();
 
+  XBT_INFO("Second snapshot");
+
   MSG_process_sleep(1);
   
   MC_ignore_stack("snap2", "test");   

diff --git a/examples/msg/mc/test/snapshot_comparison4.tesh b/examples/msg/mc/test/snapshot_comparison4.tesh
new file mode 100644 (file)
index 0000000..8485829
--- /dev/null
+++ b/examples/msg/mc/test/snapshot_comparison4.tesh
@@ -0,0 +1,28 @@
+#! ./tesh
+
+! expect signal SIGABRT
+! timeout 60
+$ ${bindir:=.}/snapshot_comparison4 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
+> [  0.000000] (0:@) Configuration change: Set 'model-check' to '1'
+> [  0.000000] (0:@) type in variable = 2
+> [  0.000000] (0:@) Check the liveness property promela
+> [  1.000000] (1:test@HostA) **** Start test ****
+> [  1.000000] (1:test@HostA) Free after first snapshot
+> [  1.000000] (1:test@HostA) Toto allocated
+> [  2.000000] (1:test@HostA) First snapshot
+> [  2.000000] (1:test@HostA) Toto free
+> [  2.000000] (1:test@HostA) Second snapshot
+> [  3.000000] (1:test@HostA) Test result : 1 (0 = state equality, 1 = different states)
+> [  3.000000] (1:test@HostA) **** End test ****
+> [  0.000000] (0:@) Next pair (depth = 5) already reached !
+> [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
+> [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [  0.000000] (0:@) Counter-example that violates formula :
+> [  0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [  0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [  0.000000] (0:@) [(1)test] MC_COMPARE_SNAPSHOTS ((null))
+> [  0.000000] (0:@) End of system requests but evolution in Büchi automaton
+> [  0.000000] (0:@) Expanded pairs = 5
+> [  0.000000] (0:@) Visited pairs = 4
+> [  0.000000] (0:@) Expanded / Visited = 0.800000
\ No newline at end of file

diff --git a/examples/msg/mc/test/snapshot_comparison_liveness5.c b/examples/msg/mc/test/snapshot_comparison5.c
similarity index 91%
rename from examples/msg/mc/test/snapshot_comparison_liveness5.c
rename to examples/msg/mc/test/snapshot_comparison5.c
index e8054f7..eef83c8 100644 (file)
--- a/examples/msg/mc/test/snapshot_comparison_liveness5.c
+++ b/examples/msg/mc/test/snapshot_comparison5.c
@@ -8,7 +8,7 @@
 #include <simgrid/modelchecker.h>
 #include "mc/mc.h"
 
-XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness5, "Debug information for snasphot comparison liveness1 test example");
+XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness5, "Debug information for snasphot comparison liveness5 test example");
 
 int test(int argc, char **argv);
 
@@ -26,6 +26,8 @@ int test(int argc, char **argv){
 
   MSG_process_sleep(1);
 
+  XBT_INFO("First snapshot");
+
   j = 1;
   XBT_INFO("j = %d", j);
  
@@ -33,6 +35,8 @@ int test(int argc, char **argv){
 
   MSG_process_sleep(1);
 
+  XBT_INFO("Second snapshot");
+
   MC_ignore_stack("snap2", "test");   
   MC_ignore_stack("snap1", "test");
 

diff --git a/examples/msg/mc/test/snapshot_comparison5.tesh b/examples/msg/mc/test/snapshot_comparison5.tesh
new file mode 100644 (file)
index 0000000..3ba1819
--- /dev/null
+++ b/examples/msg/mc/test/snapshot_comparison5.tesh
@@ -0,0 +1,28 @@
+#! ./tesh
+
+! expect signal SIGABRT
+! timeout 60
+$ ${bindir:=.}/snapshot_comparison5 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
+> [  0.000000] (0:@) Configuration change: Set 'model-check' to '1'
+> [  0.000000] (0:@) type in variable = 2
+> [  0.000000] (0:@) Check the liveness property promela
+> [  1.000000] (1:test@HostA) **** Start test ****
+> [  1.000000] (1:test@HostA) Increment local variable
+> [  1.000000] (1:test@HostA) j = 0
+> [  2.000000] (1:test@HostA) First snapshot
+> [  2.000000] (1:test@HostA) j = 1
+> [  3.000000] (1:test@HostA) Second snapshot
+> [  3.000000] (1:test@HostA) Test result : 1 (0 = state equality, 1 = different states)
+> [  3.000000] (1:test@HostA) **** End test ****
+> [  0.000000] (0:@) Next pair (depth = 5) already reached !
+> [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
+> [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [  0.000000] (0:@) Counter-example that violates formula :
+> [  0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [  0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [  0.000000] (0:@) [(1)test] MC_COMPARE_SNAPSHOTS ((null))
+> [  0.000000] (0:@) End of system requests but evolution in Büchi automaton
+> [  0.000000] (0:@) Expanded pairs = 5
+> [  0.000000] (0:@) Visited pairs = 4
+> [  0.000000] (0:@) Expanded / Visited = 0.800000