Temporal properties were violated.
Name | Value |
---|---|
<Shuttering> |
State (num = 2) |
▼ <Initial predicate> |
State (num = 1) |
▶︎ varTable |
{<<0, "a">>, <<1, "b">>} |
----------------------------- MODULE playground ----------------------------- | |
VARIABLES varTable | |
\* Initial Predicate: | |
Init == varTable = { <<0, "a">>, <<1, "b">> } | |
\* Next-state relation: | |
Next == varTable' = { <<2, "c">> } | |
\* Property: | |
Spec == <> (<<2, "c">> \in varTable) | |
============================================================================= |
TLC2 Version 2.13 of 18 July 2018 | |
Running breadth-first search Model-Checking with seed -7648242007324452927 with 4 workers on 8 cores with 1366MB heap and 2730MB offheap memory (Mac OS X 10.14.4 x86_64, Oracle Corporation 10 x86_64). | |
Starting SANY... | |
Parsing file ~/Development/tla-playground/playground.toolbox/Playground/MC.tla | |
Parsing file ~/Development/tla-playground/playground.toolbox/Playground/playground.tla | |
Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.201807180447/tla2sany/StandardModules/TLC.tla | |
Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.201807180447/tla2sany/StandardModules/Naturals.tla | |
Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.201807180447/tla2sany/StandardModules/Sequences.tla | |
Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.201807180447/tla2sany/StandardModules/FiniteSets.tla | |
Semantic processing of module playground | |
Semantic processing of module Naturals | |
Semantic processing of module Sequences | |
Semantic processing of module FiniteSets | |
Semantic processing of module TLC | |
Semantic processing of module MC | |
SANY finished. | |
Implied-temporal checking--satisfiability problem has 1 branches. | |
Computing initial states... | |
Finished computing initial states: 1 distinct state generated. | |
Checking temporal properties for the complete state space with 2 total distinct states at (2019-05-24 18:39:21) | |
Finished checking temporal properties in 00s at 2019-05-24 18:39:21 | |
3 states generated, 2 distinct states found, 0 states left on queue. |
結論
TLA+ の検証器のデフォルトの挙動である「ある仕様について弱公平性を仮定しない(stuttering)」が原因だった。
TLA+ は、複数の仕様を組み合わせても問題がおきないように、デフォルトで弱公平性を仮定しない。これが何を意味するかというと、システム A と B があったとき、A の状態遷移が生じる前に B のすべての状態遷移が終わるといったケースでもなんらかの性質を検証できるということ。TLC では、stuttering という初期・途中状態以降で何も起こらないというケースを挟み込むことでこの機能を実現している。そのため、上のコードでは Init 以降の状態遷移が stuttering で詰まったケースでは Spec が満たされないことを指摘していたのだった。
この stuttering を防ぐために、Next について弱公平性を期待する(つまり Next はいつか実行される)ように Spec を書き換えたところ、エラーが出なくなった:
謝辞
以下の方々にアドバイスをいただき、解決できました:
@masateruk
@lemmster