TLC fails to invalidate temporal invariant

[Andrew Helwer]

Here is a spec of a simple system where we have Users and Devices, and can authorize or deauthorize users to access each device:

--------------------------- MODULE TemporalTest ---------------------------

CONSTANTS
    User,
    Device

VARIABLES
    permissions

-----------------------------------------------------------------------------

TypeInvariant ==
    /\ permissions \in [User -> SUBSET Device]

TemporalInvariant ==
    /\ \E user \in User :
        /\ \E device \in Device :
            /\ <>(device \in permissions[user])

Init ==
    /\ permissions = [user \in User |-> {}]

Authorize(user, device) ==
    /\ permissions' = [permissions EXCEPT ![user] = @ \cup {device}]

Revoke(user, device) ==
    /\ permissions' = [permissions EXCEPT ![user] = @ \ {device}]

Next ==
    \/ \E user \in User :
        \/ \E device \in Device :
            /\ Authorize(user, device)
            /\ Revoke(user, device)

Vars == <<permissions>>

TemporalAssumptions ==
    /\ \A user \in User :
        /\ \A device \in Device :
            /\ WF_Vars(Authorize(user, device))
            /\ WF_Vars(Revoke(user, device))

Spec ==
    /\ Init
    /\ [][Next]_Vars
    /\ TemporalAssumptions

THEOREM Spec =>
    /\ TypeInvariant
    /\ TemporalInvariant

=============================================================================

Now, there's a critical (but easy to miss!) error in this spec - in the Next formula, instead of a disjunction between Authorize and Revoke I have a conjunction! This is a real mistake I have made on multiple occasions. No worries though, right? We have our temporal invariant stating that eventually some user gets access to some device! TLC will find that we never actually manage to do that, then spit out an error. Alas, this does not happen; model-checking terminates, and no error is reported by TLC.

I was able to catch this mistake in my spec by looking at coverage statistics and seeing that Authorize and Revoke steps are never taken, but it does seem to be some kind of bug with temporal checking. Is it?

Here's my version information, on Windows 10 64-bit:

This is Version 1.5.6 of 29 January 2018 and includes:
  - SANY Version 2.1 of 23 July 2017
  - TLC Version 2.12 of 29 January 2018
  - PlusCal Version 1.8 of 07 December 2015
  - TLATeX Version 1.0 of 20 September 2017

[Ron Pressler]

I haven't studied your spec too closely, but the problem MAY be your liveness properties. As your spec demands that Authorize and Revoke will eventually happen if continuously enabled AND your safety condition forbids that, your specification may, in fact, be empty (i.e., no behavior satisfies it) and is equivalent to FALSE. If that is the case, a FALSE specification implies anything.

[Andrew Helwer]

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?

[Stephan Merz]

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...@gmail.com> 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...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.