Skip to content

Instantly share code, notes, and snippets.

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

What would you like to do?
解決しました(コメント参照) ~~なぜ、Temporal properties were violated になるのかわかりません。。。~~
----------------------------- MODULE playground -----------------------------
\* 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.


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+
Parsing file /Applications/TLA+
Parsing file /Applications/TLA+
Parsing file /Applications/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.

This comment has been minimized.

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