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
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)
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)
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 )
${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}/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}/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}/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
)
#include "xbt/log.h"
#include "xbt/asserts.h"
#include "simgrid/modelchecker.h"
-#include "chord_liveness.h"
#include "mc/mc.h"
/** @addtogroup MSG_examples
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.
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;
+ }
}
/**
if(join_success){
XBT_INFO("Node %d joined the ring", node.id);
node_join = 1;
- //MC_compare();
}
}
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
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?
find_successor(node, id);
}
-int predJoin(void){
+static int predJoin(void){
return node_join;
}
+static int predDeliver(void){
+ return node_deliver;
+}
+
/**
* \brief Main function.
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=");
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();
--- /dev/null
+#! ./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
! 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:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
> [ 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
+
--- /dev/null
+#! ./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
--- /dev/null
+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