Re: How to introduce history variables in a modular/reusable way?

[Andrew Helwer <andrew...@xxxxxxxxx>]

If you really want, you can write your JupiterH spec something like this:

------------------------------ MODULE JupiterH ------------------------------

CONSTANTS
    Client,
    Server,
    Init,
    InitState,
    Do(_),
    Rev(_),
    SRev,
    Next,
    Vars

VARIABLES
    list,
    state

-----------------------------------------------------------------------------

VarsH == <<Vars, list, state>>

A == INSTANCE AJupiter
C == INSTANCE CJupiter

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)

=============================================================================

Then in your model, you'd define Do(_) as A!Do(_) or C!Do(_) depending on what you want to model-check.

However, a better approach might be to invert this: AJupiter and CJupiter both extend/instance/refine JupiterH, which contains the history logic.

Anyway, I'm interested in whatever solution you arrive at, as I've also been toying with the idea of specifying a bunch of different consistency models in TLA+ using histories.

Andrew

On Saturday, September 8, 2018 at 8:26:31 PM UTC-7, Hengfeng Wei wrote:

Dear all,

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)

-------------------------------------------------------------