Merge branch 'master' into Migration

* master:
  preprint submitted 2024/06/21
  adapted Kurk.adl for migration demo
  transfer Migration paper to RAMiCS
  Consolidate Kurk.adl and Migration.thy
  moved paper to directory 2024_FoIKS_Migration
  Consolidate the submission of FoIKS 2024
  submitted to FoIKS 2024
  WIP
  Final touch
  one benefit added
  small enhancements proposal brief
  proposal brief made
  teaser gemaakt
  Initial research proposal with Tim

# Conflicts:
#	Generative Software/articleMigrationRaMiCS.tex

2024_RAMiCS_Migration/Kurk.adl

@@ -0,0 +1,99 @@
+CONTEXT MigrationDemo
+PURPOSE CONTEXT MigrationDemo MARKDOWN
+{+ This script will demo part of the migration of just one relation: `r[A*B]`.
+The demo is done on the old Ampersand platform (RAP4).
+
+### Intro
+Relation: `r[A*B]` contains just one pair: `("a1", "b1")`, but there are two inconsistencies of the totality rule: Atoms `"a2"` and `"a3"` are not source atoms in any pair.
+This is shown in the left part of the screen, in column `Old`.
+Column `Migration` shows the migrated relation `r[A*B]`.
+You can demonstrate all insert and delete operations in the migration environment by adding or removing atoms in the column "Migration".
+Note the field "block". This field signals that this record can no longer violate the rule.
+This recipe works for any rule of the form `RULE a |- c`, not just totality.
+Totality has the form `a=I` and `c=r;r~`, so it has the right form.
++}
+
+POPULATION A CONTAINS [ "a1", "a2" , "a3" ]
+POPULATION B CONTAINS [ "b1", "b2" , "b3" ]
+RELATION old_r[A*B] [UNI] = [ ("a1", "b1") ]
+-- The totality of r applies in the migration system, not in the existing situation.
+-- So `RULE I |- old_r;old_r~` is not satisfied, but `RULE I |- new_r;new_r~` is.
+
+REPRESENT B TYPE ALPHANUMERIC -- This is only here to smoothen the demo.
+
+-- The following copies `old_r` to `new_r`. `copy_r` is needed to ensure that `new_r` can be edited after copying.
+-- For every relation $r$ shared by the existing and desired systems, we generate a helper relation: ${\tt copy}_r$, and a transaction to produce its population.
+RELATION copy_r[A*B]
+RELATION new_r[A*B] [UNI]
+-- We create a transactions (enforcement rules) to copy the population of relations from `old_r` to `new_r`.
+ENFORCE copy_r >: new_r /\ old_r
+ENFORCE new_r >: old_r - copy_r
+
+-- For each new blocking invariant $u$, we generate a helper relation: ${\tt fixed}_u$, to register all inconsistencies that are fixed.
+-- The helper relation is needed to ensure that the fixing of inconsistencies terminates.
+RELATION fixed_TOTr[A*A]
+-- We also need a transaction to produce its population:
+ENFORCE fixed_TOTr >: I /\ new_r;new_r~
+-- The following blocks an inconsistency from reoccurring, but allows fixing any remaining inconsistencies.
+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.")
+
+-- To signal users that there are inconsistencies that need to be fixed, we generate a business constraint for each new blocking invariant $u$:
+ROLE User MAINTAINS TOTr
+RULE TOTr : I |- new_r;new_r~
+MESSAGE "Please, make relation r[A*B] total."
+VIOLATION (TXT "Pair ", SRC I, TXT " with an (any) atom from B.")
+
+-- The migration engineer can switch all traffic to the desired system
+-- after resolving the inconsistencies that prohibit deploying the desired system.
+-- That is the case when inconsistencies of new invariants on the old population have all been fixed:
+ROLE User MAINTAINS CleanUp_TOTr
+RULE CleanUp_TOTr : V[ONE*A] ; (I - fixed_TOTr) ; V[A*ONE]
+MESSAGE "Now you can remove the migration system because relation r[A*B] is total."
+
+RELATION blocking_r[A*B] [UNI] = [ ("a1", "aap"), ("a2", "noot"), ("a3", "mies") ]
+RULE blocking_r : I[A] |- blocking_r;blocking_r~
+INTERFACE "Blocking Invariant demo" : "_SESSION";V[SESSION*A] cRud BOX<TABLE>
+        [ "r" : I cRud BOX<TABLE>
+           [ "A" : I                        cRud
+           , "B" : blocking_r               CRUd
+           ]
+        ]
+
+RELATION business_r[A*B] [UNI] = [ ("a1", "b1") ]
+RULE business_r : I[A] |- business_r;business_r~
+MESSAGE "Business constraint demo: Relatie r[A*B] moet totaal blijven."
+VIOLATION (TXT "Pair ", SRC I, TXT " with an (any) atom from B.")
+ROLE User MAINTAINS business_r
+INTERFACE "Business constraint demo" : "_SESSION";V[SESSION*A] cRud BOX<TABLE>
+        [ "" : I cRud BOX<TABLE>
+           [ "A" : I                        cRud
+           , "B" : business_r               CRUd
+           ]
+         ]
+
+INTERFACE "Migration system" : "_SESSION";V[SESSION*A] cRud BOX<TABLE>
+        [ "old_r" : I cRud BOX<TABLE>
+           [ "A" : I                        cRud
+           , "B" : old_r                    cRud
+           ]
+        , "new_r" : I cRud BOX<TABLE>
+           [ "A" : I                        cRud
+           , "B": new_r                     CRUd
+           ]
+        -- , copy_r : copy_r                   cRud
+        -- , fixed_u : fixed_TOTr              cRud
+        ]
+
+ENDCONTEXT
+
+{+ calculate the inconsistencies of the old rule. +}
+    - (Antecedent |- Consequent)
+<=>    { definition of |- }
+    -(-Antecedent \/ Consequent)
+<=>    { DeMorgan }
+    Antecedent /\ -(Consequent)
+<=>    { definition of binary - }
+    Antecedent - Consequent
++}

2022Migration/articleMigrationRaMiCS.tex → 2024_RAMiCS_Migration/articleMigrationRAMiCS.tex

@@ -483,10 +483,6 @@ \subsection{Data sets}
    For example, $\triple{\text{\atom{Peter}}}{\declare{\id{phone}}{\tt Person}{\tt TelephoneNumber}}{\text{\atom{074238991}}}$ is a triple.
 
    \begin{definition}[Data set]
-   %TODO: SJC weet niet wat hij met dit commentaar aan moet (Review 2):
-   % 
-%Before Def. 1: You could group the implicit parameters of Def. 1
-%into a ``data vocabulary'' $(\AA, \CC, \RR, \src, \trg)$.
    A data set $\dataset$ is a tuple $\pair{\triples}{\instance}$ with finite $\triples \subseteq {\Triple{\Atoms}{\Rels}{\Atoms}}$ and $\instance\subseteq\Pair{\Atoms}{\Concepts}$ that satisfies:
 \begin{eqnarray}
    \triple{a}{\declare{n}{A}{B}}{b}\in\triples&\Rightarrow&a\instance A\ \wedge\ b\instance B
@@ -568,6 +564,7 @@ \subsection{Constraints}
 \end{equation}
    Let us denote a transactional invariant as $r\mapsfrom\violC{u}$ or equivalently $r \mapsfrom \lambda \dataset.~\viol{u}{\dataset}$,
    in which $r=\enfRel{u}$.
+   The symbol $u\in\mathbb{U}$ that refers to $\enfRel{u}\mapsfrom\violC{u}$ is written as $[\enfRel{u}\mapsfrom\violC{u}]$.
 
 
 \subsection{Schemas}
@@ -582,7 +579,7 @@ \subsection{Schemas}
    in which $\concepts\subseteq\Concepts$ is a finite set of concept symbols,
    $\rels\subseteq\Rels$ is a finite set of relation symbols,
    $\rules\subseteq\Constraints$ is a finite set of symbols for blocking invariants,
-   $\transactions\subseteq\Constraints\pfun\Rels$ is a finite set of symbols for transactional invariants,
+   $\transactions\subseteq \Constraints$ is a finite set of symbols denoting transactional invariants,
    and $\busConstraints\subseteq\Constraints$ is a finite set of symbols for business constraints.
 
    \begin{definition}[Schema]
@@ -591,7 +588,7 @@ \subsection{Schemas}
    \declare{n}{A}{B}\in\rels&~\Rightarrow~ A\in\concepts\,\wedge\, B\in\concepts
    \label{eqn:relationsIntroduceConcepts}\\
    u\in\rules\cup\transactions\cup\busConstraints\ \wedge\ \sign{u}=\pair{A}{B}&~\Rightarrow~A\in\concepts\,\wedge\, B\in\concepts\label{eqn:invariant-has-type}\\
-   (\declare{n}{A}{B}\mapsfrom t)\in\mathcal\transactions&~\Rightarrow~ \declare{n}{A}{B}\in \rels\label{eqn:enforcement-has-type}
+   u\in\mathcal\transactions&~\Rightarrow~ \enfRel{u}\in \rels\label{eqn:enforcement-has-type}
 \end{align}
    \end{definition}
    Requirements~\ref{eqn:relationsIntroduceConcepts} and~\ref{eqn:invariant-has-type} ensure that concept symbols mentioned in relations and in the signature of constraints are part of the schema.
@@ -674,34 +671,16 @@ \subsection{Generating a migration script}
 % \end{verbatim}
    \begin{align}
       \rels_1={}&\{{\tt copy}_r\mid r\in\rels_{\schema'}\cap\rels_{\schema}\}\label{eqn:copy relations}\\
-      \transactions_1={}&\{\overrightarrow{r}\mapsfrom \popF{\overleftarrow{r}-{\tt copy}_r} \mid r\in\rels_{\schema'}\cap\rels_{\schema}\}\ \cup\\
-      {}&\{{\tt copy}_r\mapsfrom \popF{\overrightarrow{r}\cap\overleftarrow{r}} \mid r\in\rels_{\schema'}\cap\rels_{\schema}\}\notag
+      \transactions_1={}&\left\{\left[\overrightarrow{r}\mapsfrom \popF{\overleftarrow{r}-{\tt copy}_r}\right] \Bigm\vert r\in\rels_{\schema'}\cap\rels_{\schema}\right\}\ \cup\\
+      {}&\{\left[{\tt copy}_r\mapsfrom \popF{\overrightarrow{r}\cap\overleftarrow{r}}\right] \mid r\in\rels_{\schema'}\cap\rels_{\schema}\}\notag
    \end{align}
    The copying process terminates when:
    \begin{align}
       \forall r\in\rels_{\schema'}\cap\rels_{\schema}.~\overleftarrow{r}={\tt copy}_r\label{eqn:copyingTerminates}
    \end{align}
-
-%TODO:
-% SJC begrijpt niet helemaal wat reviewer 2 hier bedoelt:
-    %(16) Transactional invariants should be elements of $\UU$.
-    %    No such elements can be seen in (16).
-    %
-    %    Are transactional invariants repaired via transactions
-    %    with any specified granularity?
-    %    (16) looks like offering lots of opportunities for race
-    %    conditions during pre-deploy (``starts copying data'')
-    %    if the old system can also delete...
-    %    In particular, it appears that (17) would then be reachable
-    %    in states where even if $\mathcal{D}'$ was empty,
-    %    $new.r \neq old.r = copy_r$,
-    %    because for some pairs $p$ it could happen that:
-    %    1. $p$ is propagated to new.r according to the first part of (16)
-    %    2. $p$ is deleted in old.r via the ingress,
-    %    3. $p$ is not in old.r anymore, and will therefore not be
-    %       copied to copy_r
-    %    4. (17) is reached with $p$ in new.r, but not in old.r and copy.r
-    %    5. The deletion of $p$ being lost invalidates the migration.
+   Since the enforce rules only insert triples, the copying process is guaranteed to terminate.
+   However, deletions in the old system that happen during this copying process might not propagate into the migration system.
+   This may pose a risk to the business with respect to data quality.
 
 \item\label{step3}
    The new blocking invariants are $\rules_{\schema'}-\rules_{\schema}$.
@@ -786,10 +765,11 @@ \section{Proof of Concept}
    Its violations are $\pair{a_2}{a_2}$ and $\pair{a_3}{a_3}$.
    The schema of the migration system, $\schema_\migrsys$, follows from definition~\ref{eqn:schema migrsys}.
 
-   Figure~\ref{fig:PoC} exhibits four successive screenshots,
+   Figure~\ref{fig:PoC} shows four successive screenshots,
    featuring $\overleftarrow{r}$ as {\small\verb#old_r#},
    $\overrightarrow{r}$ as {\small\verb#new_r#}.
-\begin{figure}[bht]
+
+\begin{figure}[!htb]
    \begin{center}
       \includegraphics[scale=0.9]{figures/screenshots2x2.pdf}
    \end{center}