TLA+：未检查的时态属性

Question

我得到了这个玩具例子，由于某种原因，没有一个时间属性从未被断言过。即使是像[](h = 123456)这样荒谬的人也不会辜负TLC。我有什么不明白的？

intro.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

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

intro.cfg

SPECIFICATION Spec
INVARIANTS Invariants

薄层介绍

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)

Answer 1

行为规范由初始状态(Init)和下一状态公式([][Next]_h)组成.我相信这里发生的事情是IDE或TLC看到了这两个，而忽略了剩下的两个。这可能是应该的:这些附加条款并不会使行为违反您的属性:它们只是说初始状态和动作比您想象的要少。如果要使它们符合您的规范，请将这些子句添加到工具箱中的Properties中。