Re: [tlaplus] my first tla program

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello,

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

documented in http://research.microsoft.com/en-us/um/people/lamport/tla/current-tools.pdf.

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,

Stephan

On 05 Jan 2014, at 22:04, Bert_emme <bertan...@xxxxxxxxx> wrote:

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 

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.