diff --git a/prism/examples/pta/brp/brp.pm b/prism/examples/pta/brp/brp.pm
index 0c6d75d1..eae82496 100644
--- a/prism/examples/pta/brp/brp.pm
+++ b/prism/examples/pta/brp/brp.pm
@@ -1,22 +1,21 @@
 // bounded retransmission protocol [D'AJJL01]
 // gxn/dxp 23/05/2001
 
-pta
-
+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;
+// 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;
 
 module sender
-
-	// clock of the sender
-	x : clock;
+
+	// clock of the sender
+	x : clock;
 
 	s : [0..6];
 	// 0 idle
@@ -37,9 +36,9 @@ module sender
 	s_ab : bool;
 	fs : bool;
 	ls : bool;
-
-	invariant
-		(s=2 => x<=TIME_OUT) // only wait until timeout
+
+	invariant
+		(s=2 => x<=TIME_OUT) // only wait until timeout
 	endinvariant
 	
 	// idle
@@ -115,12 +114,12 @@ module checker // prevents more than one frame being set
 endmodule
 
 module	channelK
-
+
 	xK : clock;
-	k : [0..1];
-
-	invariant
-		(k=1 => xK<=TD)
+	k : [0..1];
+
+	invariant
+		(k=1 => xK<=TD)
 	endinvariant
 	
 	// idle
@@ -131,12 +130,12 @@ module	channelK
 endmodule
 
 module	channelL
-
+
 	xL : clock;
-	l : [0..1];
-
-	invariant
-		(l=1 => xL<=TD)
+	l : [0..1];
+
+	invariant
+		(l=1 => xL<=TD)
 	endinvariant
 	
 	// idle
@@ -144,8 +143,8 @@ module	channelL
 	// sending
 	[aB] (l=1) & xL<=TD -> (l'=0) & (xL'=0);
 
-endmodule
-
-rewards
-	[aF] i=1 : 1;
+endmodule
+
+rewards
+	[aF] i=1 : 1;
 endrewards