On Friday, April 12, 2013 7:19:38 PM UTC+2, Leslie Lamport wrote:
A casual glance at your specification indicates that it is not correct. Here is what I recommend that you do.
1. Stop using instantiation--that is, don't use INSTANCE. Write your
complete spec in a single module. Don't worry about splitting your
spec into multiple modules until you can correctly write one in a
2. Use TLC to debug your spec. When TLC reports an error, use the
Toolbox's help pages and the Hyperbook to figure out what caused
3. Post a further question to this group only if you get an error report
that you can't understand. In that case, include the spec, a
description of the model, and the error report.
Hi, I'm recurrance... I have a problem with instancesation...
I have a problem with NZ-system... Or I think so...
The system error is:
The configuration file did not specify the initial state predicate.
Can also be caused by trying to run TLC on a specification from
a module imported with a parameterized INSTANCE statement.
This error appear after and post my study over NZ system.
In the inner module I have write the follow restriction:
Calculate == \E r \in Nat : q'=r /\ q = r-1
I assume two costant rho and omega where I give them the value 3600 and 10
I hope I will be exaustive
Thanks in advance