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, Stephan
|