POMDP regression tests.

prism/tests/pomdps/3x3grid.prism

@@ -0,0 +1,52 @@
+// 3x3 grid
+// based on Littman, Cassandra and Kaelbling
+// Learning policies for partially observable environments: Scaling up  
+// Technical Report CS, Brown University
+
+pomdp
+
+// only the target is observable which is in the south east corner
+observables
+	o
+endobservables
+
+module grid
+	
+	x : [0..2]; // x coordinate
+	y : [0..2]; // y coordinate
+	o : [0..2]; // observables
+	// 0 - initial observation
+	// 1 - in the grid (not target)
+	// 2 - observe target
+	
+	// initially randomly placed within the grid (not at the target)
+	[] o=0 -> 1/8 : (o'=1) & (x'=0) & (y'=0)
+			+ 1/8 : (o'=1) & (x'=0) & (y'=1)
+			+ 1/8 : (o'=1) & (x'=0) & (y'=2)
+			+ 1/8 : (o'=1) & (x'=1) & (y'=0)
+			+ 1/8 : (o'=1) & (x'=1) & (y'=1)
+			+ 1/8 : (o'=1) & (x'=1) & (y'=2)
+			// + 1/8 : (o'=1) & (x'=2) & (y'=0) the target
+			+ 1/8 : (o'=1) & (x'=2) & (y'=1)
+			+ 1/8 : (o'=1) & (x'=2) & (y'=2);
+			
+	// move around the grid
+	[east] o=1 & !(x=1 & y=0) -> (x'=min(x+1,2)); // not reached target
+	[east] o=1 & x=1 & y=0 -> (x'=min(x+1,2)) & (o'=2);
+	[west] o=1 -> (x'=max(x-1,0)); // not reached target
+	[north] o=1 -> (x'=min(y+1,2)); // reached target
+	[south] o=1 & !(x=2 & y=1) -> (y'=max(y-1,0)); // not reached target
+	[south] o=1 & x=2 & y=1 -> (y'=max(y-1,0)) & (o'=2); // reached target
+	
+	// reached target
+	[done] o=2 -> true;
+	
+endmodule
+
+// reward structure for number of steps to reach the target
+rewards
+        [east] true : 1;
+        [west] true : 1;
+        [north] true : 1;
+        [south] true : 1;
+endrewards

prism/tests/pomdps/3x3grid.prism.props

@@ -0,0 +1,3 @@
+// minimum steps to reach goal
+// RESULT: [2.8496094277343733,2.8750000000000004] (grid resolution 16)
+Rmin=?[F o=2 ]

prism/tests/pomdps/3x3grid_bounded.prism

@@ -0,0 +1,61 @@
+// 3x3 grid (for step bounded properties)
+// based on Littman, Cassandra and Kaelbling
+// Learning policies for partially observable environments: Scaling up  
+// Technical Report CS, Brown University
+
+pomdp
+
+const int K; // step bound in property
+
+// only the target is observable which is in the south east corner
+// (and the step bound)
+observables
+	o, k
+endobservables
+
+module grid
+	
+	x : [0..2]; // x coordinate
+	y : [0..2]; // y coordinate
+	o : [0..2]; // observables
+	// 0 - initial observation
+	// 1 - in the grid (not target)
+	// 2 - observe target
+	
+	// initially randomly placed within the grid (not at the target)
+	[] o=0 -> 1/8 : (o'=1) & (x'=0) & (y'=0)
+			+ 1/8 : (o'=1) & (x'=0) & (y'=1)
+			+ 1/8 : (o'=1) & (x'=0) & (y'=2)
+			+ 1/8 : (o'=1) & (x'=1) & (y'=0)
+			+ 1/8 : (o'=1) & (x'=1) & (y'=1)
+			+ 1/8 : (o'=1) & (x'=1) & (y'=2)
+			// + 1/8 : (o'=1) & (x'=2) & (y'=0) the target
+			+ 1/8 : (o'=1) & (x'=2) & (y'=1)
+			+ 1/8 : (o'=1) & (x'=2) & (y'=2);
+			
+	// move around the grid
+	[east] o=1 & !(x=1 & y=0) -> (x'=min(x+1,2)); // not reached target
+	[east] o=1 & x=1 & y=0 -> (x'=min(x+1,2)) & (o'=2); // reached target
+	[west] o=1 -> (x'=max(x-1,0)); // not reached target
+	[north] o=1 -> (x'=min(y+1,2)); // reached target
+	[south] o=1 & !(x=2 & y=1) -> (y'=max(y-1,0)); // not reached target
+	[south] o=1 & x=2 & y=1 -> (y'=max(y-1,0)) & (o'=2); // reached target
+	
+	// reached target
+	[done] o=2 -> true;
+	 
+endmodule
+
+// module for the step bound
+module bound
+
+	k : [0..K];
+	
+	[east] k<K -> (k'=k+1);
+	[west] k<K -> (k'=k+1);
+	[north] k<K -> (k'=k+1);
+	[south] k<K -> (k'=k+1);
+	
+	[] k=K -> true;
+	
+endmodule

prism/tests/pomdps/3x3grid_bounded.prism.args

@@ -0,0 +1 @@
+-const K=2

prism/tests/pomdps/3x3grid_bounded.prism.props

@@ -0,0 +1,3 @@
+// max probability reach goal (use with step bound property)
+// RESULT (K=2): [0.37500000000000006,0.375000078125] (grid resolution 8)
+Pmax=?[F o=2 ]

prism/tests/pomdps/crypt3.prism

@@ -0,0 +1,92 @@
+// dining cryptographers
+// gxn 27/01/16
+
+// pomdp model
+pomdp
+
+// observable variables (for crypt3)
+// the announcements of all cryptographers 
+// only its own coin and the coin of its left neighbour
+// if it guesses correctly (this is the target so needs to be observable)
+// also local states of modules this only indicates:
+// - if a cryptographer has announced
+// - if the master has made its choice
+observables
+	coin1, coin3, m, s1, s2, s3, guess, correct, agree1, agree2, agree3
+endobservables
+
+// constants used in renaming
+const int p1=1;
+const int p2=2;
+const int p3=3;
+
+module master
+	
+	m : [0..1]; // local state (has chosen who pays)
+	pay : [1..3]; // who actually pays
+	
+	// randomly choose who pays
+	[] m=0 -> 1/2 : (m'=1) & (pay'=1) + 1/2 : (m'=1) & (pay'=2);
+	
+	// test cases
+	//[] m=0 -> (m'=1); // master pays
+	//[] m=0 -> (m'=1) & (pay'=1); // crypt 1 pays
+	//[] m=0 -> (m'=1) & (pay'=2); // crypt 2 pays
+	//[] m=0 -> (m'=1) & (pay'=3); // crypt 3 pays
+	
+endmodule
+
+module crypt1
+	
+	coin1 : [0..2]; // value of coin
+	s1 : [0..1]; // local state (has announced yet)
+	agree1 : [0..1]; // agree or not
+	
+	// flip coin and share values
+	[flip] m=1 & coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2);
+	
+	// make choice (once relevant coins have been flipped)
+	// does not pay
+	[a1] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1);
+	[d1] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1);
+	// pays
+	[d1] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1);
+	[a1] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1);
+
+	// when everyone has announced
+	[done] s1=1 -> true;
+
+endmodule
+
+// construct further cryptographers through renaming
+module crypt2 =crypt1[coin1=coin2, s1=s2, p1=p2, agree1=agree2, coin2=coin3, a1=a2, d1=d2 ] endmodule
+
+// the cryptographer that guesses who pays
+module crypt3
+	
+	coin3 : [0..2];
+	s3 : [0..1];
+	agree3 : [0..1];
+	guess : [0..3];
+	correct : [0..1];
+	
+	// flip coin
+	[flip] m=1 & coin3=0 -> 0.5 : (coin3'=1) + 0.5 : (coin3'=2);
+	
+	// make choice (once relevant coins have been flipped)
+	// assume does not pay
+	[a3] s3=0 & coin3>0 & coin1>0 & coin3=coin1 -> (s3'=1) & (agree3'=1);
+	[d3] s3=0 & coin3>0 & coin1>0 & !(coin3=coin1) -> (s3'=1);
+	// pays
+	[d3] s3=0 & coin3>0 & coin1>0 & coin3=coin1 & (pay=p3) -> (s3'=1);
+	[a3] s3=0 & coin3>0 & coin1>0 & !(coin3=coin1) & (pay=p3) -> (s3'=1) & (agree3'=1);
+	
+	// after everyone has announced guess who payed
+	[done] s3=1 & guess=0 -> (guess'=1);
+	[done] s3=1 & guess=0 -> (guess'=2);
+	
+	// check whether guessed correctly
+	[check] s3=1 & guess>0 & guess=pay -> (correct'=1);
+	[check] s3=1 & guess>0 & !(guess=pay) -> true;
+
+endmodule

prism/tests/pomdps/crypt3.prism.props

@@ -0,0 +1,10 @@
+// minimum probability guess correctly which cryptographer paid
+// RESULT: 0.5
+Pmin=? [ F correct=1 ]
+
+// maximum probability guess correctly which cryptographer paid
+// RESULT: 0.5
+Pmax=? [ F correct=1 ]
+
+
+

prism/tests/pomdps/maze.prism

@@ -0,0 +1,115 @@
+// maze example (POMDP)
+// Littman, Cassandra and Kaelbling
+// Learning policies for partially observable environments: Scaling up  
+// Technical Report CS, Brown University
+// gxn 29/01/16
+
+// state space (value of variable "s")
+
+//  0  1  2  3  4
+//  5     6     7
+//  8     10    9
+
+// 10 is the target
+
+pomdp
+
+// can observe the walls and target
+observables
+	o
+endobservables
+// o=0 - observation in initial state
+// o=1 - west and north walls (s0)
+// o=2 - north and south ways (s1 and s3)
+// o=3 - north wall (s2)
+// o=4 - east and north way (s4)
+// o=5 - east and west walls (s5, s6 and s7)
+// o=6 - east, west and south walls (s8 and s9)
+// o=7 - the target (s10)
+
+module maze
+
+	s : [-1..10];
+	o : [0..7];
+	
+	// initialisation
+	[] s=-1 -> 0.1 : (s'=0) & (o'=1)
+			 + 0.1 : (s'=1) & (o'=2)
+			 + 0.1 : (s'=2) & (o'=3)
+			 + 0.1 : (s'=3) & (o'=2)
+			 + 0.1 : (s'=4) & (o'=4)
+			 + 0.1 : (s'=5) & (o'=5)
+			 + 0.1 : (s'=6) & (o'=5)
+			 + 0.1 : (s'=7) & (o'=5)
+			 + 0.1 : (s'=8) & (o'=6)
+			 + 0.1 : (s'=9) & (o'=6);
+	
+	// moving around the maze
+
+	[east] s=0 -> (s'=1) & (o'=2);
+	[west] s=0 -> (s'=0);
+	[north] s=0 -> (s'=0);
+	[south] s=0 -> (s'=5) & (o'=5);
+
+	[east] s=1 -> (s'=2) & (o'=3);
+	[west] s=1 -> (s'=0) & (o'=1);
+	[north] s=1 -> (s'=1);
+	[south] s=1 -> (s'=1);
+
+	[east] s=2 -> (s'=3) & (o'=2);
+	[west] s=2 -> (s'=1) & (o'=2);
+	[north] s=2 -> (s'=2);
+	[south] s=2 -> (s'=6) & (o'=5);
+
+	[east] s=3 -> (s'=4) & (o'=4);
+	[west] s=3 -> (s'=2) & (o'=2);
+	[north] s=3 -> (s'=3);
+	[south] s=3 -> (s'=3);
+
+	[east] s=4 -> (s'=4);
+	[west] s=4 -> (s'=3) & (o'=2);
+	[north] s=4 -> (s'=4);
+	[south] s=4 -> (s'=7) & (o'=5);
+
+	[east] s=5 -> (s'=5);
+	[west] s=5 -> (s'=5);
+	[north] s=5 -> (s'=0) & (o'=1);
+	[south] s=5 -> (s'=8) & (o'=6);
+
+	[east] s=6 -> (s'=6);
+	[west] s=6 -> (s'=6);
+	[north] s=6 -> (s'=2) & (o'=3);
+	[south] s=6 -> (s'=10) & (o'=7);
+
+	[east] s=7 -> (s'=7);
+	[west] s=7 -> (s'=7);
+	[north] s=7 -> (s'=4) & (o'=4);
+	[south] s=7 -> (s'=9) & (o'=6);
+
+	[east] s=8 -> (s'=8);
+	[west] s=8 -> (s'=8);
+	[north] s=8 -> (s'=5) & (o'=5);
+	[south] s=8 -> (s'=8);
+
+	[east] s=9 -> (s'=9);
+	[west] s=9 -> (s'=9);
+	[north] s=9 -> (s'=7) & (o'=5);
+	[south] s=9 -> (s'=9);
+
+	// loop when we reach the target
+	[done] s=10 -> true;
+
+endmodule
+
+// reward structure (number of steps to reach the target)
+rewards
+
+	[east] true : 1;
+	[west] true : 1;
+	[north] true : 1;
+	[south] true : 1;
+
+endrewards
+
+// target observation
+label "target" = o=7;

prism/tests/pomdps/maze.prism.props

@@ -0,0 +1,3 @@
+// Minimum expected number of steps to reach the target
+// RESULT: 4.3
+Rmin=? [ F "target" ]

prism/tests/pomdps/maze2.prism

@@ -0,0 +1,135 @@
+// maze example (POMDP)
+// slightly extends that presented in
+// Littman, Cassandra and Kaelbling
+// Learning policies for partially observable environments: Scaling up  
+// Technical Report CS, Brown University
+// gxn 29/01/16
+
+// state space (value of variable "s")
+
+//  0  1  2  3  4
+//  5     6     7
+//  8     9    10
+// 11     13   12
+
+// 13 is the target
+
+pomdp
+
+// can observe the walls and target
+observables
+	o
+endobservables
+// o=0 - observation in initial state
+// o=1 - west and north walls (s0)
+// o=2 - north and south ways (s1 and s3)
+// o=3 - north wall (s2)
+// o=4 - east and north way (s4)
+// o=5 - east and west walls (s5, s6, s7, s8, s9 and s10)
+// o=6 - east, west and south walls (s11 and s12)
+// o=7 - the target (s13)
+
+module maze
+
+	s : [-1..13];
+	o : [0..7];
+	
+	// initialisation
+	[] s=-1 -> 1/13 : (s'=0) & (o'=1)
+			 + 1/13 : (s'=1) & (o'=2)
+			 + 1/13 : (s'=2) & (o'=3)
+			 + 1/13 : (s'=3) & (o'=2)
+			 + 1/13 : (s'=4) & (o'=4)
+			 + 1/13 : (s'=5) & (o'=5)
+			 + 1/13 : (s'=6) & (o'=5)
+			 + 1/13 : (s'=7) & (o'=5)
+			 + 1/13 : (s'=8) & (o'=5)
+			 + 1/13 : (s'=9) & (o'=5)
+			 + 1/13 : (s'=10) & (o'=5)
+			 + 1/13 : (s'=11) & (o'=6)
+			 + 1/13 : (s'=12) & (o'=6);
+	
+	// moving around the maze
+	
+	[east] s=0 -> (s'=1) & (o'=2);
+	[west] s=0 -> (s'=0);
+	[north] s=0 -> (s'=0);
+	[south] s=0 -> (s'=5) & (o'=5);
+
+	[east] s=1 -> (s'=2) & (o'=3);
+	[west] s=1 -> (s'=0) & (o'=1);
+	[north] s=1 -> (s'=1);
+	[south] s=1 -> (s'=1);
+
+	[east] s=2 -> (s'=3) & (o'=2);
+	[west] s=2 -> (s'=1) & (o'=2);
+	[north] s=2 -> (s'=2);
+	[south] s=2 -> (s'=6) & (o'=5);
+
+	[east] s=3 -> (s'=4) & (o'=4);
+	[west] s=3 -> (s'=2) & (o'=2);
+	[north] s=3 -> (s'=3);
+	[south] s=3 -> (s'=3);
+
+	[east] s=4 -> (s'=4);
+	[west] s=4 -> (s'=3) & (o'=2);
+	[north] s=4 -> (s'=4);
+	[south] s=4 -> (s'=7) & (o'=5);
+
+	[east] s=5 -> (s'=5);
+	[west] s=5 -> (s'=5);
+	[north] s=5 -> (s'=0) & (o'=1);
+	[south] s=5 -> (s'=8);
+
+	[east] s=6 -> (s'=6);
+	[west] s=6 -> (s'=6);
+	[north] s=6 -> (s'=2) & (o'=3);
+	[south] s=6 -> (s'=9);
+
+	[east] s=7 -> (s'=7);
+	[west] s=7 -> (s'=7);
+	[north] s=7 -> (s'=4) & (o'=4);
+	[south] s=7 -> (s'=10);
+
+	[east] s=8 -> (s'=8);
+	[west] s=8 -> (s'=8);
+	[north] s=8 -> (s'=5);
+	[south] s=8 -> (s'=11) & (o'=6);
+
+	[east] s=9 -> (s'=9);
+	[west] s=9 -> (s'=9);
+	[north] s=9 -> (s'=6);
+	[south] s=9 -> (s'=13) & (o'=7);
+
+	[east] s=10 -> (s'=9);
+	[west] s=10 -> (s'=9);
+	[north] s=10 -> (s'=7);
+	[south] s=10 -> (s'=12) & (o'=6);
+
+	[east] s=11 -> (s'=11);
+	[west] s=11 -> (s'=11);
+	[north] s=11 -> (s'=8) & (o'=5);
+	[south] s=11 -> (s'=11);
+
+	[east] s=12 -> (s'=12);
+	[west] s=12 -> (s'=12);
+	[north] s=12 -> (s'=10) & (o'=5);
+	[south] s=12 -> (s'=12);
+
+	// loop when we reach the target
+	[done] s=13 -> true;
+
+endmodule
+
+// reward structure (number of steps to reach the target)
+rewards
+
+	[east] true : 1;
+	[west] true : 1;
+	[north] true : 1;
+	[south] true : 1;
+
+endrewards
+
+// target observation
+label "target" = o=7;

prism/tests/pomdps/maze2.prism.props

@@ -0,0 +1,3 @@
+// Minimum expected number of steps to reach the target
+// RESULT: [5.199999938461538,5.230769230769232] (grid resolution 20)
+Rmin=? [ F "target" ]

prism/tests/pomdps/network2.prism

@@ -0,0 +1,93 @@
+// network unitization example with partially observable channels based on:
+// L. Yang, S. Murugesan and J. Zhang
+// Real-Kime Scheduling over Markovian Channels: When Partial Observability Meets Hard Deadlines
+// IEEE Global Kelecommunications Conference (GLOBECOM'11), pages 1-5, 2011
+
+pomdp
+
+observables
+	sched, k, t, packet1, packet2 //, chan1, chan2
+endobservables
+
+// timing constants
+const int K; // total number of time periods
+const int T; // number of slots per time period
+
+// probabilities that channels change states
+// channel of user 1
+const double p1 = 0.8; // prob remain on
+const double r1 = 0.2; // prob move from off to on
+// channel of user 2
+const double p2 = 0.6; // prob remain on
+const double r2 = 0.4; // prob move from off to on
+
+// scheduler
+module scheduler
+
+	k : [0..K-1]; // current time period
+	t : [0..T-1]; // correct slot
+	sched : [0..1]; // local state
+	
+	// next slot/time period 
+	[slot] sched=0 & t<T-1 -> (sched'=1) & (t'=t+1);
+	[slot] sched=0 & t=T-1 & k<K-1 -> (sched'=1) & (t'=0) & (k'=k+1);
+
+	// make scheduling choice
+	[idle]  sched=1 -> (sched'=0);
+	[send1] sched=1 -> (sched'=0);
+	[send2] sched=1 -> (sched'=0);
+
+	// loop when finished
+	[] sched=0 & t=T-1 & k=K-1 -> true;
+	
+endmodule
+
+// packets for first channel
+module packet1
+
+	packet1 : [0..1]; // packet to send in current period
+
+	// next slot
+	[slot] t=0 -> (packet1'=1); // new period so new packet
+	[slot] t>0 -> true;
+	// sending
+	[send1]	packet1=1 & chan1=1 -> (packet1'=0); // channel up
+	[send1]	packet1=1 & chan1=0 -> true; // channel down
+
+endmodule
+
+// construct further channels' packets through renaming
+module packet2=packet1[packet1=packet2,send1=send2,chan1=chan2] endmodule
+
+// first channel status
+module channel1
+
+	chan1 : [0..1]; // status of channel (off/on)
+
+	// initialise
+	[slot] t=0 & k=0 -> 0.5 : (chan1'=0) + 0.5 : (chan1'=1);
+	// next slot
+	[slot] chan1=0 & !(t=0 & k=0) -> 1 - r1 : (chan1'=0) + r1 : (chan1'=1);
+	[slot] chan1=1 & !(t=0 & k=0) -> 1 - p1 : (chan1'=0) + p1 : (chan1'=1);
+
+endmodule
+
+// construct further channels through renaming
+module channel2=channel1[chan1=chan2,p1=p2,r1=r2] endmodule
+
+// reward structure for number of dropped packets
+// (need to be careful as we update k and t at the start of the time slot)
+rewards "dropped_packets"
+	[slot] t=0 & k>0 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[idle] t=T-1 & k=K-1 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[send1] t=T-1 & k=K-1 & chan1=0 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[send2] t=T-1 & k=K-1 & chan2=0 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[send1] t=T-1 & k=K-1 & chan1=1 : ((packet2=0)?0:1);
+	[send2] t=T-1 & k=K-1 & chan2=1 : ((packet1=0)?0:1);
+endrewards
+
+// reward structure for number of sent packets
+rewards "packets_sent"
+	[send1] chan1=1 : 1;
+	[send2] chan2=1 : 1;
+endrewards

prism/tests/pomdps/network2.prism.args

@@ -0,0 +1 @@
+-const K=2,T=3

prism/tests/pomdps/network2.prism.props

@@ -0,0 +1,7 @@
+// minimum number of dropped packets
+// RESULT (K=2,T=3): [1.6572208448483332,1.6578400000000002] (grid resolution 50)
+R{"dropped_packets"}min=?[F sched=0 & t=T-1 & k=K-1 ]
+
+// maximum number of packets sent (dual property)
+// RESULT (K=2,T=3): [2.3421600000000002,2.342779155151662] (grid resolution 50)
+R{"packets_sent"}max=?[F sched=0 & t=T-1 & k=K-1 ]

prism/tests/pomdps/network2_noidle.prism

@@ -0,0 +1,93 @@
+// network unitization example with partially observable channels based on:
+// L. Yang, S. Murugesan and J. Zhang
+// Real-Kime Scheduling over Markovian Channels: When Partial Observability Meets Hard Deadlines
+// IEEE Global Kelecommunications Conference (GLOBECOM'11), pages 1-5, 2011
+
+pomdp
+
+observables
+	sched, k, t, packet1, packet2 //, chan1, chan2
+endobservables
+
+// timing constants
+const int K; // total number of time periods
+const int T; // number of slots per time period
+
+// probabilities that channels change states
+// channel of user 1
+const double p1 = 0.8; // prob remain on
+const double r1 = 0.2; // prob move from off to on
+// channel of user 2
+const double p2 = 0.6; // prob remain on
+const double r2 = 0.4; // prob move from off to on
+
+// scheduler
+module scheduler
+
+	k : [0..K-1]; // current time period
+	t : [0..T-1]; // correct slot
+	sched : [0..1]; // local state
+	
+	// next slot/time period 
+	[slot] sched=0 & t<T-1 -> (sched'=1) & (t'=t+1);
+	[slot] sched=0 & t=T-1 & k<K-1 -> (sched'=1) & (t'=0) & (k'=k+1);
+
+	// make scheduling choice
+	[idle]  sched=1 & packet1=0 & packet2=0 -> (sched'=0);
+	[send1] sched=1 -> (sched'=0);
+	[send2] sched=1 -> (sched'=0);
+
+	// loop when finished
+	[] sched=0 & t=T-1 & k=K-1 -> true;
+	
+endmodule
+
+// packets for first channel
+module packet1
+
+	packet1 : [0..1]; // packet to send in current period
+
+	// next slot
+	[slot] t=0 -> (packet1'=1); // new period so new packet
+	[slot] t>0 -> true;
+	// sending
+	[send1]	packet1=1 & chan1=1 -> (packet1'=0); // channel up
+	[send1]	packet1=1 & chan1=0 -> true; // channel down
+
+endmodule
+
+// construct further channels' packets through renaming
+module packet2=packet1[packet1=packet2,send1=send2,chan1=chan2] endmodule
+
+// first channel status
+module channel1
+
+	chan1 : [0..1]; // status of channel (off/on)
+
+	// initialise
+	[slot] t=0 & k=0 -> 0.5 : (chan1'=0) + 0.5 : (chan1'=1);
+	// next slot
+	[slot] chan1=0 & !(t=0 & k=0) -> 1 - r1 : (chan1'=0) + r1 : (chan1'=1);
+	[slot] chan1=1 & !(t=0 & k=0) -> 1 - p1 : (chan1'=0) + p1 : (chan1'=1);
+
+endmodule
+
+// construct further channels through renaming
+module channel2=channel1[chan1=chan2,p1=p2,r1=r2] endmodule
+
+// reward structure for number of dropped packets
+// (need to be careful as we update k and t at the start of the time slot)
+rewards "dropped_packets"
+	[slot] t=0 & k>0 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[idle] t=T-1 & k=K-1 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[send1] t=T-1 & k=K-1 & chan1=0 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[send2] t=T-1 & k=K-1 & chan2=0 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[send1] t=T-1 & k=K-1 & chan1=1 : ((packet2=0)?0:1);
+	[send2] t=T-1 & k=K-1 & chan2=1 : ((packet1=0)?0:1);
+endrewards
+
+// reward structure for number of sent packets
+rewards "packets_sent"
+	[send1] chan1=1 : 1;
+	[send2] chan2=1 : 1;
+endrewards

prism/tests/pomdps/network2_noidle.prism.args

@@ -0,0 +1 @@
+-const K=2,T=3

prism/tests/pomdps/network2_noidle.prism.props

@@ -0,0 +1,7 @@
+// minimum number of dropped packets
+// RESULT (K=2,T=3): [1.6572208448483332,1.6578400000000002] (grid resolution 50)
+R{"dropped_packets"}min=?[F sched=0 & t=T-1 & k=K-1 ]
+
+// maximum number of packets sent (dual property)
+// RESULT (K=2,T=3): [2.3421600000000002,2.342779155151662] (grid resolution 50)
+R{"packets_sent"}max=?[F sched=0 & t=T-1 & k=K-1 ]

prism/tests/pomdps/network2_priorities.prism

@@ -0,0 +1,124 @@
+// network unitization example with partially observable channels based on:
+// L. Yang, S. Murugesan and J. Zhang
+// Real-Kime Scheduling over Markovian Channels: When Partial Observability Meets Hard Deadlines
+// IEEE Global Kelecommunications Conference (GLOBECOM'11), pages 1-5, 2011
+
+pomdp
+
+observables
+	sched, k, t, packet1, packet2, priority1, priority2 //, chan1, chan2, 
+endobservables
+
+// timing constants
+const int K; // total number of time periods
+const int T; // number of slots per time period
+
+// probabilities that channels change states
+// channel of user 1
+const double p1 = 0.8; // prob remain on
+const double r1 = 0.2; // prob move from off to on
+// channel of user 2
+const double p2 = 0.6; // prob remain on
+const double r2 = 0.4; // prob move from off to on
+
+// scheduler
+module scheduler
+
+	k : [0..K-1]; // current time period
+	t : [0..T-1]; // correct slot
+	sched : [0..1]; // local state
+	
+	// next slot/time period 
+	[slot] sched=0 & t<T-1 -> (sched'=1) & (t'=t+1);
+	[slot] sched=0 & t=T-1 & k<K-1 -> (sched'=1) & (t'=0) & (k'=k+1);
+
+	// make scheduling choice
+	[idle]  sched=1 -> (sched'=0);
+	[send1] sched=1 -> (sched'=0);
+	[send2] sched=1 -> (sched'=0);
+
+    // loop when finished
+	[] sched=0 & t=T-1 & k=K-1 -> true;
+	
+endmodule
+
+// packets for first channel
+module packet1
+
+	packet1 : [0..1]; // packet to send in current period
+
+	// next slot
+	[slot] t=0 -> (packet1'=1); // new period so new packet
+	[slot] t>0 -> true;
+	// sending
+	[send1]	packet1=1 & chan1=1 -> (packet1'=0); // channel up
+	[send1]	packet1=1 & chan1=0 -> true; // channel down
+
+endmodule
+
+// construct further channels' packets through renaming
+module packet2=packet1[packet1=packet2,send1=send2,chan1=chan2] endmodule
+
+// priority of packets for first channel
+module priority1
+
+	priority1 : [0..3];
+	
+	// new period so new packet and randomly assign priority
+	[slot] t=0 -> 0.1 : (priority1'=1) + 0.3 : (priority1'=2) + 0.6 : (priority1'=3);
+	// priority already assigned for this period
+	[slot] t>0 -> true;
+	
+	// reset priority when packet has been sent
+	[send1] chan1=0 -> true;
+	[send1] chan1=1 -> (priority1'=0);
+	
+endmodule
+
+// construct further priorities through renaming
+module priority2 = priority1[priority1=priority2,chan1=chan2,send1=send2] endmodule
+
+// first channel status
+module channel1
+
+	chan1 : [0..1]; // status of channel (off/on)
+
+	// initialise
+	[slot] t=0 & k=0 -> 0.5 : (chan1'=0) + 0.5 : (chan1'=1);
+	// next slot
+	[slot] chan1=0 & !(t=0 & k=0) -> 1 - r1 : (chan1'=0) + r1 : (chan1'=1);
+	[slot] chan1=1 & !(t=0 & k=0) -> 1 - p1 : (chan1'=0) + p1 : (chan1'=1);
+
+endmodule
+
+// construct further channels through renaming
+module channel2=channel1[chan1=chan2,p1=p2,r1=r2] endmodule
+
+// reward structure for number of dropped packets
+// (need to be careful as we update k and t at the start of the time slot)
+rewards "dropped_packets"
+	[slot] t=0 & k>0 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[idle] t=T-1 & k=K-1 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[send1] t=T-1 & k=K-1 & chan1=0 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[send2] t=T-1 & k=K-1 & chan2=0 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[send1] t=T-1 & k=K-1 & chan1=1 : ((packet2=0)?0:1);
+	[send2] t=T-1 & k=K-1 & chan2=1 : ((packet1=0)?0:1);
+endrewards
+
+// reward structure for number of sent packets
+rewards "packets_sent"
+	[send1] chan1=1 : 1;
+	[send2] chan2=1 : 1;
+endrewards
+
+const double beta=1; // discount factor
+
+// (discounted) reward structure based on priorities 
+rewards "priority"
+	[send1] chan1=1 & priority1=1 :  1 * pow(beta,t + k*T);
+	[send2] chan2=1 & priority2=1 :  1 * pow(beta,t + k*T);
+	[send1] chan1=1 & priority1=2 : 10 * pow(beta,t + k*T);
+	[send2] chan2=1 & priority2=2 : 10 * pow(beta,t + k*T);
+	[send1] chan1=1 & priority1=3 : 20 * pow(beta,t + k*T);
+	[send2] chan2=1 & priority2=3 : 20 * pow(beta,t + k*T);
+endrewards

prism/tests/pomdps/network2_priorities.prism.args

@@ -0,0 +1 @@
+-const K=2,T=3

prism/tests/pomdps/network2_priorities.prism.props

@@ -0,0 +1,11 @@
+// minimum number of dropped packets
+// RESULT (K=2,T=3): [1.6560279993301588,1.6578400000000002] (grid resolution 20)
+R{"dropped_packets"}min=?[F sched=0 & t=T-1 & k=K-1 ]
+
+// maximum number of packets sent (dual property)
+// RESULT (K=2,T=3): [2.3421600000000002,2.3439720006698384] (grid resolution 20)
+R{"packets_sent"}max=?[F sched=0 & t=T-1 & k=K-1 ]
+
+// maximum reward (based on priorities)
+// RESULT (K=2,T=3): [36.321503131200004,36.33018249727175] (grid resolution 20)
+R{"priority"}max=?[F sched=0 & t=T-1 & k=K-1 ]

prism/tests/pomdps/network2_priorities_noidle.prism

@@ -0,0 +1,124 @@
+// network unitization example with partially observable channels based on:
+// L. Yang, S. Murugesan and J. Zhang
+// Real-Kime Scheduling over Markovian Channels: When Partial Observability Meets Hard Deadlines
+// IEEE Global Kelecommunications Conference (GLOBECOM'11), pages 1-5, 2011
+
+pomdp
+
+observables
+	sched, k, t, packet1, packet2, priority1, priority2 //, chan1, chan2, 
+endobservables
+
+// timing constants
+const int K; // total number of time periods
+const int T; // number of slots per time period
+
+// probabilities that channels change states
+// channel of user 1
+const double p1 = 0.8; // prob remain on
+const double r1 = 0.2; // prob move from off to on
+// channel of user 2
+const double p2 = 0.6; // prob remain on
+const double r2 = 0.4; // prob move from off to on
+
+// scheduler
+module scheduler
+
+	k : [0..K-1]; // current time period
+	t : [0..T-1]; // correct slot
+	sched : [0..1]; // local state
+	
+	// next slot/time period 
+	[slot] sched=0 & t<T-1 -> (sched'=1) & (t'=t+1);
+	[slot] sched=0 & t=T-1 & k<K-1 -> (sched'=1) & (t'=0) & (k'=k+1);
+
+	// make scheduling choice
+	[idle]  sched=1 & packet1=0 & packet2=0 -> (sched'=0);
+	[send1] sched=1 -> (sched'=0);
+	[send2] sched=1 -> (sched'=0);
+
+    // loop when finished
+    [] sched=0 & t=T-1 & k=K-1 -> true;
+	
+endmodule
+
+// packets for first channel
+module packet1
+
+	packet1 : [0..1]; // packet to send in current period
+
+	// next slot
+	[slot] t=0 -> (packet1'=1); // new period so new packet
+	[slot] t>0 -> true;
+	// sending
+	[send1]	packet1=1 & chan1=1 -> (packet1'=0); // channel up
+	[send1]	packet1=1 & chan1=0 -> true; // channel down
+
+endmodule
+
+// construct further channels' packets through renaming
+module packet2=packet1[packet1=packet2,chan1=chan2] endmodule
+
+// priority of packets for first channel
+module priority1
+
+	priority1 : [0..3];
+	
+	// new period so new packet and randomly assign priority
+	[slot] t=0 -> 0.1 : (priority1'=1) + 0.3 : (priority1'=2) + 0.6 : (priority1'=3);
+	// priority already assigned for this period
+	[slot] t>0 -> true;
+	
+	// reset priority when packet has been sent
+	[send1] chan1=0 -> true;
+	[send1] chan1=1 -> (priority1'=0);
+	
+endmodule
+
+// construct further priorities through renaming
+module priority2 = priority1[priority1=priority2,chan1=chan2,send1=send2] endmodule
+
+// first channel status
+module channel1
+
+	chan1 : [0..1]; // status of channel (off/on)
+
+	// initialise
+	[slot] t=0 & k=0 -> 0.5 : (chan1'=0) + 0.5 : (chan1'=1);
+	// next slot
+	[slot] chan1=0 & !(t=0 & k=0) -> 1 - r1 : (chan1'=0) + r1 : (chan1'=1);
+	[slot] chan1=1 & !(t=0 & k=0) -> 1 - p1 : (chan1'=0) + p1 : (chan1'=1);
+
+endmodule
+
+// construct further channels through renaming
+module channel2=channel1[chan1=chan2,send1=send2,p1=p2,r1=r2] endmodule
+
+// reward structure for number of dropped packets
+// (need to be careful as we update k and t at the start of the time slot)
+rewards "dropped_packets"
+	[slot] t=0 & k>0 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[idle] t=T-1 & k=K-1 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[send1] t=T-1 & k=K-1 & chan1=0 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[send2] t=T-1 & k=K-1 & chan2=0 : ((packet1=0)?0:1) + ((packet2=0)?0:1);
+	[send1] t=T-1 & k=K-1 & chan1=1 : ((packet2=0)?0:1);
+	[send2] t=T-1 & k=K-1 & chan2=1 : ((packet1=0)?0:1);
+endrewards
+
+// reward structure for number of sent packets
+rewards "packets_sent"
+	[send1] chan1=1 : 1;
+	[send2] chan2=1 : 1;
+endrewards
+
+const double beta=1; // discount factor
+
+// (discounted) reward structure based on priorities 
+rewards "priority"
+	[send1] chan1=1 & priority1=1 :  1 * pow(beta,t + k*T);
+	[send2] chan2=1 & priority2=1 :  1 * pow(beta,t + k*T);
+	[send1] chan1=1 & priority1=2 : 10 * pow(beta,t + k*T);
+	[send2] chan2=1 & priority2=2 : 10 * pow(beta,t + k*T);
+	[send1] chan1=1 & priority1=3 : 20 * pow(beta,t + k*T);
+	[send2] chan2=1 & priority2=3 : 20 * pow(beta,t + k*T);
+endrewards

prism/tests/pomdps/network2_priorities_noidle.prism.args

@@ -0,0 +1 @@
+-const K=2,T=3

prism/tests/pomdps/network2_priorities_noidle.prism.props

@@ -0,0 +1,11 @@
+// minimum number of dropped packets
+// RESULT (K=2,T=3): [1.578,1.578000000041999] (grid resolution 20)
+R{"dropped_packets"}min=?[F sched=0 & t=T-1 & k=K-1 ]
+
+// maximum number of packets sent (dual property)
+// RESULT (K=2,T=3): [2.66096,2.6646735594157978] (grid resolution 20)
+R{"packets_sent"}max=?[F sched=0 & t=T-1 & k=K-1 ]
+
+// maximum reward (based on priorities)
+// RESULT (K=2,T=3): [35.557181022719995,35.58142127696651] (grid resolution 20)
+R{"priority"}max=?[F sched=0 & t=T-1 & k=K-1 ]