Skip to content

Instantly share code, notes, and snippets.

@Kuniwak
Last active May 27, 2019 08:46
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save Kuniwak/074ad11292575fed691d3e68f382680a to your computer and use it in GitHub Desktop.
解決しました(コメント参照) ~~なぜ、Temporal properties were violated になるのかわかりません。。。~~
----------------------------- 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)
=============================================================================

TLC Errors

Temporal properties were violated.

Error-Trace

Name Value
 <Shuttering> State (num = 2)
<Initial predicate> State (num = 1)
▶︎ varTable {<<0, "a">>, <<1, "b">>}
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.
@Kuniwak
Copy link
Author

Kuniwak commented May 27, 2019

結論

TLA+ の検証器のデフォルトの挙動である「ある仕様について弱公平性を仮定しない(stuttering)」が原因だった。

TLA+ は、複数の仕様を組み合わせても問題がおきないように、デフォルトで弱公平性を仮定しない。これが何を意味するかというと、システム A と B があったとき、A の状態遷移が生じる前に B のすべての状態遷移が終わるといったケースでもなんらかの性質を検証できるということ。TLC では、stuttering という初期・途中状態以降で何も起こらないというケースを挟み込むことでこの機能を実現している。そのため、上のコードでは Init 以降の状態遷移が stuttering で詰まったケースでは Spec が満たされないことを指摘していたのだった。

この stuttering を防ぐために、Next について弱公平性を期待する(つまり Next はいつか実行される)ように Spec を書き換えたところ、エラーが出なくなった:

  \* Property:
- Spec == <> (<<2, "c">> \in varTable)
+ Spec == WF_vars(Next) => (<<2, "c">> \in varTable)

謝辞

以下の方々にアドバイスをいただき、解決できました:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment