From: Marion Guthmuller Date: Mon, 29 Apr 2013 11:30:41 +0000 (+0200) Subject: model-checker : cleanups in tesh examples X-Git-Tag: v3_9_90~407^2 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/7f2b2cb65aff6ae1fe4ba58b721e48d2b9149d53 model-checker : cleanups in tesh examples - rename directory: chord_liveness -> chord - add tesh for bugged2 - remove broken tests snapshot_comparison* - neverJoin in Chord is a safety property, not a liveness property --- diff --git a/buildtools/Cmake/AddTests.cmake b/buildtools/Cmake/AddTests.cmake index 55ef3ea74c..af482aa4d3 100644 --- a/buildtools/Cmake/AddTests.cmake +++ b/buildtools/Cmake/AddTests.cmake @@ -445,24 +445,22 @@ if(NOT enable_memcheck) if(HAVE_MC) ADD_TEST(mc-bugged1-thread ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:thread --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc bugged1.tesh) ADD_TEST(mc-centralized-thread ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:thread --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc centralized.tesh) + ADD_TEST(mc-chord-neverjoin-thread ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:thread --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc/chord --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc/chord chord_neverjoin.tesh) if(CONTEXT_UCONTEXT) ADD_TEST(mc-bugged1-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.tesh) + ADD_TEST(mc-bugged2-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 bugged2.tesh) 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-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) if(PROCESSOR_x86_64) # liveness model-checking works only on 64bits (for now ...) 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_liveness --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc/chord_liveness chord_neverjoin.tesh) - ADD_TEST(mc-chord-neverdeliver-ucontext ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc/chord_liveness --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc/chord_liveness chord_neverdeliver.tesh) - ADD_TEST(mc-chord-neverjoin-timeout-visited-ucontext ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc/chord_liveness --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc/chord_liveness chord_neverjoin_timeout_visited.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) + ADD_TEST(mc-chord-neverjoin-timeout-visited-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_timeout_visited.tesh) endif() 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) + ADD_TEST(mc-bugged2-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 bugged2.tesh) ADD_TEST(mc-centralized-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 centralized.tesh) + ADD_TEST(mc-chord-neverjoin-raw ${CMAKE_BINARY_DIR}/bin/tesh ${TESH_OPTION} --cfg contexts/factory:raw --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc/chord --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc/chord chord_neverjoin.tesh) endif() endif() diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt index d556a5e71c..845088eade 100644 --- a/examples/msg/mc/CMakeLists.txt +++ b/examples/msg/mc/CMakeLists.txt @@ -4,7 +4,7 @@ if(HAVE_MC) set(EXECUTABLE_OUTPUT_PATH "${CMAKE_CURRENT_BINARY_DIR}") file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/test/") - file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/chord_liveness/") + file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/chord/") add_executable(centralized centralized_mutex.c) add_executable(bugged1 bugged1.c) @@ -13,7 +13,7 @@ if(HAVE_MC) add_executable(electric_fence electric_fence.c) add_executable(bugged1_liveness bugged1_liveness.c) add_executable(bugged2_liveness bugged2_liveness.c) - add_executable(chord_liveness/chord_liveness chord_liveness/chord_liveness.c) + add_executable(chord/chord chord/chord.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) @@ -27,7 +27,7 @@ if(HAVE_MC) target_link_libraries(electric_fence simgrid ) target_link_libraries(bugged1_liveness simgrid ) target_link_libraries(bugged2_liveness simgrid ) - target_link_libraries(chord_liveness/chord_liveness simgrid ) + target_link_libraries(chord/chord simgrid ) target_link_libraries(test/snapshot_comparison1 simgrid ) target_link_libraries(test/snapshot_comparison2 simgrid ) target_link_libraries(test/snapshot_comparison3 simgrid ) @@ -39,11 +39,11 @@ endif() set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/bugged1.tesh + ${CMAKE_CURRENT_SOURCE_DIR}/bugged2.tesh ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.tesh ${CMAKE_CURRENT_SOURCE_DIR}/centralized.tesh - ${CMAKE_CURRENT_SOURCE_DIR}/chord_liveness/chord_neverjoin.tesh - ${CMAKE_CURRENT_SOURCE_DIR}/chord_liveness/chord_neverdeliver.tesh - ${CMAKE_CURRENT_SOURCE_DIR}/chord_liveness/chord_neverjoin_timeout_visited.tesh + ${CMAKE_CURRENT_SOURCE_DIR}/chord/chord_neverjoin.tesh + ${CMAKE_CURRENT_SOURCE_DIR}/chord/chord_neverjoin_timeout_visited.tesh ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison1.tesh ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison2.tesh ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison3.tesh @@ -61,7 +61,7 @@ set(xml_files ${CMAKE_CURRENT_SOURCE_DIR}/deploy_electric_fence.xml ${CMAKE_CURRENT_SOURCE_DIR}/deploy_mutex.xml ${CMAKE_CURRENT_SOURCE_DIR}/platform.xml - ${CMAKE_CURRENT_SOURCE_DIR}/chord_liveness/deploy_chord_liveness.xml + ${CMAKE_CURRENT_SOURCE_DIR}/chord/deploy_chord4.xml ${CMAKE_CURRENT_SOURCE_DIR}/test/deploy_snapshot_comparison.xml ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_platform.xml PARENT_SCOPE @@ -77,7 +77,7 @@ set(examples_src ${CMAKE_CURRENT_SOURCE_DIR}/centralized_mutex.c ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.h ${CMAKE_CURRENT_SOURCE_DIR}/bugged2_liveness.h - ${CMAKE_CURRENT_SOURCE_DIR}/chord_liveness/chord_liveness.c + ${CMAKE_CURRENT_SOURCE_DIR}/chord/chord.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 @@ -90,8 +90,6 @@ set(bin_files ${CMAKE_CURRENT_SOURCE_DIR}/parse_dwarf ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged1_liveness ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged2_liveness - ${CMAKE_CURRENT_SOURCE_DIR}/chord_liveness/promela_chord_neverjoin - ${CMAKE_CURRENT_SOURCE_DIR}/chord_liveness/promela_chord_neverdeliver ${CMAKE_CURRENT_SOURCE_DIR}/test/promela PARENT_SCOPE ) diff --git a/examples/msg/mc/bugged2.tesh b/examples/msg/mc/bugged2.tesh new file mode 100644 index 0000000000..fcd9ca5141 --- /dev/null +++ b/examples/msg/mc/bugged2.tesh @@ -0,0 +1,64 @@ +#! ./tesh + +! expect signal SIGABRT +$ ${bindir:=.}/bugged2 --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:@) Check a safety property +> [ 0.000000] (2:client@HostB) Send 1! +> [ 0.000000] (3:client@HostC) Send 2! +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (2:client@HostB) Send 1! +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (3:client@HostC) Send 2! +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) OK +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (2:client@HostB) Send 1! +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (3:client@HostC) Send 2! +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) OK +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (2:client@HostB) Send 1! +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (2:client@HostB) Send 1! +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (3:client@HostC) Send 2! +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) OK +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (2:client@HostB) Send 1! +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (3:client@HostC) Send 2! +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) OK +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (2:client@HostB) Send 1! +> [ 0.000000] (3:client@HostC) Send 2! +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) OK +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (2:client@HostB) Send 1! +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (3:client@HostC) Send 2! +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) OK +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (2:client@HostB) Send 1! +> [ 0.000000] (3:client@HostC) Send 2! +> [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (1:server@HostA) Received 2 +> [ 0.000000] (1:server@HostA) OK +> [ 0.000000] (0:@) Expanded states = 68 +> [ 0.000000] (0:@) Visited states = 132 +> [ 0.000000] (0:@) Executed transitions = 124 \ No newline at end of file diff --git a/examples/msg/mc/chord/chord b/examples/msg/mc/chord/chord new file mode 100755 index 0000000000..91e6779548 Binary files /dev/null and b/examples/msg/mc/chord/chord differ diff --git a/examples/msg/mc/chord_liveness/chord_liveness.c b/examples/msg/mc/chord/chord.c similarity index 99% rename from examples/msg/mc/chord_liveness/chord_liveness.c rename to examples/msg/mc/chord/chord.c index f7d1a0d967..6f8e6a0cf8 100644 --- a/examples/msg/mc/chord_liveness/chord_liveness.c +++ b/examples/msg/mc/chord/chord.c @@ -334,6 +334,8 @@ int node(int argc, char *argv[]) } } + MC_assert(!node_join); + if (join_success) { while (MSG_get_clock() < init_time + deadline @@ -831,7 +833,7 @@ int closest_preceding_node(node_t node, int id) */ static void stabilize(node_t node) { - XBT_DEBUG("Stabilizing node"); + XBT_DEBUG("Stabilizing node %d", node->id); // get the predecessor of my immediate successor int candidate_id; @@ -860,6 +862,8 @@ static void stabilize(node_t node) */ static void notify(node_t node, int predecessor_candidate_id) { + XBT_DEBUG("Notifying node %d", node->id); + if (node->pred_id == -1 || is_in_interval(predecessor_candidate_id, node->pred_id + 1, node->id - 1)) { diff --git a/examples/msg/mc/chord/chord_neverjoin.tesh b/examples/msg/mc/chord/chord_neverjoin.tesh new file mode 100644 index 0000000000..5e4fcfb80e --- /dev/null +++ b/examples/msg/mc/chord/chord_neverjoin.tesh @@ -0,0 +1,30 @@ +#! ./tesh + +! expect signal SIGABRT +! timeout 200 +$ ${bindir:=.}/chord ../../msg_platform.xml deploy_chord4.xml --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:@) Check a safety property +> [ 0.000000] (1:node@Jean_Yves) Joining the ring with id 6, knowing node 16 +> [ 0.000000] (2:node@Boivin) Joining the ring with id 10, knowing node 16 +> [ 0.000000] (3:node@TeX) Joining the ring with id 8, knowing node 16 +> [ 0.000000] (4:node@Jacquelin) A transfer has occured +> [ 0.000000] (4:node@Jacquelin) The task was successfully received by node 16 +> [ 0.000000] (1:node@Jean_Yves) Node 6 joined the ring +> [ 0.000000] (1:node@Jean_Yves) ************************** +> [ 0.000000] (1:node@Jean_Yves) *** PROPERTY NOT VALID *** +> [ 0.000000] (1:node@Jean_Yves) ************************** +> [ 0.000000] (1:node@Jean_Yves) Counter-example execution trace: +> [ 0.000000] (1:node@Jean_Yves) [(1)node] iSend (src=node, buff=(verbose only), size=(verbose only)) +> [ 0.000000] (1:node@Jean_Yves) [(2)node] iSend (src=node, buff=(verbose only), size=(verbose only)) +> [ 0.000000] (1:node@Jean_Yves) [(3)node] iSend (src=node, buff=(verbose only), size=(verbose only)) +> [ 0.000000] (1:node@Jean_Yves) [(4)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) +> [ 0.000000] (1:node@Jean_Yves) [(1)node] Wait (comm=(verbose only) [(1)node -> (4)node]) +> [ 0.000000] (1:node@Jean_Yves) [(1)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) +> [ 0.000000] (1:node@Jean_Yves) [(4)node] Test TRUE (comm=(verbose only) [(1)node -> (4)node]) +> [ 0.000000] (1:node@Jean_Yves) [(4)node] iSend (src=node, buff=(verbose only), size=(verbose only)) +> [ 0.000000] (1:node@Jean_Yves) [(1)node] Wait (comm=(verbose only) [(4)node -> (1)node]) +> [ 0.000000] (1:node@Jean_Yves) Expanded states = 9 +> [ 0.000000] (1:node@Jean_Yves) Visited states = 9 +> [ 0.000000] (1:node@Jean_Yves) Executed transitions = 9 + diff --git a/examples/msg/mc/chord/chord_neverjoin_timeout_visited.tesh b/examples/msg/mc/chord/chord_neverjoin_timeout_visited.tesh new file mode 100644 index 0000000000..a0afde7775 --- /dev/null +++ b/examples/msg/mc/chord/chord_neverjoin_timeout_visited.tesh @@ -0,0 +1,80 @@ +#! ./tesh + +! expect signal SIGABRT +! timeout 200 +$ ${bindir:=.}/chord ../../msg_platform.xml deploy_chord4.xml --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/timeout:1 --cfg=model-check/visited:100 +> [ 0.000000] (0:@) Configuration change: Set 'model-check' to '1' +> [ 0.000000] (0:@) Configuration change: Set 'model-check/timeout' to '1' +> [ 0.000000] (0:@) Configuration change: Set 'model-check/visited' to '100' +> [ 0.000000] (0:@) Check a safety property +> [ 0.000000] (1:node@Jean_Yves) Joining the ring with id 6, knowing node 16 +> [ 0.000000] (2:node@Boivin) Joining the ring with id 10, knowing node 16 +> [ 0.000000] (3:node@TeX) Joining the ring with id 8, knowing node 16 +> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. +> [ 0.000000] (2:node@Boivin) Cannot join the ring. +> [ 0.000000] (3:node@TeX) Cannot join the ring. +> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. +> [ 0.000000] (2:node@Boivin) Cannot join the ring. +> [ 0.000000] (3:node@TeX) Cannot join the ring. +> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. +> [ 0.000000] (2:node@Boivin) Cannot join the ring. +> [ 0.000000] (3:node@TeX) Cannot join the ring. +> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. +> [ 0.000000] (2:node@Boivin) Cannot join the ring. +> [ 0.000000] (3:node@TeX) Cannot join the ring. +> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. +> [ 0.000000] (2:node@Boivin) Cannot join the ring. +> [ 0.000000] (3:node@TeX) Cannot join the ring. +> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. +> [ 0.000000] (2:node@Boivin) Cannot join the ring. +> [ 0.000000] (3:node@TeX) Cannot join the ring. +> [ 0.000000] (4:node@Jacquelin) A transfer has occured +> [ 0.000000] (4:node@Jacquelin) The task was successfully received by node 16 +> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. +> [ 0.000000] (2:node@Boivin) Cannot join the ring. +> [ 0.000000] (3:node@TeX) Cannot join the ring. +> [ 0.000000] (4:node@Jacquelin) A transfer has occured +> [ 0.000000] (4:node@Jacquelin) The task was successfully received by node 16 +> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. +> [ 0.000000] (2:node@Boivin) Cannot join the ring. +> [ 0.000000] (3:node@TeX) Cannot join the ring. +> [ 0.000000] (4:node@Jacquelin) A transfer has occured +> [ 0.000000] (4:node@Jacquelin) The task was successfully received by node 16 +> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. +> [ 0.000000] (2:node@Boivin) Cannot join the ring. +> [ 0.000000] (3:node@TeX) Cannot join the ring. +> [ 0.000000] (4:node@Jacquelin) A transfer has occured +> [ 0.000000] (4:node@Jacquelin) The task was successfully received by node 16 +> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. +> [ 0.000000] (2:node@Boivin) Cannot join the ring. +> [ 0.000000] (3:node@TeX) Cannot join the ring. +> [ 0.000000] (4:node@Jacquelin) A transfer has occured +> [ 0.000000] (4:node@Jacquelin) The task was successfully received by node 16 +> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. +> [ 0.000000] (2:node@Boivin) Cannot join the ring. +> [ 0.000000] (4:node@Jacquelin) A transfer has occured +> [ 0.000000] (4:node@Jacquelin) The task was successfully received by node 16 +> [ 0.000000] (3:node@TeX) Cannot join the ring. +> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. +> [ 0.000000] (2:node@Boivin) Cannot join the ring. +> [ 0.000000] (4:node@Jacquelin) A transfer has occured +> [ 0.000000] (4:node@Jacquelin) The task was successfully received by node 16 +> [ 0.000000] (3:node@TeX) Node 8 joined the ring +> [ 0.000000] (3:node@TeX) ************************** +> [ 0.000000] (3:node@TeX) *** PROPERTY NOT VALID *** +> [ 0.000000] (3:node@TeX) ************************** +> [ 0.000000] (3:node@TeX) Counter-example execution trace: +> [ 0.000000] (3:node@TeX) [(1)node] iSend (src=node, buff=(verbose only), size=(verbose only)) +> [ 0.000000] (3:node@TeX) [(1)node] WaitTimeout (comm=(verbose only)) +> [ 0.000000] (3:node@TeX) [(2)node] iSend (src=node, buff=(verbose only), size=(verbose only)) +> [ 0.000000] (3:node@TeX) [(2)node] WaitTimeout (comm=(verbose only)) +> [ 0.000000] (3:node@TeX) [(3)node] iSend (src=node, buff=(verbose only), size=(verbose only)) +> [ 0.000000] (3:node@TeX) [(4)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) +> [ 0.000000] (3:node@TeX) [(3)node] Wait (comm=(verbose only) [(3)node -> (4)node]) +> [ 0.000000] (3:node@TeX) [(4)node] Test TRUE (comm=(verbose only) [(3)node -> (4)node]) +> [ 0.000000] (3:node@TeX) [(3)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) +> [ 0.000000] (3:node@TeX) [(4)node] iSend (src=node, buff=(verbose only), size=(verbose only)) +> [ 0.000000] (3:node@TeX) [(3)node] Wait (comm=(verbose only) [(4)node -> (3)node]) +> [ 0.000000] (3:node@TeX) Expanded states = 42 +> [ 0.000000] (3:node@TeX) Visited states = 170 +> [ 0.000000] (3:node@TeX) Executed transitions = 159 diff --git a/examples/msg/mc/chord_liveness/deploy_chord_liveness.xml b/examples/msg/mc/chord/deploy_chord.xml similarity index 52% rename from examples/msg/mc/chord_liveness/deploy_chord_liveness.xml rename to examples/msg/mc/chord/deploy_chord.xml index 2f870491b1..f03b06bf33 100644 --- a/examples/msg/mc/chord_liveness/deploy_chord_liveness.xml +++ b/examples/msg/mc/chord/deploy_chord.xml @@ -3,22 +3,30 @@ - - - + + + - - + + + + + + + + + - + + diff --git a/examples/msg/mc/chord/deploy_chord4.xml b/examples/msg/mc/chord/deploy_chord4.xml new file mode 100644 index 0000000000..f03b06bf33 --- /dev/null +++ b/examples/msg/mc/chord/deploy_chord4.xml @@ -0,0 +1,32 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/msg/mc/chord_liveness/chord_neverdeliver.tesh b/examples/msg/mc/chord_liveness/chord_neverdeliver.tesh deleted file mode 100644 index fed20cb111..0000000000 --- a/examples/msg/mc/chord_liveness/chord_neverdeliver.tesh +++ /dev/null @@ -1,35 +0,0 @@ -#! ./tesh - -! expect signal SIGABRT -! timeout 200 -$ ${bindir:=.}/chord_liveness ../../msg_platform.xml deploy_chord_liveness.xml --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/property:promela_chord_neverdeliver -> [ 0.000000] (0:@) Configuration change: Set 'model-check' to '1' -> [ 0.000000] (0:@) Configuration change: Set 'model-check/property' to 'promela_chord_neverdeliver' -> [ 0.000000] (0:@) Check the liveness property promela_chord_neverdeliver -> [ 0.000000] (1:node@Jean_Yves) Joining the ring with id 14, knowing node 1 -> [ 0.000000] (2:node@Boivin) Joining the ring with id 8, knowing node 1 -> [ 0.000000] (3:node@Jacquelin) A transfer has occured -> [ 0.000000] (3:node@Jacquelin) The task was successfully received by node 1 -> [ 0.000000] (1:node@Jean_Yves) Node 14 joined the ring -> [ 0.000000] (0:@) Next pair (depth = 15, 2 interleave) already reached (equal to state 13) ! -> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* -> [ 0.000000] (0:@) | ACCEPTANCE CYCLE | -> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* -> [ 0.000000] (0:@) Counter-example that violates formula : -> [ 0.000000] (0:@) [(1)node] iSend (src=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(2)node] iSend (src=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(3)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(1)node] Wait (comm=(verbose only) [(1)node -> (3)node]) -> [ 0.000000] (0:@) [(1)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(3)node] Test TRUE (comm=(verbose only) [(1)node -> (3)node]) -> [ 0.000000] (0:@) [(3)node] iSend (src=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(1)node] Wait (comm=(verbose only) [(3)node -> (1)node]) -> [ 0.000000] (0:@) [(1)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(1)node] Test FALSE (comm=(verbose only)) -> [ 0.000000] (0:@) [(1)node] MC_RANDOM (0) -> [ 0.000000] (0:@) [(1)node] MC_RANDOM (0) -> [ 0.000000] (0:@) [(1)node] MC_RANDOM (0) -> [ 0.000000] (0:@) [(1)node] MC_RANDOM (0) -> [ 0.000000] (0:@) Expanded pairs = 24 -> [ 0.000000] (0:@) Visited pairs = 14 -> [ 0.000000] (0:@) Executed transitions = 14 diff --git a/examples/msg/mc/chord_liveness/chord_neverjoin.tesh b/examples/msg/mc/chord_liveness/chord_neverjoin.tesh deleted file mode 100644 index 56d3a28f7a..0000000000 --- a/examples/msg/mc/chord_liveness/chord_neverjoin.tesh +++ /dev/null @@ -1,37 +0,0 @@ -#! ./tesh - -! expect signal SIGABRT -! timeout 200 -$ ${bindir:=.}/chord_liveness ../../msg_platform.xml deploy_chord_liveness.xml --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/property:promela_chord_neverjoin -> [ 0.000000] (0:@) Configuration change: Set 'model-check' to '1' -> [ 0.000000] (0:@) Configuration change: Set 'model-check/property' to 'promela_chord_neverjoin' -> [ 0.000000] (0:@) Check the liveness property promela_chord_neverjoin -> [ 0.000000] (1:node@Jean_Yves) Joining the ring with id 14, knowing node 1 -> [ 0.000000] (2:node@Boivin) Joining the ring with id 8, knowing node 1 -> [ 0.000000] (3:node@Jacquelin) A transfer has occured -> [ 0.000000] (3:node@Jacquelin) The task was successfully received by node 1 -> [ 0.000000] (1:node@Jean_Yves) Node 14 joined the ring -> [ 0.000000] (0:@) Next pair (depth = 15, 2 interleave) already reached (equal to state 11) ! -> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* -> [ 0.000000] (0:@) | ACCEPTANCE CYCLE | -> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* -> [ 0.000000] (0:@) Counter-example that violates formula : -> [ 0.000000] (0:@) [(1)node] iSend (src=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(2)node] iSend (src=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(3)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(1)node] Wait (comm=(verbose only) [(1)node -> (3)node]) -> [ 0.000000] (0:@) [(1)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(3)node] Test TRUE (comm=(verbose only) [(1)node -> (3)node]) -> [ 0.000000] (0:@) [(3)node] iSend (src=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(1)node] Wait (comm=(verbose only) [(3)node -> (1)node]) -> [ 0.000000] (0:@) [(1)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(1)node] Test FALSE (comm=(verbose only)) -> [ 0.000000] (0:@) [(1)node] MC_RANDOM (0) -> [ 0.000000] (0:@) [(1)node] MC_RANDOM (0) -> [ 0.000000] (0:@) [(1)node] MC_RANDOM (0) -> [ 0.000000] (0:@) [(1)node] MC_RANDOM (0) -> [ 0.000000] (0:@) Expanded pairs = 22 -> [ 0.000000] (0:@) Visited pairs = 14 -> [ 0.000000] (0:@) Executed transitions = 14 - - diff --git a/examples/msg/mc/chord_liveness/chord_neverjoin_timeout_visited.tesh b/examples/msg/mc/chord_liveness/chord_neverjoin_timeout_visited.tesh deleted file mode 100644 index ed80aeb257..0000000000 --- a/examples/msg/mc/chord_liveness/chord_neverjoin_timeout_visited.tesh +++ /dev/null @@ -1,105 +0,0 @@ -#! ./tesh - -! expect signal SIGABRT -! timeout 200 -$ ${bindir:=.}/chord_liveness ../../msg_platform.xml deploy_chord_liveness.xml --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/property:promela_chord_neverjoin --cfg=model-check/timeout:1 --cfg=model-check/visited:100 -> [ 0.000000] (0:@) Configuration change: Set 'model-check' to '1' -> [ 0.000000] (0:@) Configuration change: Set 'model-check/property' to 'promela_chord_neverjoin' -> [ 0.000000] (0:@) Configuration change: Set 'model-check/timeout' to '1' -> [ 0.000000] (0:@) Configuration change: Set 'model-check/visited' to '100' -> [ 0.000000] (0:@) Check the liveness property promela_chord_neverjoin -> [ 0.000000] (1:node@Jean_Yves) Joining the ring with id 14, knowing node 1 -> [ 0.000000] (2:node@Boivin) Joining the ring with id 8, knowing node 1 -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (3:node@Jacquelin) A transfer has occured -> [ 0.000000] (3:node@Jacquelin) The task was successfully received by node 1 -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (3:node@Jacquelin) A transfer has occured -> [ 0.000000] (3:node@Jacquelin) The task was successfully received by node 1 -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (3:node@Jacquelin) A transfer has occured -> [ 0.000000] (3:node@Jacquelin) The task was successfully received by node 1 -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (3:node@Jacquelin) A transfer has occured -> [ 0.000000] (3:node@Jacquelin) The task was successfully received by node 1 -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (3:node@Jacquelin) A transfer has occured -> [ 0.000000] (3:node@Jacquelin) The task was successfully received by node 1 -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (3:node@Jacquelin) A transfer has occured -> [ 0.000000] (3:node@Jacquelin) The task was successfully received by node 1 -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (3:node@Jacquelin) A transfer has occured -> [ 0.000000] (3:node@Jacquelin) The task was successfully received by node 1 -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (3:node@Jacquelin) A transfer has occured -> [ 0.000000] (3:node@Jacquelin) The task was successfully received by node 1 -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (3:node@Jacquelin) A transfer has occured -> [ 0.000000] (3:node@Jacquelin) The task was successfully received by node 1 -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (3:node@Jacquelin) A transfer has occured -> [ 0.000000] (3:node@Jacquelin) The task was successfully received by node 1 -> [ 0.000000] (2:node@Boivin) Cannot join the ring. -> [ 0.000000] (1:node@Jean_Yves) Cannot join the ring. -> [ 0.000000] (3:node@Jacquelin) A transfer has occured -> [ 0.000000] (3:node@Jacquelin) The task was successfully received by node 1 -> [ 0.000000] (2:node@Boivin) Node 8 joined the ring -> [ 0.000000] (0:@) Next pair (depth = 16, 2 interleave) already reached (equal to state 71) ! -> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* -> [ 0.000000] (0:@) | ACCEPTANCE CYCLE | -> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* -> [ 0.000000] (0:@) Counter-example that violates formula : -> [ 0.000000] (0:@) [(1)node] iSend (src=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(1)node] WaitTimeout (comm=(verbose only)) -> [ 0.000000] (0:@) [(2)node] iSend (src=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(3)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(2)node] Wait (comm=(verbose only) [(2)node -> (3)node]) -> [ 0.000000] (0:@) [(2)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(3)node] Test TRUE (comm=(verbose only) [(2)node -> (3)node]) -> [ 0.000000] (0:@) [(3)node] iSend (src=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(2)node] Wait (comm=(verbose only) [(3)node -> (2)node]) -> [ 0.000000] (0:@) [(2)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) -> [ 0.000000] (0:@) [(2)node] Test FALSE (comm=(verbose only)) -> [ 0.000000] (0:@) [(2)node] MC_RANDOM (0) -> [ 0.000000] (0:@) [(2)node] MC_RANDOM (0) -> [ 0.000000] (0:@) [(2)node] MC_RANDOM (0) -> [ 0.000000] (0:@) [(2)node] MC_RANDOM (0) -> [ 0.000000] (0:@) Expanded pairs = 82 -> [ 0.000000] (0:@) Visited pairs = 337 -> [ 0.000000] (0:@) Executed transitions = 360 \ No newline at end of file diff --git a/examples/msg/mc/chord_liveness/promela_chord_neverdeliver b/examples/msg/mc/chord_liveness/promela_chord_neverdeliver deleted file mode 100644 index d102137675..0000000000 --- a/examples/msg/mc/chord_liveness/promela_chord_neverdeliver +++ /dev/null @@ -1,12 +0,0 @@ -never { /* !(!(GFdeliver)) */ -T0_init : /* init */ - if - :: (deliver) -> goto accept_S1 - :: (1) -> goto T0_init - fi; -accept_S1 : /* 1 */ - if - :: (deliver) -> goto accept_S1 - :: (1) -> goto T0_init - fi; -} \ No newline at end of file diff --git a/examples/msg/mc/chord_liveness/promela_chord_neverjoin b/examples/msg/mc/chord_liveness/promela_chord_neverjoin deleted file mode 100644 index 0e9dd9dd44..0000000000 --- a/examples/msg/mc/chord_liveness/promela_chord_neverjoin +++ /dev/null @@ -1,12 +0,0 @@ -never { /* !(!(GFjoin)) */ -T0_init : /* init */ - if - :: (join) -> goto accept_S1 - :: (1) -> goto T0_init - fi; -accept_S1 : /* 1 */ - if - :: (join) -> goto accept_S1 - :: (1) -> goto T0_init - fi; -} \ No newline at end of file