diff --git a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14.nm b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14.nm index 98e49695d..bc433a7f1 100644 --- a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14.nm +++ b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14.nm @@ -26,6 +26,8 @@ const int TIME_MAX_Z = 1; // max value of clock z // OTHER CONSTANTS const int MAXCOLL = 10; // maximum number of collisions before long wait +const int M=1; // time between sending and receiving a message +const int T=14; //------------------------------------------------------------- @@ -117,7 +119,6 @@ endmodule //------------------------------------------------------------- // error automaton for the environment assumption // do not get a reply when K probes are sent -const int M=1; // time between sending and receiving a message module env_error2 @@ -150,7 +151,6 @@ endmodule //------------------------------------------------------------- // error automaton for the time bounded assumption // host does not send configured signal within T seconds -const int T=14; module time_error diff --git a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10.nm b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10.nm index daa91773c..a8485f2c9 100644 --- a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10.nm +++ b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10.nm @@ -26,7 +26,8 @@ const int TIME_MAX_Z = 1; // max value of clock z // OTHER CONSTANTS const int MAXCOLL = 10; // maximum number of collisions before long wait - +const int M=1; // time between sending and receiving a message +const int T=10; //------------------------------------------------------------- // CONCRETE HOST @@ -117,7 +118,7 @@ endmodule //------------------------------------------------------------- // error automaton for the environment assumption // do not get a reply when K probes are sent -const int M=1; // time between sending and receiving a message + module env_error4 @@ -155,7 +156,6 @@ endmodule //------------------------------------------------------------- // error automaton for the time bounded assumption // host does not send configured signal within T seconds -const int T=10; module time_error diff --git a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14.nm b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14.nm index 83b540290..4e56d344f 100644 --- a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14.nm +++ b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14.nm @@ -26,7 +26,8 @@ const int TIME_MAX_Z = 1; // max value of clock z // OTHER CONSTANTS const int MAXCOLL = 10; // maximum number of collisions before long wait - +const int M=1; // time between sending and receiving a message +const int T=14; //------------------------------------------------------------- // CONCRETE HOST @@ -117,7 +118,6 @@ endmodule //------------------------------------------------------------- // error automaton for the environment assumption // do not get a reply when K probes are sent -const int M=1; // time between sending and receiving a message module env_error4 @@ -155,7 +155,6 @@ endmodule //------------------------------------------------------------- // error automaton for the time bounded assumption // host does not send configured signal within T seconds -const int T=14; module time_error diff --git a/examples/multi-objective/mdp/zeroconf/zeroconf4.nm b/examples/multi-objective/mdp/zeroconf/zeroconf4.nm index 18f9109e7..3d5988df2 100644 --- a/examples/multi-objective/mdp/zeroconf/zeroconf4.nm +++ b/examples/multi-objective/mdp/zeroconf/zeroconf4.nm @@ -26,6 +26,7 @@ const int TIME_MAX_Z = 1; // max value of clock z // OTHER CONSTANTS const int MAXCOLL = 10; // maximum number of collisions before long wait +const int M=1; // time between sending and receiving a message //------------------------------------------------------------- @@ -117,7 +118,6 @@ endmodule //------------------------------------------------------------- // error automaton for the environment assumption // do not get a reply when K probes are sent -const int M=1; // time between sending and receiving a message module env_error4 diff --git a/examples/multi-objective/mdp/zeroconf/zeroconf6.nm b/examples/multi-objective/mdp/zeroconf/zeroconf6.nm index 571e154de..99ce361a5 100644 --- a/examples/multi-objective/mdp/zeroconf/zeroconf6.nm +++ b/examples/multi-objective/mdp/zeroconf/zeroconf6.nm @@ -26,6 +26,7 @@ const int TIME_MAX_Z = 1; // max value of clock z // OTHER CONSTANTS const int MAXCOLL = 10; // maximum number of collisions before long wait +const int M=1; // time between sending and receiving a message //------------------------------------------------------------- @@ -117,7 +118,6 @@ endmodule //------------------------------------------------------------- // error automaton for the environment assumption // do not get a reply when K probes are sent -const int M=1; // time between sending and receiving a message module env_error6 diff --git a/examples/multi-objective/mdp/zeroconf/zeroconf8.nm b/examples/multi-objective/mdp/zeroconf/zeroconf8.nm index c43363f84..871e06e2b 100644 --- a/examples/multi-objective/mdp/zeroconf/zeroconf8.nm +++ b/examples/multi-objective/mdp/zeroconf/zeroconf8.nm @@ -26,6 +26,7 @@ const int TIME_MAX_Z = 1; // max value of clock z // OTHER CONSTANTS const int MAXCOLL = 10; // maximum number of collisions before long wait +const int M=1; // time between sending and receiving a message //------------------------------------------------------------- @@ -117,7 +118,6 @@ endmodule //------------------------------------------------------------- // error automaton for the environment assumption // do not get a reply when K probes are sent -const int M=1; // time between sending and receiving a message module env_error8