If spec A has more than a one variable that does not appear in the other

spec, we unfortunately have to adapt the composition and create more
restsOfTheUniverse.

The next-state relation of this composition evaluates to false after the
initial state, because it defines variables z and zz to always have
equal values.  This is only satisfied in the special case where the
values of variables z and zz in A are equal throughout all behaviors
(e.g. Init changed to ... /\ zz = TRUE).

Author: lemmy

specifications/composition/Composition.tla

@@ -23,12 +23,14 @@ VARIABLES x, \* Abstract/very high-level representation of the overall computati
           y, \* Represents the phase that the composed system is in.
              \* This toy example has three phases: <<"A", "B", "C">>.
           z  \* z is the variable that is only going to be present in spec A.
-varsA == <<x, y, z>>
+          ,zz  \* The more the merrier.
+varsA == <<x, y, z, zz>>
 
 InitA ==
   /\ x = 0
   /\ y = "A"
   /\ z = TRUE
+  /\ zz= FALSE \* Could happen to be zz=TRUE.
 
 NextA == 
   /\ y = "A"
@@ -37,6 +39,7 @@ NextA ==
      THEN y' = "B"
      ELSE UNCHANGED y
   /\ z' = ~ z
+  /\ zz'= ~ zz
 
 ==================================
 
@@ -83,7 +86,7 @@ vars ==
 (* Down here we know about the internals  *)
 (* of spec A and B (whitebox component).  *)
 
-INSTANCE A WITH z <- restOfTheUniverse
+INSTANCE A WITH z <- restOfTheUniverse, zz <- restOfTheUniverse
 
 Spec == InitA /\ InitB /\ [][ \/ [NextA]_vars
                               \/ [OpenNextB]_vars
@@ -94,6 +97,6 @@ THEOREM Spec => Inv
 
 =============================================================================
 \* Modification History
-\* Last modified Fri Jun 12 16:30:33 PDT 2020 by markus
+\* Last modified Fri Jun 12 16:44:17 PDT 2020 by markus
 \* Last modified Fri Jun 12 16:30:19 PDT 2020 by Markus Kuppe
 \* Created Fri Jun 12 10:30:09 PDT 2020 by Leslie Lamport