Re: [tlaplus] Checking FIFO module

[TLA Plus <tlapl...@xxxxxxxxx>]

Dear Yuri,

Let me expand a bit on Stephan's reply.  First of all, in addition to
using the Toolbox, I recommend reading the Hyperbook in addition to
(or even instead of) "Specifying Systems".

It is true that TLC does not handle parametrized instantiation.  However, you don't understand what that means.  The statement 

   Inner(q) == INSTANCE InnerFIFO

in module FIFO is parametrized instantiation because of the "(q)".
The statement

   InChan == INSTANCE Channel WITH ...

in module InnerFIFO is UNparametrized instantiation.

The only kind of spec that TLC can handle is one that is logically
of the form

   Init /\ [][Next]_vars /\ some fairness condition

When analyzing a temporal specification that you give it, TLC first
looks for the Init conjunct.  If it can't find it, it reports an
error.  Formula Spec of module FIFO is not of this form because it
equals \EE q : ...  ; hence the error message saying that there was no initial state predicate.  For reasons I don't understand, TLC fails tofind the Init predicate for a specification defined by parametrized instantiation.  Hence, the "Can also be caused by..." part of the error message.

 

It is also true that TLC can't handle the \EE operator, so it won't check that a spec satisfies a property that uses \EE.

Leslie Lamport

On Wed, Apr 24, 2013 at 7:36 AM, Stephan Merz <stepha...@xxxxxxxxx> wrote:

Dear Yuri,

TLC doesn't handle quantification over variables (the \EE operator) – see Section 14.1 of "Specifying Systems". Since

   (\EE q : Inner(q)!Spec) => P

holds if and only if Inner(q)!Spec => P is true (provided P doesn't contain q), you can check properties of the FIFO queue by checking them over the specification in module InnerFIFO. If you are trying to prove that some algorithm implements a FIFO queue, i.e.

  Impl => \EE q : Inner(q)!Spec

you need to define a suitable refinement mapping, as explained in the book.

NB: Your message sounds like you are using the command-line version of TLC; I suggest that you switch to the Toolbox that simplifies specifying the model that you intend to check,

Hope this helps,

Stephan

On Apr 24, 2013, at 7:32 AM, Y2i <yur...@xxxxxxxxx> wrote:

When I run TLC Model checker on FIFO module from the Specifying Systems book, I get the following error:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException: 
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.

My configuration specified Temporal Formula: Spec and Message <- {1, 2}

Did I need to specify initial state predicate or is it because TLC does not support modules imported with parameterized INSTANCE statement?

I was able to run TLC on InnerFIFO which uses parameterized instantiation of Channel and my config file also did not have initial state predicate specified.  May be the reason is that FIFO uses  existential temporal quantifier?

Thank you in advance for your help.

Yuri

-------------------------------- MODULE FIFO --------------------------------
CONSTANT Message
VARIABLES in, out
Inner(q) == INSTANCE InnerFIFO
Spec == \EE q : Inner(q)!Spec
=============================================================================

--
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?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

--
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?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.