7 Logic Image: TLA |
7 Logic Image: TLA |
8 |
8 |
9 Lamport's "increment" example. |
9 Lamport's "increment" example. |
10 *) |
10 *) |
11 |
11 |
12 Inc = TLA + Nat + Pcount + |
12 Inc = TLA + Nat + |
|
13 |
|
14 (* program counter as an enumeration type *) |
|
15 datatype pcount = a | b | g |
13 |
16 |
14 consts |
17 consts |
15 (* program variables *) |
18 (* program variables *) |
16 x,y,sem :: "nat stfun" |
19 x,y,sem :: nat stfun |
17 pc1,pc2 :: "pcount stfun" |
20 pc1,pc2 :: pcount stfun |
18 |
21 |
19 (* names of actions and predicates *) |
22 (* names of actions and predicates *) |
20 M1,M2,N1,N2 :: "action" |
23 M1,M2,N1,N2 :: action |
21 alpha1,alpha2,beta1,beta2,gamma1,gamma2 :: "action" |
24 alpha1,alpha2,beta1,beta2,gamma1,gamma2 :: action |
22 InitPhi, InitPsi :: "action" |
25 InitPhi, InitPsi :: stpred |
23 PsiInv,PsiInv1,PsiInv2,PsiInv3 :: "action" |
26 PsiInv,PsiInv1,PsiInv2,PsiInv3 :: stpred |
24 |
27 |
25 (* temporal formulas *) |
28 (* temporal formulas *) |
26 Phi, Psi :: "temporal" |
29 Phi, Psi :: temporal |
27 |
30 |
28 rules |
31 rules |
29 (* the "base" variables, required to compute enabledness predicates *) |
32 (* the "base" variables, required to compute enabledness predicates *) |
30 Inc_base "base_var <x, y, sem, pc1, pc2>" |
33 Inc_base "basevars (x, y, sem, pc1, pc2)" |
31 |
34 |
32 (* definitions for high-level program *) |
35 (* definitions for high-level program *) |
33 InitPhi_def "InitPhi == ($x .= # 0) .& ($y .= # 0)" |
36 InitPhi_def "InitPhi == PRED x = # 0 & y = # 0" |
34 M1_def "M1 == (x$ .= Suc[$x]) .& (y$ .= $y)" |
37 M1_def "M1 == ACT x` = Suc<$x> & y` = $y" |
35 M2_def "M2 == (y$ .= Suc[$y]) .& (x$ .= $x)" |
38 M2_def "M2 == ACT y` = Suc<$y> & x` = $x" |
36 Phi_def "Phi == Init(InitPhi) .& [][M1 .| M2]_<x,y> .& \ |
39 Phi_def "Phi == TEMP Init InitPhi & [][M1 | M2]_(x,y) |
37 \ WF(M1)_<x,y> .& WF(M2)_<x,y>" |
40 & WF(M1)_(x,y) & WF(M2)_(x,y)" |
38 |
41 |
39 (* definitions for low-level program *) |
42 (* definitions for low-level program *) |
40 InitPsi_def "InitPsi == ($pc1 .= #a) .& ($pc2 .= #a) .& \ |
43 InitPsi_def "InitPsi == PRED pc1 = #a & pc2 = #a |
41 \ ($x .= # 0) .& ($y .= # 0) .& ($sem .= Suc[# 0])" |
44 & x = # 0 & y = # 0 & sem = # 1" |
42 alpha1_def "alpha1 == ($pc1 .= #a) .& (pc1$ .= #b) .& ($sem .= Suc[sem$]) .& \ |
45 alpha1_def "alpha1 == ACT $pc1 = #a & pc1$ = #b & $sem = Suc<sem`> |
43 \ unchanged(<x,y,pc2>)" |
46 & unchanged(x,y,pc2)" |
44 alpha2_def "alpha2 == ($pc2 .= #a) .& (pc2$ .= #b) .& ($sem .= Suc[sem$]) .& \ |
47 alpha2_def "alpha2 == ACT $pc2 = #a & pc2$ = #b & $sem = Suc<sem`> |
45 \ unchanged(<x,y,pc1>)" |
48 & unchanged(x,y,pc1)" |
46 beta1_def "beta1 == ($pc1 .= #b) .& (pc1$ .= #g) .& (x$ .= Suc[$x]) .& \ |
49 beta1_def "beta1 == ACT $pc1 = #b & pc1$ = #g & x$ = Suc<$x> |
47 \ unchanged(<y,sem,pc2>)" |
50 & unchanged(y,sem,pc2)" |
48 beta2_def "beta2 == ($pc2 .= #b) .& (pc2$ .= #g) .& (y$ .= Suc[$y]) .& \ |
51 beta2_def "beta2 == ACT $pc2 = #b & pc2$ = #g & y$ = Suc<$y> |
49 \ unchanged(<x,sem,pc1>)" |
52 & unchanged(x,sem,pc1)" |
50 gamma1_def "gamma1 == ($pc1 .= #g) .& (pc1$ .= #a) .& (sem$ .= Suc[$sem]) .& \ |
53 gamma1_def "gamma1 == ACT $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem> |
51 \ unchanged(<x,y,pc2>)" |
54 & unchanged(x,y,pc2)" |
52 gamma2_def "gamma2 == ($pc2 .= #g) .& (pc2$ .= #a) .& (sem$ .= Suc[$sem]) .& \ |
55 gamma2_def "gamma2 == ACT $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem> |
53 \ unchanged(<x,y,pc1>)" |
56 & unchanged(x,y,pc1)" |
54 N1_def "N1 == alpha1 .| beta1 .| gamma1" |
57 N1_def "N1 == ACT (alpha1 | beta1 | gamma1)" |
55 N2_def "N2 == alpha2 .| beta2 .| gamma2" |
58 N2_def "N2 == ACT (alpha2 | beta2 | gamma2)" |
56 Psi_def "Psi == Init(InitPsi) \ |
59 Psi_def "Psi == TEMP Init InitPsi |
57 \ .& [][N1 .| N2]_<x,y,sem,pc1,pc2> \ |
60 & [][N1 | N2]_(x,y,sem,pc1,pc2) |
58 \ .& SF(N1)_<x,y,sem,pc1,pc2> \ |
61 & SF(N1)_(x,y,sem,pc1,pc2) |
59 \ .& SF(N2)_<x,y,sem,pc1,pc2>" |
62 & SF(N2)_(x,y,sem,pc1,pc2)" |
60 |
63 |
61 PsiInv1_def "PsiInv1 == ($sem .= Suc[# 0]) .& ($pc1 .= #a) .& ($pc2 .= #a)" |
64 PsiInv1_def "PsiInv1 == PRED sem = # 1 & pc1 = #a & pc2 = #a" |
62 PsiInv2_def "PsiInv2 == ($sem .= # 0) .& ($pc1 .= #a) .& ($pc2 .= #b .| $pc2 .= #g)" |
65 PsiInv2_def "PsiInv2 == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)" |
63 PsiInv3_def "PsiInv3 == ($sem .= # 0) .& ($pc2 .= #a) .& ($pc1 .= #b .| $pc1 .= #g)" |
66 PsiInv3_def "PsiInv3 == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)" |
64 PsiInv_def "PsiInv == PsiInv1 .| PsiInv2 .| PsiInv3" |
67 PsiInv_def "PsiInv == PRED (PsiInv1 | PsiInv2 | PsiInv3)" |
65 |
68 |
66 end |
69 end |
67 |
70 |
68 ML |
71 ML |