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

Re: [tlaplus] Limiting lengths of all sequences for TLC model checking

Hi Serdar,

redefining Nat doesn't limit the length of sequences because they are built into TLC. You can redefine the Seq(_) operator, writing something like

Seq(S) == UNION { [1 .. n -> S] : n \in 0 .. 3 }

Hope this helps,
best regards,


On 22 Mar 2017, at 18:23, Serdar Tasiran <stas...@xxxxxxxxx> wrote:


I have a TLA+ module that has lots of state variables that are sequences of records. I am looking for a way to easily limit the lengths of all sequences for model checking with TLC.

Redefining Nat to be, say, {0, 1, 2, 3} didn't do the trick (limit lengths of sequences to 4) I still get the following 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

: Attempted to enumerate a set of the form [l1 : v1, ..., ln : vn],

but can't enumerate the value of the `...list" field"

Is this because TLC can't enumerate sequences or because I was unsuccessful in limiting lengths of sequences by redefining Nat?

Suggestions for a clean and convenient way of limiting all sequence lengths in a TLC module would be much appreciated. I have maps from a set to records which have fields that contain sequences of records (which themselves may contain sequences) so enumerating all state variables of type sequence and formulating a constraint on their length would be *very* clumsy.

Thank you.
Serdar Tasiran

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 post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.