From 2a56ae61b3c1dfe00f46c656ad173b4a701b9322 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Wed, 3 Apr 2013 16:18:04 +0200 Subject: [PATCH] model-checker : new examples (with tesh) for verification of liveness properties on chord --- .gitignore | 6 - buildtools/Cmake/AddTests.cmake | 16 ++- examples/msg/mc/CMakeLists.txt | 16 ++- .../chord_liveness.c | 124 ++++++++++++------ .../mc/chord_liveness/chord_neverdeliver.tesh | 35 +++++ .../chord_neverjoin.tesh | 18 ++- .../chord_neverjoin_timeout_visited.tesh | 97 ++++++++++++++ .../deploy_chord_liveness.xml | 0 .../chord_liveness/promela_chord_neverdeliver | 12 ++ .../promela_chord_neverjoin} | 0 10 files changed, 257 insertions(+), 67 deletions(-) rename examples/msg/mc/{chord => chord_liveness}/chord_liveness.c (90%) create mode 100644 examples/msg/mc/chord_liveness/chord_neverdeliver.tesh rename examples/msg/mc/{chord => chord_liveness}/chord_neverjoin.tesh (67%) create mode 100644 examples/msg/mc/chord_liveness/chord_neverjoin_timeout_visited.tesh rename examples/msg/mc/{chord => chord_liveness}/deploy_chord_liveness.xml (100%) create mode 100644 examples/msg/mc/chord_liveness/promela_chord_neverdeliver rename examples/msg/mc/{chord/promela_chord_liveness => chord_liveness/promela_chord_neverjoin} (100%) diff --git a/.gitignore b/.gitignore index 47a28887db..adb5d0e4dd 100644 --- a/.gitignore +++ b/.gitignore @@ -144,12 +144,6 @@ examples/msg/tracing/volume examples/msg/io/file examples/msg/io/file_unlink examples/msg/mc/bugged3 -examples/msg/mc/random_test -examples/msg/mc/bugged1_for_liveness -examples/msg/mc/bugged1_while_liveness -examples/msg/mc/centralized_liveness_deadlock -examples/msg/mc/test/test_heap_comparison -examples/msg/mc/chord_liveness examples/msg/mc/test/snapshot_comparison1 examples/msg/mc/test/snapshot_comparison2 examples/msg/mc/test/snapshot_comparison3 diff --git a/buildtools/Cmake/AddTests.cmake b/buildtools/Cmake/AddTests.cmake index 1b3dda1082..651f18eaa4 100644 --- a/buildtools/Cmake/AddTests.cmake +++ b/buildtools/Cmake/AddTests.cmake @@ -415,13 +415,15 @@ if(NOT enable_memcheck) 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-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) 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 --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) + 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) endif() endif() if(HAVE_RAWCTX) diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt index e6932b4abd..796d92c878 100644 --- a/examples/msg/mc/CMakeLists.txt +++ b/examples/msg/mc/CMakeLists.txt @@ -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/chord_liveness chord/chord_liveness.c) + add_executable(chord_liveness/chord_liveness chord_liveness/chord_liveness.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/chord_liveness simgrid ) + target_link_libraries(chord_liveness/chord_liveness simgrid ) target_link_libraries(test/snapshot_comparison1 simgrid ) target_link_libraries(test/snapshot_comparison2 simgrid ) target_link_libraries(test/snapshot_comparison3 simgrid ) @@ -41,7 +41,9 @@ set(tesh_files ${CMAKE_CURRENT_SOURCE_DIR}/bugged1.tesh ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.tesh ${CMAKE_CURRENT_SOURCE_DIR}/centralized.tesh - ${CMAKE_CURRENT_SOURCE_DIR}/chord/chord_neverjoin.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}/test/snapshot_comparison1.tesh ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison2.tesh ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison3.tesh @@ -59,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/deploy_chord_liveness.xml + ${CMAKE_CURRENT_SOURCE_DIR}/chord_liveness/deploy_chord_liveness.xml ${CMAKE_CURRENT_SOURCE_DIR}/test/deploy_snapshot_comparison.xml ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_platform.xml PARENT_SCOPE @@ -75,8 +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/chord_liveness.c - ${CMAKE_CURRENT_SOURCE_DIR}/chord/chord_liveness.h + ${CMAKE_CURRENT_SOURCE_DIR}/chord_liveness/chord_liveness.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 @@ -89,7 +90,8 @@ 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/promela_chord_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/chord/chord_liveness.c b/examples/msg/mc/chord_liveness/chord_liveness.c similarity index 90% rename from examples/msg/mc/chord/chord_liveness.c rename to examples/msg/mc/chord_liveness/chord_liveness.c index 48563958ae..f7d1a0d967 100644 --- a/examples/msg/mc/chord/chord_liveness.c +++ b/examples/msg/mc/chord_liveness/chord_liveness.c @@ -10,7 +10,6 @@ #include "xbt/log.h" #include "xbt/asserts.h" #include "simgrid/modelchecker.h" -#include "chord_liveness.h" #include "mc/mc.h" /** @addtogroup MSG_examples @@ -121,8 +120,9 @@ static void check_predecessor(node_t node); static void random_lookup(node_t); static void quit_notify(node_t node); -/* Global variable corresponding to atomic proposition */ +/* Global variables corresponding to atomic propositions */ int node_join = 0; +int node_deliver = 0; /** * \brief Global initialization of the Chord simulation. @@ -209,9 +209,11 @@ static void get_mailbox(int node_id, char* mailbox) static void task_free(void* task) { // TODO add a parameter data_free_function to MSG_task_create? - xbt_free(MSG_task_get_data(task)); - MSG_task_destroy(task); - task = NULL; + if(task != NULL){ + xbt_free(MSG_task_get_data(task)); + MSG_task_destroy(task); + task = NULL; + } } /** @@ -329,7 +331,6 @@ int node(int argc, char *argv[]) if(join_success){ XBT_INFO("Node %d joined the ring", node.id); node_join = 1; - //MC_compare(); } } @@ -347,34 +348,71 @@ int node(int argc, char *argv[]) if (!MSG_comm_test(node.comm_receive)) { - // no task was received: make some periodic calls - if (MSG_get_clock() >= next_stabilize_date) { - stabilize(&node); - next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay; - } - else if (MSG_get_clock() >= next_fix_fingers_date) { - fix_fingers(&node); - next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay; - } - else if (MSG_get_clock() >= next_check_predecessor_date) { - check_predecessor(&node); - next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay; - } - else if (MSG_get_clock() >= next_lookup_date) { - random_lookup(&node); - next_lookup_date = MSG_get_clock() + periodic_lookup_delay; - } - else { - // nothing to do: sleep for a while - MSG_process_sleep(5); - } + #ifdef HAVE_MC + if(MC_is_active()){ + if(MC_random()){ + stabilize(&node); + }else if(MC_random()){ + fix_fingers(&node); + }else if(MC_random()){ + check_predecessor(&node); + }else if(MC_random()){ + random_lookup(&node); + }else{ + MSG_process_sleep(5); + } + }else{ + if (MSG_get_clock() >= next_stabilize_date) { + stabilize(&node); + next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay; + } + else if (MSG_get_clock() >= next_fix_fingers_date) { + fix_fingers(&node); + next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay; + } + else if (MSG_get_clock() >= next_check_predecessor_date) { + check_predecessor(&node); + next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay; + } + else if (MSG_get_clock() >= next_lookup_date) { + random_lookup(&node); + next_lookup_date = MSG_get_clock() + periodic_lookup_delay; + } + else { + // nothing to do: sleep for a while + MSG_process_sleep(5); + } + } + #else + if (MSG_get_clock() >= next_stabilize_date) { + stabilize(&node); + next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay; + } + else if (MSG_get_clock() >= next_fix_fingers_date) { + fix_fingers(&node); + next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay; + } + else if (MSG_get_clock() >= next_check_predecessor_date) { + check_predecessor(&node); + next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay; + } + else if (MSG_get_clock() >= next_lookup_date) { + random_lookup(&node); + next_lookup_date = MSG_get_clock() + periodic_lookup_delay; + } + else { + // nothing to do: sleep for a while + MSG_process_sleep(5); + } + #endif + }else{ if (node.comm_receive) { - XBT_INFO("A transfer has occured"); + node_deliver = 0; - //MC_compare(); + XBT_INFO("A transfer has occured"); // a transfer has occured @@ -426,6 +464,7 @@ static void handle_task(node_t node, msg_task_t task) { switch (type) { case TASK_FIND_SUCCESSOR: + node_deliver = 1; XBT_DEBUG("Receiving a 'Find Successor' request from %s for id %d", task_data->issuer_host_name, task_data->request_id); // is my successor the successor? @@ -895,10 +934,14 @@ static void random_lookup(node_t node) find_successor(node, id); } -int predJoin(void){ +static int predJoin(void){ return node_join; } +static int predDeliver(void){ + return node_deliver; +} + /** * \brief Main function. @@ -906,13 +949,13 @@ int predJoin(void){ int main(int argc, char *argv[]) { MSG_init(&argc, argv); - /*if (argc < 3) { + if (argc < 3) { printf("Usage: %s [-nb_bits=n] [-timeout=t] platform_file deployment_file\n", argv[0]); - printf("example: %s ../msg_platform.xml chord.xml\n", argv[0]); + printf("example: %s ../../msg_platform.xml deploy_chord_liveness.xml\n", argv[0]); exit(1); - }*/ + } - char **options = &argv[0]; + char **options = &argv[1]; while (!strncmp(options[0], "-", 1)) { int length = strlen("-nb_bits="); @@ -934,21 +977,20 @@ int main(int argc, char *argv[]) options++; } - //const char* platform_file = options[0]; - //const char* application_file = options[1]; + const char* platform_file = options[0]; + const char* application_file = options[1]; chord_initialize(); - MSG_config("model-check/property","promela_chord_liveness"); MC_automaton_new_propositional_symbol("join", &predJoin); + MC_automaton_new_propositional_symbol("deliver", &predDeliver); - MSG_create_environment("../../msg_platform.xml"); - + MSG_create_environment(platform_file); + MSG_function_register("node", node); - MSG_launch_application("deploy_chord_liveness.xml"); + MSG_launch_application(application_file); msg_error_t res = MSG_main(); - //XBT_CRITICAL("Messages created: %ld", smx_total_comms); XBT_INFO("Simulated time: %g", MSG_get_clock()); chord_exit(); diff --git a/examples/msg/mc/chord_liveness/chord_neverdeliver.tesh b/examples/msg/mc/chord_liveness/chord_neverdeliver.tesh new file mode 100644 index 0000000000..fed20cb111 --- /dev/null +++ b/examples/msg/mc/chord_liveness/chord_neverdeliver.tesh @@ -0,0 +1,35 @@ +#! ./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/chord_neverjoin.tesh b/examples/msg/mc/chord_liveness/chord_neverjoin.tesh similarity index 67% rename from examples/msg/mc/chord/chord_neverjoin.tesh rename to examples/msg/mc/chord_liveness/chord_neverjoin.tesh index ffc6a67193..56d3a28f7a 100644 --- a/examples/msg/mc/chord/chord_neverjoin.tesh +++ b/examples/msg/mc/chord_liveness/chord_neverjoin.tesh @@ -2,15 +2,16 @@ ! expect signal SIGABRT ! timeout 200 -$ ${bindir:=.}/chord_liveness --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext +$ ${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:@) Check the liveness property promela_chord_liveness +> [ 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 = 11, 2 interleave) already reached (equal to state 11) ! +> [ 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:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* @@ -25,7 +26,12 @@ $ ${bindir:=.}/chord_liveness --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i: > [ 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:@) Expanded pairs = 14 -> [ 0.000000] (0:@) Visited pairs = 10 -> [ 0.000000] (0:@) Executed transitions = 10 +> [ 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 new file mode 100644 index 0000000000..e377b9b3c9 --- /dev/null +++ b/examples/msg/mc/chord_liveness/chord_neverjoin_timeout_visited.tesh @@ -0,0 +1,97 @@ +#! ./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] (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 62) ! +> [ 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 = 73 +> [ 0.000000] (0:@) Visited pairs = 262 +> [ 0.000000] (0:@) Executed transitions = 281 \ No newline at end of file diff --git a/examples/msg/mc/chord/deploy_chord_liveness.xml b/examples/msg/mc/chord_liveness/deploy_chord_liveness.xml similarity index 100% rename from examples/msg/mc/chord/deploy_chord_liveness.xml rename to examples/msg/mc/chord_liveness/deploy_chord_liveness.xml diff --git a/examples/msg/mc/chord_liveness/promela_chord_neverdeliver b/examples/msg/mc/chord_liveness/promela_chord_neverdeliver new file mode 100644 index 0000000000..d102137675 --- /dev/null +++ b/examples/msg/mc/chord_liveness/promela_chord_neverdeliver @@ -0,0 +1,12 @@ +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/promela_chord_liveness b/examples/msg/mc/chord_liveness/promela_chord_neverjoin similarity index 100% rename from examples/msg/mc/chord/promela_chord_liveness rename to examples/msg/mc/chord_liveness/promela_chord_neverjoin -- 2.20.1