From: Marion Guthmuller Date: Fri, 19 Oct 2012 08:31:57 +0000 (+0200) Subject: model-checker : test examples for snapshot comparison X-Git-Tag: v3_9_rc1~91^2~165 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/eb77317176edc7ac4aa1fb08d22bc44ca00261ff?ds=sidebyside model-checker : test examples for snapshot comparison --- diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt index 17cd5c2390..d561c9f405 100644 --- a/examples/msg/mc/CMakeLists.txt +++ b/examples/msg/mc/CMakeLists.txt @@ -12,6 +12,11 @@ if(HAVE_MC) add_executable(random_test random_test.c) add_executable(bugged1_liveness bugged1_liveness.c) add_executable(bugged2_liveness bugged2_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) target_link_libraries(centralized simgrid m ) target_link_libraries(bugged1 simgrid m ) @@ -20,6 +25,11 @@ if(HAVE_MC) target_link_libraries(random_test simgrid m ) target_link_libraries(bugged1_liveness simgrid m ) target_link_libraries(bugged2_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 ) endif() @@ -40,6 +50,7 @@ set(xml_files ${CMAKE_CURRENT_SOURCE_DIR}/deploy_mutex.xml ${CMAKE_CURRENT_SOURCE_DIR}/deploy_random_test.xml ${CMAKE_CURRENT_SOURCE_DIR}/platform.xml + ${CMAKE_CURRENT_SOURCE_DIR}/test/deploy_snapshot_comparison.xml PARENT_SCOPE ) set(examples_src @@ -53,6 +64,11 @@ set(examples_src ${CMAKE_CURRENT_SOURCE_DIR}/random_test.c ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.h ${CMAKE_CURRENT_SOURCE_DIR}/bugged2_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 PARENT_SCOPE ) set(bin_files @@ -60,6 +76,7 @@ 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 new file mode 100644 index 0000000000..70067b51f9 --- /dev/null +++ b/examples/msg/mc/test/deploy_snapshot_comparison.xml @@ -0,0 +1,5 @@ + + + + + \ No newline at end of file diff --git a/examples/msg/mc/test/promela b/examples/msg/mc/test/promela new file mode 100644 index 0000000000..54b9747fed --- /dev/null +++ b/examples/msg/mc/test/promela @@ -0,0 +1,10 @@ +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_comparison_liveness1.c b/examples/msg/mc/test/snapshot_comparison_liveness1.c new file mode 100644 index 0000000000..5341091988 --- /dev/null +++ b/examples/msg/mc/test/snapshot_comparison_liveness1.c @@ -0,0 +1,53 @@ +/* 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(); + + 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("**** End test ****"); + + return 0; +} + +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_comparison_liveness2.c b/examples/msg/mc/test/snapshot_comparison_liveness2.c new file mode 100644 index 0000000000..969ee85340 --- /dev/null +++ b/examples/msg/mc/test/snapshot_comparison_liveness2.c @@ -0,0 +1,56 @@ +/* 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 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("Malloc after first snapshot"); + + void *snap1 = MC_snapshot(); + + MSG_process_sleep(1); + + char *toto = xbt_malloc(5); + XBT_INFO("Toto value %s", toto); + + 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("**** End test ****"); + + return 0; +} + +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_comparison_liveness3.c b/examples/msg/mc/test/snapshot_comparison_liveness3.c new file mode 100644 index 0000000000..fdf8966abd --- /dev/null +++ b/examples/msg/mc/test/snapshot_comparison_liveness3.c @@ -0,0 +1,59 @@ +/* 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 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("Malloc and free after first snapshot"); + + void *snap1 = MC_snapshot(); + + MSG_process_sleep(1); + + char *toto = NULL; + toto = xbt_malloc(5); + XBT_INFO("Toto value %s", toto); + xbt_free(toto); + toto = NULL; + + MSG_process_sleep(1); + + void *snap2 = MC_snapshot(); + + int res = MC_compare_snapshots(snap1, snap2); + + XBT_INFO("Test result : %d (0 = state equality, 1 = different states)", res); + + XBT_INFO("**** End test ****"); + + return 0; +} + +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_comparison_liveness4.c b/examples/msg/mc/test/snapshot_comparison_liveness4.c new file mode 100644 index 0000000000..f116228f20 --- /dev/null +++ b/examples/msg/mc/test/snapshot_comparison_liveness4.c @@ -0,0 +1,58 @@ +/* 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 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("Free after first snapshot"); + + char *toto = xbt_malloc(5); + XBT_INFO("Toto value %s", toto); + + void *snap1 = MC_snapshot(); + + MSG_process_sleep(1); + + xbt_free(toto); + + 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("**** End test ****"); + + return 0; +} + +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_comparison_liveness5.c b/examples/msg/mc/test/snapshot_comparison_liveness5.c new file mode 100644 index 0000000000..acb72d1f46 --- /dev/null +++ b/examples/msg/mc/test/snapshot_comparison_liveness5.c @@ -0,0 +1,59 @@ +/* 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 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("Increment local variable"); + + int j = 0; + XBT_INFO("j = %d", j); + + void *snap1 = MC_snapshot(); + + MSG_process_sleep(1); + + j = 1; + XBT_INFO("j = %d", j); + + 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("**** End test ****"); + + return 0; +} + +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_comparison_platform.xml b/examples/msg/mc/test/snapshot_comparison_platform.xml new file mode 100644 index 0000000000..a62a6e0334 --- /dev/null +++ b/examples/msg/mc/test/snapshot_comparison_platform.xml @@ -0,0 +1,17 @@ + + + + + + + + + + + + + + + + + \ No newline at end of file