How can I modelcheck an angle-bracket action formula?

[Andrew Helwer]

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

Does TLC only support [][A]_v, not []<<A>>_v?

[Andrew Helwer]

Also it seems like monospace fonts are now broken on google groups, anybody else have this problem? Or perhaps it is only mixing monospace and ordinary fonts; I will experiment by making this entire message monospace.

[Stephan Merz]

[]<<A>>_v is not a TLA formula, I believe you meant to write 

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

Stephan

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2c52bdc7-3ffa-44f5-8672-368528f6b74bn%40googlegroups.com.

[Andrew Helwer]

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

[Andrew Helwer]

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.