How can I make long behavior specs less painful?

74 views
Skip to first unread message

davi...@gmail.com

unread,
Sep 11, 2018, 9:09:59 PM9/11/18
to tlaplus
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.

Markus Kuppe

unread,
Sep 11, 2018, 10:02:46 PM9/11/18
to tla...@googlegroups.com

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

davi...@gmail.com

unread,
Sep 11, 2018, 10:10:09 PM9/11/18
to tlaplus

It didn't even occur to me that this could work. Thanks!

- David

Ron Pressler

unread,
Sep 15, 2018, 2:18:59 PM9/15/18
to tlaplus
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.
Reply all
Reply to author
Forward
0 new messages