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!