preprint submitted 2024/06/21

2024_RAMiCS_Migration/Kurk.adl

@@ -4,7 +4,7 @@ PURPOSE CONTEXT MigrationDemo MARKDOWN
 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 violations of the totality rule: `"a2"` and `"a3"`.
+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".
@@ -29,29 +29,50 @@ RELATION new_r[A*B] [UNI]
 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 violations that are fixed.
--- The helper relation is needed to ensure that the fixing of violations terminates.
+-- 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 a violation from reoccurring, but allows fixing any remaining violation.
+-- 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 violations that need to be fixed, we generate a business constraint for each new blocking invariant $u$:
+-- 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 "Fix ", SRC I, TXT " by pairing it with an (any) atom from B.")
+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 violations that prohibit deploying the desired system.
--- That is the case when violations of new invariants on the old population have all been fixed:
+-- 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
@@ -61,13 +82,13 @@ INTERFACE "Migration system" : "_SESSION";V[SESSION*A] cRud BOX<TABLE>
            [ "A" : I                        cRud
            , "B": new_r                     CRUd
            ]
-        , copy_r : copy_r                   cRud
-        , fixed_u : fixed_TOTr              cRud
+        -- , copy_r : copy_r                   cRud
+        -- , fixed_u : fixed_TOTr              cRud
         ]
 
 ENDCONTEXT
 
-{+ calculate the violations of the old rule. +}
+{+ calculate the inconsistencies of the old rule. +}
     - (Antecedent |- Consequent)
 <=>    { definition of |- }
     -(-Antecedent \/ Consequent)