On Friday, April 12, 2013 7:19:38 PM UTC+2, Leslie Lamport wrote:
Dear Bert_emme,
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
single module.
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
the error.
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.
Leslie Lamport
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
bye