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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Wed, 18 Jan 2023 08:33:24 -0800 (PST)*References*: <2c52bdc7-3ffa-44f5-8672-368528f6b74bn@googlegroups.com> <D5F97A16-8CC2-4481-A876-8734BCF14E04@gmail.com> <d1a0494d-57bf-45b6-b9e1-f7762e9f8c0dn@googlegroups.com>

Ah, cracked open specifying systems - so you can only have [][A]_v or <><<A>>_v formulas. The first means every step must satisfy A or be a stuttering step. The second says eventually an A step occurs. []<<A>>_v doesn't make sense because stuttering is always enabled, so it would be false.

On Wednesday, January 18, 2023 at 11:29:32 AM UTC-5 Andrew Helwer wrote:

I thought [A]_x means "A is an action formula over x' and x, and either A is true or x' = x" and <<A>>_x means "A is an action formula over x' and x, and x' /= x".On Wednesday, January 18, 2023 at 11:10:30 AM UTC-5 Stephan Merz wrote:[]<<A>>_v is not a TLA formula, I believe you meant to writeMonotonic == [][x > 0 => x' < x]_xStephanOn 18 Jan 2023, at 16:50, Andrew Helwer <andrew...@xxxxxxxxx> wrote:Given this spec:---- MODULE Test ----

EXTENDS Naturals

VARIABLE x

Init == x = 10

Next == IF x > 0 THEN x' = x - 1 ELSE UNCHANGED x

Monotonic == []<<x > 0 => x' < x>>_x

====And this model:INIT Init

NEXT Next

PROPERTY MonotonicTLC gives this error:*** Errors: 1

line 6, col 14 to line 6, col 27 of module Test

[] followed by action not of form [A]_v.Does TLC only support [][A]_v, not []<<A>>_v?--

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2c52bdc7-3ffa-44f5-8672-368528f6b74bn%40googlegroups.com.

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/30bc4673-18ea-417c-be9d-e3d5235ad9aen%40googlegroups.com.

**References**:**[tlaplus] How can I modelcheck an angle-bracket action formula?***From:*Andrew Helwer

**Re: [tlaplus] How can I modelcheck an angle-bracket action formula?***From:*Stephan Merz

**Re: [tlaplus] How can I modelcheck an angle-bracket action formula?***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] How can I modelcheck an angle-bracket action formula?** - Next by Date:
**[tlaplus] Re: TLC error with INSTANCE mechanism** - Previous by thread:
**Re: [tlaplus] How can I modelcheck an angle-bracket action formula?** - Next by thread:
**[tlaplus] TLC Error ,Take 2** - Index(es):