diff --git a/test/functional/parser/prism/coin2.nm b/test/functional/parser/prism/coin2.nm
new file mode 100644
index 000000000..a08bb8741
--- /dev/null
+++ b/test/functional/parser/prism/coin2.nm
@@ -0,0 +1,60 @@
+// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] 
+// gxn/dxp 20/11/00
+
+mdp
+
+// constants
+const int N=2;
+const int K;
+const int range = 2*(K+1)*N;
+const int counter_init = (K+1)*N;
+const int left = N;
+const int right = 2*(K+1)*N - N;
+
+// shared coin
+global counter : [0..range] init counter_init;
+
+module process1
+	
+	// program counter
+	pc1 : [0..3];
+	// 0 - flip
+	// 1 - write 
+	// 2 - check
+	// 3 - finished
+	
+	// local coin
+	coin1 : [0..1];	
+
+	// flip coin
+	[] (pc1=0)  -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
+	// write tails -1  (reset coin to add regularity)
+	[] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0);
+	// write heads +1 (reset coin to add regularity)
+	[] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0);
+	// check
+	// decide tails
+	[] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0);
+	// decide heads
+	[] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1);
+	// flip again
+	[] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0);
+	// loop (all loop together when done)
+	[done] (pc1=3) -> 1 : (pc1'=3);
+
+endmodule
+
+// construct remaining processes through renaming
+module process2 = process1[pc1=pc2,coin1=coin2] endmodule
+
+// labels
+label "finished" = pc1=3 & pc2=3 ;
+label "all_coins_equal_0" = coin1=0 & coin2=0 ;
+label "all_coins_equal_1" = coin1=1 & coin2=1 ;
+label "agree" = coin1=coin2 ;
+
+// rewards
+rewards "steps"
+	true : 1;
+endrewards
+
diff --git a/test/functional/parser/prism/crowds5_5.pm b/test/functional/parser/prism/crowds5_5.pm
new file mode 100644
index 000000000..60bdaa7ea
--- /dev/null
+++ b/test/functional/parser/prism/crowds5_5.pm
@@ -0,0 +1,69 @@
+dtmc
+
+// probability of forwarding
+const double    PF = 0.8;
+const double notPF = .2;  // must be 1-PF
+// probability that a crowd member is bad
+const double  badC = .167;
+ // probability that a crowd member is good
+const double goodC = 0.833;
+// Total number of protocol runs to analyze
+const int TotalRuns = 5;
+// size of the crowd
+const int CrowdSize = 5;
+
+module crowds
+	// protocol phase
+	phase: [0..4] init 0;
+
+	// crowd member good (or bad)
+	good: bool init false;
+
+	// number of protocol runs
+	runCount: [0..TotalRuns] init 0;
+
+	// observe_i is the number of times the attacker observed crowd member i
+	observe0: [0..TotalRuns] init 0;
+
+	observe1: [0..TotalRuns] init 0;
+
+	observe2: [0..TotalRuns] init 0;
+
+	observe3: [0..TotalRuns] init 0;
+
+	observe4: [0..TotalRuns] init 0;
+
+	// the last seen crowd member
+	lastSeen: [0..CrowdSize - 1] init 0;
+
+	// get the protocol started
+	[] phase=0 & runCount<TotalRuns -> 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0);
+
+	// decide whether crowd member is good or bad according to given probabilities
+	[] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false);
+
+	// if the current member is a good member, update the last seen index (chosen uniformly)
+	[] phase=2 & good -> 1/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3);
+
+	// if the current member is a bad member, record the most recently seen index
+	[] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4);
+
+	// good crowd members forward with probability PF and deliver otherwise
+	[] phase=3 -> PF : (phase'=1) + notPF : (phase'=4);
+
+	// deliver the message and start over
+	[] phase=4 -> 1: (phase'=0);
+
+endmodule
+
+label "observe0Greater1" = observe0>1;
+label "observe1Greater1" = observe1>1;
+label "observe2Greater1" = observe2>1;
+label "observe3Greater1" = observe3>1;
+label "observe4Greater1" = observe4>1;
+label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1;
+label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1;
diff --git a/test/functional/parser/prism/csma2_2.nm b/test/functional/parser/prism/csma2_2.nm
new file mode 100644
index 000000000..18ec5c897
--- /dev/null
+++ b/test/functional/parser/prism/csma2_2.nm
@@ -0,0 +1,130 @@
+// CSMA/CD protocol - probabilistic version of kronos model (3 stations)
+// gxn/dxp 04/12/01
+
+mdp
+
+// note made changes since cannot have strict inequalities
+// in digital clocks approach and suppose a station only sends one message
+
+// simplified parameters scaled
+const int sigma=1; // time for messages to propagate along the bus
+const int lambda=30; // time to send a message
+
+// actual parameters
+const int N = 2; // number of processes
+const int K = 2; // exponential backoff limit
+const int slot = 2*sigma; // length of slot
+// const int M = floor(pow(2, K))-1 ; // max number of slots to wait
+const int M = 3 ; // max number of slots to wait
+//const int lambda=782;
+//const int sigma=26;
+
+// formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1);
+// formula min_collisions = min(cd1,cd2);
+// formula max_collisions = max(cd1,cd2);
+
+//----------------------------------------------------------------------------------------------------------------------------
+// the bus
+module bus
+	
+	b : [0..2];
+	// b=0 - idle
+	// b=1 - active
+	// b=2 - collision
+	
+	// clocks of bus
+	y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy)
+	y2 : [0..sigma+1]; // time since second send (used to find time until collision detected)
+	
+	// a sender sends (ok - no other message being sent)
+	[send1] (b=0) -> (b'=1);
+	[send2] (b=0) -> (b'=1);
+	
+	// a sender sends (bus busy - collision)
+	[send1] (b=1|b=2) & (y1<sigma) -> (b'=2);
+	[send2] (b=1|b=2) & (y1<sigma) -> (b'=2);
+	
+	// finish sending
+	[end1] (b=1) -> (b'=0) & (y1'=0);
+	[end2] (b=1) -> (b'=0) & (y1'=0);
+	
+	// bus busy
+	[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
+	[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
+	
+	// collision detected
+	[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0);
+	
+	// time passage
+	[time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0
+	[time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1
+	[time] (b=2) & (y2<sigma) -> (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected)
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+// model of first sender
+module station1
+	
+	// LOCAL STATE
+	s1 : [0..5];
+	// s1=0 - initial state
+	// s1=1 - transmit
+	// s1=2 - collision (set backoff)
+	// s1=3 - wait (bus busy)
+	// s1=4 - successfully sent
+	
+	// LOCAL CLOCK
+	x1 : [0..max(lambda,slot)];
+	
+	// BACKOFF COUNTER (number of slots to wait)
+	bc1 : [0..M];
+	
+	// COLLISION COUNTER
+	cd1 : [0..K];
+	
+	// start sending
+	[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending
+	[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff
+	
+	// transmitting
+	[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass
+	[end1]  (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished
+	[cd]   (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter)
+	[cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important
+	
+	// set backoff (no time can pass in this state)
+	// probability depends on which transmission this is (cd1)
+	[] s1=2 & cd1=1 ->  1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ;
+	[] s1=2 & cd1=2 ->  1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ;
+	
+	// wait until backoff counter reaches 0 then send again
+	[time] (s1=3) & (x1<slot) -> (x1'=x1+1); // let time pass (in slot)
+	[time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots)
+	[send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free)
+	[busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy)
+	
+	// once finished nothing matters
+	[time] (s1>=4) -> (x1'=0);
+
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// construct further stations through renaming
+module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// reward structure for expected time
+rewards "time"
+	[time] true : 1;
+endrewards
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// labels/formulae
+label "all_delivered" = s1=4&s2=4;
+label "one_delivered" = s1=4|s2=4;
+label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2);
+
diff --git a/test/functional/parser/prism/die.pm b/test/functional/parser/prism/die.pm
new file mode 100644
index 000000000..700951a05
--- /dev/null
+++ b/test/functional/parser/prism/die.pm
@@ -0,0 +1,24 @@
+// Knuth's model of a fair die using only fair coins
+dtmc
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the dice
+	d : [0..6] init 0;
+	
+	[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+	[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+	[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+	[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+	[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+	[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+	[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+	[] s=7 -> 1: (s'=7);
+	
+endmodule
+
+rewards "coin_flips"
+	[] s<7 : 1;
+endrewards
diff --git a/test/functional/parser/prism/firewire.nm b/test/functional/parser/prism/firewire.nm
new file mode 100644
index 000000000..26fa210b4
--- /dev/null
+++ b/test/functional/parser/prism/firewire.nm
@@ -0,0 +1,170 @@
+// firewire protocol with integer semantics
+// dxp/gxn 14/06/01
+
+// CLOCKS
+// x1 (x2) clock for node1 (node2)
+// y1 and y2 (z1 and z2) clocks for wire12 (wire21)
+mdp
+
+// maximum and minimum delays
+// fast
+const int rc_fast_max = 85;
+const int rc_fast_min = 76;
+// slow
+const int rc_slow_max = 167;
+const int rc_slow_min = 159;
+// delay caused by the wire length
+const int delay;
+// probability of choosing fast
+const double fast;
+const double slow=1-fast;
+
+module wire12
+	
+	// local state
+	w12 : [0..9];
+	// 0 - empty
+	// 1 -	rec_req
+	// 2 -  rec_req_ack
+	// 3 -	rec_ack
+	// 4 -	rec_ack_idle
+	// 5 -	rec_idle
+	// 6 -	rec_idle_req
+	// 7 -	rec_ack_req
+	// 8 -	rec_req_idle
+	// 9 -	rec_idle_ack
+	
+	// clock for wire12
+	y1 : [0..delay+1];
+	y2 : [0..delay+1];
+
+	// empty
+	// do not need y1 and y2 to increase as always reset when this state is left
+	// similarly can reset y1 and y2 when we re-enter this state
+	[snd_req12]  w12=0 -> (w12'=1) & (y1'=0) & (y2'=0);
+	[snd_ack12]  w12=0 -> (w12'=3) & (y1'=0) & (y2'=0);
+	[snd_idle12] w12=0 -> (w12'=5) & (y1'=0) & (y2'=0);
+	[time]       w12=0 -> (w12'=w12);	
+	// rec_req
+	[snd_req12]  w12=1 -> (w12'=1);
+	[rec_req12]  w12=1 -> (w12'=0) & (y1'=0) & (y2'=0);
+	[snd_ack12]  w12=1 -> (w12'=2) & (y2'=0);
+	[snd_idle12] w12=1 -> (w12'=8) & (y2'=0);
+	[time]       w12=1 & y2<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_req_ack
+	[snd_ack12] w12=2 -> (w12'=2);
+	[rec_req12] w12=2 -> (w12'=3);
+	[time]      w12=2 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_ack
+	[snd_ack12]  w12=3 -> (w12'=3);
+	[rec_ack12]  w12=3 -> (w12'=0) & (y1'=0) & (y2'=0);
+	[snd_idle12] w12=3 -> (w12'=4) & (y2'=0);
+	[snd_req12]  w12=3 -> (w12'=7) & (y2'=0);
+	[time]       w12=3 & y2<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_ack_idle
+	[snd_idle12] w12=4 -> (w12'=4);
+	[rec_ack12]  w12=4 -> (w12'=5);
+	[time]       w12=4 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_idle
+	[snd_idle12] w12=5 -> (w12'=5);
+	[rec_idle12] w12=5 -> (w12'=0) & (y1'=0) & (y2'=0);
+	[snd_req12]  w12=5 -> (w12'=6) & (y2'=0);
+	[snd_ack12]  w12=5 -> (w12'=9) & (y2'=0);
+	[time]       w12=5 & y2<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_idle_req
+	[snd_req12]  w12=6 -> (w12'=6);
+	[rec_idle12] w12=6 -> (w12'=1);
+	[time]       w12=6 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_ack_req
+	[snd_req12] w12=7 -> (w12'=7);
+	[rec_ack12] w12=7 -> (w12'=1);
+	[time]      w12=7 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_req_idle
+	[snd_idle12] w12=8 -> (w12'=8);
+	[rec_req12]  w12=8 -> (w12'=5);
+	[time]       w12=8 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_idle_ack
+	[snd_ack12]  w12=9 -> (w12'=9);
+	[rec_idle12] w12=9 -> (w12'=3);
+	[time]       w12=9 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	
+endmodule
+
+module node1
+	
+	// clock for node1
+	x1 : [0..168];
+	
+	// local state
+	s1 : [0..8];
+	// 0 - root contention
+	// 1 - rec_idle
+	// 2 - rec_req_fast
+	// 3 - rec_req_slow
+	// 4 - rec_idle_fast
+	// 5 - rec_idle_slow
+	// 6 - snd_req
+	// 7- almost_root
+	// 8 - almost_child
+	
+	// added resets to x1 when not considered again until after rest
+	// removed root and child (using almost root and almost child)
+	
+	// root contention immediate state)
+	[snd_idle12] s1=0 -> fast : (s1'=2) & (x1'=0) +  slow : (s1'=3) & (x1'=0);
+	[rec_idle21] s1=0 -> (s1'=1);
+	// rec_idle immediate state)
+	[snd_idle12] s1=1 -> fast : (s1'=4) & (x1'=0) +  slow : (s1'=5) & (x1'=0);
+	[rec_req21]  s1=1 -> (s1'=0);
+	// rec_req_fast
+	[rec_idle21] s1=2 -> (s1'=4);	
+	[snd_ack12]  s1=2 & x1>=rc_fast_min -> (s1'=7) & (x1'=0);
+	[time]       s1=2 & x1<rc_fast_max -> (x1'=min(x1+1,168));
+	// rec_req_slow
+	[rec_idle21] s1=3 -> (s1'=5);
+	[snd_ack12]  s1=3 & x1>=rc_slow_min -> (s1'=7) & (x1'=0);
+	[time]       s1=3 & x1<rc_slow_max -> (x1'=min(x1+1,168));
+	// rec_idle_fast
+	[rec_req21] s1=4 -> (s1'=2);
+	[snd_req12] s1=4 & x1>=rc_fast_min -> (s1'=6) & (x1'=0);
+	[time]      s1=4 & x1<rc_fast_max -> (x1'=min(x1+1,168));
+	// rec_idle_slow
+	[rec_req21] s1=5 -> (s1'=3);
+	[snd_req12] s1=5 & x1>=rc_slow_min -> (s1'=6) & (x1'=0);
+	[time]      s1=5 & x1<rc_slow_max -> (x1'=min(x1+1,168));
+	// snd_req 
+	// do not use x1 until reset (in state 0 or in state 1) so do not need to increase x1
+	// also can set x1 to 0 upon entering this state
+	[rec_req21] s1=6 -> (s1'=0);
+	[rec_ack21] s1=6 -> (s1'=8);
+	[time]      s1=6 -> (s1'=s1);
+	// almost root (immediate) 
+	// loop in final states to remove deadlock
+	[] s1=7 & s2=8 -> (s1'=s1);
+	[] s1=8 & s2=7 -> (s1'=s1);
+	[time] s1=7 -> (s1'=s1);
+	[time] s1=8 -> (s1'=s1);
+	
+endmodule
+
+// construct remaining automata through renaming
+module wire21=wire12[w12=w21, y1=z1, y2=z2, 
+	snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21,
+	rec_req12=rec_req21, rec_idle12=rec_idle21, rec_ack12=rec_ack21]
+endmodule
+module node2=node1[s1=s2, s2=s1, x1=x2, 
+	rec_req21=rec_req12, rec_idle21=rec_idle12, rec_ack21=rec_ack12,
+	snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21]
+endmodule
+
+// reward structures
+// time
+rewards "time"	
+	[time] true : 1;
+endrewards
+// time nodes sending
+rewards "time_sending"
+	[time] (w12>0 | w21>0) : 1;
+endrewards
+
+label "elected" = ((s1=8) & (s2=7)) | ((s1=7) & (s2=8));
\ No newline at end of file
diff --git a/test/functional/parser/prism/leader3.nm b/test/functional/parser/prism/leader3.nm
new file mode 100644
index 000000000..5a8cd34b5
--- /dev/null
+++ b/test/functional/parser/prism/leader3.nm
@@ -0,0 +1,96 @@
+// asynchronous leader election
+// 4 processes
+// gxn/dxp 29/01/01
+
+mdp
+
+const int N = 3; // number of processes
+
+//----------------------------------------------------------------------------------------------------------------------------
+module process1
+	
+	// COUNTER
+	c1 : [0..3-1];
+	
+	// STATES
+	s1 : [0..4];
+	// 0  make choice
+	// 1 have not received neighbours choice
+	// 2 active
+	// 3 inactive
+	// 4 leader
+	
+	// PREFERENCE
+	p1 : [0..1];
+	
+	// VARIABLES FOR SENDING AND RECEIVING
+	receive1 : [0..2];
+	// not received anything
+	// received choice
+	// received counter
+	sent1 : [0..2];
+	// not send anything
+	// sent choice
+	// sent counter
+	
+	// pick value
+	[] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1);
+	
+	// send preference
+	[p12] (s1=1) & (sent1=0) -> (sent1'=1);
+	// receive preference
+	// stay active
+	[p31] (s1=1) & (receive1=0) & !( (p1=0) & (p3=1) ) -> (s1'=2) & (receive1'=1);
+	// become inactive
+	[p31] (s1=1) & (receive1=0) & (p1=0) & (p3=1) -> (s1'=3) & (receive1'=1);
+	
+	// send preference (can now reset preference)
+	[p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0);
+	// send counter (already sent preference)
+	// not received counter yet
+	[c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2);
+	// received counter (pick again)
+	[c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	
+	// receive counter and not sent yet (note in this case do not pass it on as will send own counter)
+	[c31] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2);
+	// receive counter and sent counter
+	// only active process (decide)
+	[c31] (s1=2) & (receive1=1) & (sent1=2) & (c3=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	// other active process (pick again)
+	[c31] (s1=2) & (receive1=1) & (sent1=2) & (c3<N-1) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	
+	// send preference (must have received preference) and can now reset
+	[p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0);
+	// send counter (must have received counter first) and can now reset
+	[c12] (s1=3) & (receive1=2) & (sent1=1) ->  (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	
+	// receive preference
+	[p31] (s1=3) & (receive1=0) -> (p1'=p3) & (receive1'=1);
+	// receive counter
+	[c31] (s1=3) & (receive1=1) & (c3<N-1) -> (c1'=c3+1) & (receive1'=2);
+		
+	// done
+	[done] (s1=4) -> (s1'=s1);
+	// add loop for processes who are inactive
+	[done] (s1=3) -> (s1'=s1);
+
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// construct further stations through renaming
+module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p31=p12,c12=c23,c31=c12,p3=p1,c3=c1] endmodule
+module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p31,p31=p23,c12=c31,c31=c23,p3=p2,c3=c2] endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// reward - expected number of rounds (equals the number of times a process receives a counter)
+rewards "name"
+	[c12] true : 1;
+endrewards
+
+//----------------------------------------------------------------------------------------------------------------------------
+formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0);
+label "elected" = s1=4|s2=4|s3=4;
+
diff --git a/test/functional/parser/prism/leader3_5.pm b/test/functional/parser/prism/leader3_5.pm
new file mode 100644
index 000000000..0703e733d
--- /dev/null
+++ b/test/functional/parser/prism/leader3_5.pm
@@ -0,0 +1,85 @@
+// synchronous leader election protocol  (itai & Rodeh)
+// dxp/gxn 25/01/01
+
+dtmc
+
+// CONSTANTS
+const int N = 3; // number of processes
+const int K = 5; // range of probabilistic choice
+
+// counter module used to count the number of processes that have been read
+// and to know when a process has decided
+module counter
+	
+	// counter (c=i  means process j reading process (i-1)+j next)
+	c : [1..N-1];
+	
+	// reading
+	[read] c<N-1 -> 1:(c'=c+1);
+	// finished reading
+	[read] c=N-1 -> 1:(c'=c);
+	//decide
+	[done] u1|u2|u3 -> 1:(c'=c);
+	// pick again reset counter 
+	[retry] !(u1|u2|u3) -> 1:(c'=1);
+	// loop (when finished to avoid deadlocks)
+	[loop] s1=3 -> 1:(c'=c);
+	
+endmodule
+
+//  processes form a ring and suppose:
+// process 1 reads process 2
+// process 2 reads process 3
+// process 3 reads process 1
+module process1
+	
+	// local state
+	s1 : [0..3];
+	// s1=0 make random choice
+	// s1=1 reading
+	// s1=2 deciding
+	// s1=3 finished
+	
+	// has a unique id so far (initially true)
+	u1 : bool;
+	
+	// value to be sent to next process in the ring (initially sets this to its own value)
+	v1 : [0..K-1];
+	
+	// random choice
+	p1 : [0..K-1];
+	
+	// pick value
+	[pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true);
+	// read
+	[read] s1=1 &  u1 & c<N-1 -> 1:(u1'=(p1!=v2)) & (v1'=v2);
+	[read] s1=1 & !u1 & c<N-1 -> 1:(u1'=false) & (v1'=v2) & (p1'=0);
+	// read and move to decide
+	[read] s1=1 &  u1 & c=N-1 -> 1:(s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0);
+	[read] s1=1 & !u1 & c=N-1 -> 1:(s1'=2) & (u1'=false) & (v1'=0);
+	// deciding
+	// done
+	[done] s1=2 -> 1:(s1'=3) & (u1'=false) & (v1'=0) & (p1'=0);
+	//retry
+	[retry] s1=2 -> 1:(s1'=0) & (u1'=false) & (v1'=0) & (p1'=0);
+	// loop (when finished to avoid deadlocks)
+	[loop] s1=3 -> 1:(s1'=3);
+	
+endmodule
+
+// construct remaining processes through renaming
+module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule
+module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v1 ] endmodule
+
+// expected number of rounds
+rewards "num_rounds"
+	[pick] true : 1;
+endrewards
+
+// labels
+label "elected" = s1=3&s2=3&s3=3;
+
diff --git a/test/functional/parser/prism/two_dice.nm b/test/functional/parser/prism/two_dice.nm
new file mode 100644
index 000000000..778153138
--- /dev/null
+++ b/test/functional/parser/prism/two_dice.nm
@@ -0,0 +1,40 @@
+// sum of two dice as the asynchronous parallel composition of
+// two copies of Knuth's model of a fair die using only fair coins
+
+mdp
+
+module die1
+
+	// local state
+	s1 : [0..7] init 0;
+	// value of the dice
+	d1 : [0..6] init 0;
+
+	[] s1=0 -> 0.5 : (s1'=1) + 0.5 : (s1'=2);
+	[] s1=1 -> 0.5 : (s1'=3) + 0.5 : (s1'=4);
+	[] s1=2 -> 0.5 : (s1'=5) + 0.5 : (s1'=6);
+	[] s1=3 -> 0.5 : (s1'=1) + 0.5 : (s1'=7) & (d1'=1);
+	[] s1=4 -> 0.5 : (s1'=7) & (d1'=2) + 0.5 : (s1'=7) & (d1'=3);
+	[] s1=5 -> 0.5 : (s1'=7) & (d1'=4) + 0.5 : (s1'=7) & (d1'=5);
+	[] s1=6 -> 0.5 : (s1'=2) + 0.5 : (s1'=7) & (d1'=6);
+	[] s1=7 & s2=7 -> 1: (s1'=7);
+endmodule
+
+module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule
+
+rewards "coinflips"
+	[] s1<7 | s2<7 : 1;
+endrewards
+
+label "done" = s1=7 & s2=7;
+label "two" = s1=7 & s2=7 & d1+d2=2;
+label "three" = s1=7 & s2=7 & d1+d2=3;
+label "four" = s1=7 & s2=7 & d1+d2=4;
+label "five" = s1=7 & s2=7 & d1+d2=5;
+label "six" = s1=7 & s2=7 & d1+d2=6;
+label "seven" = s1=7 & s2=7 & d1+d2=7;
+label "eight" = s1=7 & s2=7 & d1+d2=8;
+label "nine" = s1=7 & s2=7 & d1+d2=9;
+label "ten" = s1=7 & s2=7 & d1+d2=10;
+label "eleven" = s1=7 & s2=7 & d1+d2=11;
+label "twelve" = s1=7 & s2=7 & d1+d2=12;
diff --git a/test/functional/parser/prism/wlan0_collide.nm b/test/functional/parser/prism/wlan0_collide.nm
new file mode 100644
index 000000000..1c14704e5
--- /dev/null
+++ b/test/functional/parser/prism/wlan0_collide.nm
@@ -0,0 +1,219 @@
+// WLAN PROTOCOL (two stations)
+// discrete time model
+// gxn/jzs 20/02/02
+
+mdp
+
+// COLLISIONS
+const int COL; // maximum number of collisions
+
+// TIMING CONSTRAINTS
+// we have used the FHSS parameters
+// then scaled by the value of ASLOTTIME
+const int ASLOTTIME = 1;
+const int DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice
+const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice
+const int TRANS_TIME_MAX; // scaling up
+const int TRANS_TIME_MIN = 4; // scaling down
+const int ACK_TO = 6; 
+const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice
+const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice
+// maximum constant used in timing constraints + 1
+const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1;
+
+// CONTENTION WINDOW
+// CWMIN =15 & CWMAX =16
+// this means that MAX_BACKOFF IS 2
+const int MAX_BACKOFF = 0;
+
+//-----------------------------------------------------------------//
+// THE MEDIUM/CHANNEL
+
+// FORMULAE FOR THE CHANNEL
+// channel is busy
+formula busy = c1>0 | c2>0;
+// channel is free
+formula free = c1=0 & c2=0;
+
+module medium
+	
+	// number of collisions
+	col : [0..COL];
+	
+	// medium status 
+	c1 : [0..2];
+	c2 : [0..2];
+	// ci corresponds to messages associated with station i
+	// 0 nothing being sent
+	// 1 being sent correctly
+	// 2 being sent garbled	  
+	
+	// begin sending message and nothing else currently being sent
+	[send1] c1=0 & c2=0 -> (c1'=1);
+	[send2] c2=0 & c1=0 -> (c2'=1);
+	
+	// begin sending message and  something is already being sent
+	// in this case both messages become garbled
+	[send1] c1=0 & c2>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL));
+	[send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL));
+	
+	// finish sending message
+	[finish1] c1>0 -> (c1'=0);
+	[finish2] c2>0 -> (c2'=0);
+
+endmodule
+
+//-----------------------------------------------------------------//
+// STATION 1
+module station1
+	// clock for station 1
+	x1 : [0..TIME_MAX];
+	
+	// local state
+	s1 : [1..12];
+	// 1 sense
+	// 2 wait until free before setting backoff
+	// 3 wait for DIFS then set slot
+	// 4 set backoff 
+	// 5 backoff
+	// 6 wait until free in backoff
+	// 7 wait for DIFS then resume backoff
+	// 8 vulnerable 
+	// 9 transmit
+	// 11 wait for SIFS and then ACK
+	// 10 wait for ACT_TO 
+	// 12 done
+	// BACKOFF
+	// separate into slots
+	slot1 : [0..1]; 
+	backoff1 : [0..15];
+	
+	// BACKOFF COUNTER
+	bc1 : [0..1];
+	// SENSE
+	// let time pass
+	[time] s1=1 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
+	// ready to transmit
+	[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0);
+	// found channel busy so wait until free
+	[] s1=1 & busy -> (s1'=2) & (x1'=0);
+	// WAIT UNTIL FREE BEFORE SETTING BACKOFF
+	// let time pass (no need for the clock x1 to change)
+	[time] s1=2 & busy -> (s1'=2);
+	// find that channel is free so check its free for DIFS before setting backoff
+	[] s1=2 & free -> (s1'=3);
+	// WAIT FOR DIFS THEN SET BACKOFF
+	// let time pass
+	[time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
+	// found channel busy so wait until free
+	[] s1=3 & busy -> (s1'=2) & (x1'=0);
+	// start backoff  first uniformly choose slot
+	// backoff counter 0
+	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF));
+	// SET BACKOFF (no time can pass)
+	// chosen slot now set backoff
+	[] s1=4 -> 1/16 : (s1'=5) & (backoff1'=0 )
+	         + 1/16 : (s1'=5) & (backoff1'=1 )
+	         + 1/16 : (s1'=5) & (backoff1'=2 )
+	         + 1/16 : (s1'=5) & (backoff1'=3 )
+	         + 1/16 : (s1'=5) & (backoff1'=4 )
+	         + 1/16 : (s1'=5) & (backoff1'=5 )
+	         + 1/16 : (s1'=5) & (backoff1'=6 )
+	         + 1/16 : (s1'=5) & (backoff1'=7 )
+	         + 1/16 : (s1'=5) & (backoff1'=8 )
+	         + 1/16 : (s1'=5) & (backoff1'=9 )
+	         + 1/16 : (s1'=5) & (backoff1'=10)
+	         + 1/16 : (s1'=5) & (backoff1'=11)
+	         + 1/16 : (s1'=5) & (backoff1'=12)
+	         + 1/16 : (s1'=5) & (backoff1'=13)
+	         + 1/16 : (s1'=5) & (backoff1'=14)
+	         + 1/16 : (s1'=5) & (backoff1'=15);
+	// BACKOFF
+	// let time pass
+	[time] s1=5 & x1<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX));
+	// decrement backoff
+	[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);	
+	[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);	
+	// finish backoff 
+	[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0);
+	// found channel busy
+	[] s1=5 & busy -> (s1'=6) & (x1'=0);
+	// WAIT UNTIL FREE IN BACKOFF
+	// let time pass (no need for the clock x1 to change)
+	[time] s1=6 & busy -> (s1'=6);
+	// find that channel is free
+	[] s1=6 & free -> (s1'=7);
+	
+	// WAIT FOR DIFS THEN RESUME BACKOFF
+	// let time pass
+	[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
+	// resume backoff (start again from previous backoff)
+	[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0);
+	// found channel busy
+	[] s1=7 & busy -> (s1'=6) & (x1'=0);
+	
+	// VULNERABLE
+	// let time pass
+	[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX));
+	// move to transmit
+	[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
+	// TRANSMIT
+	// let time pass
+	[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
+	// finish transmission successful	
+	[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
+	// finish transmission garbled
+	[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
+	// WAIT FOR SIFS THEN WAIT FOR ACK
+	
+	// WAIT FOR SIFS i.e. c1=0
+	// check channel and busy: go into backoff
+	[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2);
+	// check channel and free: let time pass
+	[time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
+	// let time pass
+	// following guard is always false as SIFS=1
+	// [time] s1=10 & c1=0 & x1>0 & x1<SIFS -> (x1'=min(x1+1,TIME_MAX));
+	// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
+	[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0);
+	
+	// WAIT FOR ACK i.e. c1=1
+	// let time pass
+	[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX));
+	// get acknowledgement so packet sent correctly and move to done
+	[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
+	
+	// WAIT FOR ACK_TO
+	// check channel and busy: go into backoff
+	[] s1=11 & x1=0 & busy -> (s1'=2);
+	// check channel and free: let time pass
+	[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
+	// let time pass
+	[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
+	// no acknowledgement (go to backoff waiting DIFS first)
+	[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
+		
+	// DONE
+	[time] s1=12 -> (s1'=12);
+
+endmodule	
+
+// ---------------------------------------------------------------------------- //
+// STATION 2 (rename STATION 1)
+module 
+station2=station1[x1=x2, 
+                  s1=s2,
+				  s2=s1,
+				  c1=c2,
+				  c2=c1, 
+				  slot1=slot2, 
+				  backoff1=backoff2, 
+				  bc1=bc2, 
+				  send1=send2, 
+				  finish1=finish2] 
+endmodule
+// ---------------------------------------------------------------------------- //
+
+label "twoCollisions" = col=2;
+label "fourCollisions" = col=4;
+label "sixCollisions" = col=6;
\ No newline at end of file