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
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.
|