Re: [tlaplus] TLC fails to invalidate temporal invariant

[Stephan Merz <stepha...@xxxxxxxxx>]

Hi Andrew,

indeed, there are many ways in which a formal specification can be insignificant, and most specifications are initially wrong. Model checking in particular is most informative when it returns a counter-example, not when it says that the property holds, which may be vacuous. Section 14.5 of "Specifying Systems" contains good advice on how to use TLC – in particular, look at the paragraph "Be Suspicious of Success" in 14.5.3. Inspecting the coverage information and the number of (distinct) states that TLC encountered is mandatory. Since running TLC doesn't require much effort, one should also check properties that are expected to be false and inspect the counter-example that TLC finds in order to build confidence in the specification. For example, you could have checked the invariant

\A u \in User : permissions[u] = {}

which you expected to be wrong because some permissions should be granted.

Your case is extreme in that there are no behaviors (although the safety part by itself has the trivial stuttering behavior), and perhaps TLC could detect this and output a warning. But there are less drastic cases that would still slip through, so it would be of limited use.

Regards,
Stephan


> On 2 May 2018, at 18:51, Andrew Helwer <andrew...@xxxxxxxxx> wrote:
> 
> That makes sense! I suppose we can read my spec as "if a behaviour satisfies Spec, then these invariants are true of that behaviour" and of course if no behaviours satisfy Spec then that statement is true. In this case no behaviours satisfy my spec because TemporalAssumptions and [][Next]_Vars are conjoined and in logical conflict. Do you think it's a good idea to display a warning to the user if TLC finds no behaviours satisfying the spec?
> 
> -- 
> 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+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.