TLC fails to invalidate temporal invariant

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