Merge branch 'future' into python_api

Former-commit-id: 702e62dece
9 years ago · e3d4a3c019
2 changed files with 194 additions and 0 deletions
--- a/test/performance/builder/leader5.nm
+++ b/test/performance/builder/leader5.nm
@ -1,3 +1,4 @@
+<<<<<<< HEAD
 // asynchronous leader election
 // 4 processes
 // gxn/dxp 29/01/01
@ -96,3 +97,103 @@ endrewards
 formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0);
 label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4;

+=======
+// asynchronous leader election
+// 4 processes
+// gxn/dxp 29/01/01
+
+mdp
+
+const int N= 5; // number of processes
+
+//----------------------------------------------------------------------------------------------------------------------------
+module process1
+	
+	// COUNTER
+	c1 : [0..5-1];
+	
+	// STATES
+	s1 : [0..4];
+	// 0  make choice
+	// 1 have not received neighbours choice
+	// 2 active
+	// 3 inactive
+	// 4 leader
+	
+	// PREFERENCE
+	p1 : [0..1];
+	
+	// VARIABLES FOR SENDING AND RECEIVING
+	receive1 : [0..2];
+	// not received anything
+	// received choice
+	// received counter
+	sent1 : [0..2];
+	// not send anything
+	// sent choice
+	// sent counter
+	
+	// pick value
+	[] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1);
+	
+	// send preference
+	[p12] (s1=1) & (sent1=0) -> (sent1'=1);
+	// receive preference
+	// stay active
+	[p51] (s1=1) & (receive1=0) & !( (p1=0) & (p5=1) ) -> (s1'=2) & (receive1'=1);
+	// become inactive
+	[p51] (s1=1) & (receive1=0) & (p1=0) & (p5=1) -> (s1'=3) & (receive1'=1);
+	
+	// send preference (can now reset preference)
+	[p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0);
+	// send counter (already sent preference)
+	// not received counter yet
+	[c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2);
+	// received counter (pick again)
+	[c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	
+	// receive counter and not sent yet (note in this case do not pass it on as will send own counter)
+	[c51] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2);
+	// receive counter and sent counter
+	// only active process (decide)
+	[c51] (s1=2) & (receive1=1) & (sent1=2) & (c5=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	// other active process (pick again)
+	[c51] (s1=2) & (receive1=1) & (sent1=2) & (c5<N-1) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	
+	// send preference (must have received preference) and can now reset
+	[p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0);
+	// send counter (must have received counter first) and can now reset
+	[c12] (s1=3) & (receive1=2) & (sent1=1) ->  (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	
+	// receive preference
+	[p51] (s1=3) & (receive1=0) -> (p1'=p5) & (receive1'=1);
+	// receive counter
+	[c51] (s1=3) & (receive1=1) & (c5<N-1) -> (c1'=c5+1) & (receive1'=2);
+		
+	// done
+	[done] (s1=4) -> (s1'=s1);
+	// add loop for processes who are inactive
+	[done] (s1=3) -> (s1'=s1);
+
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// construct further stations through renaming
+module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p51=p12,c12=c23,c51=c12,p5=p1,c5=c1] endmodule
+module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p51=p23,c12=c34,c51=c23,p5=p2,c5=c2] endmodule
+module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p51=p34,c12=c45,c51=c34,p5=p3,c5=c3] endmodule
+module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p51,p51=p45,c12=c51,c51=c45,p5=p4,c5=c4] endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// reward - expected number of rounds (equals the number of times a process receives a counter)
+rewards "rounds"
+	[c12] true : 1;
+endrewards
+
+//----------------------------------------------------------------------------------------------------------------------------
+formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0);
+label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4;
+
+>>>>>>> 90d2b218a044edca8062084ee89d171695149c1e
--- a/test/performance/builder/leader5_8.pm
+++ b/test/performance/builder/leader5_8.pm
@ -1,3 +1,4 @@
+<<<<<<< HEAD
 // synchronous leader election protocol  (itai & Rodeh)
 // dxp/gxn 25/01/01

@ -88,3 +89,95 @@ endrewards
 // labels
 label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3;

+=======
+// synchronous leader election protocol  (itai & Rodeh)
+// dxp/gxn 25/01/01
+
+dtmc
+
+// CONSTANTS
+const int N = 5; // number of processes
+const int K = 8; // range of probabilistic choice
+
+// counter module used to count the number of processes that have been read
+// and to know when a process has decided
+module counter
+	
+	// counter (c=i  means process j reading process (i-1)+j next)
+	c : [1..N-1];
+	
+	// reading
+	[read] c<N-1 -> (c'=c+1);
+	// finished reading
+	[read] c=N-1 -> (c'=c);
+	//decide
+	[done] u1|u2|u3|u4|u5 -> (c'=c);
+	// pick again reset counter 
+	[retry] !(u1|u2|u3|u4|u5) -> (c'=1);
+	// loop (when finished to avoid deadlocks)
+	[loop] s1=3 -> (c'=c);
+	
+endmodule
+
+//  processes form a ring and suppose:
+// process 1 reads process 2
+// process 2 reads process 3
+// process 3 reads process 1
+module process1
+	
+	// local state
+	s1 : [0..3];
+	// s1=0 make random choice
+	// s1=1 reading
+	// s1=2 deciding
+	// s1=3 finished
+	
+	// has a unique id so far (initially true)
+	u1 : bool;
+	
+	// value to be sent to next process in the ring (initially sets this to its own value)
+	v1 : [0..K-1];
+	
+	// random choice
+	p1 : [0..K-1];
+	
+	// pick value
+	[pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true);
+	// read
+	[read] s1=1 &  u1 & c<N-1 -> (u1'=(p1!=v2)) & (v1'=v2);
+	[read] s1=1 & !u1 & c<N-1 -> (u1'=false) & (v1'=v2) & (p1'=0);
+	// read and move to decide
+	[read] s1=1 &  u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0);
+	[read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0);
+	// deciding
+	// done
+	[done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0);
+	//retry
+	[retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0);
+	// loop (when finished to avoid deadlocks)
+	[loop] s1=3 -> (s1'=3);
+	
+endmodule
+
+// construct remaining processes through renaming
+module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule
+module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v4 ] endmodule
+module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v5 ] endmodule
+module process5 = process1 [ s1=s5,p1=p5,v1=v5,u1=u5,v2=v1 ] endmodule
+
+// expected number of rounds
+rewards "num_rounds"
+	[pick] true : 1;
+endrewards
+
+// labels
+label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3;
+
+>>>>>>> 90d2b218a044edca8062084ee89d171695149c1e