我有这个玩具示例，出于某种原因，从未断言过任何时间属性。即使是荒谬的，[](h = 123456)也不会失败 TLC。我不明白什么？
介绍.tla
----------------------------------------------------- MODULE intro -----------------------------------------------------
EXTENDS Naturals
VARIABLE h
Init == h \in 1..12
Invariants == h \in 1..12
Next == h' = (h%12) + 1
Spec ==
/\ Init
/\ [][Next]_h
\* None of these cause the model checker to fail
/\ (\A i \in 1..15 : []<>(h = i))
/\ []<>(h = 123456)
/\ [](h = 123456)
/\ <>(h = 123456)
/\ [](FALSE)
THEOREM Spec => []Invariants
=======================================================================================================================
介绍.cfg
SPECIFICATION Spec
INVARIANTS Invariants
tlc介绍
TLC2 Version 2.13 of 18 July 2018 (rev: bfdbe00)
Running breadth-first search Model-Checking with seed -1431825986697619670 with 8 workers on 8 cores with 7131MB heap and 64MB offheap memory (Linux 5.0.0-arch1-1-ARCH amd64, Oracle Corporation 1.8.0_202 x86_64).
Parsing file /home/golly/projects/private/talks-wip/tla/intro.tla
Parsing file /tmp/Naturals.tla
Semantic processing of module Naturals
Semantic processing of module intro
Starting... (2019-03-11 12:20:09)
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Finished computing initial states: 12 distinct states generated.
Model checking completed. No error has been found.
Estimates of the probability that TLC did not check all reachable states
because two distinct states had the same fingerprint:
calculated (optimistic): val = 7.8E-18
based on the actual fingerprints: val = 1.6E-18
24 states generated, 12 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 0.
The average outdegree of the complete state graph is 0 (minimum is 0, the maximum 0 and the 95th percentile is 0).
Finished in 00s at (2019-03-11 12:20:09)