|Thanks Markus. I am pleased it is fixed.|
-- On 19.03.19 20:14, Jonathan Ostroff wrote:
In a simple 2-process mutex (see below) there are no errors but there isHi Jonathan,please see GitHub issue 152  which tracks this problem. Note thatthe next TLC release will fix it. You can download a nightly build from to verify the fix.ThanksMarkus https://github.com/tlaplus/tlaplus/issues/152 http://nightly.tlapl.us/-- 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.Visit this group at https://groups.google.com/group/tlaplus.For more options, visit https://groups.google.com/d/optout.
a coverage warning which is coloured yellow. Clicking on the warning
points to the following line in the translation:
vars == << r, pc >>
TLC warns one when some action is never exercised during a run of the
model checker. But here the warning appears to be meaningless because
the definition of vars is not an action.
Stephan suggested that I post here to mention the issue. He also
mentions that he has seen similar examples of spurious warnings by TLC,
but he ignores them. (However, knowing that an actual action is never
executed is meaningful information.)
In a more complex _process_ version of mutex, the problem does not occur.
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.