if(HAVE_MC)
set(EXECUTABLE_OUTPUT_PATH "${CMAKE_CURRENT_BINARY_DIR}")
- file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/test/")
file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/chord/")
add_executable(centralized centralized_mutex.c)
add_executable(bugged1_liveness bugged1_liveness.c)
add_executable(bugged2_liveness bugged2_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)
- add_executable(test/snapshot_comparison4 test/snapshot_comparison4.c)
- add_executable(test/snapshot_comparison5 test/snapshot_comparison5.c)
target_link_libraries(centralized simgrid )
target_link_libraries(bugged1 simgrid )
target_link_libraries(bugged1_liveness simgrid )
target_link_libraries(bugged2_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 )
- target_link_libraries(test/snapshot_comparison4 simgrid )
- target_link_libraries(test/snapshot_comparison5 simgrid )
endif()
${CMAKE_CURRENT_SOURCE_DIR}/centralized.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}/test/snapshot_comparison4.tesh
- ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison5.tesh
PARENT_SCOPE
)
set(xml_files
${CMAKE_CURRENT_SOURCE_DIR}/deploy_mutex.xml
${CMAKE_CURRENT_SOURCE_DIR}/platform.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
)
set(examples_src
${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.h
${CMAKE_CURRENT_SOURCE_DIR}/bugged2_liveness.h
${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}/test/snapshot_comparison4.c
- ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison5.c
PARENT_SCOPE
)
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}/test/promela
PARENT_SCOPE
)
set(txt_files
+++ /dev/null
-<?xml version='1.0'?>
-<!DOCTYPE platform SYSTEM "http://simgrid.gforge.inria.fr/simgrid.dtd">
-<platform version="3">
- <process host="HostA" function="test"/>
-</platform>
\ No newline at end of file
+++ /dev/null
-never {
-T0_init : /* init */
- if
- :: (1) -> goto accept_S2
- fi;
-accept_S2 : /* 1 */
- if
- :: (1) -> goto accept_S2
- fi;
-}
\ No newline at end of file
+++ /dev/null
-/* Copyright (c) 2012. The SimGrid Team.
- * All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include <msg/msg.h>
-#include <simgrid/modelchecker.h>
-#include "mc/mc.h"
-
-XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness1, "Debug information for snasphot comparison liveness1 test example");
-
-int test(int argc, char **argv);
-
-int test(int argc, char **argv){
-
- MSG_process_sleep(1);
-
- XBT_INFO("**** Start test ****");
- XBT_INFO("Take two successive snapshots (No modification)");
-
- void *snap1 = MC_snapshot();
-
- XBT_INFO("First snapshot");
-
- MSG_process_sleep(1);
-
- void *snap2 = MC_snapshot();
-
- MSG_process_sleep(1);
-
- XBT_INFO("Second snapshot");
-
- XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
-
- XBT_INFO("**** End test ****");
-
- xbt_abort();
-}
-
-int main(int argc, char **argv){
- MSG_init(&argc, argv);
-
- MSG_config("model-check/property","promela");
-
- MSG_create_environment("snapshot_comparison_platform.xml");
-
- MSG_function_register("test", test);
-
- MSG_launch_application("deploy_snapshot_comparison.xml");
-
- MSG_main();
-
- return 0;
-}
+++ /dev/null
-#! ./tesh
-
-! expect signal SIGABRT
-! timeout 200
-$ ${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:@) Check the liveness property promela
-> [ 0.000000] (1:test@HostA) **** Start test ****
-> [ 0.000000] (1:test@HostA) Take two successive snapshots (No modification)
-> [ 0.000000] (1:test@HostA) First snapshot
-> [ 0.000000] (1:test@HostA) Second snapshot
-> [ 0.000000] (1:test@HostA) Test result : 0 (0 = state equality, 1 = different states)
-> [ 0.000000] (1:test@HostA) **** End test ****
+++ /dev/null
-/* Copyright (c) 2012. The SimGrid Team.
- * All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include <msg/msg.h>
-#include <simgrid/modelchecker.h>
-#include "mc/mc.h"
-
-XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness2, "Debug information for snasphot comparison liveness2 test example");
-
-int test(int argc, char **argv);
-
-int test(int argc, char **argv){
-
- MSG_process_sleep(1);
-
- XBT_INFO("**** Start test ****");
- XBT_INFO("Malloc after first snapshot");
-
- void *snap1 = MC_snapshot();
-
- MSG_process_sleep(1);
-
- XBT_INFO("First snapshot");
-
- char *toto = xbt_malloc(5);
- XBT_INFO("Toto allocated");
-
- void *snap2 = MC_snapshot();
-
- MSG_process_sleep(1);
-
- XBT_INFO("Second snapshot");
-
- XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
-
- XBT_INFO("**** End test ****");
-
- xbt_free(toto);
-
- xbt_abort();
-}
-
-int main(int argc, char **argv){
- MSG_init(&argc, argv);
-
- MSG_config("model-check/property","promela");
-
- MSG_create_environment("snapshot_comparison_platform.xml");
-
- MSG_function_register("test", test);
-
- MSG_launch_application("deploy_snapshot_comparison.xml");
-
- MSG_main();
-
- return 0;
-}
+++ /dev/null
-#! ./tesh
-
-! expect signal SIGABRT
-! timeout 200
-$ ${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:@) Check the liveness property promela
-> [ 0.000000] (1:test@HostA) **** Start test ****
-> [ 0.000000] (1:test@HostA) Malloc after first snapshot
-> [ 0.000000] (1:test@HostA) First snapshot
-> [ 0.000000] (1:test@HostA) Toto allocated
-> [ 0.000000] (1:test@HostA) Second snapshot
-> [ 0.000000] (1:test@HostA) Test result : 1 (0 = state equality, 1 = different states)
-> [ 0.000000] (1:test@HostA) **** End test ****
+++ /dev/null
-/* Copyright (c) 2012. The SimGrid Team.
- * All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include <msg/msg.h>
-#include <simgrid/modelchecker.h>
-#include "mc/mc.h"
-
-XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness3, "Debug information for snasphot comparison liveness3 test example");
-
-int test(int argc, char **argv);
-
-int test(int argc, char **argv){
-
- MSG_process_sleep(1);
-
- XBT_INFO("**** Start test ****");
- XBT_INFO("Malloc and free after first snapshot");
-
- char *toto = NULL;
-
- void *snap1 = MC_snapshot();
-
- MSG_process_sleep(1);
-
- XBT_INFO("First snapshot");
-
- toto = xbt_malloc(5);
- XBT_INFO("Toto allocated");
- xbt_free(toto);
- toto = NULL;
- XBT_INFO("Toto free");
-
- MSG_process_sleep(1);
-
- void *snap2 = MC_snapshot();
-
- XBT_INFO("Second snapshot");
-
- MC_ignore_stack("snap2", "test");
- MC_ignore_stack("snap1", "test");
-
- XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
-
- XBT_INFO("**** End test ****");
-
- xbt_abort();
-}
-
-int main(int argc, char **argv){
- MSG_init(&argc, argv);
-
- MSG_config("model-check/property","promela");
-
- MSG_create_environment("snapshot_comparison_platform.xml");
-
- MSG_function_register("test", test);
-
- MSG_launch_application("deploy_snapshot_comparison.xml");
-
- MSG_main();
-
- return 0;
-}
+++ /dev/null
-#! ./tesh
-
-! expect signal SIGABRT
-! timeout 200
-$ ${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:@) Check the liveness property promela
-> [ 0.000000] (1:test@HostA) **** Start test ****
-> [ 0.000000] (1:test@HostA) Malloc and free after first snapshot
-> [ 0.000000] (1:test@HostA) First snapshot
-> [ 0.000000] (1:test@HostA) Toto allocated
-> [ 0.000000] (1:test@HostA) Toto free
-> [ 0.000000] (1:test@HostA) Second snapshot
-> [ 0.000000] (1:test@HostA) Test result : 0 (0 = state equality, 1 = different states)
-> [ 0.000000] (1:test@HostA) **** End test ****
+++ /dev/null
-/* Copyright (c) 2012. The SimGrid Team.
- * All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include <msg/msg.h>
-#include <simgrid/modelchecker.h>
-#include "mc/mc.h"
-
-XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness4, "Debug information for snasphot comparison liveness4 test example");
-
-int test(int argc, char **argv);
-
-int test(int argc, char **argv){
-
- MSG_process_sleep(1);
-
- XBT_INFO("**** Start test ****");
- XBT_INFO("Free after first snapshot");
-
- char *toto = xbt_malloc(5);
- XBT_INFO("Toto allocated");
-
- void *snap1 = MC_snapshot();
-
- 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");
- MC_ignore_stack("snap1", "test");
-
- XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
-
- XBT_INFO("**** End test ****");
-
- xbt_abort();
-}
-
-int main(int argc, char **argv){
- MSG_init(&argc, argv);
-
- MSG_config("model-check/property","promela");
-
- MSG_create_environment("snapshot_comparison_platform.xml");
-
- MSG_function_register("test", test);
-
- MSG_launch_application("deploy_snapshot_comparison.xml");
-
- MSG_main();
-
- return 0;
-}
+++ /dev/null
-#! ./tesh
-
-! expect signal SIGABRT
-! timeout 200
-$ ${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:@) Check the liveness property promela
-> [ 0.000000] (1:test@HostA) **** Start test ****
-> [ 0.000000] (1:test@HostA) Free after first snapshot
-> [ 0.000000] (1:test@HostA) Toto allocated
-> [ 0.000000] (1:test@HostA) First snapshot
-> [ 0.000000] (1:test@HostA) Toto free
-> [ 0.000000] (1:test@HostA) Second snapshot
-> [ 0.000000] (1:test@HostA) Test result : 1 (0 = state equality, 1 = different states)
-> [ 0.000000] (1:test@HostA) **** End test ****
\ No newline at end of file
+++ /dev/null
-/* Copyright (c) 2012. The SimGrid Team.
- * All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include <msg/msg.h>
-#include <simgrid/modelchecker.h>
-#include "mc/mc.h"
-
-XBT_LOG_NEW_DEFAULT_CATEGORY(snapshot_comparison_liveness5, "Debug information for snasphot comparison liveness5 test example");
-
-int test(int argc, char **argv);
-
-int test(int argc, char **argv){
-
- MSG_process_sleep(1);
-
- XBT_INFO("**** Start test ****");
- XBT_INFO("Increment local variable");
-
- int j = 0;
- XBT_INFO("j = %d", j);
-
- void *snap1 = MC_snapshot();
-
- MSG_process_sleep(1);
-
- XBT_INFO("First snapshot");
-
- j = 1;
- XBT_INFO("j = %d", j);
-
- void *snap2 = MC_snapshot();
-
- MSG_process_sleep(1);
-
- XBT_INFO("Second snapshot");
-
- MC_ignore_stack("snap2", "test");
- MC_ignore_stack("snap1", "test");
-
- XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", MC_compare_snapshots(snap1, snap2));
-
- XBT_INFO("**** End test ****");
-
- xbt_abort();
-}
-
-int main(int argc, char **argv){
- MSG_init(&argc, argv);
-
- MSG_config("model-check/property","promela");
-
- MSG_create_environment("snapshot_comparison_platform.xml");
-
- MSG_function_register("test", test);
-
- MSG_launch_application("deploy_snapshot_comparison.xml");
-
- MSG_main();
-
- return 0;
-}
+++ /dev/null
-#! ./tesh
-
-! expect signal SIGABRT
-! timeout 200
-$ ${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:@) Check the liveness property promela
-> [ 0.000000] (1:test@HostA) **** Start test ****
-> [ 0.000000] (1:test@HostA) Increment local variable
-> [ 0.000000] (1:test@HostA) j = 0
-> [ 0.000000] (1:test@HostA) First snapshot
-> [ 0.000000] (1:test@HostA) j = 1
-> [ 0.000000] (1:test@HostA) Second snapshot
-> [ 0.000000] (1:test@HostA) Test result : 1 (0 = state equality, 1 = different states)
-> [ 0.000000] (1:test@HostA) **** End test ****
+++ /dev/null
-<?xml version='1.0'?>
- <!DOCTYPE platform SYSTEM "http://simgrid.gforge.inria.fr/simgrid.dtd">
- <platform version="3">
- <AS id="AS0" routing="Full">
- <host id="HostA" power="137.333Mf"/>
- <host id="HostB" power="98.095Mf"/>
- <host id="HostC" power="98.095Mf"/>
- <host id="HostD" power="98.095Mf"/>
- <link id="1" bandwidth="3.430125MBps" latency="536.941us"/>
- <link id="2" bandwidth="3.430125MBps" latency="536.941us"/>
- <link id="3" bandwidth="3.430125MBps" latency="536.941us"/>
- <route src="HostA" dst="HostB"><link_ctn id="1"/></route>
- <route src="HostA" dst="HostC"><link_ctn id="2"/></route>
- <route src="HostA" dst="HostD"><link_ctn id="3"/></route>
- </AS>
- </platform>
-
\ No newline at end of file
