mess with mc examples platform

(prepare the transition to s4u)

diff --git a/MANIFEST.in b/MANIFEST.in
index 9adbfd3..f550773 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -272,7 +272,6 @@ include examples/deprecated/msg/mc/deploy_bugged2.xml
 include examples/deprecated/msg/mc/deploy_bugged2_liveness.xml
 include examples/deprecated/msg/mc/deploy_bugged3.xml
 include examples/deprecated/msg/mc/deploy_centralized_mutex.xml
-include examples/deprecated/msg/mc/platform.xml
 include examples/deprecated/msg/mc/promela_bugged1_liveness
 include examples/deprecated/msg/mc/promela_bugged2_liveness
 include examples/deprecated/msg/trace-categories/trace-categories.c
@@ -468,7 +467,6 @@ include examples/s4u/io-file-system/s4u-io-file-system.cpp
 include examples/s4u/io-file-system/s4u-io-file-system.tesh
 include examples/s4u/maestro-set/s4u-maestro-set.cpp
 include examples/s4u/maestro-set/s4u-maestro-set.tesh
-include examples/s4u/mc-electric-fence/platform.xml
 include examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp
 include examples/s4u/mc-electric-fence/s4u-mc-electric-fence.tesh
 include examples/s4u/mc-failing-assert/s4u-mc-failing-assert.cpp
@@ -1897,6 +1895,7 @@ include examples/platforms/g5k.xml
 include examples/platforms/griffon.xml
 include examples/platforms/hosts_with_disks.xml
 include examples/platforms/meta_cluster.xml
+include examples/platforms/model_checker_platform.xml
 include examples/platforms/multicore_machine.xml
 include examples/platforms/ns3-big-cluster.xml
 include examples/platforms/onelink.xml

diff --git a/examples/deprecated/msg/mc/CMakeLists.txt b/examples/deprecated/msg/mc/CMakeLists.txt
index e83a129..31a9c38 100644 (file)
--- a/examples/deprecated/msg/mc/CMakeLists.txt
+++ b/examples/deprecated/msg/mc/CMakeLists.txt
@@ -21,11 +21,19 @@ if(SIMGRID_HAVE_MC AND SIMGRID_HAVE_MSG)
     add_dependencies(tests bugged1_liveness_cleaner_off)
   endif()
 
-  ADD_TESH_FACTORIES(mc-bugged1                "ucontext;raw" --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1.tesh)
-  ADD_TESH_FACTORIES(mc-bugged2                "ucontext;raw" --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged2.tesh)
+  ADD_TESH_FACTORIES(mc-bugged1    "ucontext;raw" --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc
+                                                  --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms 
+                                                  --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1.tesh)
+  ADD_TESH_FACTORIES(mc-bugged2    "ucontext;raw" --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc 
+                                                  --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms 
+                                                  --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged2.tesh)
   IF(HAVE_UCONTEXT_CONTEXTS AND SIMGRID_PROCESSOR_x86_64) # liveness model-checking works only on 64bits (for now ...)
-    ADD_TESH(mc-bugged1-liveness-ucontext         --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness.tesh)
-    ADD_TESH(mc-bugged1-liveness-visited-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness_visited.tesh)
+    ADD_TESH(mc-bugged1-liveness-ucontext         --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc 
+                                                  --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms 
+                                                  --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness.tesh)
+    ADD_TESH(mc-bugged1-liveness-visited-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc 
+                                                  --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms 
+                                                  --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness_visited.tesh)
     IF(HAVE_C_STACK_CLEANER)
       # This test checks if the stack cleaner is making a difference:
       ADD_TEST(mc-bugged1-liveness-stack-cleaner ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc/bugged1_liveness_stack_cleaner ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc/ ${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc/)
@@ -42,8 +50,7 @@ set(tesh_files   ${tesh_files}    ${CMAKE_CURRENT_SOURCE_DIR}/bugged1.tesh
                                   ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.tesh
                                   ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness_visited.tesh
                                   ${CMAKE_CURRENT_SOURCE_DIR}/centralized_mutex.tesh                PARENT_SCOPE)
-set(xml_files    ${xml_files}     ${CMAKE_CURRENT_SOURCE_DIR}/deploy_bugged1_liveness_visited.xml
-                                  ${CMAKE_CURRENT_SOURCE_DIR}/platform.xml                          PARENT_SCOPE)
+set(xml_files    ${xml_files}     ${CMAKE_CURRENT_SOURCE_DIR}/deploy_bugged1_liveness_visited.xml   PARENT_SCOPE)
 set(examples_src ${examples_src}                                                                    PARENT_SCOPE)
 set(bin_files    ${bin_files}     ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged1_liveness
                                   ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged2_liveness

diff --git a/examples/deprecated/msg/mc/bugged1.c b/examples/deprecated/msg/mc/bugged1.c
index efc27d6..66c0238 100644 (file)
--- a/examples/deprecated/msg/mc/bugged1.c
+++ b/examples/deprecated/msg/mc/bugged1.c
@@ -49,7 +49,7 @@ int main(int argc, char *argv[])
 {
   MSG_init(&argc, argv);
 
-  MSG_create_environment("platform.xml");
+  MSG_create_environment(argv[1]);
 
   MSG_function_register("server", server);
   MSG_function_register("client", client);

diff --git a/examples/deprecated/msg/mc/bugged1.tesh b/examples/deprecated/msg/mc/bugged1.tesh
index 2aea478..186e9a2 100644 (file)
--- a/examples/deprecated/msg/mc/bugged1.tesh
+++ b/examples/deprecated/msg/mc/bugged1.tesh
@@ -2,7 +2,7 @@
 
 ! expect return 1
 ! timeout 20
-$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack-size:256
+$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1 ${platfdir:=.}/model_checker_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack-size:256
 > [  0.000000] (0:maestro@) Check a safety property. Reduction is: dpor.
 > [  0.000000] (2:client@HostB) Sent!
 > [  0.000000] (3:client@HostC) Sent!

diff --git a/examples/deprecated/msg/mc/bugged1_liveness.tesh b/examples/deprecated/msg/mc/bugged1_liveness.tesh
index c835b72..eb75726 100644 (file)
--- a/examples/deprecated/msg/mc/bugged1_liveness.tesh
+++ b/examples/deprecated/msg/mc/bugged1_liveness.tesh
@@ -3,7 +3,7 @@
 ! expect return 2
 ! timeout 20
 ! output ignore
-$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../../platforms/small_platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack-size:256 --cfg=model-check/property:promela_bugged1_liveness
+$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${platfdir:=.}/small_platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack-size:256 --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:maestro@) Check the liveness property promela_bugged1_liveness
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (3:client@Fafard) Ask the request

diff --git a/examples/deprecated/msg/mc/bugged1_liveness_visited.tesh b/examples/deprecated/msg/mc/bugged1_liveness_visited.tesh
index f8c4584..2cd54ab 100644 (file)
--- a/examples/deprecated/msg/mc/bugged1_liveness_visited.tesh
+++ b/examples/deprecated/msg/mc/bugged1_liveness_visited.tesh
@@ -3,7 +3,7 @@
 ! expect return 2
 ! timeout 30
 ! output ignore
-$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../../platforms/small_platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack-size:256  --cfg=model-check/property:promela_bugged1_liveness
+$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${platfdir:=.}/small_platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack-size:256  --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:maestro@) Check the liveness property promela_bugged1_liveness
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (3:client@Fafard) Ask the request

diff --git a/examples/deprecated/msg/mc/bugged2.c b/examples/deprecated/msg/mc/bugged2.c
index 448c054..e8932b8 100644 (file)
--- a/examples/deprecated/msg/mc/bugged2.c
+++ b/examples/deprecated/msg/mc/bugged2.c
@@ -66,7 +66,7 @@ int main(int argc, char *argv[])
 {
   MSG_init(&argc, argv);
 
-  MSG_create_environment("platform.xml");
+  MSG_create_environment(argv[1]);
 
   MSG_function_register("server", server);
   MSG_function_register("client", client);

diff --git a/examples/deprecated/msg/mc/bugged2.tesh b/examples/deprecated/msg/mc/bugged2.tesh
index 719ffe2..d59df82 100644 (file)
--- a/examples/deprecated/msg/mc/bugged2.tesh
+++ b/examples/deprecated/msg/mc/bugged2.tesh
@@ -2,7 +2,7 @@
 
 ! expect return 1
 ! timeout 20
-$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged2 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack-size:256
+$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged2 ${platfdir:=.}/model_checker_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack-size:256
 > [  0.000000] (0:maestro@) Check a safety property. Reduction is: dpor.
 > [  0.000000] (2:client@HostB) Send 1
 > [  0.000000] (3:client@HostC) Send 2

diff --git a/examples/deprecated/msg/mc/bugged3.c b/examples/deprecated/msg/mc/bugged3.c
index 57cd689..3e326e3 100644 (file)
--- a/examples/deprecated/msg/mc/bugged3.c
+++ b/examples/deprecated/msg/mc/bugged3.c
@@ -56,7 +56,7 @@ int main(int argc, char *argv[])
 {
   MSG_init(&argc, argv);
 
-  MSG_create_environment("platform.xml");
+  MSG_create_environment(argv[1]);
 
   MSG_function_register("server", server);
   MSG_function_register("client", client);

diff --git a/examples/deprecated/msg/mc/centralized_mutex.c b/examples/deprecated/msg/mc/centralized_mutex.c
index 38f9d3b..34cc490 100644 (file)
--- a/examples/deprecated/msg/mc/centralized_mutex.c
+++ b/examples/deprecated/msg/mc/centralized_mutex.c
@@ -81,7 +81,7 @@ static int client(XBT_ATTRIB_UNUSED int argc, XBT_ATTRIB_UNUSED char* argv[])
 int main(int argc, char *argv[])
 {
   MSG_init(&argc, argv);
-  MSG_create_environment("../../platforms/small_platform.xml");
+  MSG_create_environment(argv[1]);
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_centralized_mutex.xml");

diff --git a/examples/deprecated/msg/mc/centralized_mutex.tesh b/examples/deprecated/msg/mc/centralized_mutex.tesh
index 52986c4..c4cf2a3 100644 (file)
--- a/examples/deprecated/msg/mc/centralized_mutex.tesh
+++ b/examples/deprecated/msg/mc/centralized_mutex.tesh
@@ -1,3 +1,3 @@
 #!/usr/bin/env tesh
 
-$ ${bindir:=.}/centralized_mutex
+$ ${bindir:=.}/centralized_mutex ${platfdir:=.}/model_checker_platform.xml

diff --git a/examples/deprecated/msg/mc/platform.xml b/examples/platforms/model_checker_platform.xml
similarity index 100%
rename from examples/deprecated/msg/mc/platform.xml
rename to examples/platforms/model_checker_platform.xml

diff --git a/examples/s4u/CMakeLists.txt b/examples/s4u/CMakeLists.txt
index ee5fd7b..6111467 100644 (file)
--- a/examples/s4u/CMakeLists.txt
+++ b/examples/s4u/CMakeLists.txt
@@ -73,10 +73,10 @@ foreach (example actor-create actor-daemon actor-exiting actor-join actor-kill
 #    message("Factories of ${example}: ${_${example}_factories}")
 
     ADD_TESH_FACTORIES(s4u-${example} "${_${example}_factories}"
-                                      --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example} 
-                                     --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms 
-                                     --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example} 
-                                     ${CMAKE_HOME_DIRECTORY}/examples/s4u/${example}/s4u-${example}.tesh)
+                                      --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example}
+                                      --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
+                                      --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example}
+                                      ${CMAKE_HOME_DIRECTORY}/examples/s4u/${example}/s4u-${example}.tesh)
   else()
     message(STATUS "Example ${example} disabled, thus not compiled.")
     unset(_${example}_disabled)
@@ -123,9 +123,9 @@ foreach(example app-bittorrent app-masterworkers
                 )
   ADD_TESH_FACTORIES(s4u-${example}-parallel "${parallel-factories}" --cfg contexts/nthreads:4 ${CONTEXTS_SYNCHRO}
                                              --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example} 
-                                            --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms 
-                                            --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example} 
-                                            ${CMAKE_HOME_DIRECTORY}/examples/s4u/${example}/s4u-${example}.tesh)
+                                             --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms 
+                                             --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example} 
+                                             ${CMAKE_HOME_DIRECTORY}/examples/s4u/${example}/s4u-${example}.tesh)
 endforeach()
 
 # ns3-tests
@@ -179,7 +179,6 @@ set(xml_files     ${xml_files}    ${CMAKE_CURRENT_SOURCE_DIR}/actor-create/s4u-a
                                   ${CMAKE_CURRENT_SOURCE_DIR}/dht-kademlia/s4u-dht-kademlia_d.xml
                                   ${CMAKE_CURRENT_SOURCE_DIR}/energy-boot/platform_boot.xml
                                   ${CMAKE_CURRENT_SOURCE_DIR}/io-file-remote/s4u-io-file-remote_d.xml
-                                  ${CMAKE_CURRENT_SOURCE_DIR}/mc-electric-fence/platform.xml
                                   ${CMAKE_CURRENT_SOURCE_DIR}/platform-properties/s4u-platform-properties_d.xml
                                   ${CMAKE_CURRENT_SOURCE_DIR}/platform-failures/s4u-platform-failures_d.xml
                                   ${CMAKE_CURRENT_SOURCE_DIR}/replay-comm/s4u-replay-comm-split_d.xml

diff --git a/examples/s4u/mc-electric-fence/platform.xml b/examples/s4u/mc-electric-fence/platform.xml
deleted file mode 100644 (file)
index fd7894d..0000000
--- a/examples/s4u/mc-electric-fence/platform.xml
+++ /dev/null
@@ -1,17 +0,0 @@
-<?xml version='1.0'?>
-<!DOCTYPE platform SYSTEM "https://simgrid.org/simgrid.dtd">
-<platform version="4.1">
-  <zone  id="AS0"  routing="Full">
-    <host id="HostA" speed="137.333Mf"/>
-    <host id="HostB" speed="98.095Mf"/>
-    <host id="HostC" speed="98.095Mf"/>
-    <link id="1" bandwidth="3.430125MBps" latency="536.941us"/>
-    <link id="2" 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>
-  </zone>
-</platform>

diff --git a/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp b/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp
index 0dbced1..66c250d 100644 (file)
--- a/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp
+++ b/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp
@@ -42,7 +42,7 @@ int main(int argc, char* argv[])
 {
   simgrid::s4u::Engine e(&argc, argv);
 
-  e.load_platform("platform.xml");
+  e.load_platform(argv[1]);
 
   simgrid::s4u::Actor::create("server", simgrid::s4u::Host::by_name("HostA"), server);
   simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("HostB"), client, 1);

diff --git a/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.tesh b/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.tesh
index 35b9790..f86c4a9 100644 (file)
--- a/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.tesh
+++ b/examples/s4u/mc-electric-fence/s4u-mc-electric-fence.tesh
@@ -1,6 +1,6 @@
 #!/usr/bin/env tesh
 
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-electric-fence platform.xml
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-electric-fence ${platfdir}/model_checker_platform.xml
 > [0.000000] [mc_safety/INFO] Check a safety property. Reduction is: dpor.
 > [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
 > [HostA:server:(1) 0.000000] [electric_fence/INFO] OK

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index d957410..97f04c6 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -1139,6 +1139,7 @@ set(PLATFORMS_EXAMPLES
   examples/platforms/optorsim/transform_optorsim_platform.pl
   examples/platforms/config.xml
   examples/platforms/config_tracing.xml
+  examples/platforms/model_checker_platform.xml
   examples/platforms/profiles/bourassa_state.profile
   examples/platforms/profiles/fafard_state.profile
   examples/platforms/profiles/faulty_host.profile