\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 = 0a 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...
Hi guys,
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.
Best Regards,
Changjian Zhang