Re: [tlaplus] Spurious coverage warning in TLC

Thanks Markus. I am pleased it is fixed.

Regards,

Jonathan

On Mar 19, 2019, at 11:43 PM, Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote:

On 19.03.19 20:14, Jonathan Ostroff wrote:
In a simple 2-process mutex (see below) there are no errors but there is
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.

Hi Jonathan,

please see GitHub issue 152 [1] which tracks this problem. Note that
the next TLC release will fix it. You can download a nightly build from
[2] to verify the fix.

Thanks
Markus

[1] https://github.com/tlaplus/tlaplus/issues/152
[2] 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.

--
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.