[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: How can I express Next and Until operator in TLA+?
\Next should be representable as[b = 0 => b' = 1]_<<a, b>>
Which accounts for stuttering: either b = 0 \Next b = 1 OR you stutter.
\Until should be representable using the open-system operator:b /= 1 -+-> a = 0
a is zero at least one step longer than b isn't 1. Unfortunately, -+-> is currently unimplemented in TLC and TLAPS.
On Wednesday, 21 February 2018 22:08:55 UTC-6, mlj...@xxxxxxxxx wrote:
Enter code here...
I'm currently learning TLA+ and I met a problem that how can I express Next and Until operators of LTL in TLA+.
Suppose the follow spec
VARIABLES a, b
Init == a = 0 /\ b = 0
A == b = 1 /\ a' = 1 /\ UNCHANGED b
B == b = 0 /\ b' = 1 /\ UNCHANGED a
Spec == Init /\ [A /\ B]_<<a, b>>
For the above spec, how can I assert that
1. a = 0 \Until b = 1
2. b = 0 \Next b = 1
PS: Since TLA+ allows stuttering steps, so \Next operator does not provide much meaning. The second formula should always be false due to the stuttering steps.