sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

added testfiles for multiobjective mc tests

tempestpy_adaptions
TimQu 8 years ago
parent
9c183d42b3
commit
ae3ef2f14a
9 changed files with 823 additions and 45 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 34
      resources/examples/testfiles/ma/server.ma
  2. 88
      resources/examples/testfiles/mdp/multiobj_consensus2_3_2.nm
  3. 160
      resources/examples/testfiles/mdp/multiobj_dpm100.nm
  4. 95
      resources/examples/testfiles/mdp/multiobj_scheduler05.nm
  5. 288
      resources/examples/testfiles/mdp/multiobj_team3.nm
  6. 153
      resources/examples/testfiles/mdp/multiobj_zeroconf4.nm
  7. 20
      resources/examples/testfiles/mdp/multiobjective1.nm
  8. 20
      resources/examples/testfiles/mdp/multiobjective2.nm
  9. 10
      src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp

34
resources/examples/testfiles/ma/server.ma
View File

@ -0,0 +1,34 @@
ma
const double rateProcessing = 2;
const double rateA = 1;
const double rateB = 1;
module server
s : [0..5]; // current state:
// 0: wait for request
// 1: received request from A
// 2: received request from B
// 3: starting to process request of B
// 4: processing request
// 5: error
<> s=0 -> rateA : (s'=1) + rateB : (s'=2);
[alpha] s=1 -> 1 : (s'=4);
[alpha] s=2 -> 1 : (s'=3);
[beta] s=2 -> 0.5 : (s'=0) + 0.5 : (s'=3);
[] s=3 -> 1 : (s'=4);
<> s=4 -> rateProcessing : (s'=0) + (rateA+rateB) : (s'=5);
<> s=5 -> 1 : true;
endmodule
label "error" = (s=5);
label "processB" = (s=3);

88
resources/examples/testfiles/mdp/multiobj_consensus2_3_2.nm
View File

@ -0,0 +1,88 @@
// model of randomised consensus
mdp
const int N = 2; // num processes
const int MAX = 3; // num rounds (R)
const int K = 2; // Parameter for coins
// need to turn these into local copies later so the reading phase is complete?
formula leaders_agree1 = (p1=1 | r1<max(r1,r2)) & (p2=1 | r2<max(r1,r2));
formula leaders_agree2 = (p1=2 | r1<max(r1,r2)) & (p2=2 | r2<max(r1,r2));
formula decide1 = leaders_agree1 & (p1=1 | r1<max(r1,r2)-1) & (p2=1 | r2<max(r1,r2)-1);
formula decide2 = leaders_agree2 & (p1=2 | r1<max(r1,r2)-1) & (p2=2 | r2<max(r1,r2)-1);
module process1
s1 : [0..5]; // local state
// 0 initialise/read registers
// 1 finish reading registers (make a decision)
// 1 warn of change
// 2 enter shared coin protocol
// 4 finished
// 5 error (reached max round and cannot decide)
r1 : [0..MAX]; // round of the process
p1 : [0..2]; // preference (0 corresponds to null)
// nondeterministic choice as to initial preference
[] s1=0 & r1=0 -> (p1'=1) & (r1'=1);
[] s1=0 & r1=0 -> (p1'=2) & (r1'=1);
// read registers (currently does nothing because read vs from other processes
[] s1=0 & r1>0 & r1<=MAX -> (s1'=1);
// maxke a decision
[] s1=1 & decide1 -> (s1'=4) & (p1'=1);
[] s1=1 & decide2 -> (s1'=4) & (p1'=2);
[] s1=1 & r1<MAX & leaders_agree1 & !decide1 -> (s1'=0) & (p1'=1) & (r1'=r1+1);
[] s1=1 & r1<MAX & leaders_agree2 & !decide2 -> (s1'=0) & (p1'=2) & (r1'=r1+1);
[] s1=1 & r1<MAX & !(leaders_agree1 | leaders_agree2) -> (s1'=2) & (p1'=0);
[] s1=1 & r1=MAX & !(decide1 | decide2) -> (s1'=5); // run out of rounds so error
// enter the coin procotol for the current round
[coin1_s1_start] s1=2 & r1=1 -> (s1'=3);
[coin2_s1_start] s1=2 & r1=2 -> (s1'=3);
// get response from the coin protocol
[coin1_s1_p1] s1=3 & r1=1 -> (s1'=0) & (p1'=1) & (r1'=r1+1);
[coin1_s1_p2] s1=3 & r1=1 -> (s1'=0) & (p1'=2) & (r1'=r1+1);
[coin2_s1_p1] s1=3 & r1=2 -> (s1'=0) & (p1'=1) & (r1'=r1+1);
[coin2_s1_p2] s1=3 & r1=2 -> (s1'=0) & (p1'=2) & (r1'=r1+1);
// done so loop
[done] s1>=4 -> true;
endmodule
module process2 = process1[ s1=s2,
p1=p2,p2=p1,
r1=r2,r2=r1,
coin1_s1_start=coin1_s2_start,coin2_s1_start=coin2_s2_start,
coin1_s1_p1=coin1_s2_p1,coin2_s1_p1=coin2_s2_p1,
coin1_s1_p2=coin1_s2_p2,coin2_s1_p2=coin2_s2_p2 ]
endmodule
module coin1_error
c1 : [0..1]; // 1 is the error state
v1 : [0..2]; // value of the coin returned the first time
// first returned value (any processes)
[coin1_s1_p1] v1=0 -> (v1'=1);
[coin1_s2_p1] v1=0 -> (v1'=1);
[coin1_s1_p2] v1=0 -> (v1'=2);
[coin1_s2_p2] v1=0 -> (v1'=2);
// later values returned
[coin1_s1_p1] v1=1 -> true; // good behaviour
[coin1_s2_p1] v1=1 -> true; // good behaviour
[coin1_s1_p2] v1=2 -> true; // good behaviour
[coin1_s2_p2] v1=2 -> true; // good behaviour
[coin1_s1_p1] v1=2 -> (c1'=1); // error
[coin1_s2_p1] v1=2 -> (c1'=1); // error
[coin1_s1_p2] v1=1 -> (c1'=1); // error
[coin1_s2_p2] v1=1 -> (c1'=1); // error
endmodule
// coins 2 and 3 are of no use as there are not enough rounds afterwards to decide
// Labels
label "one_proc_err" = (s1=5 | s2=5);
label "one_coin_ok" = (c1=0);

160
resources/examples/testfiles/mdp/multiobj_dpm100.nm
View File

@ -0,0 +1,160 @@
// power manager example
mdp
const int QMAX =2; // max queue size
// to model the pm making a choice and then a move being made we need
// two clock ticks for each transition
// first the pm decides tick1 and then the system moves tick2
module timer
c : [0..1];
[tick1] c=0 -> (c'=1);
[tick2] c=1 -> (c'=0);
endmodule
//-------------------------------------------------------------------------
// POWER MANAGER
module PM
pm : [0..4] init 4;
// 0 - go to active
// 1 - go to idle
// 2 - go to idlelp
// 3 - go to stby
// 4 - go to sleep
[tick1] true -> (pm'=0);
[tick1] true -> (pm'=1);
[tick1] true -> (pm'=2);
[tick1] true -> (pm'=3);
[tick1] true -> (pm'=4);
endmodule
//-------------------------------------------------------------------------
// SERVICE REQUESTER
module SR
sr : [0..1] init 0;
// 0 idle
// 1 1req
[tick2] sr=0 -> 0.898: (sr'=0) + 0.102: (sr'=1);
[tick2] sr=1 -> 0.454: (sr'=0) + 0.546: (sr'=1);
endmodule
//-------------------------------------------------------------------------
// SERVICE PROVIDER
module SP
sp : [0..10] init 9;
// 0 active
// 1 idle
// 2 active_idlelp
// 3 idlelp
// 4 idlelp_active
// 5 active_stby
// 6 stby
// 7 stby_active
// 8 active_sleep
// 9 sleep
// 10 sleep_active
// states where PM has no control (transient states)
[tick2] sp=2 -> 0.75 : (sp'=2) + 0.25 : (sp'=3); // active_idlelp
[tick2] sp=4 -> 0.25 : (sp'=0) + 0.75 : (sp'=4); // idlelp_active
[tick2] sp=5 -> 0.995 : (sp'=5) + 0.005 : (sp'=6); // active_stby
[tick2] sp=7 -> 0.005 : (sp'=0) + 0.995 : (sp'=7); // stby_active
[tick2] sp=8 -> 0.9983 : (sp'=8) + 0.0017 : (sp'=9); // active_sleep
[tick2] sp=10 -> 0.0017 : (sp'=0) + 0.9983 : (sp'=10); // sleep_active
// states where PM has control
// goto_active
[tick2] sp=0 & pm=0 -> (sp'=0); // active
[tick2] sp=1 & pm=0 -> (sp'=0); // idle
[tick2] sp=3 & pm=0 -> (sp'=4); // idlelp
[tick2] sp=6 & pm=0 -> (sp'=7); // stby
[tick2] sp=9 & pm=0 -> (sp'=10); // sleep
// goto_idle
[tick2] sp=0 & pm=1 -> (sp'=1); // active
[tick2] sp=1 & pm=1 -> (sp'=1); // idle
[tick2] sp=3 & pm=1 -> (sp'=3); // idlelp
[tick2] sp=6 & pm=1 -> (sp'=6); // stby
[tick2] sp=9 & pm=1 -> (sp'=9); // sleep
// goto_idlelp
[tick2] sp=0 & pm=2 -> (sp'=2); // active
[tick2] sp=1 & pm=2 -> (sp'=2); // idle
[tick2] sp=3 & pm=2 -> (sp'=3); // idlelp
[tick2] sp=6 & pm=2 -> (sp'=6); // stby
[tick2] sp=9 & pm=2 -> (sp'=9); // sleep
// goto_stby
[tick2] sp=0 & pm=3 -> (sp'=5); // active
[tick2] sp=1 & pm=3 -> (sp'=5); // idle
[tick2] sp=3 & pm=3 -> (sp'=5); // idlelp
[tick2] sp=6 & pm=3 -> (sp'=6); // stby
[tick2] sp=9 & pm=3 -> (sp'=9); // sleep
// goto_sleep
[tick2] sp=0 & pm=4 -> (sp'=8); // active
[tick2] sp=1 & pm=4 -> (sp'=8); // idle
[tick2] sp=3 & pm=4 -> (sp'=8); // idlelp
[tick2] sp=6 & pm=4 -> (sp'=8); // stby
[tick2] sp=9 & pm=4 -> (sp'=9); // sleep
endmodule
//-------------------------------------------------------------------------
// SQ
module SQ
q : [0..QMAX] init 0;
// serve if busy
[tick2] sr=0 & sp=0 -> (q'=max(q-1,0));
[tick2] sr=1 & sp=0 -> (q'=q);
// otherwise do nothing
[tick2] sr=0 & sp>0 -> (q'=q);
[tick2] sr=1 & sp>0 -> (q'=min(q+1,QMAX));
endmodule
//-------------------------------------------------------------------------
//rewards "time"
// [tick2] bat=1 : 1;
//endrewards
rewards "power"
[tick2] sp=0 & c=1 : 2.5;
[tick2] sp=1 & c=1 : 1.5;
[tick2] sp=2 & c=1 : 2.5;
[tick2] sp=3 & c=1 : 0.8;
[tick2] sp=4 & c=1 : 2.5;
[tick2] sp=5 & c=1 : 2.5;
[tick2] sp=6 & c=1 : 0.3;
[tick2] sp=7 & c=1 : 2.5;
[tick2] sp=8 & c=1 : 2.5;
[tick2] sp=9 & c=1 : 0.1;
[tick2] sp=10 & c=1 : 2.5;
endrewards
// is an instantaneous property but I suppose we can look at average size
// i.e. divide by the expected number of time steps
rewards "queue"
[tick2] c=1 : q;
endrewards
rewards "lost"
[tick2] sr=1 & sp>0 & q=2 : 1;
endrewards

95
resources/examples/testfiles/mdp/multiobj_scheduler05.nm
View File

@ -0,0 +1,95 @@
mdp
label "tasks_complete" = (task6=3);
const int K=5;
module scheduler
task1 : [0..3];
task2 : [0..3];
task3 : [0..3];
task4 : [0..3];
task5 : [0..3];
task6 : [0..3];
[p1_add] task1=0 -> (task1'=1);
[p2_add] task1=0 -> (task1'=2);
[p1_mult] task2=0 -> (task2'=1);
[p2_mult] task2=0 -> (task2'=2);
[p1_mult] task3=0&task1=3 -> (task3'=1);
[p2_mult] task3=0&task1=3 -> (task3'=2);
[p1_add] task4=0&task1=3&task2=3 -> (task4'=1);
[p2_add] task4=0&task1=3&task2=3 -> (task4'=2);
[p1_mult] task5=0&task3=3 -> (task5'=1);
[p2_mult] task5=0&task3=3 -> (task5'=2);
[p1_add] task6=0&task4=3&task5=3 -> (task6'=1);
[p2_add] task6=0&task4=3&task5=3 -> (task6'=2);
[p1_done] task1=1 -> (task1'=3);
[p1_done] task2=1 -> (task2'=3);
[p1_done] task3=1 -> (task3'=3);
[p1_done] task4=1 -> (task4'=3);
[p1_done] task5=1 -> (task5'=3);
[p1_done] task6=1 -> (task6'=3);
[p2_done] task1=2 -> (task1'=3);
[p2_done] task2=2 -> (task2'=3);
[p2_done] task3=2 -> (task3'=3);
[p2_done] task4=2 -> (task4'=3);
[p2_done] task5=2 -> (task5'=3);
[p2_done] task6=2 -> (task6'=3);
[time] true -> 1.0 : true;
endmodule
module P1
p1 : [0..3];
c1 : [0..2];
x1 : [0..4*K+1];
[p1_add] (p1=0) -> (p1'=1) & (x1'=0);
[] (p1=1)&(x1=1*K)&(c1=0) -> 1/3 : (p1'=3) & (x1'=0) & (c1'=0) + 2/3 : (c1'=1) & (x1'=0);
[] (p1=1)&(x1=1*K)&(c1=1) -> 1/2 : (p1'=3) & (x1'=0) & (c1'=0) + 1/2 : (c1'=2) & (x1'=0);
[p1_done] (p1=1)&(x1=1*K)&(c1=2) -> (p1'=0) & (x1'=0) & (c1'=0);
[p1_mult] (p1=0) -> (p1'=2) & (x1'=0);
[] (p1=2)&(x1=2*K)&(c1=0) -> 1/3 : (p1'=3) & (x1'=0) & (c1'=0) + 2/3 : (c1'=1) & (x1'=0);
[] (p1=2)&(x1=1*K)&(c1=1) -> 1/2 : (p1'=3) & (x1'=0) & (c1'=0) + 1/2 : (c1'=2) & (x1'=0);
[p1_done] (p1=2)&(x1=1*K)&(c1=2) -> (p1'=0) & (x1'=0) & (c1'=0);
[p1_done] (p1=3) -> (p1'=0);
[time] (p1=1=>x1+1<=1*K)&((p1=2&c1=0)=>x1+1<=2*K)&((p1=2&c1>0)=>x1+1<=1*K)&(p1=3=>x1+1<=0) -> 1.0 : (x1'=min(x1+1,4*K+1));
endmodule
module P2
p2 : [0..3];
c2 : [0..2];
x2 : [0..6*K+1];
[p2_add] (p2=0) -> (p2'=1) & (x2'=0);
[] (p2=1)&(x2=4*K)&(c2=0) -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0);
[] (p2=1)&(x2=1)&(c2=1) -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0);
[p2_done] (p2=1)&(x2=1)&(c2=2) -> (p2'=0) & (x2'=0) & (c2'=0);
[p2_mult] (p2=0) -> (p2'=2) & (x2'=0);
[] (p2=2)&(x2=6*K)&(c2=0) -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0);
[] (p2=2)&(x2=1)&(c2=1) -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0);
[p2_done] (p2=2)&(x2=1)&(c2=2) -> (p2'=0) & (x2'=0) & (c2'=0);
[p2_done] (p2=3) -> (p2'=0);
[time] ((p2=1&c2=0)=>x2+1<=4*K)&((p2=1&c2>0)=>x2+1<=1)&((p2=2&c2=0)=>x2+1<=6*K)&((p2=2&c2>0)=>x2+1<=1)&(p2=3=>x2+1<=0) -> 1.0 : (x2'=min(x2+1,6*K+1));
endmodule
rewards "time"
[time] true : 1/K;
endrewards
rewards "energy"
[time] p1=0 : 10/(1000*K);
[time] p1>0 : 90/(1000*K);
[time] p2=0 : 20/(1000*K);
[time] p2>0 : 30/(1000*K);
endrewards

288
resources/examples/testfiles/mdp/multiobj_team3.nm
View File

@ -0,0 +1,288 @@
mdp
// parameters
const int n_resources = 3;
const int n_tasks = 2;
const int n_sensors = 3;
// sensor resources
const int resource1=1;
const int resource2=2;
const int resource3=3;
// network configuration
const int e12=1;
const int e13=1;
const int e21=e12;
const int e23=1;
const int e31=e13;
const int e32=e23;
// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;
// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2;
// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 > 0;
// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3);
// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))) / (e12+e13);
module controller // schedules the algorithm
// algorithm status
status : [0..6];
// task resource indicator variables
t1_r1 : [0..1];
t1_r2 : [0..1];
t1_r3 : [0..1];
t2_r1 : [0..1];
t2_r2 : [0..1];
t2_r3 : [0..1];
// schedule placeholders
turn1 : [0..n_sensors];
turn2 : [0..n_sensors];
turn3 : [0..n_sensors];
// selecting schedule uniformly at random
[] status=0 -> 1/6 : (turn1'=1) & (turn2'=2) & (turn3'=3) & (status'=1)
+ 1/6 : (turn1'=1) & (turn2'=3) & (turn3'=2) & (status'=1)
+ 1/6 : (turn1'=2) & (turn2'=1) & (turn3'=3) & (status'=1)
+ 1/6 : (turn1'=2) & (turn2'=3) & (turn3'=1) & (status'=1)
+ 1/6 : (turn1'=3) & (turn2'=1) & (turn3'=2) & (status'=1)
+ 1/6 : (turn1'=3) & (turn2'=2) & (turn3'=1) & (status'=1);
// initialising non-empty tasks uniformly at random
[] status=1 -> 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+ 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2);
// executing the schedule
// 1st round
[str1] status=2 & turn1=1 -> (status'=2);
[fin1] status=2 & turn1=1 -> (status'=3);
[str2] status=2 & turn1=2 -> (status'=2);
[fin2] status=2 & turn1=2 -> (status'=3);
[str3] status=2 & turn1=3 -> (status'=2);
[fin3] status=2 & turn1=3 -> (status'=3);
// 2nd round
[str1] status=3 & turn2=1 -> (status'=3);
[fin1] status=3 & turn2=1 -> (status'=4);
[str2] status=3 & turn2=2 -> (status'=3);
[fin2] status=3 & turn2=2 -> (status'=4);
[str3] status=3 & turn2=3 -> (status'=3);
[fin3] status=3 & turn2=3 -> (status'=4);
// 3rd round
[str1] status=4 & turn3=1 -> (status'=4);
[fin1] status=4 & turn3=1 -> (status'=5);
[str2] status=4 & turn3=2 -> (status'=4);
[fin2] status=4 & turn3=2 -> (status'=5);
[str3] status=4 & turn3=3 -> (status'=4);
[fin3] status=4 & turn3=3 -> (status'=5);
[] status=5 -> (status'=6);
[] status=6 -> true;
endmodule
module sensor1
state1 : [0..1];
// team membership indicators
m1_t1 : [0..1];
m1_t2 : [0..1];
// starting turn, selecting order of tasks
[str1] state1=0 -> (state1'=1);
// if there is no team and has required skill - initiating the team
[] state1=1 & !committed & team_size_t1=0 & has_resource_t1 -> (m1_t1'=1);
[] state1=1 & !committed & team_size_t2=0 & has_resource_t2 -> (m1_t2'=1);
// if team already exists and one of the neighbours is in it - joining the team
[] state1=1 & !committed & team_size_t1>0 & can_join_t1 & has_resource_t1 & !resource_filled_t1 -> (m1_t1'=1);
[] state1=1 & !committed & team_size_t2>0 & can_join_t2 & has_resource_t2 & !resource_filled_t2 -> (m1_t2'=1);
[fin1] state1>0 -> (state1'=0);
endmodule
module sensor2 = sensor1
[
state1=state2,
str1=str2,
fin1=fin2,
m1_t1=m2_t1,
m1_t2=m2_t2,
m2_t1=m1_t1,
m2_t2=m1_t2,
resource1=resource2,
resource2=resource1,
e12=e21,
e13=e23,
e14=e24,
e15=e25,
e21=e12,
e23=e13,
e24=e14,
e25=e15
]
endmodule
module sensor3 = sensor1
[
state1=state3,
str1=str3,
fin1=fin3,
m1_t1=m3_t1,
m1_t2=m3_t2,
m3_t1=m1_t1,
m3_t2=m1_t2,
resource1=resource3,
resource3=resource1,
e12=e32,
e13=e31,
e14=e34,
e15=e35,
e31=e13,
e32=e12,
e34=e14,
e35=e15
]
endmodule
// labels and formulae for property specification
formula finished = (status=5);
label "end" = (status=6);
formula task1_completed = finished
& ((t1_r1=1)=>((m1_t1=1&resource1=1)|(m2_t1=1&resource2=1)|(m3_t1=1&resource3=1)))
& ((t1_r2=1)=>((m1_t1=1&resource1=2)|(m2_t1=1&resource2=2)|(m3_t1=1&resource3=2)))
& ((t1_r3=1)=>((m1_t1=1&resource1=3)|(m2_t1=1&resource2=3)|(m3_t1=1&resource3=3)));
formula task2_completed = finished
& ((t2_r1=1)=>((m1_t2=1&resource1=1)|(m2_t2=1&resource2=1)|(m3_t2=1&resource3=1)))
& ((t2_r2=1)=>((m1_t2=1&resource1=2)|(m2_t2=1&resource2=2)|(m3_t2=1&resource3=2)))
& ((t2_r3=1)=>((m1_t2=1&resource1=3)|(m2_t2=1&resource2=3)|(m3_t2=1&resource3=3)));
formula agent1_joins_successful_team = (task1_completed & m1_t1=1) | (task2_completed & m1_t2=1);
formula agent1_joins_successful_team_of_1 = (task1_completed & m1_t1=1 & team_size_t1=1) | (task2_completed & m1_t2=1 & team_size_t2=1);
formula agent1_joins_successful_team_of_2 = (task1_completed & m1_t1=1 & team_size_t1=2) | (task2_completed & m1_t2=1 & team_size_t2=2);
formula agent1_joins_successful_team_of_3 = (task1_completed & m1_t1=1 & team_size_t1=3) | (task2_completed & m1_t2=1 & team_size_t2=3);
formula agent2_joins_successful_team = (task1_completed & m2_t1=1) | (task2_completed & m2_t2=1);
formula agent2_joins_successful_team_of_1 = (task1_completed & m2_t1=1 & team_size_t1=1) | (task2_completed & m2_t2=1 & team_size_t2=1);
formula agent2_joins_successful_team_of_2 = (task1_completed & m2_t1=1 & team_size_t1=2) | (task2_completed & m2_t2=1 & team_size_t2=2);
formula agent2_joins_successful_team_of_3 = (task1_completed & m2_t1=1 & team_size_t1=3) | (task2_completed & m2_t2=1 & team_size_t2=3);
formula agent3_joins_successful_team = (task1_completed & m3_t1=1) | (task2_completed & m3_t2=1);
formula agent3_joins_successful_team_of_1 = (task1_completed & m3_t1=1 & team_size_t1=1) | (task2_completed & m3_t2=1 & team_size_t2=1);
formula agent3_joins_successful_team_of_2 = (task1_completed & m3_t1=1 & team_size_t1=2) | (task2_completed & m3_t2=1 & team_size_t2=2);
formula agent3_joins_successful_team_of_3 = (task1_completed & m3_t1=1 & team_size_t1=3) | (task2_completed & m3_t2=1 & team_size_t2=3);
// rewards
rewards "w_1_total"
[] agent1_joins_successful_team : 1;
[] agent2_joins_successful_team : 1;
[] agent3_joins_successful_team : 1;
endrewards
rewards "w_2_total"
[] task1_completed : 1;
[] task2_completed : 1;
endrewards

153
resources/examples/testfiles/mdp/multiobj_zeroconf4.nm
View File

@ -0,0 +1,153 @@
// IPv4: PTA model with digitial clocks
// multi-objective model of the host
// gxn/dxp 28/09/09
mdp
//-------------------------------------------------------------
// VARIABLES
const int N=20; // number of abstract hosts
const int K=4; // number of probes to send
// PROBABILITIES
const double old = N/65024; // probability pick an ip address being used
//const double old = 0.5; // probability pick an ip address being used
const double new = (1-old); // probability pick a new ip address
// TIMING CONSTANTS
const int CONSEC = 2; // time interval between sending consecutive probles
const int TRANSTIME = 1; // upper bound on transmission time delay
const int LONGWAIT = 60; // minimum time delay after a high number of address collisions
const int DEFEND = 10;
const int TIME_MAX_X = 60; // max value of clock x
const int TIME_MAX_Y = 10; // max value of clock y
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
//-------------------------------------------------------------
// CONCRETE HOST
module host0
x : [0..TIME_MAX_X]; // first clock of the host
y : [0..TIME_MAX_Y]; // second clock of the host
coll : [0..MAXCOLL]; // number of address collisions
probes : [0..K]; // counter (number of probes sent)
mess : [0..1]; // need to send a message or not
defend : [0..1]; // defend (if =1, try to defend IP address)
ip : [1..2]; // ip address (1 - in use & 2 - fresh)
l : [0..4] init 1; // location
// 0 : RECONFIGURE
// 1 : RANDOM
// 2 : WAITSP
// 3 : WAITSG
// 4 : USE
// RECONFIGURE
[reset] l=0 -> (l'=1);
// RANDOM (choose IP address)
[rec0] (l=1) -> true; // get message (ignore since have no ip address)
[rec1] (l=1) -> true; // get message (ignore since have no ip address)
// small number of collisions (choose straight away)
[] l=1 & coll<MAXCOLL -> 1/3*old : (l'=2) & (ip'=1) & (x'=0)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2);
// large number of collisions: (wait for LONGWAIT)
[time] l=1 & coll=MAXCOLL & x<LONGWAIT -> (x'=min(x+1,TIME_MAX_X));
[] l=1 & coll=MAXCOLL & x=LONGWAIT -> 1/3*old : (l'=2) & (ip'=1) & (x'=0)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2);
// WAITSP
// let time pass
[time] l=2 & x<2 -> (x'=min(x+1,2));
// send probe
[send1] l=2 & ip=1 & x=2 & probes<K -> (x'=0) & (probes'=probes+1);
[send2] l=2 & ip=2 & x=2 & probes<K -> (x'=0) & (probes'=probes+1);
// sent K probes and waited 2 seconds
[] l=2 & x=2 & probes=K -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0);
// get message and ip does not match: ignore
[rec0] l=2 & ip!=0 -> (l'=l);
[rec1] l=2 & ip!=1 -> (l'=l);
// get a message with matching ip: reconfigure
[rec1] l=2 & ip=1 -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
// WAITSG (sends two gratuitious arp probes)
// time passage
[time] l=3 & mess=0 & defend=0 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X));
[time] l=3 & mess=0 & defend=1 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X)) & (y'=min(y+1,DEFEND));
// receive message and same ip: defend
[rec1] l=3 & mess=0 & ip=1 & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
// receive message and same ip: defer
[rec1] l=3 & mess=0 & ip=1 & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
// receive message and different ip
[rec0] l=3 & mess=0 & ip!=0 -> (l'=l);
[rec1] l=3 & mess=0 & ip!=1 -> (l'=l);
// send probe reply or message for defence
[send1] l=3 & ip=1 & mess=1 -> (mess'=0);
[send2] l=3 & ip=2 & mess=1 -> (mess'=0);
// send first gratuitous arp message
[send1] l=3 & ip=1 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1);
[send2] l=3 & ip=2 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1);
// send second gratuitous arp message (move to use)
[send1] l=3 & ip=1 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
[send2] l=3 & ip=2 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
// USE (only interested in reaching this state so do not need to add anything here)
[] l=4 -> true;
endmodule
//-------------------------------------------------------------
// error automaton for the environment assumption
// do not get a reply when K probes are sent
module env_error4
env : [0..1]; // 0 active and 1 done
k : [0..4]; // counts the number of messages sent
c1 : [0..M+1]; // time since first message
c2 : [0..M+1]; // time since second message
c3 : [0..M+1]; // time since third message
c4 : [0..M+1]; // time since fourth message
error : [0..1];
// message with new ip address arrives so done
[send2] error=0 & env=0 -> (env'=1);
// message with old ip address arrives so count
[send1] error=0 & env=0 -> (k'=min(k+1,K));
// time passgae so update relevant clocks
[time] error=0 & env=0 & k=0 -> true;
[time] error=0 & env=0 & k=1 & min(c1,c2,c3,c4)<M -> (c1'=min(c1+1,M+1));
[time] error=0 & env=0 & k=2 & min(c1,c2,c3,c4)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1));
[time] error=0 & env=0 & k=3 & min(c1,c2,c3,c4)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1)) & (c3'=min(c3+1,M+1));
[time] error=0 & env=0 & k=4 & min(c1,c2,c3,c4)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1)) & (c3'=min(c3+1,M+1)) & (c4'=min(c4+1,M+1));
// all clocks reached their bound so an error
[time] error=0 & env=0 & min(c1,c2,c3,c4)=M -> (error'=1);
// send a reply (then done)
[rec1] error=0 & env=0 & k>0 & min(c1,c2,c3,c4)<=M -> (env'=1);
// finished so any action can be performed
[time] error=1 | env=1 -> true;
[send1] error=1 | env=1 -> true;
[send2] error=1 | env=1 -> true;
[send2] error=1 | env=1 -> true;
[rec1] error=1 | env=1 -> true;
endmodule

20
resources/examples/testfiles/mdp/multiobjective1.nm
View File

@ -1,20 +0,0 @@
mdp
module module1
// local state
s : [0..2] init 0;
[A] s=0 -> 0.6 : (s'=1) + 0.4 : (s'=2);
[B] s=0 -> 0.3 : (s'=0) + 0.7 : (s'=1);
[C] s=0 -> 0.2 : (s'=0) + 0.8 : (s'=2);
[D] s=1 -> 0.25 : (s'=0) + 0.75 : (s'=2);
[] s=2 -> 1 : (s'=s);
endmodule
rewards "rew"
[A] true : 10;
[D] true : 4;
endrewards

20
resources/examples/testfiles/mdp/multiobjective2.nm
View File

@ -1,20 +0,0 @@
mdp
module module1
s : [0..2] init 0;
[A] s=0 -> 1 : (s'=1);
[B] s=0 -> 1 : (s'=2);
[C] s=1 -> 1 : true;
[D] s=1 -> 1 : (s'=2);
[E] s=2 -> 1 : true;
endmodule
rewards "rew"
[A] true : 10;
[C] true : 3;
[E] true : 1;
endrewards

10
src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp
View File

@ -14,7 +14,7 @@
TEST(SparseMdpPcaaModelCheckerTest, consensus) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/consensus2_3_2.nm";
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_consensus2_3_2.nm";
std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical
formulasAsString += "; \n multi(P>=0.1 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (true)
formulasAsString += "; \n multi(P>=0.11 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (false)
@ -44,7 +44,7 @@ TEST(SparseMdpPcaaModelCheckerTest, consensus) {
TEST(SparseMdpPcaaModelCheckerTest, zeroconf) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/zeroconf4.nm";
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_zeroconf4.nm";
std::string formulasAsString = "multi(Pmax=? [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical
// programm, model, formula
@ -63,7 +63,7 @@ TEST(SparseMdpPcaaModelCheckerTest, zeroconf) {
TEST(SparseMdpPcaaModelCheckerTest, team3with3objectives) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/team3obj_3.nm";
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm";
std::string formulasAsString = "multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // numerical
// programm, model, formula
@ -82,7 +82,7 @@ TEST(SparseMdpPcaaModelCheckerTest, team3with3objectives) {
TEST(SparseMdpPcaaModelCheckerTest, scheduler) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/scheduler05.nm";
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_scheduler05.nm";
std::string formulasAsString = "multi(R{\"time\"}<= 11.778[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) ";
// programm, model, formula
@ -100,7 +100,7 @@ TEST(SparseMdpPcaaModelCheckerTest, scheduler) {
TEST(SparseMdpPcaaModelCheckerTest, dpm) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/dpm100.nm";
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_dpm100.nm";
std::string formulasAsString = "multi(R{\"power\"}min=? [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // numerical
// programm, model, formula

Write Preview
Loading…
Cancel
Save