When TLC was implemented, it was decided that it would be a waste to compute a state and then not check invariants on it. The problem you describe was discovered soon afterwards. As you observed, the solution involves adjusting the invariant or the constraint so the invariant is not violated by the first state encountered that does not satisfy the constraint. There exists a trivial way to do that--namely, have TLC check the invariant Invariant \/ ~Constraint, but in practice a simpler solution usually exists. It was therefore decided that this problem was not serious enough to warrant changing the decision to check invariants on all computed states.
Leslie
On Friday, September 28, 2012 9:50:14 AM UTC-8, Chris Newcombe wrote:
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