[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...
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