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

*From*: Rodrigo <deepma...@xxxxxxxxx>*Date*: Fri, 5 Oct 2018 17:07:44 -0700 (PDT)*References*: <CAH4a_VUMA9f5-Nt3iGRDavnpViG-+H468KzYnd356pQxc4sGwQ@mail.gmail.com> <A799BB28-D7EB-4570-828E-0D033521168D@gmail.com> <CAH4a_VVHnC4Bvy0TYuQRviTQwxyKf1mgBet1mW7PEG3pyFcDsg@mail.gmail.com>

Hello, I'm facing the same problem as Bekir and I wasn't able to find any solution yet, could someone give some help? I'm trying to specify an atomic broadcast protocol that uses many instances of Paxos, and my first idea was to do something like below (I pasted only the relevant parts of the spec): ------ VARIABLE maxVBalPerInst,maxValPerInst,msgsPerInst MPaxos(i) == INSTANCE Paxos WITH maxVBal <- maxVBalPerInst[i], maxVal <- maxValPerInst[i], msgs <- msgsPerInst[i] ... Init == /\ maxVBal = [i \in Instances |-> [a \in Acceptor |-> -1]] /\ maxVal = [i \in Instances |-> [a \in Acceptor |-> None]] /\ imsgs = [i \in Instances |-> {}] ... Phase1b(a) == \A i \in Instances: MPaxos(i)!Phase1b(a) ... ------ I just want to use Paxos logic to decide through each value on the atomic broadcast spec, but I got the same error mentioned on this thread and I don't know how to apply the Stephan suggestion in this scenario, because I don't want to rewrite the whole Paxos logic inside my protocol. Is it possible to do some workaround on it? Do you have some suggestion of how I could specify such a thing? A spec that uses many (possibly infinity) instances of other and keeps/collect the results of each one of these instances. Thanks Em quarta-feira, 5 de setembro de 2018 14:34:35 UTC+2, Bekir Oguz escreveu: > Dear Stepan, > Thanks a lot for your nice answer. Indeed my design of using instances was not working and I already switched to the design you suggested. > > Also trying out PlusCal to see if that’s an easier and cleaner way of writing my spec or not. > > Thanks again for the tutorial on the instance variable substitutions. > > Kind regards, > Bekir > > > Op di 4 sep. 2018 om 18:35 schreef Stephan Merz <step...@xxxxxxxxx> > > Hello Bekir, > > > the specific issue that TLC complains about is that when evaluating the initial-state predicate in module Node (instantiated in Cluster), the second conjunct is > > > memberSelf[n] = n > > > (where n is bound to an element of set nodes). The evaluation fails because the variable `memberSelf' has not yet been assigned a value in the initial state that TLC is currently constructing. When evaluating an initial condition, TLC interprets an equality "variable = expression" as an assignment if `variable' has not yet been assigned a value. However, your equality is not of that form: the left-hand side is not just a variable. > > > More generally, the approach that you chose for specifying your system will not work. Let me illustrate the problem using a very simple example where you have a finite set of processes, each of which uses a counter variable. It may be tempting to try and specify the system as follows: > > > ---- MODULE Proc ---- > > > VARIABLE c > > > Init == c = 0 > Next == c' = c + 1 > > > ==== > > > ---- MODULE System ---- > CONSTANT PSet > > > VARIABLE counter > > > P(n) == INSTANCE Proc WITH c <- counter[n] > > > Init == \A n \in PSet : P(n)!Init > Next == \E n \in PSet : P(n)!Next > > > ==== > > > Unfortunately, a formula such as > > > \A n \in 1..5 : counter[n] = 0 > > > does not unambiguously describe the value that the variable counter should have. For example, it is satisfied by all sequences <<0, 0, ..., 0>> whose length is at least 5. Even more, TLA+ does not specify the values of `42[0]' or `{1,2,3}[0]', and we do not know if the formula evaluates to true or false when counter = 42 or counter = {1,2,3}. Not only is TLC not clever enough to compute the right initial value, but the specification is too weak for characterizing the set of such values. The case of the next-state relation is even worse: the above specification only says that some counter component gets incremented but does not constrain at all the behavior of the other counter components. > > > You could in principle correct these problems as follows: > > > ---- MODULE System ---- > CONSTANT PSet > > VARIABLE counter > > P(n) == INSTANCE Proc WITH c <- counter[n] > > Init == > /\ counter \in [PSet -> Nat] \* fix the shape of the overall value > /\ \A n \in PSet : P(n)!Init \* initialize each component > > > Next == > /\ counter' \in [PSet -> Nat] \* fix the shape of the value in the next state > /\ \E n \in PSet : P(n)!Next \* let one process do its step ... > /\ \A m \in PSet \ {n} : UNCHANGED P(m)!c \* and constrain the other processes to stutter > ==== > > > However, now TLC will complain about being unable to enumerate the (infinite) set [PSet -> Nat]. It will work if you replace Nat by a finite set, but state computation will be extremely inefficient because TLC will first enumerate all sets of suitable functions and then filter out those that satisfy the specification. > > > In practice, it is best to give up on the idea of specifying processes individually in a base module and specify the composition (and interaction) of these processes in a main module that instantiates the base module. We will rather want to write something like the following (and similarly for your specification): > > > ---- MODULE System ---- > CONSTANT PSet > > VARIABLE counter > > Init == counter = [n \in PSet |-> 0] > > Inc(n) == counter' = [counter EXCEPT ![n] = @+1] > > Next == \E n \in PSet : Inc(n) > > ==== > > > > Note that both the initialization and the update using the EXCEPT operate on entire arrays (functions) rather than on individual array positions. > Chapter 10 of "Specifying Systems" discusses the issue of composing specifications in much detail. > > > Hope this helps, > Stephan > > > > > > > > On 31 Aug 2018, at 17:48, Bekir Oguz <bek...@xxxxxxxxx> wrote: > > > Dear all, > I am trying to write a spec (Cluster) which refers to n number of instances of another spec (Node) and getting a substitution error like this: > > > In evaluation, the identifier memberSelf is either undefined or not an operator. > line 17, col 37 to line 17, col 46 of module Cluster > > > I am new to TLA and does not understand well how this instance substitutions work in general. Looks like, during the Init operator of Node, I try to set the prime value of self, and then the model checker tries to substitute the self value to memberSelf[n] then it fails. > > > Source code could be found here: > https://github.com/ing-bank/baker/blob/781c999602375526e9702c85d610d350aa7fe4de/tla/Cluster.tla ; > > https://github.com/ing-bank/baker/blob/781c999602375526e9702c85d610d350aa7fe4de/tla/Node.tla ; > > > > And the error trace is like this: > > > > In evaluation, the identifier memberSelf is either undefined or not an operator. > line 18, col 37 to line 18, col 46 of module Cluster > > > The error occurred when TLC was evaluating the nested > expressions at the following positions: > 0. CInit > 1. Line 21, column 10 to line 22, column 67 in Cluster > 2. Line 21, column 13 to line 21, column 42 in Cluster > 3. Line 21, column 30 to line 21, column 42 in Cluster > 4. Line 16, column 1 to line 19, column 63 in Cluster > 5. Line 54, column 9 to line 60, column 59 in Node > 6. Line 54, column 12 to line 54, column 51 in Node > 7. Line 10, column 22 to line 10, column 45 in Node > 8. Line 55, column 12 to line 55, column 26 in Node > 9. Line 55, column 12 to line 55, column 15 in Node > 10. Line 18, column 37 to line 18, column 49 in Cluster > 11. Line 18, column 37 to line 18, column 46 in Cluster > > > > > Thanks in advance, > Bekir > > > > > > -- > > You received this message because you are subscribed to the Google Groups "tlaplus" group. > > To unsubscribe from this group and stop receiving emails from it, send an email to tlaplu...@xxxxxxxxxxxxxxxx. > > To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. > > Visit this group at https://groups.google.com/group/tlaplus. > > For more options, visit https://groups.google.com/d/optout. > > > > > > > > -- > > You received this message because you are subscribed to the Google Groups "tlaplus" group. > > To unsubscribe from this group and stop receiving emails from it, send an email to tlaplu...@xxxxxxxxxxxxxxxx. > > To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. > > Visit this group at https://groups.google.com/group/tlaplus. > > For more options, visit https://groups.google.com/d/optout.

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

**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

- Prev by Date:
**Re: [tlaplus] Re: understanding temporal properties** - Next by Date:
**Re: [tlaplus] Problem with instance substitutions** - Previous by thread:
**Re: [tlaplus] Problem with instance substitutions** - Next by thread:
**Re: [tlaplus] Problem with instance substitutions** - Index(es):