Limiting lengths of all sequences for TLC model checking

[Serdar Tasiran]

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

 

[Stephan Merz]

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,

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

[Leslie Lamport]

Here's a little more detail to explain Stephan's response.  TLC has a mechanism for replacing a definition in a module with Java methods that TLC uses to evaluate expressions containing the defined operator.  This mechanism is used for the definition of Seq in the standard Sequences module.  It allows TLC to evaluate an expression like  <<-42>> \in Seq(Nat) even though TLC can't evaluate Seq(Nat).  In the Sequences module, Seq is defined in terms of Nat.  However, because TLC does not use that definition in evaluating expressions containing Seq, overriding the definition of Nat does not change how TLC evaluates expressions containing Seq.

I believe that all the definitions in most of the standard modules are replaced by Java code in this way.  (I'm not sure about the Bags module.)  I also believe that overriding a definition in a model does what it should.  In your example, overriding the definition of Seq with the definition that appears in the Sequences model should work.  Thus you could use the definition

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

in the model.  (The Nat in this definition will be the one defined by your overriding of the definition of Nat.)

I haven't tested this; please let us know if anything I've written is incorrect.

Leslie

[Serdar Tasiran]

Thank you very much, Stephan and Leslie, for your quick responses and explanations. I will try your suggestions and report.

Serdar