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

Re: [tlaplus] Verifying refinement

Hello Pedro,

since your high-level spec says that both variables change in one step, a refinement cannot change them one variable at a time. Indeed, let’s assume for simplicity that value1 and value2 are distinct from the initial values of the variables and that your action is the only non-stuttering action of the spec. Then the “simple” spec satisfies the invariant [](var1=value1 <=> var2=value2), but the low-level spec does not. The point of refinement is that all high-level properties proved of the high-level spec continue to hold of the implementation.

Your split is a valid refinement if one variable, say var1, is an internal variable of the high-level specification and cannot be observed from the environment, i.e. if your high-level specification is really 

\EE var1 : Simple!Spec

TLC cannot check properties that contain flexible quantifiers but you can define a refinement mapping when you instantiate the high-level module, as follows (with the analogous simplifying assumptions as above and denoting the initial value of var1 by init1):

hvar1 == IF var2=value2 THEN value1 ELSE init1
Simple == INSTANCE Highlevel WITH var1 <- hvar1

Now you can use TLC to verify Simple!Spec (which is a copy of the formula Spec in module Highlevel where var1 has been replaced by hvar1). In effect, SplitAction1 now appears like a stuttering action to the high-level spec, whereas SplitAction2 appears to update both variables.

Hope this helps,

On 11 Mar 2018, at 19:45, Pedro Paiva <pedr...@xxxxxxxxx> wrote:

Hi there,

Suppose we have two modules and one module should be the refinement of the other one (let's call them module Simple and module Implementation). Module Simple has one action that is split into two actions within module Implementation. For example

SimpleAction ==
    /\ var1' = value1
    /\ var2' = value2

SplitAction1 ==
    /\ var1' = value1
    /\ UNCHANGED var2

SplitAction2 ==
    /\ var2' = value2
    /\UNCHANGED var1

When I try to check "Simple!Spec" would it produce an error trace? Since in module Simple, there are no actions that change the values of "var1" and "var2" separately. Is it incorrect thinking that module Implementation is a refinement of module  Simple? I mean, in this situation am I conceptually wrong about refinement? Thanks!


Pedro Yuri Arbs Paiva
Engenheiro Eletrônico
Instituto Tecnológico de Aeronáutica (T-16)
(+55) 12 98106-4129

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 https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.