Skip to content

Commit

Permalink
minor textual edits
Browse files Browse the repository at this point in the history
  • Loading branch information
sjcjoosten committed Jun 7, 2024
1 parent bdf30f7 commit c16512e
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions 2022Migration/articleMigrationRaMiCS.tex
Original file line number Diff line number Diff line change
Expand Up @@ -657,7 +657,7 @@ \subsection{Generating a migration script}
Let $\pair{\dataset}{\schema}$ be the existing system.
Let $\pair{\dataset'}{\schema'}$ be the desired system in its initial state.
\begin{enumerate}
\item We take a disjoint union of the data sets by relabeling relation names, so the migration script can refer to relations from both systems:
\item We take a disjoint union of the data sets by relabeling relation symbols, so the migration script can refer to relations from both systems:
\begin{align}
\dataset_\migrsys={}&\overleftarrow{\dataset}\cup\overrightarrow{\dataset'}
\end{align}
Expand Down Expand Up @@ -733,7 +733,7 @@ \subsection{Generating a migration script}
\transactions_2\ =\ \{{\tt fixed}_u\mapsfrom\lambda\dataset.~\cmpl{\viol{u}{\dataset} \cup \pop{{\tt fixed}_u}{\dataset}}\mid u\in\overrightarrow{\rules_{\schema'}-\rules_{\schema}}\}\label{eqn:enforceForRules}
% Opmerking van SJC: de {\tt fixed}_u aan de rechterkant is nodig om aan (\ref{eqn:transaction}) te voldoen.
\end{equation}
\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$:
\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 denoted by $u$:
% \begin{verbatim}
% ROLE User MAINTAINS TOTr
% RULE TOTr : I |- new.r;new.r~
Expand All @@ -750,7 +750,7 @@ \subsection{Generating a migration script}
&\mid u\in\overrightarrow{\rules_{\schema'}-\rules_{\schema}}\}\notag
\end{align}
In some cases, a migration engineer can invent ways to satisfy these invariants automatically.
For this purpose, the generator must produce source code (as opposed to compiled code) to allow the migration engineer
This is one of the places where it is useful for the generator to produce source code (as opposed to compiled code) to allow the migration engineer
to replace a business constraint with transactional invariants of her own making.
After all violations are fixed, i.e. when equation~\ref{eqn:readyForMoC} is satisfied,
the migration engineer can switch the ingress to the desired system.
Expand Down

0 comments on commit c16512e

Please sign in to comment.