Hi,
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