[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Hillel Wayne <hwa...@xxxxxxxxx>*Date*: Thu, 1 Mar 2018 14:08:44 -0800 (PST)*References*: <c3bc5e44-2ef5-4b4b-8955-9973ee7a45f0@googlegroups.com>

\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:

[][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 specVARIABLES 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 that1. a = 0 \Until b = 12. b = 0 \Next b = 1PS: 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

**References**:**How can I express Next and Until operator in TLA+?***From:*mlj . . .

- Prev by Date:
**Re: [tlaplus] Assign tuple to a constant** - Next by Date:
**Re: TLA+ parser (Haskell library)** - Previous by thread:
**Re: How can I express Next and Until operator in TLA+?** - Next by thread:
**Multi-threaded TLC Simulation Mode** - Index(es):