Re: [tlaplus] my first tla program

[Bert_emme <bertan...@xxxxxxxxx>]

hi Merz,

I have two questions:

1) If i don't use INSTANCE I use a recursive function to define Prime module? 

2) If I have two module either with one variable prime but in the second module I call three different time the first module, I need to specify the INLness? The INLness is essential relate at one module or a the relation between two module?For example the clock module  if it has more than two variable primed needs the INLness, but if I call a module for three time I have the exclude the possibility that these three call happend the same time? I have to exclude the possibility that the change of the primed variable of the first module happends when change the primed variable of the second module?

I'm  so much in trouble...

I must to re-read the chapter... I think

thanks in advance

Mauro

On Monday, January 6, 2014 9:34:07 AM UTC+1, Stephan Merz wrote:

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 <bert...@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...@googlegroups.com.
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.