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

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

• From: Stephan Merz <Stepha...@xxxxxxxxx>
• Date: Sun, 6 Jul 2014 14:13:51 +0200
• References: <16e13377-95ec-4927-bbe1-2e14186ce9fd@googlegroups.com>

 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 : InternalA 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 => Propertyholds if and only if   Internal => Propertyholds (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 => Specfor 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 Implementationsuch 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 <- ximplthen check (using for example TLC) that you have the implementation   Implementation => HL!InternalI recommend that you also look at sections 6.6ff. or sections 8.4ff. of the hyperbook.Hope this helps,StephanOn 06 Jul 2014, at 13:45, Amira Methni wrote:Hi,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.