Documentation on transformations

doc/transformations.rst

@@ -38,18 +38,130 @@ We will now continue on how to specify a model transformation through modelling.
 RAMification
 ^^^^^^^^^^^^
 
-Explain how RAMification works and what it does.
-Specifically, which attributes does it add etc.
+To support model transformation, the Modelverse makes use of RAMification.
+In RAMification, the original metamodel is Relaxed, Augmented, and Modified.
+As such, the new metamodel can be used to define model transformation rules.
+
+This consists of the following three phases:
+1. The metamodel is **Relaxed**, such that lower cardinalities are no longer applied.
+   Similarly, constraints are removed, and abstract entities can be instantiated.
+   This is done because in model transformations, we only use a specific part of the metamodel.
+2. The metamodel is **Augmented**, such that new attributes and concepts are added.
+   These new attributes are *label* and *constraint* in the LHS, and *label* and *action* in the right hand side.
+   New concepts that are added, are the LHS and RHS entity.
+   These are the containers for all elements of the LHS and the RHS, respectively.
+3. The metamodel is **Modified**, such that existing attributes are renamed and their types are altered.
+   All attributes have to become constraints on that specific attribute in the LHS, and actions for the new value in the RHS.
+   For example, the *tokens* attribute of a place becomes a constraint function (returning True or False), instead of an attribute of type integer.
+
+RAMification happens in the background in the Modelverse.
+Users can, of course, open the RAMified metamodel just like any other metamodel.
+
+As RAMification makes a distinction between the LHS and RHS, all entities in the metamodel are effectively duplicated: the LHS entities are prefixed with *Pre_*, and the RHS entities are prefixed with *Post_*.
+Similarly, the names of all attributes are prefixed with *constraint_* and *value_*, respectively.
+
+Implicit merge
+^^^^^^^^^^^^^^
+
+As a model transformation considers multiple languages, both for its input and output, it must be possible somewhere to join them.
+For example, a transformation from PetriNets to a ReachabilityGraph formalism, makes use of entities from both metamodels, in the same model.
+To allow for this, all used metamodels are implicitly merged before RAMification.
+Therefore, the metamodel becomes a combination of all metamodels that were originally specified, making it possible to use all of them in a single model.
+
+Note, however, that the metamodels might use similar concepts: both a PetriNet and a ReachabilityGraph have the notion of a *Place*, but it means something different in both cases.
+Therefore, the elemens are prepended with the tag that was used to define them.
+As such, the model transformation has no notion of *Place*, but only of *PetriNets/Place* and *ReachabilityGraph/Place*.
+In all operations in the transformation, it is necessary to use this notation.
+
+As the same metamodel might be used multiple times, but in different contexts (i.e., with different tags), the metamodels are sometimes added multiple times.
+Each time, however, a different tag is prepended.
+This allows model transformations that combine, or alter, models of the same type, while still distinguishing between the two of them.
+Recall the *master/Place* discussion from the beginning of this section.
 
 Rule specification
 ^^^^^^^^^^^^^^^^^^
 
-How to specify a rule
+Now we actually get to define a rule.
+Rules are themselves just models of the RAMified (and merged) metamodel.
+As such, they are created just like any other model.
+This is the code parameter of the *transformation_add_MT* operation, which takes a Modelverse model.
+An example specification is shown below, which will copy the highest number of tokens between places that have the same name, assuming that only one has a non-zero number of tokens::
+
+    LHS {
+        Pre_PetriNets/Place {
+            label = "pn_place_master"
+            constraint_tokens = $
+                    Boolean function constraint(value : Integer):
+                        return value > 0!
+                $
+        }
+
+        Pre_PetriNets/Place {
+            label = "pn_place_slave"
+            constraint_tokens = $
+                    Boolean function constraint(value : Integer):
+                        return value == 0!
+                $
+
+        constraint = $
+            Boolean function constraint(host_model : Element, mapping : Element):
+                return value_eq(read_attribute(host_model, mapping["pn_place_master"], "name"), 
+                                read_attribute(host_model, mapping["pn_place_slave"], "name"))!
+                $
+    }
+    RHS {
+        Pre_PetriNets/Place {
+            label = "pn_place_master"
+        }
+        Pre_PetriNets/Place {
+            label = "pn_place_slave"
+            value_tokens = $
+                Integer function value(host_model : Element, name : Element, mapping : Element):
+                $
+        }
+    }
+
+Some remarks, specifically in relation to users of AToMPM:
+1. Unspecified attributes in the LHS are always fulfilled (i.e., *result = True* in AToMPM notation).
+2. Unspecified attributes in the RHS are always copied as-is (i.e., *result = get_attr()* in AToMPM notation).
+3. Just like in AToMPM, labels are strings and can be used as such.
+4. While *mapping* contains a mapping for the labels to their elements in the host model, all elements of the host model an technically be used, even those not occuring in the LHS.
+5. During rewriting, it is possible to access the values of all elements of the host model, including those matched before in the LHS.
+   Newly created elements in the RHS can of course not be referenced.
+   Elements removed in the RHS can no longer be referenced either, though this will likely be updated in future versions.
 
 Schedule
 ^^^^^^^^
 
-Scheduling constructs
+The rule we have previously applied, does not yet do much in itself: it needs to be scheduled.
+Scheduling consists of defining in which order rules are executed, but also defining how the rule is to be executed: as a query (*Query*), for one match (*Atomic*), or for all matches (*ForAll*).
+For scheduling purposes, each rule has a *onSuccess* and *onFailure* association.
+*onSuccess* associations are followed when the rule has been applied successfully (i.e., at least one match was found), and the *onFailure* association is followed otherwise.
+Rules can also be composites, in which case they define a schedule themselves.
+
+Each schedule, including the main schedule, has exactly one *Initial* element, and possibly (some) *Success* and *Failure* elements.
+When the *Success* (*Failure*) node is reached, the composite rule is said to succeed (fail).
+On the topmost schedule, success indicates that the model transformation is to be applied.
+When the topmost schedule ends in a failure node, the model transformation as a whole is deemed to fail, and all changes are reverted.
+As such, users are guarenteed that an intermediate model will never be visible, or corrupt previous models.
+
+An example schedule, which applies the previous rule for as long as it matches, is shown below::
+
+    Composite composite {
+        ForAll copy_tokens {
+            LHS {
+                ...
+            }
+            RHS {
+                ...
+            }
+        }
+        Success success {}
+    }
+
+    Initial (composite, copy_tokens) {}
+    OnSuccess (copy_tokens, copy_tokens) {}
+    OnFailure (copy_tokens, success) {}
 
 Invocation
 ----------
@@ -69,7 +181,44 @@ Also, model transformations always happen on a copy of the original model.
 As such, it is also possible to restore the model to before the transformation.
 When a model transformation fails (i.e., the schedule ends in a *Failure*), no output models are written and the models are left untouched.
 
+Signature
+^^^^^^^^^
+
+After a model transformation is defined, it is easy to forget exactly which parameters it takes, and what were the types of these parameters.
+Therefore, the *transformation_read_signature* function can be used to read out the signature of model transformations::
+
+    >>> transformation_read_signature("pn_simulate")
+    ({"pn": "PetriNets"}, {"pn": "PetriNets"})
+    >>> transformation_read_signature("pn_merge")
+    ({"master": "PetriNets", "slave": "Petrinets"}, {"result": "PetriNets"})
+
+Querying
+^^^^^^^^
+
+Similarly, it is often easy to forget which transformations are supported between a source and target metamodel.
+Therefore the *transformation_between* function can be used to query for all transformations that take a certain metamodel as input, and generate another metamodel as output::
+
+    >>> transformation_between("PetriNets", "PetriNets")
+    ["pn_optimize", "pn_simulate", "pn_rename", "pn_combine"]
+
+    >>> transformation_between("PetriNets", "ReachabilityGraph")
+    ["pn_analyze"]
+
+Note that this operation does not take into account other input or output metamodels::
+
+    >>> transformation_between("PetriNets", "Boolean")
+    ["analyze_query", "is_safe", "conforms"]
+
 Tracability links
 -----------------
 
-How do tracability links work?
+As the metamodels are merged together into a single metamodel, models can contain elements from both.
+It is often useful to create some kind of link between these different metamodels.
+However, a simple merge does not allow for this, as the different metamodels form their own "islands".
+To create links between them, for example for matching, or for tracability, we need tracability links.
+
+Definition
+^^^^^^^^^^
+
+Use
+^^^