From: Marion Guthmuller Date: Mon, 5 Aug 2013 13:33:33 +0000 (+0200) Subject: model-checker : remove obsolete examples X-Git-Tag: v3_9_90~128^2~40 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/799c4fd899768d0184af411ea5b76377589aa9c6 model-checker : remove obsolete examples --- diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt index 845088eade..fb284c8dff 100644 --- a/examples/msg/mc/CMakeLists.txt +++ b/examples/msg/mc/CMakeLists.txt @@ -3,7 +3,6 @@ cmake_minimum_required(VERSION 2.6) 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) @@ -14,11 +13,6 @@ if(HAVE_MC) 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 ) @@ -28,11 +22,6 @@ if(HAVE_MC) 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() @@ -44,11 +33,6 @@ set(tesh_files ${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 @@ -62,8 +46,6 @@ 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 @@ -78,11 +60,6 @@ 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 @@ -90,7 +67,6 @@ 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 diff --git a/examples/msg/mc/test/deploy_snapshot_comparison.xml b/examples/msg/mc/test/deploy_snapshot_comparison.xml deleted file mode 100644 index 70067b51f9..0000000000 --- a/examples/msg/mc/test/deploy_snapshot_comparison.xml +++ /dev/null @@ -1,5 +0,0 @@ - - - - - \ No newline at end of file diff --git a/examples/msg/mc/test/promela b/examples/msg/mc/test/promela deleted file mode 100644 index 54b9747fed..0000000000 --- a/examples/msg/mc/test/promela +++ /dev/null @@ -1,10 +0,0 @@ -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 diff --git a/examples/msg/mc/test/snapshot_comparison1.c b/examples/msg/mc/test/snapshot_comparison1.c deleted file mode 100644 index 126c590243..0000000000 --- a/examples/msg/mc/test/snapshot_comparison1.c +++ /dev/null @@ -1,55 +0,0 @@ -/* 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 -#include -#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; -} diff --git a/examples/msg/mc/test/snapshot_comparison1.tesh b/examples/msg/mc/test/snapshot_comparison1.tesh deleted file mode 100644 index 119844a1f2..0000000000 --- a/examples/msg/mc/test/snapshot_comparison1.tesh +++ /dev/null @@ -1,13 +0,0 @@ -#! ./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 **** diff --git a/examples/msg/mc/test/snapshot_comparison2.c b/examples/msg/mc/test/snapshot_comparison2.c deleted file mode 100644 index 9c08973e5c..0000000000 --- a/examples/msg/mc/test/snapshot_comparison2.c +++ /dev/null @@ -1,60 +0,0 @@ -/* 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 -#include -#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; -} diff --git a/examples/msg/mc/test/snapshot_comparison2.tesh b/examples/msg/mc/test/snapshot_comparison2.tesh deleted file mode 100644 index 230bbcce5c..0000000000 --- a/examples/msg/mc/test/snapshot_comparison2.tesh +++ /dev/null @@ -1,14 +0,0 @@ -#! ./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 **** diff --git a/examples/msg/mc/test/snapshot_comparison3.c b/examples/msg/mc/test/snapshot_comparison3.c deleted file mode 100644 index e46578fe99..0000000000 --- a/examples/msg/mc/test/snapshot_comparison3.c +++ /dev/null @@ -1,66 +0,0 @@ -/* 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 -#include -#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; -} diff --git a/examples/msg/mc/test/snapshot_comparison3.tesh b/examples/msg/mc/test/snapshot_comparison3.tesh deleted file mode 100644 index 6589319479..0000000000 --- a/examples/msg/mc/test/snapshot_comparison3.tesh +++ /dev/null @@ -1,15 +0,0 @@ -#! ./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 **** diff --git a/examples/msg/mc/test/snapshot_comparison4.c b/examples/msg/mc/test/snapshot_comparison4.c deleted file mode 100644 index bff95bfe0a..0000000000 --- a/examples/msg/mc/test/snapshot_comparison4.c +++ /dev/null @@ -1,64 +0,0 @@ -/* 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 -#include -#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; -} diff --git a/examples/msg/mc/test/snapshot_comparison4.tesh b/examples/msg/mc/test/snapshot_comparison4.tesh deleted file mode 100644 index 6f4ca6546d..0000000000 --- a/examples/msg/mc/test/snapshot_comparison4.tesh +++ /dev/null @@ -1,15 +0,0 @@ -#! ./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 diff --git a/examples/msg/mc/test/snapshot_comparison5.c b/examples/msg/mc/test/snapshot_comparison5.c deleted file mode 100644 index 307885419a..0000000000 --- a/examples/msg/mc/test/snapshot_comparison5.c +++ /dev/null @@ -1,64 +0,0 @@ -/* 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 -#include -#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; -} diff --git a/examples/msg/mc/test/snapshot_comparison5.tesh b/examples/msg/mc/test/snapshot_comparison5.tesh deleted file mode 100644 index d483ae3c7d..0000000000 --- a/examples/msg/mc/test/snapshot_comparison5.tesh +++ /dev/null @@ -1,15 +0,0 @@ -#! ./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 **** diff --git a/examples/msg/mc/test/snapshot_comparison_platform.xml b/examples/msg/mc/test/snapshot_comparison_platform.xml deleted file mode 100644 index cc4ea2c55b..0000000000 --- a/examples/msg/mc/test/snapshot_comparison_platform.xml +++ /dev/null @@ -1,17 +0,0 @@ - - - - - - - - - - - - - - - - - \ No newline at end of file