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-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)
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_executable(bugged1_liveness bugged1_liveness.c)
add_executable(bugged2_liveness bugged2_liveness.c)
add_executable(chord/chord_liveness chord/chord_liveness.c)
- add_executable(test/snapshot_comparison_liveness1 test/snapshot_comparison_liveness1.c)
- add_executable(test/snapshot_comparison_liveness2 test/snapshot_comparison_liveness2.c)
- add_executable(test/snapshot_comparison_liveness3 test/snapshot_comparison_liveness3.c)
- add_executable(test/snapshot_comparison_liveness4 test/snapshot_comparison_liveness4.c)
- add_executable(test/snapshot_comparison_liveness5 test/snapshot_comparison_liveness5.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_comparison4 test/snapshot_comparison4.c)
+ add_executable(test/snapshot_comparison5 test/snapshot_comparison5.c)
target_link_libraries(centralized simgrid m )
target_link_libraries(bugged1 simgrid m )
target_link_libraries(bugged1_liveness simgrid m )
target_link_libraries(bugged2_liveness simgrid m )
target_link_libraries(chord/chord_liveness simgrid m )
- target_link_libraries(test/snapshot_comparison_liveness1 simgrid m )
- target_link_libraries(test/snapshot_comparison_liveness2 simgrid m )
- target_link_libraries(test/snapshot_comparison_liveness3 simgrid m )
- target_link_libraries(test/snapshot_comparison_liveness4 simgrid m )
- target_link_libraries(test/snapshot_comparison_liveness5 simgrid m )
+ target_link_libraries(test/snapshot_comparison1 simgrid m )
+ target_link_libraries(test/snapshot_comparison2 simgrid m )
+ target_link_libraries(test/snapshot_comparison3 simgrid m )
+ target_link_libraries(test/snapshot_comparison4 simgrid m )
+ target_link_libraries(test/snapshot_comparison5 simgrid m )
endif()
${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}/test/snapshot_comparison_liveness1.c
- ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness2.c
- ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness3.c
- ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness4.c
- ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness5.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_comparison4.c
+ ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison5.c
PARENT_SCOPE
)
set(bin_files
void *snap1 = MC_snapshot();
+ XBT_INFO("First snapshot");
+
MSG_process_sleep(1);
void *snap2 = MC_snapshot();
MSG_process_sleep(1);
-
- int res = MC_compare_snapshots(snap1, snap2);
- XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", res);
+ XBT_INFO("Second snapshot");
+
+ XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
XBT_INFO("**** End test ****");
--- /dev/null
+#! ./tesh
+
+! expect signal SIGABRT
+! timeout 60
+$ ${bindir:=.}/snapshot_comparison1 --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:@) type in variable = 2
+> [ 0.000000] (0:@) Check the liveness property promela
+> [ 1.000000] (1:test@HostA) **** Start test ****
+> [ 1.000000] (1:test@HostA) Take two successive snapshots (No modification)
+> [ 1.000000] (1:test@HostA) First snapshot
+> [ 3.000000] (1:test@HostA) Second snapshot
+> [ 3.000000] (1:test@HostA) Test result : 0 (0 = state equality, 1 = different states)
+> [ 3.000000] (1:test@HostA) **** End test ****
+> [ 0.000000] (0:@) Next pair (depth = 5) already reached !
+> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [ 0.000000] (0:@) | ACCEPTANCE CYCLE |
+> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [ 0.000000] (0:@) Counter-example that violates formula :
+> [ 0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [ 0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [ 0.000000] (0:@) [(1)test] MC_COMPARE_SNAPSHOTS ((null))
+> [ 0.000000] (0:@) End of system requests but evolution in Büchi automaton
+> [ 0.000000] (0:@) Expanded pairs = 5
+> [ 0.000000] (0:@) Visited pairs = 4
+> [ 0.000000] (0:@) Expanded / Visited = 0.800000
#include <simgrid/modelchecker.h>
#include "mc/mc.h"
-XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness2, "Debug information for snasphot comparison liveness1 test example");
+XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness2, "Debug information for snasphot comparison liveness2 test example");
int test(int argc, char **argv);
MSG_process_sleep(1);
+ XBT_INFO("First snapshot");
+
char *toto = xbt_malloc(5);
XBT_INFO("Toto allocated");
MSG_process_sleep(1);
- int res = MC_compare_snapshots(snap1, snap2);
+ XBT_INFO("Second snapshot");
- XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", res);
+ XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
XBT_INFO("**** End test ****");
--- /dev/null
+#! ./tesh
+
+! expect signal SIGABRT
+! timeout 60
+$ ${bindir:=.}/snapshot_comparison2 --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:@) type in variable = 2
+> [ 0.000000] (0:@) Check the liveness property promela
+> [ 1.000000] (1:test@HostA) **** Start test ****
+> [ 1.000000] (1:test@HostA) Malloc after first snapshot
+> [ 2.000000] (1:test@HostA) First snapshot
+> [ 2.000000] (1:test@HostA) Toto allocated
+> [ 3.000000] (1:test@HostA) Second snapshot
+> [ 3.000000] (1:test@HostA) Test result : 1 (0 = state equality, 1 = different states)
+> [ 3.000000] (1:test@HostA) **** End test ****
+> [ 0.000000] (0:@) Next pair (depth = 5) already reached !
+> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [ 0.000000] (0:@) | ACCEPTANCE CYCLE |
+> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [ 0.000000] (0:@) Counter-example that violates formula :
+> [ 0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [ 0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [ 0.000000] (0:@) [(1)test] MC_COMPARE_SNAPSHOTS ((null))
+> [ 0.000000] (0:@) End of system requests but evolution in Büchi automaton
+> [ 0.000000] (0:@) Expanded pairs = 5
+> [ 0.000000] (0:@) Visited pairs = 4
+> [ 0.000000] (0:@) Expanded / Visited = 0.800000
#include <simgrid/modelchecker.h>
#include "mc/mc.h"
-XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness3, "Debug information for snasphot comparison liveness1 test example");
+XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness3, "Debug information for snasphot comparison liveness3 test example");
int test(int argc, char **argv);
MSG_process_sleep(1);
+ XBT_INFO("First snapshot");
+
toto = xbt_malloc(5);
XBT_INFO("Toto allocated");
xbt_free(toto);
void *snap2 = MC_snapshot();
+ XBT_INFO("Second snapshot");
+
MC_ignore_stack("snap2", "test");
MC_ignore_stack("snap1", "test");
--- /dev/null
+#! ./tesh
+
+! expect signal SIGABRT
+! timeout 60
+$ ${bindir:=.}/snapshot_comparison3 --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:@) type in variable = 2
+> [ 0.000000] (0:@) Check the liveness property promela
+> [ 1.000000] (1:test@HostA) **** Start test ****
+> [ 1.000000] (1:test@HostA) Malloc and free after first snapshot
+> [ 2.000000] (1:test@HostA) First snapshot
+> [ 2.000000] (1:test@HostA) Toto allocated
+> [ 2.000000] (1:test@HostA) Toto free
+> [ 3.000000] (1:test@HostA) Second snapshot
+> [ 3.000000] (1:test@HostA) Test result : 0 (0 = state equality, 1 = different states)
+> [ 3.000000] (1:test@HostA) **** End test ****
+> [ 0.000000] (0:@) Next pair (depth = 5) already reached !
+> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [ 0.000000] (0:@) | ACCEPTANCE CYCLE |
+> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [ 0.000000] (0:@) Counter-example that violates formula :
+> [ 0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [ 0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [ 0.000000] (0:@) [(1)test] MC_COMPARE_SNAPSHOTS ((null))
+> [ 0.000000] (0:@) End of system requests but evolution in Büchi automaton
+> [ 0.000000] (0:@) Expanded pairs = 5
+> [ 0.000000] (0:@) Visited pairs = 4
+> [ 0.000000] (0:@) Expanded / Visited = 0.800000
#include <simgrid/modelchecker.h>
#include "mc/mc.h"
-XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness4, "Debug information for snasphot comparison liveness1 test example");
+XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness4, "Debug information for snasphot comparison liveness4 test example");
int test(int argc, char **argv);
MSG_process_sleep(1);
+ XBT_INFO("First snapshot");
+
xbt_free(toto);
XBT_INFO("Toto free");
void *snap2 = MC_snapshot();
+ XBT_INFO("Second snapshot");
+
MSG_process_sleep(1);
MC_ignore_stack("snap2", "test");
--- /dev/null
+#! ./tesh
+
+! expect signal SIGABRT
+! timeout 60
+$ ${bindir:=.}/snapshot_comparison4 --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:@) type in variable = 2
+> [ 0.000000] (0:@) Check the liveness property promela
+> [ 1.000000] (1:test@HostA) **** Start test ****
+> [ 1.000000] (1:test@HostA) Free after first snapshot
+> [ 1.000000] (1:test@HostA) Toto allocated
+> [ 2.000000] (1:test@HostA) First snapshot
+> [ 2.000000] (1:test@HostA) Toto free
+> [ 2.000000] (1:test@HostA) Second snapshot
+> [ 3.000000] (1:test@HostA) Test result : 1 (0 = state equality, 1 = different states)
+> [ 3.000000] (1:test@HostA) **** End test ****
+> [ 0.000000] (0:@) Next pair (depth = 5) already reached !
+> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [ 0.000000] (0:@) | ACCEPTANCE CYCLE |
+> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [ 0.000000] (0:@) Counter-example that violates formula :
+> [ 0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [ 0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [ 0.000000] (0:@) [(1)test] MC_COMPARE_SNAPSHOTS ((null))
+> [ 0.000000] (0:@) End of system requests but evolution in Büchi automaton
+> [ 0.000000] (0:@) Expanded pairs = 5
+> [ 0.000000] (0:@) Visited pairs = 4
+> [ 0.000000] (0:@) Expanded / Visited = 0.800000
\ No newline at end of file
#include <simgrid/modelchecker.h>
#include "mc/mc.h"
-XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness5, "Debug information for snasphot comparison liveness1 test example");
+XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness5, "Debug information for snasphot comparison liveness5 test example");
int test(int argc, char **argv);
MSG_process_sleep(1);
+ XBT_INFO("First snapshot");
+
j = 1;
XBT_INFO("j = %d", j);
MSG_process_sleep(1);
+ XBT_INFO("Second snapshot");
+
MC_ignore_stack("snap2", "test");
MC_ignore_stack("snap1", "test");
--- /dev/null
+#! ./tesh
+
+! expect signal SIGABRT
+! timeout 60
+$ ${bindir:=.}/snapshot_comparison5 --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:@) type in variable = 2
+> [ 0.000000] (0:@) Check the liveness property promela
+> [ 1.000000] (1:test@HostA) **** Start test ****
+> [ 1.000000] (1:test@HostA) Increment local variable
+> [ 1.000000] (1:test@HostA) j = 0
+> [ 2.000000] (1:test@HostA) First snapshot
+> [ 2.000000] (1:test@HostA) j = 1
+> [ 3.000000] (1:test@HostA) Second snapshot
+> [ 3.000000] (1:test@HostA) Test result : 1 (0 = state equality, 1 = different states)
+> [ 3.000000] (1:test@HostA) **** End test ****
+> [ 0.000000] (0:@) Next pair (depth = 5) already reached !
+> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [ 0.000000] (0:@) | ACCEPTANCE CYCLE |
+> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
+> [ 0.000000] (0:@) Counter-example that violates formula :
+> [ 0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [ 0.000000] (0:@) [(1)test] MC_SNAPSHOT ((null))
+> [ 0.000000] (0:@) [(1)test] MC_COMPARE_SNAPSHOTS ((null))
+> [ 0.000000] (0:@) End of system requests but evolution in Büchi automaton
+> [ 0.000000] (0:@) Expanded pairs = 5
+> [ 0.000000] (0:@) Visited pairs = 4
+> [ 0.000000] (0:@) Expanded / Visited = 0.800000