Rules for writing formulae with primed variables

[Mathew Kuthur James]

Hi, I was playing around with a simple TLA+ model and noticed the following:

---- MODULE m ----

EXTENDS Integers, FiniteSets

VARIABLES t

_Init == t = 0

_Next == t' \in 1..10

====

TLC ran successfully. When I edited it like so:

---- MODULE m ----

EXTENDS Integers, FiniteSets

VARIABLES t

_Init == t = 0

_Next == t' <= 10 /\ t' >= 0

====

It produced an error message:

"TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
:
In evaluation, the identifier t is either undefined or not an operator."

This happens on both the VSCode extension and the toolbox. Is there a set of rules about how expressions involving primed variables ought to be written? From what I understand, both specs mean the same thing.

[Markus Kuppe]

No, the two specifications are not equivalent. Remember that TLA+ is untyped, so you cannot infer from

  t' ≤ 10 ∧ t' ≥ 0

that

  t' ∈ 1‥10.

Adding the conjunct t' ∈ Nat makes Apalache accept the spec, but for TLC you will also have to redefine Nat to something like 0..100 for it to evaluate your spec. That is obviously not what you intend.

Note that the TLA Proof System (TLAPS) will happily discharge the following:

THEOREM
ASSUME NEW t
PROVE t ∈ 0..10 ⇔ (t ≥ 0 ∧ t ≤ 10 ∧ t ∈ Nat)
OBVIOUS

M.

---- MODULE m ----
EXTENDS Integers

MyNat == 0..100

VARIABLES
\* @type: Int;
t

Init == t = 0

Next == t' \in Nat /\ t' <= 10 /\ t' >= 0

THEOREM ASSUME NEW q PROVE q \in 0..10 <=> q >= 0 /\ q <= 10 /\ q \in Nat OBVIOUS
====
---- CONFIG m ----
INIT Init
NEXT Next
CONSTANT Nat <- MyNat
====

[Andrew Helwer]

Specifying Systems page 230 has a section titled “What TLC Can Cope With” which covers TLC’s abilities. For primed variables it can pretty much only handle expressions like x' = value and x’ \in set. However, once the value of x’ has been “fixed” in an expression by either of these, you can use x’ in any TLA+ expression and it will resolve to the fixed value. So you could write:

/\ x’ \in 1 .. 10

/\ x’ > 3

/\ x’ <= 5

And this would be true of steps where the next value of x is 4 or 5.

--
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 visit https://groups.google.com/d/msgid/tlaplus/D9EC5A11-8476-4043-AF2E-5DCC1F3E359E%40lemmster.de.

[Rob Fielding]

is it not the case that you use the primed symbol once, after you evaluated the unprimed guards.

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUWc-nrPN8qXnXLtbxna7i2U4xg99K221ZVL8mYwxjnuuA%40mail.gmail.com.

--

https://rfielding.github.io

https://github.com/rfielding

[Andrew Helwer]

Nope, you can use the primed variables as many times as you want. This is a way of writing postconditions, in the same way you write preconditions using unprimed variables. Of course if your postconditions are contradictory then that action will not generate/match any next states.

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CADvX%2BjUtHzAkOO2bByNcHDnWVmgEHssy7b9U_BLLHF-z-Peumg%40mail.gmail.com.