State-constraints and invariants

[Chris Newcombe <chris.n...@xxxxxxxxx>]

Page 242 of Specifying Systems[1] describes how TLC checks invariants on a state, before it checks whether the state (step) satisfies the state-constraint (action-constraint).

That makes things slightly awkward in the case described below.  I have a clumsy workaround, also described below.  
Is there a better way?

thanks,

Chris

I have a variable drawn from a large set of numeric identifiers

Ids == Nat    \* In the real system, the set of identifiers is practically unbounded.

And a variable which uses it, plus a type-invariant that checks it:

TypeInvariant == currentId \in Ids

When model-checking my specification, TLC apparently need to enumerate the set Ids.
So I override the definition of Ids with a finite set, say

Ids <- 0..4

But even with that override, TypeInvariant can still be violated when actions do things like

 currentId' = currentId + 1

So I also use a state-constraint to bound the state-space. 
First I tried the obvious:

MC_StateConstraint == currentId \in Ids

But this state-constraint isn't strong enough to prevent TypeInvariant from being violated,  because TLC checks invariants before it checks the state-constraint.  

In this case there's an obvious if somewhat clunky workaround:

MC_StateConstraint ==
    LET constrained_ids == Ids \ {Max(Ids)}
    IN  currentId \in constrained_ids

But in the general case with more complex values (nested values), I suspect the state-constraint could get quite messy. 
I admit that's speculation at the moment.  For now my workaround is fine.

[1] http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf