Advanced analysis of ATL transformations
Constraints can be written directly in the ATL transformation file as helpers specially annotated. There are three kinds of annotations for pre-conditions, target constraints (e.g., invariants or post-conditions) and transformations contracts.
A pre-condition is indicated annotating a helper with
the @precondition
tag. A pre-condition can only
access source elements. The following is pre-condition
for a class-to-table transformation.
-- Every class must have at least one key attribute -- @precondition helper def : attrKeys : Boolean = CLASS!Class.allInstances()->forAll(t | t.attrs->select(a | a.isKey)->size() >= 1)
A target constraint is indicated annotating a helper with
the @target_constraint
tag. It can only access
target elements.
-- All tables have at lest one primary key -- @target_constraint helper def : hasPkeys : Boolean = TABLE!Table.allInstances()->forAll(t | t.pkeys->size() >= 1 );
A transformation contract establishes a relationship between
source and target elements. It is indicated annotating a heper with
the @contract
tag.
-- @contract helper def : enoughColumns : Boolean = CLASS!Attribute.allInstances()->size() <= TABLE!Column.allInstances()->size();
We have evaluated our method to infer advanced constraints using mutation techniques. We have used four transformations as seeds and we have mutated them to obtain variants with which test the precision and recall of the infered advanced constraints.
The raw experimetal data is available here:
The experiment shows an almost perfect precision and perfect recall. The evaluation uncovered one kind of false positive (FP). It refers to a limitation of our method to handle 1-to-n rules, which happens when syntactically correct invariant expressions test for impossible reachabilities between target objects which are satisfiable in the source. The following is a minimal example to illustrate this issue.
Let us consider the following constraint over Petri nets.
-- @target_constraint helper def: isStateMachine : Boolean = PN!Transition.allInstances()->forAll(t | PN!TPArc.allInstances()->one(arc | arc.input = t ) and PN!PTArc.allInstances()->one(arc | arc.input = t ) -- arc.input = t is always false, because the type of -- PTArc::input is Place, while the type of t is Transition );
Then, let us suppose a rule which transforms Generator objects (i.e., belonging to Factory DSL). This is a 1-to-3 rule, which means that the target elements come from the same source element.
rule Generator2Transition { from m : FAC!Generator to t : PN!Transition ( ... ), p : PN!Place ( ... ), p2t : PN!PTArc ( weight <- 1, input <- p, output <- t, net <- m.factory ) }
The advanced constraint generated by the method is as follows. As can be observed this is trivially satisfiable. The problem is that sub-expression in the third line is satisfiable, but it is generated from a target constraint which is not satisfiable. This particular case can be detected statically and avoid generating an incorrect source constraint.
FAC!Generator.allInstances()->forAll(t | FAC!Generator.allInstances()->one(arc | arc = t) and FAC!Generator.allInstances()->one(arc | arc = t))