Temporal formula not applied to initial states

[riz0id]

The model checker does not apply a specifications temporal formula to initial states. A minimal example of the issue is:

type Spec = '[]

specInit :: Initial Spec ()
specInit = return ()

specNext :: Action Spec Bool
specNext = return True

specProp :: Invariant Spec Bool
specProp = always (return False)

checkSpec :: Either [MCError Spec] ModelMetrics
checkSpec = modelCheck (Specification specInit specNext specProp Nothing unfair)

The expected behavior from running checkSpec would be that the always (return False) invariant was violated; however, the actual behavior is that the model checking terminates successfully after generating the initial states.