You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
128 lines
5.6 KiB
128 lines
5.6 KiB
// Lehmann-Rabin algorithm [LR82] (dining philosophers)
|
|
// we suppose an action takes 1 time unit
|
|
// an a process can wait at most K time units before making a transition
|
|
// gxn/dxp 01/02/00
|
|
|
|
mdp
|
|
|
|
// CONSTANTS
|
|
const K;
|
|
|
|
// COUNTER FORMULAE
|
|
// ci number of steps since process last moved
|
|
// removing trying and remainder states since
|
|
// these are controlled by the process not the adversary
|
|
|
|
// process can go if it does not stop one of the other processes round counter reaching n+1
|
|
// added complication if two processes counter equals n-1, then if neither makes a transition
|
|
// both reach n, and hence one must reach n+1 which we must disallow
|
|
|
|
formula can1 = !((c2=K) | (c3=K) | (c4=K) | ((c2=K-1) & (c3=K-1)) | ((c2=K-1) & (c4=K-1)) | ((c3=K-1) & (c4=K-1)) | ((c2=K-2) & (c3=K-2) & (c4=K-2)));
|
|
formula can2 = !((c1=K) | (c3=K) | (c4=K) | ((c1=K-1) & (c3=K-1)) | ((c1=K-1) & (c4=K-1)) | ((c3=K-1) & (c4=K-1)) | ((c1=K-2) & (c3=K-2) & (c4=K-2)));
|
|
formula can3 = !((c1=K) | (c2=K) | (c4=K) | ((c1=K-1) & (c2=K-1)) | ((c1=K-1) & (c4=K-1)) | ((c2=K-1) & (c4=K-1)) | ((c1=K-2) & (c2=K-2) & (c4=K-2)));
|
|
formula can4 = !((c1=K) | (c2=K) | (c3=K) | ((c1=K-1) & (c2=K-1)) | ((c1=K-1) & (c3=K-1)) | ((c2=K-1) & (c3=K-1)) | ((c1=K-2) & (c2=K-2) & (c3=K-2)));
|
|
|
|
// when a process moves the counters of the other processes increase
|
|
// but only when they are not in trying or remainder
|
|
|
|
formula count1 = (p1!=13) & (p1!=0);
|
|
formula count2 = (p2!=13) & (p2!=0);
|
|
formula count3 = (p3!=13) & (p3!=0);
|
|
formula count4 = (p4!=13) & (p4!=0);
|
|
formula ncount1 = (p1=13) | (p1=0);
|
|
formula ncount2 = (p2=13) | (p2=0);
|
|
formula ncount3 = (p3=13) | (p3=0);
|
|
formula ncount4 = (p4=13) | (p4=0);
|
|
|
|
module counter
|
|
|
|
c1 : [0..K];
|
|
c2 : [0..K];
|
|
c3 : [0..K];
|
|
c4 : [0..K];
|
|
|
|
// process 1 moves
|
|
[s1] can1 & ncount2 & ncount3 & ncount4 -> (c1'=0);
|
|
[s1] can1 & ncount2 & ncount3 & count4 -> (c1'=0) & (c4'=c4+1);
|
|
[s1] can1 & ncount2 & count3 & ncount4 -> (c1'=0) & (c3'=c3+1);
|
|
[s1] can1 & ncount2 & count3 & count4 -> (c1'=0) & (c3'=c3+1) & (c4'=c4+1);
|
|
[s1] can1 & count2 & ncount3 & ncount4 -> (c1'=0) & (c2'=c2+1);
|
|
[s1] can1 & count2 & ncount3 & count4 -> (c1'=0) & (c2'=c2+1) & (c4'=c4+1);
|
|
[s1] can1 & count2 & count3 & ncount4 -> (c1'=0) & (c2'=c2+1) & (c3'=c3+1);
|
|
[s1] can1 & count2 & count3 & count4 -> (c1'=0) & (c2'=c2+1) & (c3'=c3+1) & (c4'=c4+1);
|
|
// process 2 moves
|
|
[s2] can2 & ncount1 & ncount3 & ncount4 -> (c2'=0);
|
|
[s2] can2 & ncount1 & ncount3 & count4 -> (c2'=0) & (c4'=c4+1);
|
|
[s2] can2 & ncount1 & count3 & ncount4 -> (c2'=0) & (c3'=c3+1);
|
|
[s2] can2 & ncount1 & count3 & count4 -> (c2'=0) & (c3'=c3+1) & (c4'=c4+1);
|
|
[s2] can2 & count1 & ncount3 & ncount4 -> (c2'=0) & (c1'=c1+1);
|
|
[s2] can2 & count1 & ncount3 & count4 -> (c2'=0) & (c1'=c1+1) & (c4'=c4+1);
|
|
[s2] can2 & count1 & count3 & ncount4 -> (c2'=0) & (c1'=c1+1) & (c3'=c3+1);
|
|
[s2] can2 & count1 & count3 & count4 -> (c2'=0) & (c1'=c1+1) & (c3'=c3+1) & (c4'=c4+1);
|
|
// process 3 moves
|
|
[s3] can3 & ncount1 & ncount2 & ncount4 -> (c3'=0);
|
|
[s3] can3 & ncount1 & ncount2 & count4 -> (c3'=0) & (c4'=c4+1);
|
|
[s3] can3 & ncount1 & count2 & ncount4 -> (c3'=0) & (c2'=c2+1);
|
|
[s3] can3 & ncount1 & count2 & count4 -> (c3'=0) & (c2'=c2+1) & (c4'=c4+1);
|
|
[s3] can3 & count1 & ncount2 & ncount4 -> (c3'=0) & (c1'=c1+1);
|
|
[s3] can3 & count1 & ncount2 & count4 -> (c3'=0) & (c1'=c1+1) & (c4'=c4+1);
|
|
[s3] can3 & count1 & count2 & ncount4 -> (c3'=0) & (c1'=c1+1) & (c2'=c2+1);
|
|
[s3] can3 & count1 & count2 & count4 -> (c3'=0) & (c1'=c1+1) & (c2'=c2+1) & (c4'=c4+1);
|
|
// process 4 moves
|
|
[s4] can4 & ncount1 & ncount2 & ncount3 -> (c4'=0);
|
|
[s4] can4 & ncount1 & ncount2 & count3 -> (c4'=0) & (c3'=c3+1);
|
|
[s4] can4 & ncount1 & count2 & ncount3 -> (c4'=0) & (c2'=c2+1);
|
|
[s4] can4 & ncount1 & count2 & count3 -> (c4'=0) & (c2'=c2+1) & (c3'=c3+1);
|
|
[s4] can4 & count1 & ncount2 & ncount3 -> (c4'=0) & (c1'=c1+1);
|
|
[s4] can4 & count1 & ncount2 & count3 -> (c4'=0) & (c1'=c1+1) & (c3'=c3+1);
|
|
[s4] can4 & count1 & count2 & ncount3 -> (c4'=0) & (c1'=c1+1) & (c2'=c2+1);
|
|
[s4] can4 & count1 & count2 & count3 -> (c4'=0) & (c1'=c1+1) & (c2'=c2+1) & (c3'=c3+1);
|
|
|
|
endmodule
|
|
|
|
// PHILOSOPHER 1
|
|
// atomic formule
|
|
// left fork and right fork free resp.
|
|
formula lfree = p2>=0&p2<=4|p2=6|p2=11|p2=13;
|
|
formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=12|p3=13;
|
|
|
|
module phil1
|
|
|
|
p1 : [0..13];
|
|
|
|
[s1] (p1=0) -> (p1'=0); // try
|
|
[s1] (p1=0) -> (p1'=1);
|
|
[s1] (p1=1) -> 0.5 : (p1'=2) + 0.5 : (p1'=3); // flip
|
|
[s1] (p1=2) & lfree -> (p1'=4); // wl and l free
|
|
[s1] (p1=2) & !lfree -> (p1'=2); // wl and l taken
|
|
[s1] (p1=3) & rfree -> (p1'=5); // wr and r free
|
|
[s1] (p1=3) & !rfree -> (p1'=3); // wr and r taken
|
|
[s1] (p1=4) & rfree -> (p1'=8); // l and r free
|
|
[s1] (p1=4) & !rfree -> (p1'=6); // l and r taken
|
|
[s1] (p1=5) & lfree -> (p1'=8); // r and l free
|
|
[s1] (p1=5) & !lfree -> (p1'=7); // r and l taken
|
|
[s1] (p1=6) -> (p1'=1); // nr
|
|
[s1] (p1=7) -> (p1'=1); // nl
|
|
[s1] (p1=8) -> (p1'=9); // pre_crit
|
|
[s1] (p1=9) -> (p1'=10); // crit
|
|
[s1] (p1=10) -> (p1'=11); // exit
|
|
[s1] (p1=10) -> (p1'=12);
|
|
[s1] (p1=11) -> (p1'=13); // put down left first
|
|
[s1] (p1=12) -> (p1'=13); // put down right first
|
|
[s1] (p1=13) -> (p1'=0); // remainder
|
|
[s1] (p1=13) -> (p1'=13);
|
|
|
|
endmodule
|
|
|
|
// construct further processes through renaming
|
|
module phil2=phil1 [p1=p2, p2=p3, p3=p4, p4=p1, s1=s2] endmodule
|
|
module phil3=phil1 [p1=p3, p2=p4, p3=p1, p4=p2, s1=s3] endmodule
|
|
module phil4=phil1 [p1=p4, p2=p1, p3=p2, p4=p3, s1=s4] endmodule
|
|
|
|
// reward structure - number of steps
|
|
rewards "steps"
|
|
[s1] true : 1;
|
|
[s2] true : 1;
|
|
[s3] true : 1;
|
|
[s4] true : 1;
|
|
endrewards
|