[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Spurious coverage warning in TLC
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.
please see GitHub issue 152  which tracks this problem. Note that
the next TLC release will fix it. You can download a nightly build from
 to verify the fix.
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.