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

*From*: Anand Kumar <akkeshavan@xxxxxxxxx>*Date*: Thu, 1 Sep 2022 19:11:34 +0530*References*: <eb83eb50-5e91-4330-9e1b-9999a530e268n@googlegroups.com> <7C62B09E-48AE-4447-B935-BC6C0EB403F3@gmail.com> <CAJp900+3bmZn9PeYX-p9MeV_jn9iJaC7YqUHHMuOkNSkLVDC-w@mail.gmail.com> <387EAB74-26BE-4987-8810-9174DA514449@gmail.com>

Thank you very much for your prompt reply.

On Thu, 1 Sep 2022, 18:05 Stephan Merz, <stephan.merz@xxxxxxxxx> wrote:

--Please note that Specifying Systems introduces the language TLA+, a priori without consideration for TLC, which is restricted to a subset of TLA+, as explained in the corresponding chapter.I'd suggest using the examples used in the video course. There is also a collection of TLA+ specifications available on GitHub [1]. In particular, [2] is a collection of specs from Specifying Systems that can be checked with TLC.Regards,StephanOn 1 Sep 2022, at 14:25, Anand Kumar <akkeshavan@xxxxxxxxx> wrote:What is your recommendation, then? should I continue with 'Specifying systems" or use the examples in the Hyperbook to learn this? Most of these examples don't seem to work-- Even the Channel example ends up in a deadlock ( I mean in the 'Specifying systems book).On Thu, Sep 1, 2022 at 12:05 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:Hello,TLC cannot handle specifications that involve unbounded quantification or quantification over state variables. In your case, `q' is a state variable and Spec should really be defined asSpec == \EE q: Inner(q)!Init /\ [][BNext(q)]_<<in,out,q>>

where \EE denotes quantification over a state variable (i.e., a sequence of values). Such specifications are not handled by any of the existing verification tools for TLA+.Regards,StephanOn 1 Sep 2022, at 06:27, Anand Kumar <akkeshavan@xxxxxxxxx> wrote:Hi,"The configuration file did not specify the initial state predicate.

Can also be caused by trying to run TLC on a specification from

a module imported with a parameterized INSTANCE statement."

This is my spec, what am I doing wrong? Similar error comes in the FIFO spec lso. I have checked your earlier answer, but that doesn;t seem to provide a solution. I understand the Professor Lamport prefers us to use the Hyperbook, but that gives a lot fo permission errors etc on a mac.

Sorry to trouble you with this-- but since i am new to this I would really appreciate the help.

EXTENDSNaturals, Sequences

CONSTANTMessage,N

VARIABLESin, out

ASSUME(N \in Nat) /\ (N > 0 )

Inner(q) ==

INSTANCEInnerFIFO

BNext(q) ==

/\ Inner(q)! Next

/\ Inner(q)! BufReceive => (Len(q) < N )

Spec == \E q: Inner(q)!Init /\ [][BNext(q)]_<<in,out,q>>

--

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/eb83eb50-5e91-4330-9e1b-9999a530e268n%40googlegroups.com.

--

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.

To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/aASP2cDy1-c/unsubscribe.

To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7C62B09E-48AE-4447-B935-BC6C0EB403F3%40gmail.com.

--(Please read my books, if you like programming:Listen to my music:Thank you)--

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/CAJp900%2B3bmZn9PeYX-p9MeV_jn9iJaC7YqUHHMuOkNSkLVDC-w%40mail.gmail.com.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.

To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/aASP2cDy1-c/unsubscribe.

To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/387EAB74-26BE-4987-8810-9174DA514449%40gmail.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/CAJp900KOsOz8ad769QF23AMXC1NUZ3RPgdF_OYTtqYdfaqbf%3DQ%40mail.gmail.com.

**References**:**[tlaplus] Specifying Systems- BoundedFIFO error- Figure 4.2***From:*Anand Kumar

**Re: [tlaplus] Specifying Systems- BoundedFIFO error- Figure 4.2***From:*Stephan Merz

**Re: [tlaplus] Specifying Systems- BoundedFIFO error- Figure 4.2***From:*Anand Kumar

**Re: [tlaplus] Specifying Systems- BoundedFIFO error- Figure 4.2***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Specifying Systems- BoundedFIFO error- Figure 4.2** - Next by Date:
**[tlaplus] How do we use the transaction api in spec？** - Previous by thread:
**Re: [tlaplus] Specifying Systems- BoundedFIFO error- Figure 4.2** - Next by thread:
**[tlaplus] How do we use the transaction api in spec？** - Index(es):