Re: [tlaplus] How can I make long behavior specs less painful?

I remember that this was one of the most confusing things for me when I learned TLA+ and didn't yet have a clear mental picture of how things worked. I still thought of TLA+ in terms of programming, and considered the subscript of [] and <> actions, as well as those of the fairness operators as some special case where the variables are somehow treated specially, as a tuple where the variables are somehow considered "by name" as opposed as "by value." Really, the subscript is any state function (a "level 1" _expression_, or any _expression_ that does not depend on any primed variable). You can define this state function as a single vars definition, split it further into subsets (as in `vars1 == <<a, b, c>>`, `vars2 == <<d, e>>`, `vars == <<vars1, vars2>>`) or as any other state function, although that is rarely done.

If you want to dig further into what those subscripts mean precisely -- and so understand why there's nothing magical or special about them -- you can read my summary in the section Stuttering Invariance and Machine Closure, in my post about the temporal logic of actions, or in the book Specifying Systems.

On Wednesday, September 12, 2018 at 3:10:09 AM UTC+1, dav...@xxxxxxxxx wrote:

On Tuesday, September 11, 2018 at 7:02:46 PM UTC-7, Markus Alexander Kuppe wrote:
> On 11.09.2018 18:09, dav...@xxxxxxxxx
> wrote:
>
>
>
> I'm new to this so there may be an easy answer here but I have a spec that needs a fairness condition. My behavior spec ends up looking like this:
>
> Init /\ [][Next]_<<idx,queue,pnext, cnext,pcount, ccount,porder, corder,pmo, cmo,write, read,pread, pwrite,cread, cwrite,newpwrite, newcread>> /\ WF_<<idx,queue,pnext, cnext,pcount, ccount,porder, corder,pmo, cmo,write, read,pread, pwrite,cread, cwrite,newpwrite, newcread>>(ProducerNext) /\ WF_<<idx,queue,pnext, cnext,pcount, ccount,porder, corder,pmo, cmo,write, read,pread, pwrite,cread, cwrite,newpwrite, newcread>>(ConsumerNext)
>
> (I'm testing a lock-free producer-consumer queue. The WF conditions are an attempt to make sure it doesn't eternally try to produce in a full queu or consume from an empty one.)
>
> My spec does check (whether or not its right is questionable but unimportant). My concern is the obvious waste in the variable list -- it certainly feels like its missing something. Is there some canonical way to cut that down to be more intelligible? Keeping it in sync across all models with changes to the spec is very time consuming.
>
>
> Hi,
>
> have a look at e.g. the EWD840 example [1] and the definition of
> vars in particular.
>
> Hope this helps,
>
>
>
> Markus
>
>
>
>
>
> [1]
> https://github.com/tlaplus/Examples/blob/master/specifications/ewd840/EWD840.tla
It didn't even occur to me that this could work. Thanks!
- David