Suppose that I have two modules AJupiter and CJupiter which are two implementations of the Jupiter protocol.
To check a global property of Jupiter, I need to collect states.
To do this, I write another module called AJupiterH which introduces a history variable ("list" in the code below)
to AJupiter by extending it.
Similarly, for CJupiter, I create a new module CJupiterH
which is exactly the same with AJupiterH except that it extends CJupiter instead of AJupiter.
How can I re-organize these modules, maybe using EXTENDS and/or INSTANCE,
to eliminate the duplication of AJupiterH and CJupiterH?
In other words, I want to make the way of defining the history variable "list" more reusable.
----------------------------- MODULE AJupiterH -----------------------------
(***************************************************************************)
(* AJupiter with a history of all list states across the system. *)
(***************************************************************************)
EXTENDS AJupiter
-------------------------------------------------------------
VARIABLE list
varsH == <<vars, list>>
TypeOKH == TypeOK /\ (list \subseteq List)
-------------------------------------------------------------
InitH == Init /\ list = {InitState}
DoH(c) == Do(c) /\ list' = list \cup {state'[c]}
RevH(c) == Rev(c) /\ list' = list \cup {state'[c]}
SRevH == SRev /\ list' = list \cup {state'[Server]}
-------------------------------------------------------------
NextH ==
\/ \E c \in Client: DoH(c) \/ RevH(c)
\/ SRevH
SpecH == InitH /\ [][NextH]_varsH /\ WF_varsH(NextH)
-------------------------------------------------------------