model-checker : new examples (with tesh) for verification of liveness properties...

diff --git a/.gitignore b/.gitignore
index 47a2888..adb5d0e 100644 (file)
--- 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/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
 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 1b3dda1..651f18e 100644 (file)
--- 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-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)
       endif()
     endif()
     if(HAVE_RAWCTX)

diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt
index e6932b4..796d92c 100644 (file)
--- 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(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)
   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(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 )
   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}/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
   ${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}/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
   ${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}/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
   ${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}/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
   )
   ${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 4856395..f7d1a0d 100644 (file)
--- 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 "xbt/log.h"
 #include "xbt/asserts.h"
 #include "simgrid/modelchecker.h"

-#include "chord_liveness.h"

 #include "mc/mc.h"
 
 /** @addtogroup MSG_examples
 #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);
 
 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_join = 0;

+int node_deliver = 0;

 
 /**
  * \brief Global initialization of the Chord simulation.
 
 /**
  * \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?
 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; 
     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)) {
 
 
       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) {
 
       }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
 
 
           // 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:
   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?
       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);
 }
 
   find_successor(node, id);
 }
 

-int predJoin(void){
+static int predJoin(void){

   return node_join;
 }
 
   return node_join;
 }
 

+static int predDeliver(void){
+  return node_deliver;
+}
+

 
 /**
  * \brief Main function.
 
 /**
  * \brief Main function.


@@ -906,13 +949,13 @@ int predJoin(void){
 int main(int argc, char *argv[])
 {
   MSG_init(&argc, argv);
 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("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);
     exit(1);

-    }*/
+  }

 
 

-  char **options = &argv[0];
+  char **options = &argv[1];

   while (!strncmp(options[0], "-", 1)) {
 
     int length = strlen("-nb_bits=");
   while (!strncmp(options[0], "-", 1)) {
 
     int length = strlen("-nb_bits=");


@@ -934,21 +977,20 @@ int main(int argc, char *argv[])
     options++;
   }
 
     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();
 
 
   chord_initialize();
 

-  MSG_config("model-check/property","promela_chord_liveness");

   MC_automaton_new_propositional_symbol("join", &predJoin);
   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_function_register("node", node);

-  MSG_launch_application("deploy_chord_liveness.xml");
+  MSG_launch_application(application_file);

 
   msg_error_t res = MSG_main();
 
   msg_error_t res = MSG_main();

-  //XBT_CRITICAL("Messages created: %ld", smx_total_comms);

   XBT_INFO("Simulated time: %g", MSG_get_clock());
 
   chord_exit();
   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 (file)
index 0000000..fed20cb
--- /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 ffc6a67..56d3a28 100644 (file)
--- 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
 
 ! 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:@) 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] (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:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  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:@) [(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 (file)
index 0000000..e377b9b
--- /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 (file)
index 0000000..d102137
--- /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