Search code examples
tla+

How do I model-check a module that depends on an unbound variable?

I'm going through Specifying Systems right now and I'm a little puzzled about how I'd model-check the following module:

---------------------------- MODULE BoundedFIFO ----------------------------
EXTENDS Naturals, Sequences
VARIABLES in, out
CONSTANT Message, N
ASSUME (N \in Nat) /\ (N > 0)

Inner(q) == INSTANCE InnerFIFO

BNext(q) == /\ Inner(q)!Next
            /\ Inner(q)!BufRcv => (Len(q) < N)

Spec == \EE q : Inner(q)!Init /\ [][BNext(q)]_<<in, out, q>>
=============================================================================

I see that both the Init and BNext formulas are operators, parameterized by q. How would I supply this to the model checker?

Solution

  • You can't: \E x : P(x) is an unbounded expression, which TLC cannot handle. Many of the specs in Specifying Systems can't be modeled. More recent guides, such as the TLA+ Hyperbook or Learn TLA+, are more careful to keep all of their specs modelable.