[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: "Rodrigo Q. Saramago" <deepma...@xxxxxxxxx>*Date*: Sun, 7 Oct 2018 04:28:10 -0700 (PDT)*References*: <CAH4a_VUMA9f5-Nt3iGRDavnpViG-+H468KzYnd356pQxc4sGwQ@mail.gmail.com> <A799BB28-D7EB-4570-828E-0D033521168D@gmail.com> <CAH4a_VVHnC4Bvy0TYuQRviTQwxyKf1mgBet1mW7PEG3pyFcDsg@mail.gmail.com> <f59bc8a4-cba1-4315-a8bc-6edb30e412bd@googlegroups.com> <fea04d7d-3089-449e-aecf-7a50b0821c46@googlegroups.com> <9e7b2394-ec6f-44ed-bb96-c3a17b7e3a96@googlegroups.com> <f80eb53e-ee03-4bb6-8d09-7ad3982096f6@googlegroups.com> <d541ba1c-6095-448e-ac8b-e53b2e5c6ed4@googlegroups.com>

Oh! I'll take a look on that chapter! Thanks!

Your spec should not trigger the TLC bug, because that seems to affect

only the instantiation of expressions containing a subscript. I don't

think TLC will handle your spec, but it should if you rearrange the

conjuncts to satisfy TLC's requirements for a next-state relation,

which are explained in the chapter on TLC in "Specifying Systems".

The superfluous UNCHANGED conjunct will cause no harm.

There should be a bug report on the instantiation problem inGithub. I haven't looked at very much of the TLC code, and I

don't know where to look for this bug. But the fact that it seems

to affect only expressions with subscripts should help one find

the problem.

Leslie

On Saturday, October 6, 2018 at 6:50:19 AM UTC-7, Rodrigo Q. Saramago wrote:Hi Leslie, thank you very much for your suggestion, after watching the lectures I was able to make it works. Here is a simple example that I made to test the solution proposed by Stephan, where I use many instances of consensus, each one to choose on one value:

---------------------------- MODULE SimpleNConsensus ----------------------------

EXTENDS FiniteSets, Naturals

CONSTANT Value, N

VARIABLE consensusInst

ASSUME N \in Nat /\ N > 0

Instances == 1..N

vars == <<consensusInst>>

TypeOK == consensusInst \in [Instances -> SUBSET Value]

C(i) == INSTANCE Consensus WITH chosen <- consensusInst[i]

Init == /\ consensusInst \in [Instances -> SUBSET Value]

/\ \A i \in Instances: C(i)!Init

Choose(v) == /\ consensusInst' \in [Instances -> SUBSET Value]

/\ \A i \in DOMAIN consensusInst: v \notin consensusInst[i]

/\ \E i \in Instances:

/\ C(i)!Next

/\ consensusInst' = [consensusInst EXCEPT ![i] = @ \cup {v}]

/\ \A j \in Instances \ {i} : UNCHANGED consensusInst[j]

Next == \E v \in Value: Choose(v)

Spec == Init /\ [][Next]_vars

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

(*********************************************************** ****************)

(* Safety: At most one value is chosen for all instances *)

(*********************************************************** ****************)

Inv == /\ TypeOK

/\ \A i \in Instances: Cardinality(consensusInst[i]) \leq 1

THEOREM Invariance == Spec => []Inv

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

(*********************************************************** ****************)

(* Liveness: A non-trivial value is eventually chosen for all instances *)

(*********************************************************** ****************)

NonTriviality == \A i \in Instances: <>(consensusInst[i] # {} /\ consensusInst[i] \subseteq Value)

LiveSpec == Spec /\ WF_vars(Next)

THEOREM LivenessTheorem == LiveSpec => NonTriviality

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

\* Modification History

\* Last modified Sat Oct 06 15:34:11 CEST 2018 by rodrigo

\* Created Wed Oct 03 17:25:53 CEST 2018 by rodrigoEm sábado, 6 de outubro de 2018 10:51:57 UTC+2, Leslie Lamport escreveu:If your spec were correct, TLC would not be able to handle it because

of a long-standing bug: it doesn't correctly handle parametrized

instantiation. I suspect that this bug is not hard to fix, but there

have always been more pressing issues to handle. It would make a nice

project for someone who wants to help.About the bug, is there some issue already open for that? Or do you know where in the code, someone interested in helping, could start looking?And thank you for taking your time on this!BestHowever, your spec seems to have the same error that Stephan

pointed out in Bekir's example. If you didn't understand Stephan's

explanation, try the one at around 11 minutes 40 seconds of the 5th

TLA+ video lecture.Leslie

**Follow-Ups**:**Re: [tlaplus] Problem with instance substitutions***From:*Balaji Arun

**References**:**Problem with instance substitutions***From:*Bekir Oguz

**Re: [tlaplus] Problem with instance substitutions***From:*Stephan Merz

**Re: [tlaplus] Problem with instance substitutions***From:*Bekir Oguz

**Re: [tlaplus] Problem with instance substitutions***From:*Rodrigo

**Re: [tlaplus] Problem with instance substitutions***From:*Rodrigo Q. Saramago

**Re: [tlaplus] Problem with instance substitutions***From:*Leslie Lamport

**Re: [tlaplus] Problem with instance substitutions***From:*Rodrigo Q. Saramago

**Re: [tlaplus] Problem with instance substitutions***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Alternatives to for loops in PlusCal** - Next by Date:
**Re: [tlaplus] Alternatives to for loops in PlusCal** - Previous by thread:
**Re: [tlaplus] Problem with instance substitutions** - Next by thread:
**Re: [tlaplus] Problem with instance substitutions** - Index(es):