Put PTA files in main examples dir.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2144 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago · 745794c57a
81 changed files with 9368 additions and 0 deletions
--- a/prism-examples/pta/args-abovebelow
+++ b/prism-examples/pta/args-abovebelow
@ -0,0 +1,14 @@
+# no pre (or as little as poss)
+-aroptions nopre,noopt
+-aroptions nopre,opt
+-aroptions nopre,opt,above
+
+-aroptions noprob1,noopt
+-aroptions noprob1,opt
+-aroptions noprob1,opt,above
+
+# pre
+-aroptions pre,noopt
+-aroptions pre,opt
+-aroptions pre,opt,above
+
--- a/prism-examples/pta/brp/README
+++ b/prism-examples/pta/brp/README
@ -0,0 +1,27 @@
+This case study is based on the bounded retransmission protocol (BRP) [HSV94], a variant of the alternating bit protocol.
+
+Its parameters are:
+
+  N = number of chunks in a file
+  MAX = maximum number of retransmissions
+  TD = the transition delay
+  TIME_OUT = the time the sender waits before timing out
+
+TIME_OUT should be greater than the time to send and receive an ack (i.e. greater than 2*TD)
+
+For more information, see the untimed version: http://www.prismmodelchecker.org/casestudies/brp.php
+
+The PTA extension is based on that used in [HH09]
+
+=====================================================================================
+
+[HSV94]
+L. Helmink, M. Sellink and F Vaandrager
+Proof checking a data link protocol
+In Proc. Types for Proofs and Programs (TYPES'93), LNCS 806, pp 127-165, Springer-Verlag, 1994
+
+[HH09]
+A. Hartmanns and H. Hermanns
+A Modest Approach to Checking Probabilistic Timed Automata
+Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09), IEEE, 2009
+
--- a/prism-examples/pta/brp/auto
+++ b/prism-examples/pta/brp/auto
@ -0,0 +1,7 @@
+#!/bin/csh
+
+foreach N (16 32 64)
+	foreach MAX (2 3 4 5)
+		prism brp.pm brp.pctl -const N=$N,MAX=$MAX,TD=2,TIME_OUT=5 -fixdl
+	end
+end
--- a/prism-examples/pta/brp/brp.pctl
+++ b/prism-examples/pta/brp/brp.pctl
@ -0,0 +1,22 @@
+// properties taken from [D'AJJL01]
+
+// property A
+P=? [ true U srep=1 & rrep=3 & recv ];
+
+// property B
+P=? [ true U srep=3 & !(rrep=3) & recv ];
+
+// property 1
+P=? [ true U s=5 ];
+
+// property 2
+P=? [ true U s=5 & srep=2 ];
+
+// property 3
+P=? [ true U s=5 & srep=1 & i>8 ];
+
+// property 4
+P=? [ true U !(srep=0) & !recv ];
+
+// rewards
+R=? [ F "deadlock" ];
--- a/prism-examples/pta/brp/brp.pm
+++ b/prism-examples/pta/brp/brp.pm
@ -0,0 +1,150 @@
+// bounded retransmission protocol [D'AJJL01]
+// gxn/dxp 23/05/2001
+
+pta
+
+// number of chunks
+const int N;
+// maximum number of retransmissions
+const int MAX;
+// max time to send a message (transition delay)
+const int TD;
+// time out limit (greater than TD+TD - the max time to send a message and receive an ack)
+const int TIME_OUT = 2*TD + 1;
+
+module sender
+
+	// clock of the sender
+	x : clock;
+
+	s : [0..6];
+	// 0 idle
+	// 1 next_frame	
+	// 2 wait_ack
+	// 3 retransmit
+	// 4 success
+	// 5 error
+	// 6 wait sync
+	srep : [0..3];
+	// 0 bottom
+	// 1 not ok (nok)
+	// 2 do not know (dk)
+	// 3 ok (ok)
+	nrtr : [0..MAX];
+	i : [0..N];
+	bs : bool;
+	s_ab : bool;
+	fs : bool;
+	ls : bool;
+
+	invariant
+		(s=2 => x<=TIME_OUT) // only wait until timeout
+	endinvariant
+	
+	// idle
+	[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
+	// next_frame
+	[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0) & (x'=0);
+	// wait_ack
+	[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
+	[] (s=2) & x=TIME_OUT -> (s'=3); // time out
+	// retransmit
+	[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1) & (x'=0);
+	[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
+	[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
+	// success
+	[] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
+	[] (s=4) & (i=N) -> (s'=0) & (srep'=3);
+	// error
+	[SyncWait] (s=5) -> (s'=6); 
+	// wait sync
+	[SyncWait] (s=6) -> (s'=0) & (s_ab'=false); 
+	
+endmodule
+
+module receiver
+
+	r : [0..5];
+	// 0 new_file
+	// 1 fst_safe
+	// 2 frame_received
+	// 3 frame_reported
+	// 4 idle
+	// 5 resync
+	rrep : [0..4];
+	// 0 bottom
+	// 1 fst
+	// 2 inc
+	// 3 ok
+	// 4 nok
+	fr : bool;
+	lr : bool;
+	br : bool;
+	r_ab : bool;
+	recv : bool;
+	
+	
+	// new_file
+	[SyncWait] (r=0) -> (r'=0);
+	[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+	// fst_safe_frame
+	[] (r=1) -> (r'=2) & (r_ab'=br);
+	// frame_received
+	[] (r=2) & (r_ab=br) & (fr=true) & (lr=false)  -> (r'=3) & (rrep'=1);
+	[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
+	[] (r=2) & (r_ab=br) & (fr=false) & (lr=true)  -> (r'=3) & (rrep'=3);
+	[aA] (r=2) & !(r_ab=br) -> (r'=4);  
+	// frame_reported
+	[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
+	// idle
+	[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+	[SyncWait] (r=4) & (ls=true) -> (r'=5);
+	[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
+	// resync
+	[SyncWait] (r=5) -> (r'=0) & (rrep'=0);
+	
+endmodule
+	
+module checker // prevents more than one frame being set
+
+	T : bool;
+	
+	[NewFile] (T=false) -> (T'=true);
+	
+endmodule
+
+module	channelK
+
+	xK : clock;
+	k : [0..1];
+
+	invariant
+		(k=1 => xK<=TD)
+	endinvariant
+	
+	// idle
+	[aF] (k=0) -> 0.98 : (k'=1) & (xK'=0) + 0.02 : (k'=0) & (xK'=0);
+	// sending
+	[aG] (k=1) & xK<=TD -> (k'=0) & (xK'=0);
+	
+endmodule
+
+module	channelL
+
+	xL : clock;
+	l : [0..1];
+
+	invariant
+		(l=1 => xL<=TD)
+	endinvariant
+	
+	// idle
+	[aA] (l=0) -> 0.99 : (l'=1) & (xL'=0) + 0.02 : (l'=0) & (xL'=0);
+	// sending
+	[aB] (l=1) & xL<=TD -> (l'=0) & (xL'=0);
+
+endmodule
+
+rewards
+	[aF] i=1 : 1;
+endrewards
--- a/prism-examples/pta/csma/abst/args
+++ b/prism-examples/pta/csma/abst/args
@ -0,0 +1 @@
+-aroptions refine=all,nopre
--- a/prism-examples/pta/csma/abst/auto
+++ b/prism-examples/pta/csma/abst/auto
@ -0,0 +1,7 @@
+#!/bin/csh
+
+prism csma.nm -const bmax=1 eventually.pctl -aroptions refine=all,nopre,opt
+
+prism csma.nm -const bmax=1 deadline.pctl -const T=1000 -aroptions refine=all,nopre,opt
+prism csma.nm -const bmax=1 deadline.pctl -const T=2000 -aroptions refine=all,nopre,opt
+prism csma.nm -const bmax=1 deadline.pctl -const T=3000 -aroptions refine=all,nopre,opt
--- a/prism-examples/pta/csma/abst/csma.nm
+++ b/prism-examples/pta/csma/abst/csma.nm
@ -0,0 +1,139 @@
+// CSMA/CD protocol - probabilistic version of kronos model adapted to model a single station
+// gxn/dxp 04/12/01
+
+pta
+
+// note made changes since cannot have strict inequalities
+// in digital clocks approach and suppose a station only sends one message
+
+//----------------------------------------------------------------------------------------------------------------------------
+// actual parameters
+const int bmax; // exponential backoff limit
+const int slot=2*sigma; // length of slot
+const int sigma=26;
+const int lambda=808;
+
+//----------------------------------------------------------------------------------------------------------------------------
+// the bus
+module bus
+	
+	b : [0..2];
+	// b=0 - idle
+	// b=1 - active
+	// b=2 - collision
+	
+	// clock of bus
+	y : clock;
+
+	invariant
+		(b=0 => true) &
+		(b=1 => true) &
+		(b=2 => y<=sigma)
+	endinvariant
+	
+	// station starts sending
+	[send1] (b=0) -> (b'=1) & (y'=0); // no message being sent
+	[send2] (b=0) -> (b'=1) & (y'=0); // no message being sent
+
+	[send1] (b=1) & (y<sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
+	[send2] (b=1) & (y<sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
+	
+	// message being sent
+	[busy1]  (b=1) & (y>=sigma) -> (b'=1); 
+	[busy2]  (b=1) & (y>=sigma) -> (b'=1); 
+	
+	// station finishes
+	[end1] (b=1) -> (b'=0) & (y'=0);
+	[end2] (b=1) -> (b'=0) & (y'=0);
+	
+	// collision detected
+	[cd] (b=2) & (y<=sigma) -> (b'=0) & (y'=0);
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+// model of first sender
+module station1
+	
+	// LOCAL STATE
+	s1 : [0..4];
+	// s1=0 - initial state
+	// s1=1 - transmit
+	// s1=2 - collision (set backoff)
+	// s1=3 - wait (bus busy)
+	// s1=4 -done (since sending only one message)
+	// LOCAL CLOCK
+	x1 : clock;
+	// COLLISION COUNTER
+	cd1 : [0..bmax];
+
+	invariant
+		(s1=0 => x1=0) &
+		(s1=1 => x1<=lambda) &
+		(s1=2 => x1=0) &
+		(s1=3 => x1<=pow(2, cd1)*slot) &
+		(s1=4 => true)
+	endinvariant
+
+	// start sending
+	[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending
+	[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(bmax,cd1+1)); // detects channel is busy so go into backoff
+	
+	// transmitting
+	[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished
+	[cd]   (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(bmax,cd1+1)); // collision detected
+	
+	// set backoff (no time can pass in this state)
+	// first retransmission
+	[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (x1'=0*slot) 
+	                 + 1/2 : (s1'=3) & (x1'=1*slot);
+	// second retransmission
+	[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (x1'=0*slot)
+	                 + 1/4 : (s1'=3) & (x1'=1*slot)
+	                 + 1/4 : (s1'=3) & (x1'=2*slot)
+	                 + 1/4 : (s1'=3) & (x1'=3*slot);
+	// thrid retransmission
+	[] s1=2 & cd1=3 -> 1/8 : (s1'=3) & (x1'=0*slot)
+	                 + 1/8 : (s1'=3) & (x1'=1*slot)
+	                 + 1/8 : (s1'=3) & (x1'=2*slot)
+	                 + 1/8 : (s1'=3) & (x1'=3*slot)
+	                 + 1/8 : (s1'=3) & (x1'=4*slot)
+	                 + 1/8 : (s1'=3) & (x1'=5*slot)
+	                 + 1/8 : (s1'=3) & (x1'=6*slot)
+	                 + 1/8 : (s1'=3) & (x1'=7*slot);
+	// fourth retransmission 
+	[] s1=2 & cd1=4 -> 1/16 : (s1'=3) & (x1'=0*slot)
+	                 + 1/16 : (s1'=3) & (x1'=1*slot)
+	                 + 1/16 : (s1'=3) & (x1'=2*slot)
+	                 + 1/16 : (s1'=3) & (x1'=3*slot)
+	                 + 1/16 : (s1'=3) & (x1'=4*slot)
+	                 + 1/16 : (s1'=3) & (x1'=5*slot)
+	                 + 1/16 : (s1'=3) & (x1'=6*slot)
+	                 + 1/16 : (s1'=3) & (x1'=7*slot)
+	                 + 1/16 : (s1'=3) & (x1'=8*slot)
+	                 + 1/16 : (s1'=3) & (x1'=9*slot)
+	                 + 1/16 : (s1'=3) & (x1'=10*slot)
+	                 + 1/16 : (s1'=3) & (x1'=11*slot)
+	                 + 1/16 : (s1'=3) & (x1'=12*slot)
+	                 + 1/16 : (s1'=3) & (x1'=13*slot)
+	                 + 1/16 : (s1'=3) & (x1'=14*slot)
+	                 + 1/16 : (s1'=3) & (x1'=15*slot);
+	
+	// finished backoff
+	[send1] (s1=3) & (x1=pow(2, cd1)*slot) -> (s1'=1) & (x1'=0); // channel free
+	[busy1] (s1=3) & (x1=pow(2, cd1)*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(bmax,cd1+1)); // channel busy
+	
+	// once finished nothing matters
+	[done] (s1=4) -> true;
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// construct further stations through renaming
+module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+// LABELS
+
+label "done" = s1=4 & s2=4;
--- a/prism-examples/pta/csma/abst/csma1-digital.nm
+++ b/prism-examples/pta/csma/abst/csma1-digital.nm
@ -0,0 +1,100 @@
+// CSMA/CD protocol - probabilistic version of kronos model adapted to model a single station
+// gxn/dxp 04/12/01
+
+nondeterministic
+
+// note made changes since cannot have strict inequalities
+// in digital clocks approach and suppose a station only sends one message
+
+//----------------------------------------------------------------------------------------------------------------------------
+// actual parameters
+const int K=1; // exponential backoff limit
+const int slot=2*sigma; // length of slot
+const int M=floor(pow(2, K)); // max number of slots to wait
+const int sigma=26;
+const int lambda=808;
+
+//----------------------------------------------------------------------------------------------------------------------------
+// the bus
+module bus
+	
+	b : [0..2];
+	// b=0 - idle
+	// b=1 - active
+	// b=2 - collision
+	
+	// clock of bus
+	y : [0..sigma+1];
+	
+	// station starts sending
+	[send1] (b=0) -> (b'=1) & (y'=0); // no message being sent
+	[send2] (b=0) -> (b'=1) & (y'=0); // no message being sent
+	[send1] (b=1) & (y<=sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
+	[send2] (b=1) & (y<=sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
+	
+	// message being sent
+	[busy1]  (b=1) & (y>=sigma) -> (b'=1); 
+	[busy2]  (b=1) & (y>=sigma) -> (b'=1); 
+	
+	// station finishes
+	[end1] (b=1) -> (b'=0) & (y'=0);
+	[end2] (b=1) -> (b'=0) & (y'=0);
+	
+	// collision detected
+	[cd] (b=2) & (y<=sigma) -> (b'=0) & (y'=0);
+	
+	// time transitions
+	[time] (b=0) -> (y'=min(y+1,sigma+1)); // value of y does not matter in state 0
+	[time] (b=1) -> (y'=min(y+1,sigma+1)); // no invariant in state 1
+	[time] (b=2) & (y<sigma) -> (y'=min(y+1,sigma+1)); // invariant in state 2
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+// model of first sender
+module station1
+	
+	// LOCAL STATE
+	s1 : [0..4];
+	// s1=0 - initial state
+	// s1=1 - transmit
+	// s1=2 - collision (set backoff)
+	// s1=3 - wait (bus busy)
+	// s1=4 -done (since sending only one message)
+	// LOCAL CLOCK
+	x1 : [0..max(lambda,M*slot)+1];
+	// 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
+	
+	// set backoff (no time can pass in this state)
+	// first retransmission
+	[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (x1'=0*slot) 
+	                 + 1/2 : (s1'=3) & (x1'=1*slot);
+	
+	// wait until backoff counter reaches 0 then send again
+	[time] (s1=3) & (cd1=1) & (x1<2*slot) -> (x1'=x1+1); // let time pass (in slot)
+	
+	// finished backoff
+	[send1] (s1=3) & cd1=1 & (x1=2*slot)  -> (s1'=1) & (x1'=0); // channel free
+	[busy1] (s1=3) & cd1=1 & (x1=2*slot)  -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
+	
+	// finished
+	[done] (s1=4) -> true;
+	[time] (s1=4) -> (x1'=min(x1+1,max(lambda,M*slot)+1));
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// construct further stations through renaming
+module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule
+
--- a/prism-examples/pta/csma/abst/csma1-test.nm
+++ b/prism-examples/pta/csma/abst/csma1-test.nm
@ -0,0 +1,106 @@
+// CSMA/CD protocol - probabilistic version of kronos model adapted to model a single station
+// gxn/dxp 04/12/01
+
+pta
+
+// note made changes since cannot have strict inequalities
+// in digital clocks approach and suppose a station only sends one message
+
+//----------------------------------------------------------------------------------------------------------------------------
+// actual parameters
+const int K=1; // exponential backoff limit
+const int slot=2*sigma; // length of slot
+const int sigma=26;
+const int lambda=808;
+
+//----------------------------------------------------------------------------------------------------------------------------
+// the bus
+module bus
+	
+	b : [0..2];
+	// b=0 - idle
+	// b=1 - active
+	// b=2 - collision
+	
+	// clock of bus
+	y : clock;
+
+	invariant
+		(b=0 => true) &
+		(b=1 => true) &
+		(b=2 => y<=sigma)
+	endinvariant
+	
+	// station starts sending
+	[send1] (b=0) -> (b'=1) & (y'=0); // no message being sent
+	[send2] (b=0) -> (b'=1) & (y'=0); // no message being sent
+	[send1] (b=1) & (y<=sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
+	[send2] (b=1) & (y<=sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
+	
+	// message being sent
+	[busy1]  (b=1) & (y>=sigma) -> (b'=1); 
+	[busy2]  (b=1) & (y>=sigma) -> (b'=1); 
+	
+	// station finishes
+	[end1] (b=1) -> (b'=0) & (y'=0);
+	[end2] (b=1) -> (b'=0) & (y'=0);
+	
+	// collision detected
+	[cd] (b=2) & (y<=sigma) -> (b'=0) & (y'=0);
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+// model of first sender
+module station1
+	
+	// LOCAL STATE
+	s1 : [0..4];
+	// s1=0 - initial state
+	// s1=1 - transmit
+	// s1=2 - collision (set backoff)
+	// s1=3 - wait (bus busy)
+	// s1=4 -done (since sending only one message)
+
+	// LOCAL CLOCK
+	x1 : clock;
+
+	invariant
+		(s1=0 => x1=0) &
+		(s1=1 => x1<=lambda) &
+		(s1=2 => x1<=0) &
+		(s1=3 => x1<=104) &
+		(s1=4 => true)
+	endinvariant
+
+	// start sending
+	[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending
+	[busy1] (s1=0) -> (s1'=2) & (x1'=0); // detects channel is busy so go into backoff
+	
+	// transmitting
+	[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished
+	[cd]   (s1=1) -> (s1'=2) & (x1'=0); // collision detected
+	
+	// set backoff (no time can pass in this state)
+	// first retransmission
+	[] s1=2 -> 1/2 : (s1'=3) & (x1'=0) 
+	                          + 1/2 : (s1'=3) & (x1'=52);
+	
+	// finished backoff
+	[send1] s1=3 & x1>=104 -> (s1'=1) & (x1'=0); // channel free
+	[busy1] s1=3 & x1>=104 -> (s1'=2) & (x1'=0); // channel busy
+	
+	// once finished nothing matters
+	[done] s1=4 -> true;
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// construct further stations through renaming
+module station2=station1[s1=s2,x1=x2,send1=send2,busy1=busy2,end1=end2] endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+// LABELS
+
+label "done" = s1=4 & s2=4;
--- a/prism-examples/pta/csma/abst/csma2-digital.nm
+++ b/prism-examples/pta/csma/abst/csma2-digital.nm
@ -0,0 +1,109 @@
+// CSMA/CD protocol - probabilistic version of kronos model adapted to model a single station
+// gxn/dxp 04/12/01
+
+nondeterministic
+
+// note made changes since cannot have strict inequalities
+// in digital clocks approach and suppose a station only sends one message
+
+//----------------------------------------------------------------------------------------------------------------------------
+// actual parameters
+const int K=2; // exponential backoff limit
+const int slot=2*sigma; // length of slot
+const int M=floor(pow(2, K)); // max number of slots to wait
+const int sigma=26;
+const int lambda=808;
+
+//----------------------------------------------------------------------------------------------------------------------------
+// the bus
+module bus
+	
+	b : [0..2];
+	// b=0 - idle
+	// b=1 - active
+	// b=2 - collision
+	
+	// clock of bus
+	y : [0..sigma+1];
+	
+	// station starts sending
+	[send1] (b=0) -> (b'=1) & (y'=0); // no message being sent
+	[send2] (b=0) -> (b'=1) & (y'=0); // no message being sent
+	[send1] (b=1) & (y<=sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
+	[send2] (b=1) & (y<=sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
+	
+	// message being sent
+	[busy1]  (b=1) & (y>=sigma) -> (b'=1); 
+	[busy2]  (b=1) & (y>=sigma) -> (b'=1); 
+	
+	// station finishes
+	[end1] (b=1) -> (b'=0) & (y'=0);
+	[end2] (b=1) -> (b'=0) & (y'=0);
+	
+	// collision detected
+	[cd] (b=2) & (y<=sigma) -> (b'=0) & (y'=0);
+	
+	// time transitions
+	[time] (b=0) -> (y'=min(y+1,sigma+1)); // value of y does not matter in state 0
+	[time] (b=1) -> (y'=min(y+1,sigma+1)); // no invariant in state 1
+	[time] (b=2) & (y<sigma) -> (y'=min(y+1,sigma+1)); // invariant in state 2
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+// model of first sender
+module station1
+	
+	// LOCAL STATE
+	s1 : [0..4];
+	// s1=0 - initial state
+	// s1=1 - transmit
+	// s1=2 - collision (set backoff)
+	// s1=3 - wait (bus busy)
+	// s1=4 -done (since sending only one message)
+	// LOCAL CLOCK
+	x1 : [0..max(lambda,M*slot)+1];
+	// 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
+	
+	// set backoff (no time can pass in this state)
+	// first retransmission
+	[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (x1'=0*slot) 
+	                 + 1/2 : (s1'=3) & (x1'=1*slot);
+	// second retransmission
+	[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (x1'=0*slot)
+	                 + 1/4 : (s1'=3) & (x1'=1*slot)
+	                 + 1/4 : (s1'=3) & (x1'=2*slot)
+	                 + 1/4 : (s1'=3) & (x1'=3*slot);
+	
+	// wait until backoff counter reaches 0 then send again
+	[time] (s1=3) & (cd1=1) & (x1<2*slot) -> (x1'=x1+1); // let time pass (in slot)
+	[time] (s1=3) & (cd1=2) & (x1<4*slot) -> (x1'=x1+1); // let time pass (in slot)
+	
+	// finished backoff
+	[send1] (s1=3) & cd1=1 & (x1=2*slot)  -> (s1'=1) & (x1'=0); // channel free
+	[busy1] (s1=3) & cd1=1 & (x1=2*slot)  -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
+	
+	[send1] (s1=3) & cd1=2 & (x1=4*slot)  -> (s1'=1) & (x1'=0); // channel free
+	[busy1] (s1=3) & cd1=2 & (x1=4*slot)  -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
+	
+	// finished
+	[done] (s1=4) -> true;
+	[time] (s1=4) -> (x1'=min(x1+1,max(lambda,M*slot)+1));
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// construct further stations through renaming
+module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule
+
--- a/prism-examples/pta/csma/abst/csma3-digital.nm
+++ b/prism-examples/pta/csma/abst/csma3-digital.nm
@ -0,0 +1,122 @@
+// CSMA/CD protocol - probabilistic version of kronos model adapted to model a single station
+// gxn/dxp 04/12/01
+
+nondeterministic
+
+// note made changes since cannot have strict inequalities
+// in digital clocks approach and suppose a station only sends one message
+
+//----------------------------------------------------------------------------------------------------------------------------
+// actual parameters
+const int K=3; // exponential backoff limit
+const int slot=2*sigma; // length of slot
+const int M=floor(pow(2, K)); // max number of slots to wait
+const int sigma=26;
+const int lambda=808;
+
+//----------------------------------------------------------------------------------------------------------------------------
+// the bus
+module bus
+	
+	b : [0..2];
+	// b=0 - idle
+	// b=1 - active
+	// b=2 - collision
+	
+	// clock of bus
+	y : [0..sigma+1];
+	
+	// station starts sending
+	[send1] (b=0) -> (b'=1) & (y'=0); // no message being sent
+	[send2] (b=0) -> (b'=1) & (y'=0); // no message being sent
+	[send1] (b=1) & (y<sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
+	[send2] (b=1) & (y<sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
+	
+	// message being sent
+	[busy1]  (b=1) & (y>=sigma) -> (b'=1); 
+	[busy2]  (b=1) & (y>=sigma) -> (b'=1); 
+	
+	// station finishes
+	[end1] (b=1) -> (b'=0) & (y'=0);
+	[end2] (b=1) -> (b'=0) & (y'=0);
+	
+	// collision detected
+	[cd] (b=2) & (y<=sigma) -> (b'=0) & (y'=0);
+	
+	// time transitions
+	[time] (b=0) -> (y'=min(y+1,sigma+1)); // value of y does not matter in state 0
+	[time] (b=1) -> (y'=min(y+1,sigma+1)); // no invariant in state 1
+	[time] (b=2) & (y<sigma) -> (y'=min(y+1,sigma+1)); // invariant in state 2
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+// model of first sender
+module station1
+	
+	// LOCAL STATE
+	s1 : [0..4];
+	// s1=0 - initial state
+	// s1=1 - transmit
+	// s1=2 - collision (set backoff)
+	// s1=3 - wait (bus busy)
+	// s1=4 -done (since sending only one message)
+	// LOCAL CLOCK
+	x1 : [0..max(lambda,M*slot)+1];
+	// 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
+	
+	// set backoff (no time can pass in this state)
+	// first retransmission
+	[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (x1'=0*slot) 
+	                 + 1/2 : (s1'=3) & (x1'=1*slot);
+	// second retransmission
+	[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (x1'=0*slot)
+	                 + 1/4 : (s1'=3) & (x1'=1*slot)
+	                 + 1/4 : (s1'=3) & (x1'=2*slot)
+	                 + 1/4 : (s1'=3) & (x1'=3*slot);
+	// thrid retransmission
+	[] s1=2 & cd1=3 -> 1/8 : (s1'=3) & (x1'=0*slot)
+	                 + 1/8 : (s1'=3) & (x1'=1*slot)
+	                 + 1/8 : (s1'=3) & (x1'=2*slot)
+	                 + 1/8 : (s1'=3) & (x1'=3*slot)
+	                 + 1/8 : (s1'=3) & (x1'=4*slot)
+	                 + 1/8 : (s1'=3) & (x1'=5*slot)
+	                 + 1/8 : (s1'=3) & (x1'=6*slot)
+	                 + 1/8 : (s1'=3) & (x1'=7*slot);
+	
+	// wait until backoff counter reaches 0 then send again
+	[time] (s1=3) & (cd1=1) & (x1<2*slot) -> (x1'=x1+1); // let time pass (in slot)
+	[time] (s1=3) & (cd1=2) & (x1<4*slot) -> (x1'=x1+1); // let time pass (in slot)
+	[time] (s1=3) & (cd1=3) & (x1<8*slot) -> (x1'=x1+1); // let time pass (in slot)
+	
+	// finished backoff
+	[send1] (s1=3) & cd1=1 & (x1=2*slot)  -> (s1'=1) & (x1'=0); // channel free
+	[busy1] (s1=3) & cd1=1 & (x1=2*slot)  -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
+	
+	[send1] (s1=3) & cd1=2 & (x1=4*slot)  -> (s1'=1) & (x1'=0); // channel free
+	[busy1] (s1=3) & cd1=2 & (x1=4*slot)  -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
+	
+	[send1] (s1=3) & cd1=3 & (x1=8*slot)  -> (s1'=1) & (x1'=0); // channel free
+	[busy1] (s1=3) & cd1=3 & (x1=8*slot)  -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
+	
+	// finished
+	[done] (s1=4) -> true;
+	[time] (s1=4) -> (x1'=min(x1+1,max(lambda,M*slot)+1));
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// construct further stations through renaming
+module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule
+
--- a/prism-examples/pta/csma/abst/csma4-digital.nm
+++ b/prism-examples/pta/csma/abst/csma4-digital.nm
@ -0,0 +1,139 @@
+// CSMA/CD protocol - probabilistic version of kronos model adapted to model a single station
+// gxn/dxp 04/12/01
+
+nondeterministic
+
+// note made changes since cannot have strict inequalities
+// in digital clocks approach and suppose a station only sends one message
+
+// actual parameters
+const int K=4; // exponential backoff limit
+const int slot=2*sigma; // length of slot
+const int M=floor(pow(2, K)); // max number of slots to wait
+const int sigma=26;
+const int lambda=808;
+
+//----------------------------------------------------------------------------------------------------------------------------
+// the bus
+module bus
+	
+	b : [0..2];
+	// b=0 - idle
+	// b=1 - active
+	// b=2 - collision
+	
+	// clock of bus
+	y : [0..sigma+1];
+	
+	// station starts sending
+	[send1] (b=0) -> (b'=1) & (y'=0); // no message being sent
+	[send2] (b=0) -> (b'=1) & (y'=0); // no message being sent
+	[send1] (b=1) & (y<sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
+	[send2] (b=1) & (y<sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
+	
+	// message being sent
+	[busy1]  (b=1) & (y>=sigma) -> (b'=1); 
+	[busy2]  (b=1) & (y>=sigma) -> (b'=1); 
+	
+	// station finishes
+	[end1] (b=1) -> (b'=0) & (y'=0);
+	[end2] (b=1) -> (b'=0) & (y'=0);
+	
+	// collision detected
+	[cd] (b=2) & (y<=sigma) -> (b'=0) & (y'=0);
+	
+	// time transitions
+	[time] (b=0) -> (y'=min(y+1,sigma+1)); // value of y does not matter in state 0
+	[time] (b=1) -> (y'=min(y+1,sigma+1)); // no invariant in state 1
+	[time] (b=2) & (y<sigma) -> (y'=min(y+1,sigma+1)); // invariant in state 2
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+// model of first sender
+module station1
+	
+	// LOCAL STATE
+	s1 : [0..4];
+	// s1=0 - initial state
+	// s1=1 - transmit
+	// s1=2 - collision (set backoff)
+	// s1=3 - wait (bus busy)
+	// s1=4 -done (since sending only one message)
+	// LOCAL CLOCK
+	x1 : [0..max(lambda,M*slot)+1];
+	// 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
+	
+	// set backoff (no time can pass in this state)
+	// first retransmission
+	[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (x1'=0*slot) 
+	                 + 1/2 : (s1'=3) & (x1'=1*slot);
+	// second retransmission
+	[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (x1'=0*slot)
+	                 + 1/4 : (s1'=3) & (x1'=1*slot)
+	                 + 1/4 : (s1'=3) & (x1'=2*slot)
+	                 + 1/4 : (s1'=3) & (x1'=3*slot);
+	// thrid retransmission
+	[] s1=2 & cd1=3 -> 1/8 : (s1'=3) & (x1'=0*slot)
+	                 + 1/8 : (s1'=3) & (x1'=1*slot)
+	                 + 1/8 : (s1'=3) & (x1'=2*slot)
+	                 + 1/8 : (s1'=3) & (x1'=3*slot)
+	                 + 1/8 : (s1'=3) & (x1'=4*slot)
+	                 + 1/8 : (s1'=3) & (x1'=5*slot)
+	                 + 1/8 : (s1'=3) & (x1'=6*slot)
+	                 + 1/8 : (s1'=3) & (x1'=7*slot);
+	// fourth retransmission 
+	[] s1=2 & cd1=4 -> 1/16 : (s1'=3) & (x1'=0*slot)
+	                 + 1/16 : (s1'=3) & (x1'=1*slot)
+	                 + 1/16 : (s1'=3) & (x1'=2*slot)
+	                 + 1/16 : (s1'=3) & (x1'=3*slot)
+	                 + 1/16 : (s1'=3) & (x1'=4*slot)
+	                 + 1/16 : (s1'=3) & (x1'=5*slot)
+	                 + 1/16 : (s1'=3) & (x1'=6*slot)
+	                 + 1/16 : (s1'=3) & (x1'=7*slot)
+	                 + 1/16 : (s1'=3) & (x1'=8*slot)
+	                 + 1/16 : (s1'=3) & (x1'=9*slot)
+	                 + 1/16 : (s1'=3) & (x1'=10*slot)
+	                 + 1/16 : (s1'=3) & (x1'=11*slot)
+	                 + 1/16 : (s1'=3) & (x1'=12*slot)
+	                 + 1/16 : (s1'=3) & (x1'=13*slot)
+	                 + 1/16 : (s1'=3) & (x1'=14*slot)
+	                 + 1/16 : (s1'=3) & (x1'=15*slot);
+	
+	// wait until backoff counter reaches 0 then send again
+	[time] (s1=3) & (cd1=1) & (x1<2*slot) -> (x1'=x1+1); // let time pass (in slot)
+	[time] (s1=3) & (cd1=2) & (x1<4*slot) -> (x1'=x1+1); // let time pass (in slot)
+	[time] (s1=3) & (cd1=3) & (x1<8*slot) -> (x1'=x1+1); // let time pass (in slot)
+	[time] (s1=3) & (cd1=4) & (x1<16*slot) -> (x1'=x1+1); // let time pass (in slot)
+	
+	// finished backoff
+	[send1] (s1=3) & cd1=1 & (x1=2*slot)  -> (s1'=1) & (x1'=0); // channel free
+	[busy1] (s1=3) & cd1=1 & (x1=2*slot)  -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
+	[send1] (s1=3) & cd1=2 & (x1=4*slot)  -> (s1'=1) & (x1'=0); // channel free
+	[busy1] (s1=3) & cd1=2 & (x1=4*slot)  -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
+	[send1] (s1=3) & cd1=3 & (x1=8*slot)  -> (s1'=1) & (x1'=0); // channel free
+	[busy1] (s1=3) & cd1=3 & (x1=8*slot)  -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
+	[send1] (s1=3) & cd1=4 & (x1=16*slot) -> (s1'=1) & (x1'=0); // channel free
+	[busy1] (s1=3) & cd1=4 & (x1=16*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
+	
+	// finished
+	[done] (s1=4) -> true;
+	[time] (s1=4) -> (x1'=min(x1+1,max(lambda,M*slot)+1));
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// construct further stations through renaming
+module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule
+
--- a/prism-examples/pta/csma/abst/deadline.pctl
+++ b/prism-examples/pta/csma/abst/deadline.pctl
@ -0,0 +1,3 @@
+const int T;
+
+Pmin=? [ F<=T "done" ]
--- a/prism-examples/pta/csma/abst/eventually.pctl
+++ b/prism-examples/pta/csma/abst/eventually.pctl
@ -0,0 +1,2 @@
+Pmin=? [ F "done" ]
+
--- a/prism-examples/pta/csma/abst/models
+++ b/prism-examples/pta/csma/abst/models
@ -0,0 +1,2 @@
+csma.nm -const bmax=1
+
--- a/prism-examples/pta/csma/abst/props
+++ b/prism-examples/pta/csma/abst/props
@ -0,0 +1,4 @@
+eventually.pctl
+deadline.pctl -const T=1000
+deadline.pctl -const T=2000
+deadline.pctl -const T=3000
--- a/prism-examples/pta/csma/full/args
+++ b/prism-examples/pta/csma/full/args
@ -0,0 +1 @@
+-aroptions refine=all,nopre
--- a/prism-examples/pta/csma/full/auto
+++ b/prism-examples/pta/csma/full/auto
@ -0,0 +1,11 @@
+#!/bin/csh
+
+prism csma.nm collisions.pctl -const bmax=2,K=4 -aroptions refine=all,nopre,opt
+prism csma.nm collisions.pctl -const bmax=2,K=8 -aroptions refine=all,nopre,opt
+prism csma.nm collisions.pctl -const bmax=4,K=4 -aroptions refine=all,nopre,opt
+prism csma.nm collisions.pctl -const bmax=4,K=8 -aroptions refine=all,nopre,opt
+
+prism csma.nm time.pctl -const bmax=1,K=0 -aroptions refine=all,nopre,opt
+prism csma.nm time.pctl -const bmax=2,K=0 -aroptions refine=all,nopre,opt
+prism csma.nm time.pctl -const bmax=3,K=0 -aroptions refine=all,nopre,opt
+prism csma.nm time.pctl -const bmax=4,K=0 -aroptions refine=all,nopre,opt
--- a/prism-examples/pta/csma/full/collisions.pctl
+++ b/prism-examples/pta/csma/full/collisions.pctl
@ -0,0 +1 @@
+Pmax=?[F "cmax" ]
--- a/prism-examples/pta/csma/full/csma-digital.nm
+++ b/prism-examples/pta/csma/full/csma-digital.nm
--- a/prism-examples/pta/csma/full/csma-slots.nm
+++ b/prism-examples/pta/csma/full/csma-slots.nm
--- a/prism-examples/pta/csma/full/csma.nm
+++ b/prism-examples/pta/csma/full/csma.nm
--- a/prism-examples/pta/csma/full/eventually.pctl
+++ b/prism-examples/pta/csma/full/eventually.pctl
@ -0,0 +1,5 @@
+Pmin=?[ F "s1_done"]
+Pmin=?[ F "s2_done"]
+Pmin=?[ F "done" ]
+Pmin=?[ F cd1=2 ]
+Pmax=?[ F cd1=2 ]
--- a/prism-examples/pta/csma/full/models
+++ b/prism-examples/pta/csma/full/models
@ -0,0 +1,5 @@
+csma.nm -const bmax=2,K=4
+csma.nm -const bmax=2,K=8
+csma.nm -const bmax=4,K=4
+csma.nm -const bmax=4,K=8
+
--- a/prism-examples/pta/csma/full/props
+++ b/prism-examples/pta/csma/full/props
@ -0,0 +1 @@
+collisions.pctl
--- a/prism-examples/pta/csma/full/time.pctl
+++ b/prism-examples/pta/csma/full/time.pctl
@ -0,0 +1,2 @@
+R{"time"}min=? [ F "done" ]
+
--- a/prism-examples/pta/firewire/abst/args
+++ b/prism-examples/pta/firewire/abst/args
@ -0,0 +1 @@
+-aroptions refine=all,nopre
--- a/prism-examples/pta/firewire/abst/auto
+++ b/prism-examples/pta/firewire/abst/auto
@ -0,0 +1,9 @@
+#!/bin/csh
+
+prism firewire.nm eventually.pctl -const delay=360 -aroptions nopre,refine=all,opt
+
+prism firewire.nm deadline.pctl -const delay=360,T=5000 -aroptions nopre,refine=all,opt
+prism firewire.nm deadline.pctl -const delay=360,T=10000 -aroptions nopre,refine=all,opt
+prism firewire.nm deadline.pctl -const delay=360,T=20000 -aroptions nopre,refine=all,opt
+
+#prism firewire.nm time.pctl -const delay=360 -aroptions nopre,refine=all,opt
--- a/prism-examples/pta/firewire/abst/deadline-max.pctl
+++ b/prism-examples/pta/firewire/abst/deadline-max.pctl
@ -0,0 +1,3 @@
+// Minimum probability that a leader has been elected by deadline T
+Pmax=? [ F "done_after" ]
+
--- a/prism-examples/pta/firewire/abst/deadline.pctl
+++ b/prism-examples/pta/firewire/abst/deadline.pctl
@ -0,0 +1,5 @@
+const int T;
+
+// Minimum probability that a leader has been elected by deadline T
+Pmin=? [ F<=T "done" ]
+
--- a/prism-examples/pta/firewire/abst/eventually.pctl
+++ b/prism-examples/pta/firewire/abst/eventually.pctl
@ -0,0 +1,3 @@
+// Minimum probability that a leader is eventually elected
+Pmin=? [ F "done" ]
+
--- a/prism-examples/pta/firewire/abst/firewire-digital.nm
+++ b/prism-examples/pta/firewire/abst/firewire-digital.nm
@ -0,0 +1,74 @@
+// discrete version of abstract firewire protocol
+// gxn 23/05/2001
+
+nondeterministic
+
+// wire delay
+const int delay;
+
+// probability of choosing fast and slow
+const double fast;
+const double slow = 1-fast;
+
+// maximal constant
+const int kx = 167;
+
+module abstract_firewire
+	
+	// clock 
+	x : [0..kx+1];
+	
+	// local state
+	s : [0..9];
+	// 0 -start_start
+	// 1 -fast_start
+	// 2 -start_fast
+	// 3 -start_slow
+	// 4 -slow_start
+	// 5 -fast_fast
+	// 6 -fast_slow
+	// 7 -slow_fast
+	// 8 -slow_slow
+	// 9 -done
+	
+	// initial state
+	[time] s=0 & x<delay -> (x'=min(x+1,kx+1));
+	[round] s=0 -> fast : (s'=1) + slow : (s'=4);
+	[round] s=0 -> fast : (s'=2) + slow : (s'=3);
+	// fast_start
+	[time] s=1 & x<delay -> (x'=min(x+1,kx+1));
+	[] s=1 -> fast : (s'=5) & (x'=0) + slow : (s'=6) & (x'=0);
+	// start_fast
+	[time] s=2 & x<delay -> (x'=min(x+1,kx+1));
+	[] s=2 -> fast : (s'=5) & (x'=0) + slow : (s'=7) & (x'=0);
+	// start_slow
+	[time] s=3 & x<delay -> (x'=min(x+1,kx+1));
+	[] s=3 -> fast : (s'=6) & (x'=0) + slow : (s'=8) & (x'=0);
+	// slow_start
+	[time] s=4 & x<delay -> (x'=min(x+1,kx+1));
+	[] s=4 -> fast : (s'=7) & (x'=0) + slow : (s'=8) & (x'=0);
+	// fast_fast
+	[time] s=5 & (x<85) -> (x'=min(x+1,kx+1));
+	[] s=5 & (x>=76) -> (s'=0) & (x'=0);
+	[] s=5 & (x>=76-delay) -> (s'=9) & (x'=0);
+	// fast_slow
+	[time] s=6 & x<167 -> (x'=min(x+1,kx+1));
+	[] s=6 & x>=159-delay -> (s'=9) & (x'=0);
+	// slow_fast
+	[time] s=7 & x<167 -> (x'=min(x+1,kx+1));
+	[] s=7 & x>=159-delay -> (s'=9) & (x'=0);
+	// slow_slow
+	[time] s=8 & x<167 -> (x'=min(x+1,kx+1));
+	[] s=8 & x>=159 -> (s'=0) & (x'=0);
+	[] s=8 & x>=159-delay -> (s'=9) & (x'=0);
+	// done
+	[] s=9 -> (s'=s);
+	
+endmodule
+
+// labels
+label "done" = (s=9);
+
+rewards
+	[time] true : 1;
+endrewards
--- a/prism-examples/pta/firewire/abst/firewire-max.nm
+++ b/prism-examples/pta/firewire/abst/firewire-max.nm
@ -0,0 +1,82 @@
+// Abstract model of Firewire protocol (PTA model)
+// dxp/gxn 08/07/09
+
+pta
+
+// maximum and minimum delays
+// fast
+const int rc_fast_max = 850;
+const int rc_fast_min = 760;
+// slow
+const int rc_slow_max = 1670;
+const int rc_slow_min = 1590;
+// delay caused by the wire length
+const int delay;
+// probability of choosing fast and slow
+const double fast = 0.5;
+const double slow = 1-fast;
+const int T;
+
+module abstract_firewire
+
+	// clock 
+	x : clock;
+	z : clock;
+	// local state
+	s : [0..9];
+	// 0 - start_start
+	// 1 - fast_start
+	// 2 - start_fast
+	// 3 - start_slow
+	// 4 - slow_start
+	// 5 - fast_fast
+	// 6 - fast_slow
+	// 7 - slow_fast
+	// 8 - slow_slow
+	// 9 - done
+
+	// clock invariant
+	invariant
+		(s=0 => x<=delay) &
+		(s=1 => x<=delay) &
+		(s=2 => x<=delay) &
+		(s=3 => x<=delay) &
+		(s=4 => x<=delay) &
+		(s=5 => x<=rc_fast_max) &
+		(s=6 => x<=rc_slow_max) &
+		(s=7 => x<=rc_slow_max) &
+		(s=8 => x<=rc_slow_max) &
+		(s=9 => x<=0)
+	endinvariant
+	
+	// start_start (initial state)
+	[] s=0 -> fast : (s'=1) + slow : (s'=4);
+	[] s=0 -> fast : (s'=2) + slow : (s'=3);
+	// fast_start
+	[] s=1 -> fast : (s'=5) & (x'=0) + slow : (s'=6) & (x'=0);
+	// start_fast
+	[] s=2 -> fast : (s'=5) & (x'=0) + slow : (s'=7) & (x'=0);
+	// start_slow
+	[] s=3 -> fast : (s'=6) & (x'=0) + slow : (s'=8) & (x'=0);
+	// slow_start
+	[] s=4 -> fast : (s'=7) & (x'=0) + slow : (s'=8) & (x'=0);
+	// fast_fast
+	[] s=5 & (x>=rc_fast_min)       -> (s'=0) & (x'=0);
+	[] s=5 & (x>=rc_fast_min-delay) -> (s'=9) & (x'=0);
+	// fast_slow
+	[] s=6 & x>=rc_slow_min-delay -> (s'=9) & (x'=0);
+	// slow_fast
+	[] s=7 & x>=rc_slow_min-delay -> (s'=9) & (x'=0);
+	// slow_slow
+	[] s=8 & x>=rc_slow_min       -> (s'=0) & (x'=0);
+	[] s=8 & x>=rc_slow_min-delay -> (s'=9) & (x'=0);
+	// done
+	[] s=9 & z>=T -> (s'=10);
+	[] s=9 & z<T -> (s'=11);
+	[] s>9 -> true;
+	
+endmodule
+
+// labels
+label "done_after" = (s=10);
+
--- a/prism-examples/pta/firewire/abst/firewire.nm
+++ b/prism-examples/pta/firewire/abst/firewire.nm
@ -0,0 +1,84 @@
+// Abstract model of Firewire protocol (PTA model)
+// dxp/gxn 08/07/09
+
+pta
+
+// maximum and minimum delays
+// fast
+const int rc_fast_max = 850;
+const int rc_fast_min = 760;
+// slow
+const int rc_slow_max = 1670;
+const int rc_slow_min = 1590;
+// delay caused by the wire length
+const int delay;
+// probability of choosing fast and slow
+const double fast = 0.5;
+const double slow = 1-fast;
+
+module abstract_firewire
+
+	// clock 
+	x : clock;
+	// local state
+	s : [0..9];
+	// 0 - start_start
+	// 1 - fast_start
+	// 2 - start_fast
+	// 3 - start_slow
+	// 4 - slow_start
+	// 5 - fast_fast
+	// 6 - fast_slow
+	// 7 - slow_fast
+	// 8 - slow_slow
+	// 9 - done
+
+	// clock invariant
+	invariant
+		(s=0 => x<=delay) &
+		(s=1 => x<=delay) &
+		(s=2 => x<=delay) &
+		(s=3 => x<=delay) &
+		(s=4 => x<=delay) &
+		(s=5 => x<=rc_fast_max) &
+		(s=6 => x<=rc_slow_max) &
+		(s=7 => x<=rc_slow_max) &
+		(s=8 => x<=rc_slow_max) &
+		(s=9 => x<=0)
+	endinvariant
+	
+	// start_start (initial state)
+	[] s=0 -> fast : (s'=1) + slow : (s'=4);
+	[] s=0 -> fast : (s'=2) + slow : (s'=3);
+	// fast_start
+	[] s=1 -> fast : (s'=5) & (x'=0) + slow : (s'=6) & (x'=0);
+	// start_fast
+	[] s=2 -> fast : (s'=5) & (x'=0) + slow : (s'=7) & (x'=0);
+	// start_slow
+	[] s=3 -> fast : (s'=6) & (x'=0) + slow : (s'=8) & (x'=0);
+	// slow_start
+	[] s=4 -> fast : (s'=7) & (x'=0) + slow : (s'=8) & (x'=0);
+	// fast_fast
+	[] s=5 & (x>=rc_fast_min)       -> (s'=0) & (x'=0);
+	[] s=5 & (x>=rc_fast_min-delay) -> (s'=9) & (x'=0);
+	// fast_slow
+	[] s=6 & x>=rc_slow_min-delay -> (s'=9) & (x'=0);
+	// slow_fast
+	[] s=7 & x>=rc_slow_min-delay -> (s'=9) & (x'=0);
+	// slow_slow
+	[] s=8 & x>=rc_slow_min       -> (s'=0) & (x'=0);
+	[] s=8 & x>=rc_slow_min-delay -> (s'=9) & (x'=0);
+	// done
+	[] s=9 -> true;
+	
+endmodule
+
+// labels
+label "done" = (s=9);
+
+// reward structures
+// time
+rewards "time"
+	true : 1;
+endrewards
+
--- a/prism-examples/pta/firewire/abst/models
+++ b/prism-examples/pta/firewire/abst/models
@ -0,0 +1,3 @@
+#firewire.nm -const delay=30
+firewire.nm -const delay=360
+
--- a/prism-examples/pta/firewire/abst/props
+++ b/prism-examples/pta/firewire/abst/props
@ -0,0 +1,4 @@
+eventually.pctl
+deadline.pctl -const T=5000
+deadline.pctl -const T=10000
+deadline.pctl -const T=20000
--- a/prism-examples/pta/firewire/abst/time.pctl
+++ b/prism-examples/pta/firewire/abst/time.pctl
@ -0,0 +1,3 @@
+// Maximum expected time to elect a leader
+R{"time"}min=? [ F "done" ]
+
--- a/prism-examples/pta/firewire/impl/args
+++ b/prism-examples/pta/firewire/impl/args
@ -0,0 +1 @@
+-aroptions refine=all,nopre
--- a/prism-examples/pta/firewire/impl/auto
+++ b/prism-examples/pta/firewire/impl/auto
@ -0,0 +1,7 @@
+#!/bin/csh
+
+prism firewire.nm eventually.pctl -const delay=360 -aroptions nopre,refine=all,opt
+
+prism firewire.nm deadline.pctl -const delay=360,T=2500 -aroptions nopre,refine=all,opt
+prism firewire.nm deadline.pctl -const delay=360,T=5000 -aroptions nopre,refine=all,opt
+prism firewire.nm deadline.pctl -const delay=360,T=7500 -aroptions nopre,refine=all,opt
--- a/prism-examples/pta/firewire/impl/deadline.pctl
+++ b/prism-examples/pta/firewire/impl/deadline.pctl
@ -0,0 +1,5 @@
+const int T;
+
+// Minimum probability that a leader has been elected by deadline T
+Pmin=? [ F<=T "done" ]
+
--- a/prism-examples/pta/firewire/impl/eventually.pctl
+++ b/prism-examples/pta/firewire/impl/eventually.pctl
@ -0,0 +1,3 @@
+// Minimum probability that a leader is eventually elected
+Pmin=? [ F "done" ]
+
--- a/prism-examples/pta/firewire/impl/firewire-digital.nm
+++ b/prism-examples/pta/firewire/impl/firewire-digital.nm
@ -0,0 +1,167 @@
+// 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)
+
+// 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 = 0.5;
+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 ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// 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 & x1=0 -> fast : (s1'=2) +  slow : (s1'=3);
+	[rec_idle21] s1=0 & x1=0 -> (s1'=1);
+	// rec_idle immediate state)
+	[snd_idle12] s1=1 & x1=0 -> fast : (s1'=4) +  slow : (s1'=5);
+	[rec_req21]  s1=1 & x1=0 -> (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) & (x1'=0);
+	[rec_ack21] s1=6 -> (s1'=8) & (x1'=0);
+	[time]      s1=6 -> (x1'=min(x1+1,168));
+	// almost root (immediate) 
+	// loop in final states to remove deadlock
+	[loop] s1=7 & s2=8 -> (s1'=s1);
+	[loop] s1=8 & s2=7 -> (s1'=s1);
+	[time] s1=7 -> (x1'=min(x1+1,168));
+	[time] s1=8 -> (x1'=min(x1+1,168));
+	
+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,done1=done2,done2=done1]
+endmodule
+
+// reward structures
+// time
+rewards "time"	
+	[time] true : 1;
+endrewards
+// time nodes sending
+rewards "time_sending"
+	[time] (w12>0 | w21>0) : 1;
+endrewards
--- a/prism-examples/pta/firewire/impl/firewire.nm
+++ b/prism-examples/pta/firewire/impl/firewire.nm
@ -0,0 +1,179 @@
+// Firewire protocol (PTA model)
+// dxp/gxn 08/07/09
+
+pta
+
+// CLOCKS
+// x1 (x2) clock for node1 (node2)
+// y1 and y2 (z1 and z2) clocks for wire12 (wire21)
+
+// maximum and minimum delays
+// fast
+const int rc_fast_max = 850;
+const int rc_fast_min = 760;
+// slow
+const int rc_slow_max = 1670;
+const int rc_slow_min = 1590;
+// delay caused by the wire length
+const int delay;
+// probability of choosing fast and slow
+const double fast = 0.5;
+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 : clock;
+	y2 : clock;
+
+	// clock invariant
+	invariant
+	    (w12=1 => y2<=delay)
+	  & (w12=2 => y1<=delay)
+	  & (w12=3 => y2<=delay)
+	  & (w12=4 => y1<=delay)
+	  & (w12=5 => y2<=delay)
+	  & (w12=6 => y1<=delay)
+	  & (w12=7 => y1<=delay)
+	  & (w12=8 => y1<=delay)
+	  & (w12=9 => y1<=delay)
+	endinvariant
+
+	// 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);
+	// 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);
+	// rec_req_ack
+	[snd_ack12] w12=2 -> (w12'=2);
+	[rec_req12] w12=2 -> (w12'=3);
+	// 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);
+	// rec_ack_idle
+	[snd_idle12] w12=4 -> (w12'=4);
+	[rec_ack12]  w12=4 -> (w12'=5);
+	// 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);
+	// rec_idle_req
+	[snd_req12]  w12=6 -> (w12'=6);
+	[rec_idle12] w12=6 -> (w12'=1);
+	// rec_ack_req
+	[snd_req12] w12=7 -> (w12'=7);
+	[rec_ack12] w12=7 -> (w12'=1);
+	// rec_req_idle
+	[snd_idle12] w12=8 -> (w12'=8);
+	[rec_req12]  w12=8 -> (w12'=5);
+	// rec_idle_ack
+	[snd_ack12]  w12=9 -> (w12'=9);
+	[rec_idle12] w12=9 -> (w12'=3);
+	
+endmodule
+
+module node1
+	
+	// clock for node1
+	x1 : clock;
+	
+	// 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
+	
+	// clock invariant
+	invariant
+	    (s1=2 => x1<=rc_fast_max)
+	  & (s1=3 => x1<=rc_slow_max)
+	  & (s1=4 => x1<=rc_fast_max)
+	  & (s1=5 => x1<=rc_slow_max)
+	  // urgency:
+	  & (s1=0 => x1<=0)
+	  & (s1=1 => x1<=0)
+	endinvariant
+	
+	// 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 & x1=0 -> fast : (s1'=2) +  slow : (s1'=3);
+	[rec_idle21] s1=0 & x1=0 -> (s1'=1);
+	// rec_idle immediate state)
+	[snd_idle12] s1=1 & x1=0 -> fast : (s1'=4) +  slow : (s1'=5);
+	[rec_req21]  s1=1 & x1=0 -> (s1'=0);
+	// rec_req_fast
+	[rec_idle21] s1=2 -> (s1'=4);	
+	[snd_ack12]  s1=2 & x1>=rc_fast_min -> (s1'=7) & (x1'=0);
+	// rec_req_slow
+	[rec_idle21] s1=3 -> (s1'=5);
+	[snd_ack12]  s1=3 & x1>=rc_slow_min -> (s1'=7) & (x1'=0);
+	// rec_idle_fast
+	[rec_req21] s1=4 -> (s1'=2);
+	[snd_req12] s1=4 & x1>=rc_fast_min -> (s1'=6) & (x1'=0);
+	// rec_idle_slow
+	[rec_req21] s1=5 -> (s1'=3);
+	[snd_req12] s1=5 & x1>=rc_slow_min -> (s1'=6) & (x1'=0);
+	// 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) & (x1'=0);
+	[rec_ack21] s1=6 -> (s1'=8) & (x1'=0);
+	// almost root or almost child (immediate) 
+	// loop in final states to remove deadlock
+	[loop] s1=7 -> true;
+	[loop] s1=8 -> true;
+	
+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
+
+// labels
+label "done" = (s1=8 & s2=7) | (s1=7 & s2=8);
+
+// reward structures
+// time
+rewards "time"	
+	true : 1;
+endrewards
+// time nodes sending
+rewards "time_sending"
+	(w12>0 | w21>0) : 1;
+endrewards
--- a/prism-examples/pta/firewire/impl/models
+++ b/prism-examples/pta/firewire/impl/models
@ -0,0 +1,3 @@
+#firewire.nm -const delay=30
+firewire.nm -const delay=360
+
--- a/prism-examples/pta/firewire/impl/props
+++ b/prism-examples/pta/firewire/impl/props
@ -0,0 +1,4 @@
+eventually.pctl
+deadline.pctl -const T=2500
+deadline.pctl -const T=5000
+deadline.pctl -const T=7500
--- a/prism-examples/pta/firewire/impl/time.pctl
+++ b/prism-examples/pta/firewire/impl/time.pctl
@ -0,0 +1,3 @@
+// Maximum expected time to elect a leader
+R{"time"}min=? [ F "done" ]
+
--- a/prism-examples/pta/formats09.sh
+++ b/prism-examples/pta/formats09.sh
@ -0,0 +1,36 @@
+# FORMATS'09 Case Studies
+
+prism csma/full/csma.nm csma/full/collisions.pctl -const bmax=2,K=4 -aroptions refine=all,nopre
+prism csma/full/csma.nm csma/full/collisions.pctl -const bmax=2,K=8 -aroptions refine=all,nopre
+prism csma/full/csma.nm csma/full/collisions.pctl -const bmax=4,K=4 -aroptions refine=all,nopre
+#prism csma/full/csma.nm csma/full/collisions.pctl -const bmax=4,K=8 -aroptions refine=all,nopre
+
+prism csma/abst/csma.nm -const bmax=1 csma/abst/eventually.pctl -aroptions refine=all,nopre
+prism csma/abst/csma.nm -const bmax=1 csma/abst/deadline.pctl -const T=1000 -aroptions refine=all,nopre
+prism csma/abst/csma.nm -const bmax=1 csma/abst/deadline.pctl -const T=2000 -aroptions refine=all,nopre
+#prism csma/abst/csma.nm -const bmax=1 csma/abst/deadline.pctl -const T=3000 -aroptions refine=all,nopre
+
+prism firewire/impl/firewire.nm firewire/impl/eventually.pctl -const delay=360 -aroptions refine=all,nopre
+prism firewire/impl/firewire.nm firewire/impl/deadline.pctl -const delay=360,T=2500 -aroptions refine=all,nopre
+prism firewire/impl/firewire.nm firewire/impl/deadline.pctl -const delay=360,T=5000 -aroptions refine=all,nopre
+prism firewire/impl/firewire.nm firewire/impl/deadline.pctl -const delay=360,T=7500 -aroptions refine=all,nopre
+
+prism firewire/abst/firewire.nm firewire/abst/eventually.pctl -const delay=360 -aroptions refine=all,nopre
+prism firewire/abst/firewire.nm firewire/abst/deadline.pctl -const delay=360,T=5000 -aroptions refine=all,nopre
+prism firewire/abst/firewire.nm firewire/abst/deadline.pctl -const delay=360,T=10000 -aroptions refine=all,nopre
+prism firewire/abst/firewire.nm firewire/abst/deadline.pctl -const delay=360,T=20000 -aroptions refine=all,nopre
+
+prism zeroconf/zeroconf.nm zeroconf/incorrect.pctl -aroptions refine=all,nopre
+prism zeroconf/zeroconf.nm zeroconf/deadline.pctl -const T=100 -aroptions refine=all,nopre
+prism zeroconf/zeroconf.nm zeroconf/deadline.pctl -const T=150 -aroptions refine=all,nopre
+prism zeroconf/zeroconf.nm zeroconf/deadline.pctl -const T=200 -aroptions refine=all,nopre
+
+prism repudiation/honest/repudiation.nm repudiation/honest/eventually.pctl -aroptions refine=all,nopre
+prism repudiation/honest/repudiation.nm repudiation/honest/deadline.pctl -const T=40 -aroptions refine=all,nopre
+prism repudiation/honest/repudiation.nm repudiation/honest/deadline.pctl -const T=80 -aroptions refine=all,nopre
+prism repudiation/honest/repudiation.nm repudiation/honest/deadline.pctl -const T=100 -aroptions refine=all,nopre
+
+prism repudiation/malicious/repudiation.nm repudiation/malicious/eventually.pctl -aroptions refine=all,nopre
+prism repudiation/malicious/repudiation.nm repudiation/malicious/deadline.pctl -const T=5 -aroptions refine=all,nopre
+prism repudiation/malicious/repudiation.nm repudiation/malicious/deadline.pctl -const T=10 -aroptions refine=all,nopre
+#prism repudiation/malicious/repudiation.nm repudiation/malicious/deadline.pctl -const T=20 -aroptions refine=all,nopre,eref=1e-8
--- a/prism-examples/pta/repudiation/honest/args
+++ b/prism-examples/pta/repudiation/honest/args
@ -0,0 +1 @@
+-aroptions refine=all,nopre
--- a/prism-examples/pta/repudiation/honest/auto
+++ b/prism-examples/pta/repudiation/honest/auto
@ -0,0 +1,7 @@
+#!/bin/csh
+
+prism repudiation.nm eventually.pctl -aroptions refine=all,opt
+
+prism repudiation.nm deadline.pctl -aroptions refine=all,opt -const T=40
+prism repudiation.nm deadline.pctl -aroptions refine=all,opt -const T=80
+prism repudiation.nm deadline.pctl -aroptions refine=all,opt -const T=100
--- a/prism-examples/pta/repudiation/honest/deadline.pctl
+++ b/prism-examples/pta/repudiation/honest/deadline.pctl
@ -0,0 +1,5 @@
+const int T;
+
+// Minimum probability that protocol terminates successfully by the deadline
+Pmin=? [ F<T "terminated_successfully" ]
+
--- a/prism-examples/pta/repudiation/honest/eventually.pctl
+++ b/prism-examples/pta/repudiation/honest/eventually.pctl
@ -0,0 +1,4 @@
+
+// Minimum probability that the protocol terminates successfully
+Pmin=? [ F "terminated_successfully" ]
+
--- a/prism-examples/pta/repudiation/honest/models
+++ b/prism-examples/pta/repudiation/honest/models
@ -0,0 +1 @@
+repudiation.nm
--- a/prism-examples/pta/repudiation/honest/props
+++ b/prism-examples/pta/repudiation/honest/props
@ -0,0 +1,4 @@
+eventually.pctl
+deadline.pctl -const T=40
+deadline.pctl -const T=80
+deadline.pctl -const T=100
--- a/prism-examples/pta/repudiation/honest/repudiation.nm
+++ b/prism-examples/pta/repudiation/honest/repudiation.nm
@ -0,0 +1,93 @@
+pta
+
+module originator
+	o : [0..12];
+	// 0 - init
+	// 1 - send
+	// 2 - wait
+	// 3 - last
+	// 4 - early
+	// 5 - error
+	// 6 - sent_random
+	// 7 - sent_last
+	// 8 - done
+	// 9 - done_early
+	// 10 - done_error
+	// 11 - wait_random
+	// 12 - wait_last
+
+	x : clock;
+
+	invariant
+		(o=0 => true) &
+		(o=1 => x<=0) &
+		(o=2 => x<=5) & // x<=AD+1
+		(o=3 => x<=0) &
+		(o=4 => x<=0) &
+		(o=5 => x<=0) &
+		(o=6 => true) &
+		(o=7 => true) &
+		(o=8 => true) &
+		(o=9 => true) &
+		(o=10 => true) &
+		(o=11 => x<=5) & // x<=AD+1
+		(o=12 => x<=5) // x<=AD+1
+	endinvariant
+
+	[req] o=0 -> (o'=1) & (x'=0);
+	[message] o=1 & x<=0 -> (o'=2);
+	[ack]  o=2 & (x>=1 & x<=4) -> 0.9 : (o'=1) & (x'=0) + 0.1 :  (o'=3) & (x'=0); // guard x>=ad,x<=AD
+	[] o=2 & x>4 -> 0.9 : (o'=1) & (x'=0) + 0.1 :  (o'=3) & (x'=0); // guard x>AD
+	[decode] o=2 -> 0.9 : (o'=6) + 0.1 :  (o'=7);
+	[finished] o=3 -> (o'=8) & (x'=0);
+
+	[] o=8 -> (o'=8);
+	[] o=9 -> (o'=9);
+	[] o=10 -> (o'=10);
+
+	[stop] o=4 -> (o'=9); 
+	[error] o=5 -> (o'=10);
+
+	[decoded_random] o=6 -> (o'=11);
+	[decoded_last] o=7 -> (o'=12);
+
+	[ack] o=11 & (x>=1 & x<=4) -> (o'=1) & (x'=0);  // guard x>=ad,x<=AD
+	[stop] o=11 & x>4 ->  (o'=9) & (x'=0); 
+
+	[ack] o=12 & (x>=1 & x<=4) -> (o'=3) & (x'=0);  // guard x>=ad,x<=AD
+	[stop] o=12  & x>4 -> (o'=10) & (x'=0); 
+
+endmodule
+
+module recipient
+
+	r : [0..3];
+	// 0 - request
+	// 1 - wait
+	// 2 - ack
+	// 3 - done
+
+	y : clock;
+
+	invariant
+		(r=0 => y<=0) &
+		(r=1 => true) &
+		(r=2 => y<=4) &
+		(r=3 => true)
+	endinvariant
+
+	[req] r=0 & y=0 -> (r'=1);
+	[message] r=1 -> (r'=2) & (y'=0);
+	[finished] r=1 -> (r'=3);
+	[ack] r=2 & (y>=1 & y<=4) -> (r'=1) & (y'=0);
+
+	// honest recipient never tries decoding but added actions to final state
+	// so the same originator is used for honest and malicious recipient
+	[decode] r=3 -> (r'=3);
+	[decoded_random] r=3 -> (r'=3);
+	[decoded_last] r=3 -> (r'=3);
+
+endmodule
+
+label "terminated_successfully" = o=8;
+
--- a/prism-examples/pta/repudiation/malicious/args
+++ b/prism-examples/pta/repudiation/malicious/args
@ -0,0 +1 @@
+-aroptions refine=all,nopre
--- a/prism-examples/pta/repudiation/malicious/auto
+++ b/prism-examples/pta/repudiation/malicious/auto
@ -0,0 +1,7 @@
+#!/bin/csh
+
+prism repudiation.nm eventually.pctl -aroptions refine=all,opt
+
+prism repudiation.nm deadline.pctl -aroptions refine=all,opt -const T=5
+prism repudiation.nm deadline.pctl -aroptions refine=all,opt -const T=10
+prism repudiation.nm deadline.pctl -aroptions refine=all,opt -const T=20
--- a/prism-examples/pta/repudiation/malicious/deadline.pctl
+++ b/prism-examples/pta/repudiation/malicious/deadline.pctl
@ -0,0 +1,5 @@
+const int T;
+
+// Maximum probability that malicious recepient gains information by deadline T
+Pmax=? [ F<T "gains_information" ]
+
--- a/prism-examples/pta/repudiation/malicious/eventually.pctl
+++ b/prism-examples/pta/repudiation/malicious/eventually.pctl
@ -0,0 +1,4 @@
+
+// Maximum probability that malicious recepient gains information
+Pmax=? [ F "gains_information" ]
+
--- a/prism-examples/pta/repudiation/malicious/models
+++ b/prism-examples/pta/repudiation/malicious/models
@ -0,0 +1 @@
+repudiation.nm
--- a/prism-examples/pta/repudiation/malicious/props
+++ b/prism-examples/pta/repudiation/malicious/props
@ -0,0 +1,4 @@
+eventually.pctl
+deadline.pctl -const T=5
+deadline.pctl -const T=10
+deadline.pctl -const T=20
--- a/prism-examples/pta/repudiation/malicious/repudiation.nm
+++ b/prism-examples/pta/repudiation/malicious/repudiation.nm
@ -0,0 +1,117 @@
+pta
+
+module originator
+
+	o : [0..12];
+	// 0 - init
+	// 1 - send
+	// 2 - wait
+	// 3 - last
+	// 4 - early
+	// 5 - error
+	// 6 - sent_random
+	// 7 - sent_last
+	// 8 - done
+	// 9 - done_early
+	// 10 - done_error
+	// 11 - wait_random
+	// 12 - wait_last
+
+	x : clock;
+
+	invariant
+		(o=0 => true) &
+		(o=1 => x<=0) &
+		(o=2 => x<=5) & // x<=AD+1
+		(o=3 => x<=0) &
+		(o=4 => x<=0) &
+		(o=5 => x<=0) &
+		(o=6 => true) &
+		(o=7 => true) &
+		(o=8 => true) &
+		(o=9 => true) &
+		(o=10 => true) &
+		(o=11 => x<=5) & // x<=AD+1
+		(o=12 => x<=5) // x<=AD+1
+	endinvariant
+
+	[req] o=0 -> (o'=1) & (x'=0);
+	[message] o=1 & x<=0 -> (o'=2);
+	[ack]  o=2 & (x>=1 & x<=4) -> 0.9 : (o'=1) & (x'=0) + 0.1 :  (o'=3) & (x'=0); // guard x>=ad,x<=AD
+	[] o=2 & x>4 -> 0.9 : (o'=4) & (x'=0) + 0.1 :  (o'=5) & (x'=0); // guard x>AD
+	[decode] o=2 -> 0.9 : (o'=6) + 0.1 :  (o'=7);
+	[finished] o=3 -> (o'=8) & (x'=0);
+
+	[] o=8 -> (o'=8);
+	[] o=9 -> (o'=9);
+	[] o=10 -> (o'=10);
+
+	[stop] o=4 -> (o'=9); 
+	[error] o=5 -> (o'=10);
+
+	[decoded_random] o=6 -> (o'=11);
+	[decoded_last] o=7 -> (o'=12);
+
+	[ack] o=11 & (x>=1 & x<=4) -> (o'=1) & (x'=0);  // guard x>=ad,x<=AD
+	[stop] o=11 & x>4 ->  (o'=9) & (x'=0); 
+
+	[ack] o=12 & (x>=1 & x<=4) -> (o'=3) & (x'=0);  // guard x>=ad,x<=AD
+	[stop] o=12  & x>4 -> (o'=10) & (x'=0); 
+
+endmodule
+
+module recipient
+
+	r : [0..9];
+	// 0 - request
+	// 1 - wait
+	// 2 - ack
+	// 3 - done
+	// 4 - decode1
+	// 5 - decode2
+	// 6 - terminate
+	// 7 - decode
+	// 8 - decoded
+	// 9 - random
+
+	y : clock;
+
+	invariant
+		(r=0 => y<=0) &
+		(r=1 => true) &
+		(r=2 => true) &
+		(r=3 => true) &
+		(r=4 => y<=1) &
+		(r=5 => y<=3) &
+		(r=6 => true) &
+		(r=7 => y<=0) &
+		(r=8 => y<=0) &
+		(r=9 => y<=0)
+	endinvariant
+
+	[req] r=0 & y=0 -> (r'=1);
+	[message] r=1 -> (r'=2) & (y'=0);
+	[finished] r=1 -> (r'=3);
+
+	[ack] r=2 -> (r'=1);
+	[] r=2 -> (r'=4) & (y'=0);
+	[] r=2 -> (r'=5) & (y'=0);
+	[] r=2 -> (r'=6);
+
+	[] r=3 -> (r'=3);
+	[] r=6 -> (r'=6);
+
+	[] r=4 & y=1 -> 0.01 : (r'=7) & (y'=0) + 0.99 : (r'=2) & (y'=0);
+	[] r=5 & y=3 -> 0.05 : (r'=7) & (y'=0) + 0.95 : (r'=2) & (y'=0);
+
+	[decode] r=7 & y=0 -> (r'=8);
+	[decoded_random] r=8 & y=0 -> (r'=9);
+	[decoded_last] r=8 & y=0 -> (r'=6);
+	[ack] r=9 -> (r'=1);
+	[] r=9 -> (r'=6);
+
+endmodule
+
+label "gains_information" = o=10;
+
+
--- a/prism-examples/pta/simple/auto
+++ b/prism-examples/pta/simple/auto
@ -0,0 +1,3 @@
+#!/bin/csh
+
+prism formats09.nm formats09.pctl -prop 1 -aroptions refine=first
--- a/prism-examples/pta/simple/formats09.nm
+++ b/prism-examples/pta/simple/formats09.nm
@ -0,0 +1,26 @@
+// PTA used as running example in FORMATS'09 paper
+
+pta
+
+module M
+
+	s : [0..3];
+	x : clock;
+	y : clock;
+	
+	[] s=0 -> 0.6 : (s'=1) + 0.4 : (s'=2)&(x'=0);
+	[] s=1 & x=0 -> (s'=3);
+	[] s=1 & y>2 -> (s'=1)&(y'=0);
+	[] s=2 & x=0 & y=1 -> (s'=3)&(y'=0);
+	[] s=2 & x>2 -> (s'=1)&(y'=0);
+	[] s=3 -> (s'=3);
+
+endmodule
+
+label "target" = s=3;
+label "end" = s=3 | s=1;
+
+rewards "time"
+	true : 1;
+endrewards
+
--- a/prism-examples/pta/simple/formats09.pctl
+++ b/prism-examples/pta/simple/formats09.pctl
@ -0,0 +1,3 @@
+Pmax=? [ F "target" ]
+
+// Rmin=? [ F "end" ]
--- a/prism-examples/pta/tests-prism.sh
+++ b/prism-examples/pta/tests-prism.sh
@ -0,0 +1,9 @@
+
+prism-benchmark -exec prism-explicit -logs logs csma
+prism-benchmark -exec prism-explicit -logs logs csma/abst
+prism-benchmark -exec prism-explicit -logs logs firewire/impl
+prism-benchmark -exec prism-explicit -logs logs firewire/abst
+prism-benchmark -exec prism-explicit -logs logs zeroconf
+prism-benchmark -exec prism-explicit -logs logs repudiation/honest
+prism-benchmark -exec prism-explicit -logs logs repudiation/malicious
+
--- a/prism-examples/pta/zeroconf/args
+++ b/prism-examples/pta/zeroconf/args
@ -0,0 +1 @@
+-aroptions refine=all,nopre
--- a/prism-examples/pta/zeroconf/auto
+++ b/prism-examples/pta/zeroconf/auto
@ -0,0 +1,20 @@
+#!/bin/csh
+
+# full (multi-variable)
+
+prism zeroconf.nm incorrect.pctl -aroptions refine=all,nopre,opt
+
+prism zeroconf.nm deadline.pctl -const T=100 -aroptions refine=all,nopre,opt
+prism zeroconf.nm deadline.pctl -const T=150 -aroptions refine=all,nopre,opt
+prism zeroconf.nm deadline.pctl -const T=200 -aroptions refine=all,nopre,opt
+
+prism zeroconf.nm time.pctl -aroptions refine=all,nopre,opt
+
+# simple (single variable)
+
+prism zeroconf-simple.nm incorrect.pctl -aroptions refine=all,nopre,opt
+
+prism zeroconf-simple.nm deadline.pctl -const T=100 -aroptions refine=all,nopre,opt
+prism zeroconf-simple.nm deadline.pctl -const T=150 -aroptions refine=all,nopre,opt
+prism zeroconf-simple.nm deadline.pctl -const T=200 -aroptions refine=all,nopre,opt
+
--- a/prism-examples/pta/zeroconf/deadline.pctl
+++ b/prism-examples/pta/zeroconf/deadline.pctl
@ -0,0 +1,5 @@
+const int T;
+
+// Maximum probability of configuring incorrectly (using unfresh address) by time T
+Pmax=? [ F<=T "incorrect" ]
+
--- a/prism-examples/pta/zeroconf/eventually.pctl
+++ b/prism-examples/pta/zeroconf/eventually.pctl
@ -0,0 +1,3 @@
+// Maximum probably use unfresh address
+Pmax=? [ F "done" ]
+
--- a/prism-examples/pta/zeroconf/incorrect.pctl
+++ b/prism-examples/pta/zeroconf/incorrect.pctl
@ -0,0 +1,3 @@
+// Maximum probability of configuring incorrectly (using unfresh address)
+Pmax=? [ F "incorrect" ]
+
--- a/prism-examples/pta/zeroconf/models
+++ b/prism-examples/pta/zeroconf/models
@ -0,0 +1 @@
+zeroconf.nm
--- a/prism-examples/pta/zeroconf/props
+++ b/prism-examples/pta/zeroconf/props
@ -0,0 +1,4 @@
+incorrect.pctl
+deadline.pctl -const T=100
+deadline.pctl -const T=150
+deadline.pctl -const T=200
--- a/prism-examples/pta/zeroconf/time.pctl
+++ b/prism-examples/pta/zeroconf/time.pctl
@ -0,0 +1,3 @@
+// Maximum expected time to elect a leader
+R{"time"}min=? [ F "done" ]
+
--- a/prism-examples/pta/zeroconf/used.pctl
+++ b/prism-examples/pta/zeroconf/used.pctl
@ -0,0 +1 @@
+P=?[ F s=2 & ip=2 ]
--- a/prism-examples/pta/zeroconf/zeroconf-digital.nm
+++ b/prism-examples/pta/zeroconf/zeroconf-digital.nm
@ -0,0 +1,42 @@
+// prism model of pta version of zeroconf
+// using digitial clocks
+
+mdp
+
+module sender
+
+	s : [0..2]; //local state
+	probes : [0..4]; // probes sent
+	ip : [0..2]; // ip address not chosen, fresh or in use
+	x : [0..21]; // local clock
+
+	// selct probe	
+	// [] s=0 -> 0.99969242125984251969 : (s'=1) & (ip'=0) + 0.00030757874015748031 : (s'=1) & (ip'=1);
+	
+	[] s=0 -> 0.5 : (s'=1) & (ip'=1) + 0.5 : (s'=1) & (ip'=2);
+	// send probes
+	[time] s=1 & x<20 -> (x'=x+1);
+	[send_used]  s=1 & x=20 & ip=2 & probes<4 -> (probes'=probes+1) & (x'=0);	
+	[send_fresh] s=1 & x=20 & ip=1 & probes<4 -> (probes'=probes+1) & (x'=0);
+	[] s=1 & x=20 & probes=4 -> (s'=2) & (x'=0);
+	[recv] s=1 -> (s'=0) & (x'=0) & (ip'=0) & (probes'=0);
+
+	[time] s=2 -> (x'=min(21,x+1));
+
+endmodule
+
+module environment
+	
+	e : [0..2]; // ready, send reply
+	y : [0..6];
+
+	[time] e=0 -> (y'=min(y+1,6));
+	[send_fresh] e=0 -> true;
+	[send_used]  e=0 -> 0.1 : (e'=0) + 0.9 : (e'=1);
+
+	[time] e>0 & y<5 -> (y'=y+1);
+	[] e=1 & y>=1 -> 0.1 : (e'=0) & (y'=0) + 0.9 : (e'=2) & (y'=0);
+	[recv] e=2 & y>=1 -> (e'=0) & (y'=0);
+
+endmodule
+
--- a/prism-examples/pta/zeroconf/zeroconf-full.nm
+++ b/prism-examples/pta/zeroconf/zeroconf-full.nm
@ -0,0 +1,299 @@
+// IPv4: PTA model with digitial clocks
+// one concrete host attempting to choose an ip address 
+// when a number of (abstract) hosts have already got ip addresses
+// gxn/dxp/jzs 02/05/03
+
+// reset or noreset model
+const bool reset=true;
+
+//-------------------------------------------------------------
+
+// we suppose that
+// - the abstract hosts have already picked their addresses 
+//   and always defend their addresses
+// - the concrete host never picks the same ip address twice 
+//   (this can happen only with a verys small probability)
+
+// under these assumptions we do not need message types because:
+// 1) since messages to the concrete host will never be a probe, 
+//    this host will react to all messages in the same way
+// 2) since the abstract hosts always defend their addresses, 
+//    all messages from the host will get an arp reply if the ip matches
+
+// following from the above assumptions we require only three abstract IP addresses
+// (0,1 and 2) which correspond to the following sets of IP addresses:
+
+// 0 - the IP addresses of the abstract hosts which the concrete host 
+//     previously tried to configure
+// 1 - an IP address of an abstract host which the concrete host is 
+//     currently trying to configure
+// 2 - a fresh IP address which the concrete host is currently trying to configure
+
+// if the host picks an address that is being used it may end up picking another ip address
+// in which case there may still be messages corresponding to the old ip address
+// to be sent both from and to the host which the host should now disregard
+// (since it will never pick the same ip address)
+
+// to deal with this situation: when a host picks a new ip address we reconfigure the 
+// messages that are still be be sent or are being sent by changing the ip address to 0 
+// (an old ip address of the host)
+
+// all the messages from the abstract hosts for the 'old' address (in fact the
+// set of old addresses since it may have started again more than once)  
+// can arrive in any order since they are equivalent to the host - it ignores then all
+
+// also the messages for the old and new address will come from different hosts
+// (the ones with that ip address) which we model by allowing them to arrive in any order
+// i.e. not neccessarily in the order they where sent
+
+//-------------------------------------------------------------
+// model is an pta
+pta
+
+//-------------------------------------------------------------
+// VARIABLES
+const int N=1000; // number of abstract hosts
+const int K=2; // number of probes to send
+const double loss = 0.1; // probability of message loss
+
+// PROBABILITIES
+const double old = N/65024; // 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
+// size of buffers for other hosts
+const int B0 = 20;  // buffer size for one abstract host
+const int B1 = 8;  // buffer sizes for all abstract hosts
+
+//-------------------------------------------------------------
+// ENVIRONMENT - models: medium, output buffer of concrete host and all other hosts
+module environment
+	
+	// buffer of concrete host
+	b_ip7 : [0..2]; // ip address of message in buffer position 8
+	b_ip6 : [0..2]; // ip address of message in buffer position 7
+	b_ip5 : [0..2]; // ip address of message in buffer position 6
+	b_ip4 : [0..2]; // ip address of message in buffer position 5
+	b_ip3 : [0..2]; // ip address of message in buffer position 4
+	b_ip2 : [0..2]; // ip address of message in buffer position 3
+	b_ip1 : [0..2]; // ip address of message in buffer position 2
+	b_ip0 : [0..2]; // ip address of message in buffer position 1
+	n : [0..8]; // number of places in the buffer used (from host)
+	
+	// messages to be sent from abstract hosts to concrete host
+	n0  : [0..B0]; // number of messages which do not have the host's current ip address
+	n1  : [0..B1]; // number of messages which have the host's current ip address
+	
+	b : [0..2]; // local state
+	// 0 - idle
+	// 1 - sending message from concrete host 
+	// 2 - sending message from abstract host
+	
+	z : clock; // clock of environment (needed for the time to send a message)
+	
+	ip_mess : [0..2]; // ip in the current message being sent
+	// 0 - different from concrete host
+	// 1 - same as the concrete host and in use
+	// 2 - same as the concrete host and not in use
+
+	invariant
+		(b=0 & n=0 & n0=0 & n1=0 => true) & // nothing to send
+		(b=0 & !(n=0 & n0=0 & n1=0) => z<=0) & // something to send
+		(b>0 => z<=1) // sending
+	endinvariant
+	
+	// RESET/RECONFIG: when host is about to choose new ip address
+	// suppose that the host cannot choose the same ip address
+	// (since happens with very small probability). 
+	// Therefore all messages will have a different ip address, 
+	// i.e. all n1 messages become n0 ones.
+	// Note this include any message currently being sent (ip is set to zero 0)
+	[reset] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers 
+	               & (ip_mess'=0) // message being set
+	               & (n'=(reset)?0:n) // concrete buffer (remove this update to get NO_RESET model)
+	               & (b_ip7'=0) 
+	               & (b_ip6'=0) 
+	               & (b_ip5'=0) 
+	               & (b_ip4'=0) 
+	               & (b_ip3'=0) 
+	               & (b_ip2'=0) 
+	               & (b_ip1'=0) 
+	               & (b_ip0'=0);
+	// note: prevent anything else from happening when reconfiguration needs to take place
+	
+	// get messages to be sent (so message has same ip address as host)
+	[send1] n=0 -> (b_ip0'=1) & (n'=n+1);
+	[send1] n=1 -> (b_ip1'=1) & (n'=n+1);
+	[send1] n=2 -> (b_ip2'=1) & (n'=n+1);
+	[send1] n=3 -> (b_ip3'=1) & (n'=n+1);
+	[send1] n=4 -> (b_ip4'=1) & (n'=n+1);
+	[send1] n=5 -> (b_ip5'=1) & (n'=n+1);
+	[send1] n=6 -> (b_ip6'=1) & (n'=n+1);
+	[send1] n=7 -> (b_ip7'=1) & (n'=n+1);
+	[send1] n=8 -> (n'=n); // buffer full so lose message
+
+	[send2] n=0 -> (b_ip0'=2) & (n'=n+1);
+	[send2] n=1 -> (b_ip1'=2) & (n'=n+1);
+	[send2] n=2 -> (b_ip2'=2) & (n'=n+1);
+	[send2] n=3 -> (b_ip3'=2) & (n'=n+1);
+	[send2] n=4 -> (b_ip4'=2) & (n'=n+1);
+	[send2] n=5 -> (b_ip5'=2) & (n'=n+1);
+	[send2] n=6 -> (b_ip6'=2) & (n'=n+1);
+	[send2] n=7 -> (b_ip7'=2) & (n'=n+1);
+	[send2] n=8 -> (n'=n); // buffer full so lose message
+	
+	// start sending message from host
+	[a] b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0) 
+	                                & (n'=n-1)
+	                                & (b_ip7'=0) 
+	                                & (b_ip6'=b_ip7) 
+	                                & (b_ip5'=b_ip6) 
+	                                & (b_ip4'=b_ip5) 
+	                                & (b_ip3'=b_ip4) 
+	                                & (b_ip2'=b_ip3) 
+	                                & (b_ip1'=b_ip2) 
+	                                & (b_ip0'=b_ip1) // send message
+	                         + loss : (n'=n-1)
+	                                & (b_ip7'=0) 
+	                                & (b_ip6'=b_ip7) 
+	                                & (b_ip5'=b_ip6) 
+	                                & (b_ip4'=b_ip5) 
+	                                & (b_ip3'=b_ip4) 
+	                                & (b_ip2'=b_ip3) 
+	                                & (b_ip1'=b_ip2) 
+	                                & (b_ip0'=b_ip1); // lose message
+	
+	// start sending message to host
+	[a] b=0 & n0>0 -> (1-loss) : (b'=2) & (ip_mess'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip
+	[a] b=0 & n1>0 -> (1-loss) : (b'=2) & (ip_mess'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip
+	
+	// finish sending message from host
+	[a] b=1 & ip_mess=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip_mess'=0);
+	[a] b=1 & ip_mess=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip_mess'=0);
+	[a] b=1 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0);
+	
+	// finish sending message to host
+	[rec0] b=2 & ip_mess=0 -> (b'=0) & (z'=0) & (ip_mess'=0);
+	[rec1] b=2 & ip_mess=1 -> (b'=0) & (z'=0) & (ip_mess'=0);
+	[rec2] b=2 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0);
+	
+endmodule
+
+//-------------------------------------------------------------
+// CONCRETE HOST
+module host0
+	
+	x : clock; // first clock of the host
+	y : clock; // 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
+	
+	invariant
+		(l=0 => x<=0) & 
+		(l=1 & coll<MAXCOLL => x<=0) & 
+		(l=1 & coll=MAXCOLL => x<=LONGWAIT) & 
+		(l=2 => x<=CONSEC) & 
+		(l=3 => x<=CONSEC) &
+		(l=4 => true) 
+	endinvariant
+
+	// needed to prevent environment from moving before a reset
+	[a] l>0 -> true;
+
+	// 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)
+	[rec2] (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)
+	[]     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 
+	// send probe
+	[send1] l=2 & ip=1 & probes<K & x>=2 -> (x'=0) & (probes'=probes+1);
+	[send2] l=2 & ip=2 & probes<K & x>=2 -> (x'=0) & (probes'=probes+1);
+	// sent K probes and waited 2 seconds
+	[] l=2 & probes=K & x>=2 -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0);
+	// get message and ip does not match: ignore
+	[rec0] l=2 & 0!=ip -> (l'=l);
+	[rec1] l=2 & 1!=ip -> (l'=l);
+	[rec2] l=2 & 2!=ip -> (l'=l);
+	// get a message with matching ip: reconfigure
+	[rec0] l=2 & 0=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
+	[rec1] l=2 & 1=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
+	[rec2] l=2 & 2=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
+	
+	// receive message and same ip: defend
+	[rec0] l=3 & mess=0 & 0=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
+	[rec1] l=3 & mess=0 & 1=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
+	[rec2] l=3 & mess=0 & 2=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
+	// receive message and same ip: defer
+	[rec0] l=3 & mess=0 & 0=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
+	[rec1] l=3 & mess=0 & 1=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
+	[rec2] l=3 & mess=0 & 2=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
+	// receive message and different ip
+	[rec0] l=3 & mess=0 & 0!=ip -> (l'=l);
+	[rec1] l=3 & mess=0 & 1!=ip -> (l'=l);
+	[rec2] l=3 & mess=0 & 2!=ip -> (l'=l);
+	
+	// send probe reply or message for defence
+	[send1] l=3 & mess=1 & ip=1 -> (mess'=0);
+	[send2] l=3 & mess=1 & ip=2 -> (mess'=0);
+	// send first gratuitous arp message
+	[send1] l=3 & mess=0 & probes<1 & ip=1 & x>=CONSEC -> (x'=0) & (probes'=probes+1);
+	[send2] l=3 & mess=0 & probes<1 & ip=2 & x>=CONSEC -> (x'=0) & (probes'=probes+1);
+	// send second gratuitous arp message (move to use)
+	[send1] l=3 & mess=0 & probes=1 & ip=1 & x>=CONSEC -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
+	[send2] l=3 & mess=0 & probes=1 & ip=2 & x>=CONSEC -> (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
+
+//-------------------------------------------------------------
+rewards "time"
+	true : 1;
+endrewards
+
+label "done" = l=4;
+label "done_error" = l=4 & ip=0;
+label "done_fresh" = l=4 & ip=1;
+
--- a/prism-examples/pta/zeroconf/zeroconf-full.pctl
+++ b/prism-examples/pta/zeroconf/zeroconf-full.pctl
@ -0,0 +1,3 @@
+Pmin=?[F "done"]
+Pmin=?[F "done_fresh"]
+Pmax=?[F "done_error"]
--- a/prism-examples/pta/zeroconf/zeroconf-full4.nm
+++ b/prism-examples/pta/zeroconf/zeroconf-full4.nm
@ -0,0 +1,277 @@
+// IPv4: PTA model with digitial clocks
+// one concrete host attempting to choose an ip address 
+// when a number of (abstract) hosts have already got ip addresses
+// gxn/dxp/jzs 02/05/03
+
+// reset or noreset model
+const bool reset=true;
+
+//-------------------------------------------------------------
+
+// we suppose that
+// - the abstract hosts have already picked their addresses 
+//   and always defend their addresses
+// - the concrete host never picks the same ip address twice 
+//   (this can happen only with a verys small probability)
+
+// under these assumptions we do not need message types because:
+// 1) since messages to the concrete host will never be a probe, 
+//    this host will react to all messages in the same way
+// 2) since the abstract hosts always defend their addresses, 
+//    all messages from the host will get an arp reply if the ip matches
+
+// following from the above assumptions we require only three abstract IP addresses
+// (0,1 and 2) which correspond to the following sets of IP addresses:
+
+// 0 - the IP addresses of the abstract hosts which the concrete host 
+//     previously tried to configure
+// 1 - an IP address of an abstract host which the concrete host is 
+//     currently trying to configure
+// 2 - a fresh IP address which the concrete host is currently trying to configure
+
+// if the host picks an address that is being used it may end up picking another ip address
+// in which case there may still be messages corresponding to the old ip address
+// to be sent both from and to the host which the host should now disregard
+// (since it will never pick the same ip address)
+
+// to deal with this situation: when a host picks a new ip address we reconfigure the 
+// messages that are still be be sent or are being sent by changing the ip address to 0 
+// (an old ip address of the host)
+
+// all the messages from the abstract hosts for the 'old' address (in fact the
+// set of old addresses since it may have started again more than once)  
+// can arrive in any order since they are equivalent to the host - it ignores then all
+
+// also the messages for the old and new address will come from different hosts
+// (the ones with that ip address) which we model by allowing them to arrive in any order
+// i.e. not neccessarily in the order they where sent
+
+//-------------------------------------------------------------
+// model is an pta
+pta
+
+//-------------------------------------------------------------
+// VARIABLES
+const int N=1000; // number of abstract hosts
+const int K=2; // number of probes to send
+const double loss = 0.1; // probability of message loss
+
+// PROBABILITIES
+const double old = N/65024; // 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
+// size of buffers for other hosts
+//const int B0 = 20;  // buffer size for one abstract host
+//const int B1 = 8;  // buffer sizes for all abstract hosts
+const int B0 = 4;  // buffer size for one abstract host
+const int B1 = 4;  // buffer sizes for all abstract hosts
+
+//-------------------------------------------------------------
+// ENVIRONMENT - models: medium, output buffer of concrete host and all other hosts
+module environment
+	
+	// buffer of concrete host
+	b_ip3 : [0..2]; // ip address of message in buffer position 4
+	b_ip2 : [0..2]; // ip address of message in buffer position 3
+	b_ip1 : [0..2]; // ip address of message in buffer position 2
+	b_ip0 : [0..2]; // ip address of message in buffer position 1
+	n : [0..4]; // number of places in the buffer used (from host)
+	
+	// messages to be sent from abstract hosts to concrete host
+	n0  : [0..B0]; // number of messages which do not have the host's current ip address
+	n1  : [0..B1]; // number of messages which have the host's current ip address
+	
+	b : [0..2]; // local state
+	// 0 - idle
+	// 1 - sending message from concrete host 
+	// 2 - sending message from abstract host
+	
+	z : clock; // clock of environment (needed for the time to send a message)
+	
+	ip_mess : [0..2]; // ip in the current message being sent
+	// 0 - different from concrete host
+	// 1 - same as the concrete host and in use
+	// 2 - same as the concrete host and not in use
+
+	invariant
+		(b=0 & n=0 & n0=0 & n1=0 => true) & // nothing to send
+		(b=0 & !(n=0 & n0=0 & n1=0) => z<=0) & // something to send
+		(b>0 => z<=1) // sending
+	endinvariant
+	
+	// RESET/RECONFIG: when host is about to choose new ip address
+	// suppose that the host cannot choose the same ip address
+	// (since happens with very small probability). 
+	// Therefore all messages will have a different ip address, 
+	// i.e. all n1 messages become n0 ones.
+	// Note this include any message currently being sent (ip is set to zero 0)
+	[reset] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers 
+	               & (ip_mess'=0) // message being set
+	               & (n'=(reset)?0:n) // concrete buffer (remove this update to get NO_RESET model)
+	               & (b_ip3'=0) 
+	               & (b_ip2'=0) 
+	               & (b_ip1'=0) 
+	               & (b_ip0'=0);
+	// note: prevent anything else from happening when reconfiguration needs to take place
+	
+	// get messages to be sent (so message has same ip address as host)
+	[send1] n=0 -> (b_ip0'=1) & (n'=n+1);
+	[send1] n=1 -> (b_ip1'=1) & (n'=n+1);
+	[send1] n=2 -> (b_ip2'=1) & (n'=n+1);
+	[send1] n=3 -> (b_ip3'=1) & (n'=n+1);
+	[send1] n=4 -> (n'=n); // buffer full so lose message
+
+	[send2] n=0 -> (b_ip0'=2) & (n'=n+1);
+	[send2] n=1 -> (b_ip1'=2) & (n'=n+1);
+	[send2] n=2 -> (b_ip2'=2) & (n'=n+1);
+	[send2] n=3 -> (b_ip3'=2) & (n'=n+1);
+	[send2] n=4 -> (n'=n); // buffer full so lose message
+	
+	// start sending message from host
+	[a] b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0) 
+	                                & (n'=n-1)
+	                                & (b_ip3'=0) 
+	                                & (b_ip2'=b_ip3) 
+	                                & (b_ip1'=b_ip2) 
+	                                & (b_ip0'=b_ip1) // send message
+	                         + loss : (n'=n-1)
+	                                & (b_ip3'=0) 
+	                                & (b_ip2'=b_ip3) 
+	                                & (b_ip1'=b_ip2) 
+	                                & (b_ip0'=b_ip1); // lose message
+	
+	// start sending message to host
+	[a] b=0 & n0>0 -> (1-loss) : (b'=2) & (ip_mess'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip
+	[a] b=0 & n1>0 -> (1-loss) : (b'=2) & (ip_mess'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip
+	
+	// finish sending message from host
+	[a] b=1 & ip_mess=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip_mess'=0);
+	[a] b=1 & ip_mess=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip_mess'=0);
+	[a] b=1 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0);
+	
+	// finish sending message to host
+	[rec0] b=2 & ip_mess=0 -> (b'=0) & (z'=0) & (ip_mess'=0);
+	[rec1] b=2 & ip_mess=1 -> (b'=0) & (z'=0) & (ip_mess'=0);
+	[rec2] b=2 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0);
+	
+endmodule
+
+//-------------------------------------------------------------
+// CONCRETE HOST
+module host0
+	
+	x : clock; // first clock of the host
+	y : clock; // 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
+	
+	invariant
+		(l=0 => x<=0) & 
+		(l=1 & coll<MAXCOLL => x<=0) & 
+		(l=1 & coll=MAXCOLL => x<=LONGWAIT) & 
+		(l=2 => x<=CONSEC) & 
+		(l=3 => x<=CONSEC) &
+		(l=4 => true) 
+	endinvariant
+
+	// needed to prevent environment from moving before a reset
+	[a] l>0 -> true;
+
+	// 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)
+	[rec2] (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)
+	[]     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 
+	// send probe
+	[send1] l=2 & ip=1 & probes<K & x>=2 -> (x'=0) & (probes'=probes+1);
+	[send2] l=2 & ip=2 & probes<K & x>=2 -> (x'=0) & (probes'=probes+1);
+	// sent K probes and waited 2 seconds
+	[] l=2 & probes=K & x>=2 -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0);
+	// get message and ip does not match: ignore
+	[rec0] l=2 & 0!=ip -> (l'=l);
+	[rec1] l=2 & 1!=ip -> (l'=l);
+	[rec2] l=2 & 2!=ip -> (l'=l);
+	// get a message with matching ip: reconfigure
+	[rec0] l=2 & 0=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
+	[rec1] l=2 & 1=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
+	[rec2] l=2 & 2=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
+	
+	// receive message and same ip: defend
+	[rec0] l=3 & mess=0 & 0=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
+	[rec1] l=3 & mess=0 & 1=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
+	[rec2] l=3 & mess=0 & 2=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
+	// receive message and same ip: defer
+	[rec0] l=3 & mess=0 & 0=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
+	[rec1] l=3 & mess=0 & 1=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
+	[rec2] l=3 & mess=0 & 2=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
+	// receive message and different ip
+	[rec0] l=3 & mess=0 & 0!=ip -> (l'=l);
+	[rec1] l=3 & mess=0 & 1!=ip -> (l'=l);
+	[rec2] l=3 & mess=0 & 2!=ip -> (l'=l);
+	
+	// send probe reply or message for defence
+	[send1] l=3 & mess=1 & ip=1 -> (mess'=0);
+	[send2] l=3 & mess=1 & ip=2 -> (mess'=0);
+	// send first gratuitous arp message
+	[send1] l=3 & mess=0 & probes<1 & ip=1 & x>=CONSEC -> (x'=0) & (probes'=probes+1);
+	[send2] l=3 & mess=0 & probes<1 & ip=2 & x>=CONSEC -> (x'=0) & (probes'=probes+1);
+	// send second gratuitous arp message (move to use)
+	[send1] l=3 & mess=0 & probes=1 & ip=1 & x>=CONSEC -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
+	[send2] l=3 & mess=0 & probes=1 & ip=2 & x>=CONSEC -> (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
+
+//-------------------------------------------------------------
+rewards "time"
+	true : 1;
+endrewards
+
+label "done" = l=4;
+label "done_error" = l=4 & ip=0;
+label "done_fresh" = l=4 & ip=1;
+
--- a/prism-examples/pta/zeroconf/zeroconf-simple.nm
+++ b/prism-examples/pta/zeroconf/zeroconf-simple.nm
@ -0,0 +1,79 @@
+pta
+
+module sender
+	sender : [0..12] init 0;
+	// 0 - reconf
+	// 1 used0
+	// 2 used1
+	// 3 used2
+	// 4 used3
+	// 5 used_wait
+	// 6 used_use
+	// 7 fresh0
+	// 8 fresh1
+	// 9 fresh2
+	// 10 fresh3
+	// 11 fresh_wait
+	// 12 fresh_use
+
+	x : clock;
+
+	invariant
+			(sender=0 => x<=0) &
+			(sender>=1 & sender<=10 => x<=20) &
+			(sender>10 => true)
+	endinvariant
+
+	// reconfiguring
+	[] sender=0 ->0.5 : (sender'=1) + 0.5 : (sender'=7);
+	[recv] sender=1  -> (sender'=0) & (x'=0);
+	[recv] sender=2  -> (sender'=0) & (x'=0);
+	[recv] sender=3  -> (sender'=0) & (x'=0);
+	[recv] sender=4  -> (sender'=0) & (x'=0);
+	[recv] sender=5  -> (sender'=0) & (x'=0);
+	[recv] sender=7  -> (sender'=0) & (x'=0);
+	[recv] sender=8  -> (sender'=0) & (x'=0);
+	[recv] sender=9  -> (sender'=0) & (x'=0);
+	[recv] sender=10 -> (sender'=0) & (x'=0);
+	[recv] sender=11 -> (sender'=0) & (x'=0);
+
+	// sending fresh
+	[send_used] sender=1 & x>=20 -> (sender'=2) & (x'=0);
+	[send_used] sender=2 & x>=20 -> (sender'=3) & (x'=0);
+	[send_used] sender=3 & x>=20 -> (sender'=4) & (x'=0);
+	[send_used] sender=4 & x>=20 -> (sender'=5) & (x'=0);
+	// sending used
+	[send_fresh] sender=7 & x>=20 -> (sender'=8) & (x'=0);
+	[send_fresh] sender=8 & x>=20 -> (sender'=9) & (x'=0);
+	[send_fresh] sender=9 & x>=20 -> (sender'=10) & (x'=0);
+	[send_fresh] sender=10 & x>=20 -> (sender'=11) & (x'=0);
+
+	// finished
+	[] sender=5  & x>=20 -> (sender'=6) & (x'=0);
+	[] sender=11 & x>=20 -> (sender'=12) & (x'=0);
+	[] sender=6 -> (sender'=6);
+	[] sender=12 -> (sender'=12);
+
+endmodule
+
+module environment
+
+	env : [0..2] init 0;
+	// 0,1,2 - ready,send,reply
+
+	y : clock;
+
+	invariant
+			(env=0 => true) &
+			(env>=1 => y<=5)
+	endinvariant
+
+	[send_fresh] env=0 -> true;
+	[send_used] env=0 -> 0.1 : (env'=0) & (y'=0) + 0.9 : (env'=1) & (y'=0);
+	[] env=1  & y>=1 ->  0.1 : (env'=0) & (y'=0) + 0.9 : (env'=2) & (y'=0);
+	[recv] env=2 & y>=1 -> (env'=0) & (y'=0);
+
+endmodule
+
+label "incorrect" = sender=6;
+
--- a/prism-examples/pta/zeroconf/zeroconf.nm
+++ b/prism-examples/pta/zeroconf/zeroconf.nm
@ -0,0 +1,56 @@
+// prism model of pta version of zeroconf
+// using digitial clocks
+
+pta
+
+module sender
+
+	s : [0..2]; //local state
+	probes : [0..4]; // probes sent
+	ip : [0..2]; // ip address not chosen, fresh or in use
+	x : clock; // local clock
+
+	invariant
+	(s=0 => x<=0) &
+	(s=1 => x<=20) &
+	(s=2 => true)
+	endinvariant
+
+	// selct probe	
+	// [] s=0 -> 0.99969242125984251969 : (s'=1) & (ip'=0) + 0.00030757874015748031 : (s'=1) & (ip'=1);
+	[] s=0 -> 0.5 : (s'=1) & (ip'=1) + 0.5 : (s'=1) & (ip'=2);
+	// send probes
+	[send_used]  s=1 & x=20 & ip=2 & probes<4 -> (probes'=probes+1) & (x'=0);	
+	[send_fresh] s=1 & x=20 & ip=1 & probes<4 -> (probes'=probes+1) & (x'=0);
+	[] s=1 & x=20 & probes=4 -> (s'=2) & (x'=0);
+	[recv] s=1 -> (s'=0) & (x'=0) & (ip'=0) & (probes'=0);
+	[] s=2 -> true;
+
+endmodule
+
+module environment
+	
+	e : [0..2]; // ready, send reply
+	y : clock;
+
+	invariant
+	(e=0 => true) &
+	(e>=1 => y<=5)
+	endinvariant
+
+	[send_fresh] e=0 -> true;
+	[send_used]  e=0 -> 0.1 : (e'=0) & (y'=0) + 0.9 : (e'=1) & (y'=0);
+	[] e=1 & y>=1 -> 0.1 : (e'=0) & (y'=0) + 0.9 : (e'=2) & (y'=0);
+	[recv] e=2 & y>=1 -> (e'=0) & (y'=0);
+
+endmodule
+
+
+// time
+rewards "time"
+	true : 1;
+endrewards
+
+label "incorrect" = s=2 & ip=2;
+label "done" = s=2;
+