[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: TLC fails to invalidate temporal invariant

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.

On Wednesday, May 2, 2018 at 2:33:46 AM UTC+1, Andrew Helwer wrote:
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 ---------------------------




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

    /\ 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