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()
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)
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)
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 )
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
${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
${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
${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
)
--- /dev/null
+#! ./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
}
}
+ MC_assert(!node_join);
+
if (join_success) {
while (MSG_get_clock() < init_time + deadline
*/
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;
*/
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)) {
--- /dev/null
+#! ./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
+
--- /dev/null
+#! ./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
<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>
--- /dev/null
+<?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>
+++ /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
+++ /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
-> [ 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
-
-
+++ /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] (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
+++ /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
+++ /dev/null
-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
exit 1
fi
+HOSTFILETMP=0
if [ -z "${HOSTFILE}" ] ; then
HOSTFILETMP=1
HOSTFILE="$(mktemp tmphostXXXXXX)"
export SMPI_GLOBAL_SIZE=${NUMPROCS}
if [ -n "${KEEP}" ] ; then
echo ${EXEC} ${TRACEOPTIONS} ${SIMOPTS} ${PLATFORMTMP} ${APPLICATIONTMP}
- if [ ${HOSTFILETMP} == 1 ] ; then
+ if [ ${HOSTFILETMP} = 1 ] ; then
echo "Generated hostfile ${HOSTFILE} keeped."
fi
fi
if [ -z "${PLATFORM}" ]; then
rm ${PLATFORMTMP}
fi
- if [ ${HOSTFILETMP} == 1 ] ; then
+ if [ ${HOSTFILETMP} = 1 ] ; then
rm ${HOSTFILE}
fi
rm ${APPLICATIONTMP}