1- /*
2- * abp.lmn -- Alternating Bit Protocol Model
3- *
4- * @author Masato Gocho
5- * @date 2008.10.20
6- *
7- * Property0: Respons
8- * Property1: Respons under the Strong Fairness
9- */
10-
11- % msg(Message, Bit).
12- sender{
13- mnum(1).
14- msg(0,0).
15- ackOK @@ exp(I,B), mnum(Max), ack(0,A) :- A=:=B,J=(I+1) mod Max, C=1-B |
16- msg(J,C), mnum(Max).
17- ackNG @@ exp(I,B), ack(0,A) :- A=\=B |
18- msg(I,B).
19- }.
20-
21- % ack(0, Ack) key(ExpectedBit).
22-
23- recver{
24- key(0).
25- bit_OK @@ key(K), msg(I,B) :- int(I), K=:=B, A=1-K |
26- key(A), ack(0,B).
27- bit_NG @@ key(K), msg(I,B) :- int(I), K=\=B, A=1-K |
28- key(K), ack(0,A).
29- }.
30-
31- % message channel
32- daemon{
33- msg_pass @@ msg(I,B) :- m2r(I,B).
34- msg_lost @@ msg(I,B) :- int(I), int(B) | .
35- // msg_err_ @@ msg(I,B) :- int(I), Z=1-B | m2r(I,Z).
36- ack_pass @@ ack(0,A) :- r2s(0,A).
37- ack_lost @@ ack(0,A) :- int(A) | .
38- // ack_err_ @@ ack(0,A) :- int(A), B=1-A | r2s(0,B).
39- }.
40-
41- % communication between processes
42- s_2_d @@ sender{$s,@s, msg(M,N)}, daemon{$d,@d} :- int(M),int(N) |
43- sender{$s,@s, exp(M,N)}, daemon{$d,@d, msg(M,N)}.
44- d_2_r @@ daemon{$d,@d, m2r(M,N)}, recver{$r,@r} :- int(M),int(N) |
45- recver{$r,@r, msg(M,N)}, daemon{$d,@d}.
46- r_2_d @@ recver{$r,@r, ack(0,A)}, daemon{$d,@d} :- int(A) |
47- daemon{$d,@d, ack(0,A)}, recver{$r,@r}.
48- d_2_s @@ daemon{$d,@d, r2s(0,A)}, sender{$s,@s} :- int(A) |
49- sender{$s,@s, ack(0,A)}, daemon{$d,@d}.
50- t_out @@ daemon{@d}, recver{key(K),@r}, sender{exp(M,N), mnum(Max), @s,$s[]}/ :- int(K),int(M),int(N),int(Max) |
1+ /*
2+ * abp.lmn -- Alternating Bit Protocol Model
3+ *
4+ * @author Masato Gocho
5+ * @date 2008.10.20
6+ *
7+ * Property0: Respons
8+ * Property1: Respons under the Strong Fairness
9+ */
10+
11+ % msg(Message, Bit).
12+ sender{
13+ mnum(10000).
14+ msg(0,0).
15+ ackOK @@ exp(I,B), mnum(Max), ack(0,A) :- A=:=B,J=(I+1) mod Max, C=1-B |
16+ msg(J,C), mnum(Max).
17+ ackNG @@ exp(I,B), ack(0,A) :- A=\=B |
18+ msg(I,B).
19+ }.
20+
21+ % ack(0, Ack) key(ExpectedBit).
22+
23+ recver{
24+ key(0).
25+ bit_OK @@ key(K), msg(I,B) :- int(I), K=:=B, A=1-K |
26+ key(A), ack(0,B).
27+ bit_NG @@ key(K), msg(I,B) :- int(I), K=\=B, A=1-K |
28+ key(K), ack(0,A).
29+ }.
30+
31+ % message channel
32+ daemon{
33+ msg_pass @@ msg(I,B) :- m2r(I,B).
34+ msg_lost @@ msg(I,B) :- int(I), int(B) | .
35+ // msg_err_ @@ msg(I,B) :- int(I), Z=1-B | m2r(I,Z).
36+ ack_pass @@ ack(0,A) :- r2s(0,A).
37+ ack_lost @@ ack(0,A) :- int(A) | .
38+ // ack_err_ @@ ack(0,A) :- int(A), B=1-A | r2s(0,B).
39+ }.
40+
41+ % communication between processes
42+ s_2_d @@ sender{$s,@s, msg(M,N)}, daemon{$d,@d} :- int(M),int(N) |
43+ sender{$s,@s, exp(M,N)}, daemon{$d,@d, msg(M,N)}.
44+ d_2_r @@ daemon{$d,@d, m2r(M,N)}, recver{$r,@r} :- int(M),int(N) |
45+ recver{$r,@r, msg(M,N)}, daemon{$d,@d}.
46+ r_2_d @@ recver{$r,@r, ack(0,A)}, daemon{$d,@d} :- int(A) |
47+ daemon{$d,@d, ack(0,A)}, recver{$r,@r}.
48+ d_2_s @@ daemon{$d,@d, r2s(0,A)}, sender{$s,@s} :- int(A) |
49+ sender{$s,@s, ack(0,A)}, daemon{$d,@d}.
50+ t_out @@ daemon{@d}, recver{key(K),@r}, sender{exp(M,N), mnum(Max), @s,$s[]}/ :- int(K),int(M),int(N),int(Max) |
5151 daemon{@d}, recver{key(K),@r}, sender{msg(M,N), mnum(Max), @s}.
0 commit comments