fixes to brp model

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@897 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism-examples/brp/brp.pctl

@@ -1,19 +1,21 @@
 // properties taken from [D'AJJL01]
 
 // property A
-P=? [ true U srep=1 & rrep=3 & recv ]
+P=? [ true U srep=1 & rrep=3 & recv ];
 
 // property B
-P=? [ true U srep=3 & !(rrep=3) & recv ]
+P=? [ true U srep=3 & !(rrep=3) & recv ];
 
 // property 1
-P=? [ true U s=5 & T ]
+P=? [ true U s=5 ];
 
 // property 2
-P=? [ true U s=5 & T & srep=2 ]
+P=? [ true U s=5 & srep=2 ];
 
 // property 3
-P=? [ true U s=5 & T & srep=1 & i>8 ]
+P=? [ true U s=5 & srep=1 & i>8 ];
 
 // property 4
-P=? [ true U !(srep=0) & T & !recv ]
+P=? [ true U !(srep=0) & !recv ];
+// rewards
+R=? [ F "deadlock" ];

prism-examples/brp/brp.pm

@@ -95,11 +95,10 @@ module receiver
 	
 endmodule
 	
-module checker
+module checker // prevents more than one frame being set
 
 	T : bool;
 	
-//	[NewFile] (T=false) -> (T'=false);
 	[NewFile] (T=false) -> (T'=true);
 	
 endmodule
@@ -128,4 +127,8 @@ module	channelL
 	// lost
 	[TO_Ack] (l=2) -> (l'=0);
 	
-endmodule
+endmodule
+
+rewards
+	[aF] i=1 : 1;
+endrewards