From: Marion Guthmuller Date: Tue, 20 Nov 2012 18:10:02 +0000 (+0100) Subject: model-checker : new tesh for snapshot comparison tests X-Git-Tag: v3_9_rc1~91^2~59 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/1619b56e8f7f377298f37c4004406c0aab78a151 model-checker : new tesh for snapshot comparison tests --- diff --git a/buildtools/Cmake/AddTests.cmake b/buildtools/Cmake/AddTests.cmake index 224e0dc9c5..8a820de15e 100644 --- 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 7f08a4c91e..9a246b799c 100644 --- 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 5341091988..982b1466ee 100644 --- 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 index 0000000000..a2f0e014cc --- /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 e81f3f8a65..e3b04b03e4 100644 --- a/examples/msg/mc/test/snapshot_comparison_liveness2.c +++ b/examples/msg/mc/test/snapshot_comparison2.c @@ -8,7 +8,7 @@ #include #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 index 0000000000..b1e8aab547 --- /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 27703a7a4c..8c3efd3a67 100644 --- a/examples/msg/mc/test/snapshot_comparison_liveness3.c +++ b/examples/msg/mc/test/snapshot_comparison3.c @@ -8,7 +8,7 @@ #include #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 index 0000000000..224e513040 --- /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 9c38d3072c..e87c65c0ce 100644 --- a/examples/msg/mc/test/snapshot_comparison_liveness4.c +++ b/examples/msg/mc/test/snapshot_comparison4.c @@ -8,7 +8,7 @@ #include #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 index 0000000000..8485829f1b --- /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 e8054f7e72..eef83c8651 100644 --- a/examples/msg/mc/test/snapshot_comparison_liveness5.c +++ b/examples/msg/mc/test/snapshot_comparison5.c @@ -8,7 +8,7 @@ #include #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 index 0000000000..3ba1819976 --- /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