-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathAB2H.tla
107 lines (90 loc) · 5.39 KB
/
AB2H.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
-------------------------------- MODULE AB2H --------------------------------
(***************************************************************************)
(* This is spec AB2 with history variables AtoB and BtoA added so the spec *)
(* implements spec AB under the identity refinement mapping. *)
(***************************************************************************)
EXTENDS Integers, Sequences
CONSTANT Data, Bad
ASSUME Bad \notin (Data \X {0,1}) \cup {0,1}
\* We need to asssume that Bad is different from any of the legal
\* messsages.
VARIABLES AVar, BVar, \* The same as in module ABSpec
AtoB2, \* The sequence of data messages in transit from sender to receiver
BtoA2 \* The sequence of ack messages in transit from receiver to sender
\* Messages are sent by appending them to the end of the sequence
\* and received by removing them from the head of the sequence.
AB2 == INSTANCE AB2
(***************************************************************************)
(* We define RemoveBad so that RemoveBad(seq) removes from the sequence *)
(* seq all elements that equal Bad. *)
(***************************************************************************)
RECURSIVE RemoveBad(_)
RemoveBad(seq) ==
IF seq = << >> THEN << >>
ELSE (IF Head(seq) = Bad THEN << >> ELSE <<Head(seq)>>)
\o RemoveBad(Tail(seq))
RECURSIVE RemoveBad2(_)
RemoveBad2(seq) ==
IF seq = << >> THEN << >>
ELSE IF Head(seq) = Bad
THEN RemoveBad(Tail(seq))
ELSE <<Head(seq)>> \o RemoveBad(Tail(seq))
VARIABLES AtoB, BtoA \* Note that TLA+ allows multiple VARIABLE statements.
SpecH == /\ AB2!Spec
/\ [] /\ AtoB \in Seq(Data \X {0,1})
/\ BtoA \in Seq({0,1})
AB == INSTANCE AB
(***************************************************************************)
(* The following theorem asserts that SpecH implements/refines the AB *)
(* protocol. However, it can't be checked by TLC because it doesn't have *)
(* the form TLC requires of a specification. *)
(***************************************************************************)
THEOREM SpecH => AB!Spec
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now define SpecHH to be a specification that is equivalent to SpecH *)
(* and that TLC can check. We write the definition of SpecHH in a way *)
(* that should makes it clear that SpecHH is equivalent to SpecH. *)
(***************************************************************************)
TypeOKH == /\ AB2!TypeOK
/\ AtoB \in Seq(Data \X {0,1})
/\ BtoA \in Seq({0,1})
InitH == /\ AB2!Init
/\ AtoB = RemoveBad(AtoB2)
/\ BtoA = RemoveBad(BtoA2)
NextH == /\ AB2!Next
/\ AtoB' = RemoveBad(AtoB2')
/\ BtoA' = RemoveBad(BtoA2')
(***************************************************************************)
(* We would normally define varsH to be the tuple of all the variables of *)
(* the current module. However, we can use the following shorter *)
(* definition instead because *)
(* *)
(* UNCHANGED << <<AVar, ... , BtoA2>>, AtoB, BtoA >> *)
(* *)
(* equals *)
(* *)
(* UNCHANGED << AVar, ... , BtoA2, AtoB, BtoA >> *)
(***************************************************************************)
varsH == << AB2!vars, AtoB, BtoA >>
SpecHH == InitH /\ [][NextH]_varsH
(***************************************************************************)
(* The following theorem asserts that SpecHH and SpecH are equivalent *)
(* specifications. It is equivalent to *)
(* *)
(* /\ SpecHH => SpecH *)
(* /\ SpecH => SpecHH *)
(* *)
(* TLC can check the first of these implications by showing that SpecH is *)
(* a property satisfied by the specification SpecHH, but not the second. *)
(***************************************************************************)
THEOREM SpecHH <=> SpecH
(***************************************************************************)
(* We can deduce that SpecH implies AB!Spec from SpecHH <=> SpecH and the *)
(* following theorem, which TLC can check. *)
(***************************************************************************)
THEOREM SpecHH => AB!Spec
=============================================================================
\* Modification History
\* Last modified Wed Jan 03 11:47:33 PST 2018 by lamport
\* Created Wed Mar 25 11:53:40 PDT 2015 by lamport