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

*From*: Mursel Musabasic <murselmurga@xxxxxxxxx>*Date*: Wed, 4 Mar 2020 01:43:49 -0800 (PST)*References*: <b23791fe-5aa0-48b4-ae13-151105e94d3f@googlegroups.com> <BE5C1A4C-BD12-4F3C-892A-EF1E902EA102@gmail.com> <17e8cb76-2256-4f80-8b89-982187e33eda@googlegroups.com> <7AA48EF6-EC08-45F8-A8AA-EFAD96963737@gmail.com>

So, the Next-state formula will not be satisfied (Spec will not be also satisfied) until all previous states/formulas are not satisfied/constructed?

On Wednesday, March 4, 2020 at 8:41:44 AM UTC+1, Stephan Merz wrote:

-- On Wednesday, March 4, 2020 at 8:41:44 AM UTC+1, Stephan Merz wrote:

The formula Spec (and its sub-formulas Init, Next etc.) express the algorithm as a TLA+ specification, and we then want to verify properties such asSpec => []MutualExclusionTherefore, Spec does not need to be checked, it can be assumed to hold (the implication is trivially true of state sequences that do not satisfy Spec). Concretely, TLC interprets Init and Next in order to construct the initial state(s) and the successor states of any states it has already constructed. For the latter, it considers the different disjuncts in the definition of Next: any successor state allowed by some of these formulas is allowed by Next. For details on how TLC interprets these formulas, please see Specifying Systems, and if you have not yet done so, watch the video lectures on TLA+.Regards,StephanOn 4 Mar 2020, at 01:04, Mursel Musabasic <murse...@xxxxxxxxx> wrote:Thanks for quick explanation.I'm reading this paper on Peterson's algorithm (https://tla.msr-inria.inria.fr/tlaps/doc/IFM2010/Peterson_ ) and on page 4 it say's:IFM2010.pdf "Now we can define proc(self) as the fact that one of the previous actions is being accomplished:proc(self) == \/ a0(self) \/ a1(self) \/ a2(self) \/ a3a(self) \/ a3b(self) \/ cs(self) \/ a4(self)Finally, we define the Next action, as the fact that either proc is accomplished for one of the processes, or the algorithm has finished (to prevent deadlock on termination).Next == \E self \in {0,1}: proc(self)"I have a few questions:1. When TLC will check proc(self) formula? Will this happen after it checks all previous formula's from a0 to a4?2. Will proc(self) formula be satisfied when all previous formula's satisfied (a0 to a4)?3. Next formula is satisfied if proc(self) is satisfied where self is element of 0 and 1 (process 0 or 1). Is this correct?Thanks in advance!

On Wednesday, February 26, 2020 at 3:49:57 PM UTC+1, Stephan Merz wrote:Hello,the corresponding TLA+ module is contained in the distribution of the TLA Proof System [1] and also available from [2] (with the temporal reasoning steps omitted because TLAPS didn't support them at the time). In short, the module has the definitionsvars == << flag, turn, pc >>Spec == Init /\ [][Next]_vars

This is the idiomatic form of TLA+ specifications: the next-state relation allows stuttering steps in which the variables declared in the specification do not change their values.Stephan[2] https://members.loria.fr/SMerz/papers/fm2012.html Hi there,I was looking for formal specification on Peterson algorithm and came across this publication (https://lamport.azurewebsites.net/pubs/tlaps. ) where it says, I quote:"The temporal formula Spec is the complete specification. It characterizes behaviors (ω-sequences of states) that start in a state satisfying Init and where every pair of successive states either satisfies Next or else leaves the values of the tuple vars unchanged."I'm having problem with understanding of tuplevarsin specified formula. Can anyone explain to me how these variables (turn, flag and pc) relate to tuplevars? I can understand that some variables stays unchanged during verification, but couldn't get it in final Spec temporal formula.Best regards,Mursel--

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 tla...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b23791fe- .5aa0-48b4-ae13-151105e94d3f% 40googlegroups.com --

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 tla...@googlegroups.com .

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/17e8cb76- .2256-4f80-8b89-982187e33eda% 40googlegroups.com

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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b4c626f9-2b3c-4ae5-a59f-7fce4c814a6c%40googlegroups.com.

**References**:**[tlaplus] Spec formula for Peterson algorithm***From:*Mursel Musabasic

**Re: [tlaplus] Spec formula for Peterson algorithm***From:*Stephan Merz

**Re: [tlaplus] Spec formula for Peterson algorithm***From:*Mursel Musabasic

**Re: [tlaplus] Spec formula for Peterson algorithm***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] TCP/IP client/server communication protocol** - Next by Date:
**Re: [tlaplus] Model Checking the Bakery Algorithm** - Previous by thread:
**Re: [tlaplus] Spec formula for Peterson algorithm** - Next by thread:
**[tlaplus] Best practice when building a series of model refinements?** - Index(es):