|
On 11.09.2018 18:09, davi...@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 |