WIP

2022Migration/articleMigrationFACS.tex

@@ -640,8 +640,10 @@ \subsection{Algorithm for generating a migration script}
       \dataset_\migrsys={}&\overleftarrow{\dataset}\cup\overrightarrow{\dataset'}
    \end{align}
 \item\label{step2} We create transactional invariants to copy the population of relations from $\dataset$ to $\dataset'$:
-For every relation $r$ shared by the existing and desired systems, we generate a helper relation: ${\tt copy}_r$, and a transactional invariant to produce its population.
-We also generate a transactional invariant to populate the relation $\overrightarrow{r}$ (in the desired system).
+   For every relation $r$ shared by the existing and desired systems, we generate a helper relation: ${\tt copy}_r$, and two transactional invariants.
+   The first transactional invariant populates relation $r$ and the second populates ${\tt copy}_r$.
+   The helper relation ${\tt copy}_r$ contains the triples that have been copied.
+   We use the helper relation to keep the transactional invariants from immediately repopulating $\overrightarrow{r}$ when a user deletes triples in it.
 % \begin{verbatim}
 %    RELATION copy.r[A*B]
 %    RELATION new.r[A*B] [UNI]
@@ -650,38 +652,21 @@ \subsection{Algorithm for generating a migration script}
 % \end{verbatim}
    \begin{align}
       \rels_1={}&\{{\tt copy}_r\mid r \in \rels_{\schema'}\cap\rels_{\schema}\}\\
-      \transactions_1={}&\{{\tt copy}_r\mapsfrom \popF{\overrightarrow{r}\cap\overleftarrow{r}} \mid r \in\rels_1\}\cup\{\overrightarrow{r}\mapsfrom \popF{\overleftarrow{r}-{\tt copy}_r} \mid r \in\rels_1\}
+      \transactions_1={}&\{\overrightarrow{r}\mapsfrom \popF{\overleftarrow{r}-{\tt copy}_r} \mid r \in\rels_1\}\cup\{{\tt copy}_r\mapsfrom \popF{\overrightarrow{r}\cap\overleftarrow{r}} \mid r \in\rels_1\}
    \end{align}
-   The helper relation is needed to ensure that the copying process terminates,
-   which is the case when:
+   The copying process terminates when:
    \begin{align}
       \forall r\in\rels_1.~\overleftarrow{r}={\tt copy}_r\label{eqn:copyingTerminates}
    \end{align}
-   (Step~\ref{step2} contains a problem: How can we be sure that last minute deletes in the existing system are propagated to the desired system?)
 
-\item The new blocking invariants are $\rules_{\schema'}-\rules_{\schema}$.
-   For each new blocking invariant $u$, we generate a helper relation: ${\tt fixed}_u$, to register all violations that are fixed.
-   We also need a transactional invariant to produce its population:
-% \begin{verbatim}
-%    RELATION fixed_TOTr[A*A]
-%    ENFORCE fixed_TOTr >: I /\ new.r;new.r~
-% \end{verbatim}
-   \begin{align}
-      \rels_2={}&\{{\tt fixed}_u\mid u \in \rules_{\schema'}-\rules_{\schema}\}\\
-      \transactions_2={}&\{{\tt fixed}_u\mapsfrom\lambda\dataset.~\viol{\overleftarrow{u}}{\dataset}-\viol{\overrightarrow{u}}{\dataset}\mid u\in\rules_{\schema'}-\rules_{\schema}\}\label{eqn:enforceForRules}
-   \end{align}
-   The helper relation is needed to ensure that the fixing of violations terminates,
-   which is the case when:
-   \begin{align}
-      \forall u\in\rules_{\schema'}-\rules_{\schema}.~\viol{\overrightarrow{u}}{\dataset}={\tt fixed}_u\label{eqn:fixingTerminates}
-   \end{align}
-\item For each new blocking invariant $u$, we generate another blocking invariant $v$ in the migration system that blocks fixed violations from recurring:
+\item\label{step3} For each new blocking invariant $u$, we generate another blocking invariant $v$ in the migration system that blocks fixed violations from recurring:
 % \begin{verbatim}
 %    RULE Block_TOTr : fixed_TOTr |- new.r;new.r~
 %    MESSAGE "Relation r[A*B] must remain total."
 %    VIOLATION (TXT "Atom ", SRC I, TXT " must remain paired with an atom from B.")
 % \end{verbatim}
    \begin{align}
+      \rels_2={}&\{{\tt fixed}_u\mid u \in \rules_{\schema'}-\rules_{\schema}\}\\
       \rules_\text{block}={}&\{v\ 
       \begin{array}[t]{l}
          \text{\bf with}\\
@@ -691,7 +676,22 @@ \subsection{Algorithm for generating a migration script}
       &\mid u\in\rules_{\schema'}-\rules_{\schema}\}\notag
    \end{align}
    Note that the blocking invariants from $\schema'\cap\schema$ are also used in $\migrsys$ to ensure continuity.
-\item To signal users that there are violations that need to be fixed, we generate a business constraint for each new blocking invariant $u$:
+\item\label{step4} The new blocking invariants are $\rules_{\schema'}-\rules_{\schema}$.
+   For each new blocking invariant $u$, we generate a helper relation: ${\tt fixed}_u$, to register all violations that are fixed.
+   We also need a transactional invariant to produce its population:
+% \begin{verbatim}
+%    RELATION fixed_TOTr[A*A]
+%    ENFORCE fixed_TOTr >: I /\ new.r;new.r~
+% \end{verbatim}
+   \begin{align}
+      \transactions_2={}&\{{\tt fixed}_u\mapsfrom\lambda\dataset.~\viol{\overleftarrow{u}}{\dataset}-\viol{\overrightarrow{u}}{\dataset}\mid u\in\rules_{\schema'}-\rules_{\schema}\}\label{eqn:enforceForRules}
+   \end{align}
+   The helper relation is needed to keep violations from reoccurring after they have been fixed.
+   The process is complete when:
+   \begin{align}
+      \forall u\in\rules_{\schema'}-\rules_{\schema}.~\viol{\overrightarrow{u}}{\dataset}={\tt fixed}_u\label{eqn:fixingTerminates}
+   \end{align}
+\item\label{step5} To signal users that there are violations that need to be fixed, we generate a business constraint for each new blocking invariant $u$:
 % \begin{verbatim}
 %    ROLE User MAINTAINS TOTr
 %    RULE TOTr : I |- new.r;new.r~
@@ -868,7 +868,7 @@ \subsection{System properties}
 \section{Proof of Concept}
 \label{sct:PoC}
    By way of proof of concept (PoC), we have built a migration system in Ampersand.
-   To demonstrate it in the context of this paper, the existing system, $\pair{\dataset}{\schema}$, is almost trivial.
+   To demonstrate it in the context of this paper, the existing system, $\pair{\dataset}{\schema}$, is rather trivial.
    It has no constraints and just one relation, $\declare{r}{A}{B}$.
    Its population is $A=\{a_1,a_2,a_3\}$, $B=\{b_1\}$, and $\pop{r}{\dataset}=\{\pair{a_1}{b_1}\}$.
    The schema of the migration system, $\schema_\migrsys$, follows from definition~\ref{eqn:schema migrsys}.