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 55ef3ea..af482aa 100644 (file)
--- 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 d556a5e..845088e 100644 (file)
--- 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 (file)
index 0000000..fcd9ca5
--- /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 (executable)
index 0000000..91e6779
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 f7d1a0d..6f8e6a0 100644 (file)
--- 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 (file)
index 0000000..5e4fcfb
--- /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 (file)
index 0000000..a0afde7
--- /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 2f87049..f03b06b 100644 (file)
--- a/examples/msg/mc/chord_liveness/deploy_chord_liveness.xml
+++ b/examples/msg/mc/chord/deploy_chord.xml
@@ -3,22 +3,30 @@
 <platform version="3">
  
   <process host="Jean_Yves" function="node">
-    <argument value="14"/>        <!-- my id -->
-    <argument value="1"/>         <!-- known id -->
-    <argument value="400"/>        <!-- time to sleep before it starts-->
+    <argument value="6"/>        <!-- my id -->
+    <argument value="16"/>         <!-- known id -->
+    <argument value="300"/>        <!-- time to sleep before it starts-->
     <argument value ="600"/>           <!-- deadline -->
   </process>
   
   <process host="Boivin" function="node">
-    <argument value="8"/>         <!-- my id -->
-    <argument value="1"/>         <!-- known id -->
+    <argument value="10"/>         <!-- my id -->
+    <argument value="16"/>         <!-- known id -->
     <argument value="300"/>         <!-- time to sleep before it starts-->
     <argument value ="600"/>           <!-- deadline -->
   </process>
 
+  <process host="TeX" function="node">
+    <argument value="8"/>         <!-- my id -->
+    <argument value="16"/>         <!-- known id -->
+    <argument value="100"/>         <!-- time to sleep before it starts-->
+    <argument value ="600"/>           <!-- deadline -->
+  </process>
+
   <process host="Jacquelin" function="node">
-    <argument value="1"/>         <!-- my id -->
+    <argument value="16"/>         <!-- my id -->
     <argument value ="600"/>             <!-- deadline -->
   </process>
 
+
 </platform>

diff --git a/examples/msg/mc/chord/deploy_chord4.xml b/examples/msg/mc/chord/deploy_chord4.xml
new file mode 100644 (file)
index 0000000..f03b06b
--- /dev/null
+++ b/examples/msg/mc/chord/deploy_chord4.xml
@@ -0,0 +1,32 @@
+<?xml version='1.0'?>
+<!DOCTYPE platform SYSTEM "http://simgrid.gforge.inria.fr/simgrid.dtd">
+<platform version="3">
+ 
+  <process host="Jean_Yves" function="node">
+    <argument value="6"/>        <!-- my id -->
+    <argument value="16"/>         <!-- known id -->
+    <argument value="300"/>        <!-- time to sleep before it starts-->
+    <argument value ="600"/>           <!-- deadline -->
+  </process>
+  
+  <process host="Boivin" function="node">
+    <argument value="10"/>         <!-- my id -->
+    <argument value="16"/>         <!-- known id -->
+    <argument value="300"/>         <!-- time to sleep before it starts-->
+    <argument value ="600"/>           <!-- deadline -->
+  </process>
+
+  <process host="TeX" function="node">
+    <argument value="8"/>         <!-- my id -->
+    <argument value="16"/>         <!-- known id -->
+    <argument value="100"/>         <!-- time to sleep before it starts-->
+    <argument value ="600"/>           <!-- deadline -->
+  </process>
+
+  <process host="Jacquelin" function="node">
+    <argument value="16"/>         <!-- my id -->
+    <argument value ="600"/>             <!-- deadline -->
+  </process>
+
+
+</platform>

diff --git a/examples/msg/mc/chord_liveness/chord_neverdeliver.tesh b/examples/msg/mc/chord_liveness/chord_neverdeliver.tesh
deleted file mode 100644 (file)
index fed20cb..0000000
--- 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 (file)
index 56d3a28..0000000
--- 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 (file)
index ed80aeb..0000000
--- 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 (file)
index d102137..0000000
--- 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 (file)
index 0e9dd9d..0000000
--- 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