6 The Communication Network |
6 The Communication Network |
7 |
7 |
8 From Misra, "A Logic for Concurrent Programming" (1994), section 5.7 |
8 From Misra, "A Logic for Concurrent Programming" (1994), section 5.7 |
9 *) |
9 *) |
10 |
10 |
11 Network = UNITY + |
11 theory Network = UNITY: |
12 |
12 |
13 (*The state assigns a number to each process variable*) |
13 (*The state assigns a number to each process variable*) |
14 |
14 |
15 datatype pvar = Sent | Rcvd | Idle |
15 datatype pvar = Sent | Rcvd | Idle |
16 |
16 |
17 datatype pname = Aproc | Bproc |
17 datatype pname = Aproc | Bproc |
18 |
18 |
19 types state = "pname * pvar => nat" |
19 types state = "pname * pvar => nat" |
20 |
20 |
|
21 locale F_props = |
|
22 fixes F |
|
23 assumes rsA: "F : stable {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}" |
|
24 and rsB: "F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}" |
|
25 and sent_nondec: "F : stable {s. m <= s(proc,Sent)}" |
|
26 and rcvd_nondec: "F : stable {s. n <= s(proc,Rcvd)}" |
|
27 and rcvd_idle: "F : {s. s(proc,Idle) = Suc 0 & s(proc,Rcvd) = m} |
|
28 co {s. s(proc,Rcvd) = m --> s(proc,Idle) = Suc 0}" |
|
29 and sent_idle: "F : {s. s(proc,Idle) = Suc 0 & s(proc,Sent) = n} |
|
30 co {s. s(proc,Sent) = n}" |
|
31 |
|
32 |
|
33 lemmas (in F_props) |
|
34 sent_nondec_A = sent_nondec [of _ Aproc] |
|
35 and sent_nondec_B = sent_nondec [of _ Bproc] |
|
36 and rcvd_nondec_A = rcvd_nondec [of _ Aproc] |
|
37 and rcvd_nondec_B = rcvd_nondec [of _ Bproc] |
|
38 and rcvd_idle_A = rcvd_idle [of Aproc] |
|
39 and rcvd_idle_B = rcvd_idle [of Bproc] |
|
40 and sent_idle_A = sent_idle [of Aproc] |
|
41 and sent_idle_B = sent_idle [of Bproc] |
|
42 |
|
43 and rs_AB = stable_Int [OF rsA rsB] |
|
44 and sent_nondec_AB = stable_Int [OF sent_nondec_A sent_nondec_B] |
|
45 and rcvd_nondec_AB = stable_Int [OF rcvd_nondec_A rcvd_nondec_B] |
|
46 and rcvd_idle_AB = constrains_Int [OF rcvd_idle_A rcvd_idle_B] |
|
47 and sent_idle_AB = constrains_Int [OF sent_idle_A sent_idle_B] |
|
48 and nondec_AB = stable_Int [OF sent_nondec_AB rcvd_nondec_AB] |
|
49 and idle_AB = constrains_Int [OF rcvd_idle_AB sent_idle_AB] |
|
50 and nondec_idle = constrains_Int [OF nondec_AB [unfolded stable_def] |
|
51 idle_AB] |
|
52 |
|
53 lemma (in F_props) |
|
54 shows "F : stable {s. s(Aproc,Idle) = Suc 0 & s(Bproc,Idle) = Suc 0 & |
|
55 s(Aproc,Sent) = s(Bproc,Rcvd) & |
|
56 s(Bproc,Sent) = s(Aproc,Rcvd) & |
|
57 s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}" |
|
58 apply (unfold stable_def) |
|
59 apply (rule constrainsI) |
|
60 apply (drule constrains_Int [OF rs_AB [unfolded stable_def] nondec_idle, |
|
61 THEN constrainsD], assumption) |
|
62 apply simp_all |
|
63 apply (blast intro!: order_refl del: le0, clarify) |
|
64 apply (subgoal_tac "s' (Aproc, Rcvd) = s (Aproc, Rcvd)") |
|
65 apply (subgoal_tac "s' (Bproc, Rcvd) = s (Bproc, Rcvd)") |
|
66 apply simp |
|
67 apply (blast intro: order_antisym le_trans eq_imp_le)+ |
|
68 done |
|
69 |
21 end |
70 end |