109 lines
5.3 KiB
Text
109 lines
5.3 KiB
Text
-------------------------------- 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, in both directions.
|
|
|
|
VARIABLES AVar, \* The last <<value, bit>> pair A decided to send.
|
|
BVar \* The last <<value, bit>> pair B received.
|
|
VARIABLES
|
|
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) is the value obtained by *)
|
|
(* removing 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))
|
|
|
|
\* Only difference with RemoveBad is the parenthesizing.
|
|
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
|