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

[Hengfeng Wei <hengx...@xxxxxxxxx>]

Dear Andrew,

Great thanks for your advice.

I prefer the second approach, letting AJupiter and CJupiter both extend/instance Jupiter/JupiterH.

However, I have not succeed in applying it yet.

Specifically, I have some difficulty in choosing "EXTENDS" and/or "INSTANCE".

I don't understand the meaning of extending a parameterized operator, such as Do(_) here.

Maybe we should "EXTENDS" the constants, like Client, Server, InitState, which represent the states of the protocols, 

and "INSTANCE" the parameterized operators, like Init, Do(_), Rev(_), and SRev, which represent the actions.

I am not sure and I will keep working on it.

(My project can be found here (with little docs now): https://github.com/Disalg-ICS-NJU/tlaplus-lamport-projects/tree/master/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla)

By the way, I am also very interested in specifying consistency models in TLA+ (and reasoning about them with the aid of automated theorem provers or SMT solvers.) Hope to learn more from you. Thanks again.

Best regards,

Hengfeng Wei

On Tuesday, September 11, 2018 at 2:57:28 AM UTC+8, Andrew Helwer wrote:

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)

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