Re: Limiting lengths of all sequences for TLC model checking

[Leslie Lamport <tlapl...@xxxxxxxxx>]

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