Added models for TAC journal

models/tac24/case-studies/dpm-b/easy.props

@@ -0,0 +1,2 @@
+R{"lostH"} <= 1 [ F "finished" ]
+R{"power"} <= 140 [ F "finished" ]

models/tac24/case-studies/dpm-b/lost.props

@@ -0,0 +1,2 @@
+//R{"lostH"}min = ? [ F "finished" ]
+R{"lostL"}min = ? [ F "finished" ]

models/tac24/case-studies/dpm-b/power.props

@@ -0,0 +1 @@
+R{"power"}min = ? [ F "finished" ]

models/tac24/case-studies/dpm-b/sketch.props

@@ -0,0 +1,2 @@
+R{"lost"} <= 1 [ F "finished" ]
+R{"power"}min = ? [ F "finished" ]

models/tac24/case-studies/dpm-b/sketch.templ

@@ -0,0 +1,266 @@
+dtmc
+
+// To make it more challenging, we can extend the model and consider low and  high priority requests
+// using two request queues.
+
+const int CMAX = 10;
+
+hole int X11 in {0,1,2};
+hole int X21 in {0,1,2};
+hole int X31 in {0,1,2};
+hole int X41 in {0,1,2};
+hole int X12 in {0,1,2};
+hole int X22 in {0,1,2};
+hole int X32 in {0,1,2};
+hole int X42 in {0,1,2};
+hole int X13 in {0,1,2};
+hole int X23 in {0,1,2};
+hole int X33 in {0,1,2};
+hole int X43 in {0,1,2};
+hole int X14 in {0,1,2};
+hole int X24 in {0,1,2};
+hole int X34 in {0,1,2};
+hole int X44 in {0,1,2};
+
+
+const int LT1 = 3;
+const int LT2 = 5;
+const int LT3 = 7;
+const int HT1 = 3;
+const int HT2 = 5;
+const int HT3 = 7;
+
+// This system can achieve
+
+//R{"power"}<= 18000 [ F (bat=0) ]
+
+//R{"lostH"}<= 0.3 [ F (bat=0) ]
+
+//R{"lostL"}<= 0.6 [ F (bat=0) ]
+
+
+module CLOCK
+
+	c : [0..1];
+
+	[tick1] bat>0 & c=0 -> (c'=1);
+	[tick2] bat>0 & c=1 -> (c'=0);
+
+endmodule
+
+// POWER MANAGER
+
+module PM
+
+	pm  :  [0..3] init 3;
+	// 0 - go to active
+	// 1 - go to active for LOW
+	// 2 - go to idle
+	// 3 - go to sleep
+
+
+	[tick1] qL*10 <= LT1*CMAX & q*10 <= HT1*CMAX   -> (pm'=X11);
+
+	[tick1] qL*10 > LT1*CMAX & qL*10 <= LT2*CMAX &  q*10 <= HT1*CMAX -> (pm'=X21);
+
+	[tick1] qL*10 > LT2*CMAX & qL*10 <= LT3*CMAX &  q*10 <= HT1*CMAX -> (pm'=X31);
+
+    [tick1] qL*10 > LT3*CMAX &  q*10 <= HT1*CMAX -> (pm'=X41);
+
+    [tick1] qL*10 <= LT1*CMAX & q*10 > HT1*CMAX & q*10 <= HT2*CMAX -> (pm'=X12);
+
+    [tick1] qL*10 > LT1*CMAX & qL*10 <= LT2*CMAX &  q*10 > HT1*CMAX & q*10 <= HT2*CMAX -> (pm'=X22);
+
+	[tick1] qL*10 > LT2*CMAX & qL*10 <= LT3*CMAX &  q*10 > HT1*CMAX & q*10 <= HT2*CMAX -> (pm'=X32);
+
+    [tick1] qL*10 > LT3*CMAX &  q*10 > HT1*CMAX & q*10 <= HT2*CMAX -> (pm'=X42);
+
+    [tick1] qL*10 <= LT1*CMAX & q*10 > HT2*CMAX & q*10 <= HT3*CMAX -> (pm'=X13);
+
+	[tick1] qL*10 > LT1*CMAX & qL*10 <= LT2*CMAX &  q*10 > HT2*CMAX & q*10 <= HT3*CMAX -> (pm'=X23);
+
+	[tick1] qL*10 > LT2*CMAX & qL*10 <= LT3*CMAX &  q*10 > HT2*CMAX & q*10 <= HT3*CMAX -> (pm'=X33);
+
+    [tick1] qL*10 > LT3*CMAX &  q*10 > HT2*CMAX & q*10 <= HT3*CMAX -> (pm'=X43);
+
+    [tick1] qL*10 <= LT1*CMAX & q*10 > HT3*CMAX   -> (pm'=X14);
+
+	[tick1] qL*10 > LT1*CMAX & qL*10 <= LT2*CMAX &  q*10 > HT3*CMAX -> (pm'=X24);
+
+	[tick1] qL*10 > LT2*CMAX & qL*10 <= LT3*CMAX &  q*10 > HT3*CMAX -> (pm'=X34);
+
+    [tick1] qL*10 > LT3*CMAX &  q*10 > HT3*CMAX -> (pm'=X44);
+
+endmodule
+
+// SERVICE PROVIDER
+
+module SP
+
+	sp : [0..8] init 3;
+	// 0 active
+	// 1 active for LOW
+	// 2 idle
+	// 3 sleep
+
+	// 4 active_both_to_sleep
+	// 5 idle_to_sleep
+
+	// 6 sleep_to_idle
+	// 7 sleep_to_active
+	// 8 sleep_to_active_L
+
+	// states where PM has no control (transient states)
+
+	[tick2] sp=4  -> 0.9  : (sp'=4) + 0.1  : (sp'=3);
+	[tick2] sp=5  -> 0.9   : (sp'=5) + 0.1   : (sp'=3);
+
+	[tick2] sp=6  -> 0.9   : (sp'=6) + 0.1   : (sp'=2);
+
+	[tick2] sp=7  -> 0.9  : (sp'=7) + 0.1  : (sp'=0);
+	[tick2] sp=8  -> 0.9  : (sp'=8) + 0.1  : (sp'=1);
+
+
+	// states where PM has control
+	// goto_active
+	[tick2] sp=0 & pm=0 -> (sp'=0); // from active
+	[tick2] sp=1 & pm=0 -> (sp'=0); // from activeL
+	[tick2] sp=2 & pm=0 -> (sp'=0); // from idle
+	[tick2] sp=3 & pm=0 -> (sp'=7); // from sleep
+
+
+	// goto_active_L
+	[tick2] sp=0 & pm=1 -> (sp'=1); // from active
+	[tick2] sp=1 & pm=1 -> (sp'=1); // from activeL
+	[tick2] sp=2 & pm=1 -> (sp'=1); // from idle
+	[tick2] sp=3 & pm=1 -> (sp'=8); // from sleep
+
+	// goto_idle
+	[tick2] sp=0 & pm=2 -> (sp'=2); // from active
+	[tick2] sp=1 & pm=2 -> (sp'=2); // from active_L
+	[tick2] sp=2 & pm=2 -> (sp'=2); // from idle
+	[tick2] sp=3 & pm=2 -> (sp'=6); // from sleep
+
+	// goto_sleep
+	[tick2] sp=0 & pm=3 -> (sp'=4); // from active
+	[tick2] sp=1 & pm=3 -> (sp'=4); // from active_L
+	[tick2] sp=2 & pm=3 -> (sp'=5); // idle
+	[tick2] sp=3 & pm=3 -> (sp'=3); // sleep
+
+endmodule
+
+
+// SERVICE REQUESTER
+module SR
+
+	//a two-queue varinat
+
+	sr : [0..2] init 0; // 0 - idle, 1 - Hreq, 2-Lreq
+
+	[tick2] sr=0 -> 0.898: (sr'=0) + 0.051: (sr'=1) + 0.051: (sr'=2);
+	[tick2] sr=1 -> 0.254: (sr'=0) + 0.373: (sr'=1) + 0.373: (sr'=2);
+	[tick2] sr=2 -> 0.254: (sr'=0) + 0.373: (sr'=1) + 0.373: (sr'=2);
+
+endmodule
+
+
+// SERVICE REQUEST QUEUES
+module SRQ
+
+	q : [0..CMAX] init 0;
+	qL : [0..CMAX] init 0;
+
+	[tick2] sr=0 & sp!=0 & sp!=1 -> true; // do not serve and nothing arrives
+
+	[tick2] sr=1 & sp!=0 & sp!=1 -> (q'=min(q+1,CMAX)); // do not serve and a request arrives
+	[tick2] sr=2 & sp!=0 & sp!=1 -> (qL'=min(qL+1,CMAX)); // do not serve and a request arrives
+
+	[tick2] sr=0 & sp=0 -> (q'=max(q-1,0)); // serve and nothing arrives
+	[tick2] sr=0 & sp=1 -> (qL'=max(qL-1,0)); // serve and nothing arrives
+
+	// serve and a request arrives arrives -- it actually performs two actions
+	[tick2] sr=2 & sp=0 -> (q'=max(q-1,0)) & (qL'=min(qL+1,CMAX));
+	[tick2] sr=1 & sp=1 -> (qL'=max(qL-1,0)) & (q'=min(q+1,CMAX));
+
+	[tick2] sr=1 & sp=0 -> true;
+	[tick2] sr=2 & sp=1 -> true;
+
+endmodule
+
+
+
+
+
+// BATTERY
+module BAT
+
+	bat : [0..1] init 1; // 0 empty, 1 - operational
+
+	[] bat=0 -> (bat'=0); // loop when battery empty
+
+	[tick2] bat=1 -> 0.001 : (bat'=0) + 0.999 : (bat'=1);
+
+endmodule
+
+// queue size
+rewards "queueH"
+
+	c=1 : q;
+
+endrewards
+
+rewards "queueL"
+
+	c=1 : qL;
+
+endrewards
+
+// customers lost
+rewards "lostH"
+
+	[tick2] q=CMAX & sr=1 & sp!=0 : 1;
+
+endrewards
+
+rewards "lostL"
+
+	[tick2] qL=CMAX & sr=2 & sp!=1 : 1;
+
+endrewards
+
+rewards "lost"
+
+	[tick2] q=CMAX & sr=1 & sp!=0 : 1;
+	[tick2] qL=CMAX & sr=2 & sp!=1 : 1;
+
+endrewards
+
+
+// power consumption
+rewards "power"
+
+// in contrasr to the PRISM model we assume that the transient states have the power consuption
+// equal to the source state
+
+	sp=1 & c=1 : 2.5;
+	sp=0 & c=1 : 2.5;
+	sp=4 & c=1 : 2.5;
+
+	sp=2 & c=1 : 1.5;
+	sp=5 & c=1 : 1.5;
+
+	sp=3 & c=1 : 0.1;
+	sp=6 & c=1 : 0.1;
+	sp=7 & c=1 : 0.1;
+	sp=8 & c=1 : 0.1;
+
+endrewards
+
+// time
+rewards "time"
+
+    [tick2] true : 1;
+
+endrewards
+
+label "finished" = bat = 0;

models/tac24/case-studies/grid-meet-all-obs-1fsc/sketch.props

@@ -0,0 +1,6 @@
+R{"moves"}min=? [F "goal"]
+
+//R{"steps"}min=? [F "goal"]
+
+
+//Pmax=? [F "goal"]