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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Wed, 18 Jan 2023 07:50:48 -0800 (PST)

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

====

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 Monotonic

NEXT Next

PROPERTY Monotonic

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

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+unsubscribe@xxxxxxxxxxxxxxxx.

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

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

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

- Prev by Date:
**[tlaplus] Re: TLC error with INSTANCE mechanism** - Next by Date:
**[tlaplus] Re: How can I modelcheck an angle-bracket action formula?** - Previous by thread:
**Re: [tlaplus] Confusing line in paxos tlaps proof (USE TRUE /\ TRUE)** - Next by thread:
**[tlaplus] Re: How can I modelcheck an angle-bracket action formula?** - Index(es):