Fix and update ewd840 spec #1178
Conversation
| /// The following property says that eventually all nodes will terminate | ||
| /// assuming that from some point onwards no messages are sent. It is not | ||
| /// supposed to hold: any node may indefinitely perform local computations. | ||
| /// However, this property is verified if the fairness condition WF_vars(step) | ||
| /// is used instead of only WF_vars(System) that requires fairness of the | ||
| /// actions controlled by termination detection. | ||
| /// | ||
| /// Quint translation note: we cannot add `init` to this property since, in quint, | ||
| /// it is an action - not a predicate | ||
| temporal SpecWFstep = always(step.orKeep(vars) and step.weakFair(vars)) // and init | ||
|
|
||
| // The following property is not expressible in quint (for now), as it negates an action | ||
| // temporal AllNodesTerminateIfNoMessages = ( |
There was a problem hiding this comment.
I think "the following property" refers to AllNodesTerminateIfNoMessages, not to SpecWFstep. I got confused here, I think this meaning is lost with the current formatting.
There was a problem hiding this comment.
Ah, yes, I haven't noticed that. Will fix.
| /// | ||
| /// Quint translation note: we cannot add `init` to this property since, in quint, | ||
| /// it is an action - not a predicate | ||
| temporal SpecWFstep = always(step.orKeep(vars) and step.weakFair(vars)) // and init |
There was a problem hiding this comment.
I guess we should check with @konnov on how to treat init in temporal formulas, and note this here with a reference to an issue.
There was a problem hiding this comment.
@konnov pinging you here since you probably missed it!
There was a problem hiding this comment.
ah, I think it is the fifth time I am staring at it. Let me open an issue.
There was a problem hiding this comment.
Let's maybe refer to the issue and comment out the whole formula?
There was a problem hiding this comment.
Thanks! Ok, will do
| System, | ||
| Environment, | ||
| } | ||
|
|
||
| val vars = (active, color, tpos, tcolor) | ||
|
|
||
| // temporal Spec = Init and always(Next.orKeep(vars) and System.weakFair(vars)) | ||
| // temporal Spec = init and always(step.orKeep(vars) and System.weakFair(vars)) |
There was a problem hiding this comment.
I assume we already had this commented out because of init?
Probably good to treat it the same as below (i.e., just comment out init, or whatever we decide to do there)
Hello
This fixes #581 by:
AllNodesTerminateIfNoMessageswhich has a negation of an action, not allowed by quint's effect systemand initsection ofSpecWFstepsinceinitis an action in quint and therefore cannot be used as a predicateWe should think about whether we want so support this stuff in quint and, if so, how.
In order to make this work with
verify, I also had to:oneOf()was called in aval(and notnondet). See Infer effects for non-determinism ofoneOf#381Inv(copied fromEWD840.tlain the apalache project), as apalache doesn't support non constant values in ranges (tpos).I also made cosmetic changes in comments and renamed
Node->Nodes.CHANGELOG.mdfor any new functionalityREADME.mdupdated for any listed functionality