anATLyzer

Advanced analysis of ATL transformations

Analysis of target constraints

AnATLyzer has a feature to support the analysis of target constraints based on rewriting them as source constraints. Source constraints obtained from a target constraint are called advanced constraints. This method has many applications like ensuring strong executability of a model-to-model transformation (i.e., checking if there exists a source model satifying the transformation pre-conditions which could violate a target constraint), characterizing classes of target models and checking transformation contracts.

Screencast

Specifying constraints

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.

Experimental results

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))