Питання по TLA+
Всім привіт.
Є декілька питань по temporal properties у TLA+.
UPDATE. Поки стаття проходила перевірку цензури на DOU, зрозумів в чому була проблема: потрібно в Spec додати:
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
Тому питань більш немає.
Всім дякую за увагу.
Приклад:
EXTENDS Integers
VARIABLES step, state
vars == <<step, state>>TypeOK ==
state \in {“created”, “inProgress”, “completed”}Init ==
/\ step = 1
/\ state = “created”InProgress ==
/\ state = “created”
/\ step’ = step + 1
/\ state’ = “inProgress”Completed ==
/\ state = “inProgress”
/\ step’ = step + 1
/\ state’ = “completed”Next ==
\/ InProgress
\/ CompletedSpec == Init /\ [][Next]_vars
Обидва наступних Temporal properties дають stuttering помилку:
- (state = “created”) ~> (state = “completed”) що означає: якщо спрацював предикат state = “created”, то в якийсь момент у майбутньому повинен спрацювати предикат state = “completed”
- <>(state = “completed”) що означає: в якийсь момент state повинен дорівнювати “completed”
Чому?
Немає коментарів
Додати коментар Підписатись на коментаріВідписатись від коментарів