Skip to content

Instantly share code, notes, and snippets.

@Kuniwak Kuniwak/1-playground.tla
Last active May 27, 2019

Embed
What would you like to do?
解決しました(コメント参照) ~~なぜ、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

This comment has been minimized.

Copy link
Owner Author

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
You can’t perform that action at this time.