[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] create a specification from another one and eliminating some variables

Hello Amira,

I am not sure I understand your question. The canonical way for hiding an internal variable x from a specification is existential quantification:

   Internal == ... \* specification involving x and y

   Spec == \EE x : Internal

A behavior (i.e., a sequence of states) satisfies Spec if there is a way to assign suitable values to x at every state such that the resulting behavior satisfies Internal. (The fine print is explained for example in chapters 4 and 8.8 of "Specifying Systems".)

Perhaps your question is how one can verify properties of a specification involving such quantifiers? Neither TLC nor TLAPS currently support quantification over state variables. In order to prove properties of Spec above, note that

   Spec => Property

holds if and only if

   Internal => Property

holds (this is just an application of a standard quantifier rule), so you may just as well use the formula without the quantifier. In order to prove refinement of Spec, i.e. verify

   Implementation => Spec

for some formula Implementation that represents a lower-level implementation of your specification, the standard approach is to use a refinement mapping: define a state function

   ximpl == ...  \* defined in terms of the variables of formula Implementation

such that you have

   Implementation => Internal[ximpl / x]

where the latter denotes formula Internal with x substituted by ximpl. TLA+ does not have explicit syntax for substitution, so you'll write something like (in the module containing formula Implementation, and assuming that formula Internal appears in a module called Highlevel)

   HL == INSTANCE Highlevel WITH x <- ximpl

then check (using for example TLC) that you have the implementation

   Implementation => HL!Internal

I recommend that you also look at sections 6.6ff. or sections 8.4ff. of the hyperbook.

Hope this helps,


On 06 Jul 2014, at 13:45, Amira Methni <methni...@xxxxxxxxx> wrote:


I have a specification S1 with two variables "x" and "y". And the value of "y" depends on "x".
I'm interested to create a specification S2 through S1, based only on the values of "y" with eliminating "x". So, the space state of S2 is based only on the values of "y". 
Is it possible to do this in TLA+?

Thank you

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/d/optout.