without seeing your spec it is impossible to guess what the problem is.
1. Did you follow Leslie's advice and write your specification as a single module? In particular, Leslie told you in a previous message about the limitation of TLC handling parameterized instantiation as in
Op(x) == INSTANCE SomeModule WITH someConstant <- x
2. The definition
Calculate == \E r \in Nat : q'=r /\ q = r-1
cannot be evaluated by TLC because it contains quantification over an infinite set. You can instruct TLC to substitute a finite set for Nat (see Advanced Options -> Definition Override). But this does not seem to be the cause of your problem because you would have gotten a different error message.
Hope this helps,
On 05 Jan 2014, at 22:04, Bert_emme <bertan...@xxxxxxxxx> wrote: