Skip to content

Graph Constraint Evaluation over Partial Models by Constraint Rewriting

Jump to bottom
Oszkár Semeráth edited this page Mar 9, 2017 · 12 revisions

This page discusses the measurement for the paper "Graph Constraint Evaluation over Partial Models by Constraint Rewriting".

Target Metamodel

Representation of MAVO uncertainty

In our approach, standard Ecore models are used to define partial models enriched with special annotations on model elements which are adapted from [1]. A simple metamodel for partial modeling is visible below. This partial model representation has three important characteristics: (1) Reference elements represents the objects of the base model. (2) The uncertainty annotations are added to the objects by may, set, variable references, and to the partial model itself by the open attribute. (3) Finally, the new reference helps gain more control over the open uncertainty: new contains prototypical elements for each concrete (non-abstract) class of the metamodel that can be instantiated if open is true.

Representation of Uncertainty

In our approach, must- and may-matches are calculated by (1) constructing uncertain model indexers, which collect the possible and necessary elements of the concretizations, and (2) deriving approximated patterns with the help of uncertain model indexers. These patterns can be evaluated over partial models as a regular graph pattern matching problem, and the matches are interpreted as may- and must-matches of the original pattern p with MAVO semantics.

Modal Indexing of Partial Model Elements

Similarly to the role of model indexers in graph query tools, an uncertain property indexer for a partial model P collects basic properties of each model M that M∈ P. In our approach four properties are indexed: (1) what can be the objects (2) what can be the types of objects in the model (3) what are the references between objects, and (4) what attribute values can be in the model. In the following, we describe how those basic properties can be over- and under-approximated by appropriate graph patterns.

Object existence

First, the set of objects in a concertized model (Objects) are either objects that are present in the base graph model (referred to by ele- ments) or newly created objects (contained by new). As defined in Section 2.3, an object in the base model B not marked by may label must exist in every con- crete model, which makes them a good under-approximation for o ∈ Objects. Additionally, a concretization may contain (1) objects labelled by may, or (2) newly created objects represented by the prototype objects contained by new. This over-approximates the objects in Objects. Graph patterns calculating those approximations are illustrated in Figure 4a.

pattern mustExist(p,e){
  elements(p,e);
  neg find may(p,e);
}

pattern mayExist(p,e){
  open(p,true);
  new(p,e);
} or {
  elements(p,e);
  may(p,e);
} or {
  find mustExist(p,e);
}

Equivalence

An object of the base model not labeled by set will represent a unique single object in all concretizations. Therefore, variables o1 and o2 referring to this object must be equals (creating o1 = o2). For over-approximation there are three other options: (1) an object labelled by set may still refer to a single object, (2) a var object may be merged to another object wit the same type thus making them equal, and two symbolic new object may refer to the same newly created one. Matching on those criteria makes a good over-approximation for o1 = o2. Patterns for equivalence checking are illustrated below.

pattern mustEqual(p,e1,e2) {
  elements(p,e1);
  e1 == e2;
  neg find may(p,e1);
  neg find set(p,e1); }

pattern mayEqual(p,e1,e2) {
  set(p,e1); e1 == e2;
} or {
  var(p,e1);
  complatible(e1,e2);
} or{
  var(p,e2);
  complatible(e1,e2);
} or{
  open(p,true);
  new(p,e1);
  e1 == e2;
} or {
  find mustEqual(p,e1,e2);
}

Types

As the type of an object cannot change during refinement or creation, a type predicate can be simply evaluated by checking C(o).

References and Attributes.

The indexing of potential and necessary references and attributes is a more complex, as illustrated in the pattern template in below. First, R(s,t) must hold if there is reference in the base model be- tween two elements that must exist. However, possible pairs of objects included in an over-approximation of R(s,t) have to satisfy several structural constraints: (1) s and t are objects that may exist, (2) s and t have the correct types, (3) there must not be more outgoing references of type R from s than the upper multiplicity of R, (4) for containment references, it must not create (4.1) loops in the containment hierarchy or (4.2) multiple parents, and finally, (5) if R has an inverse reference it also have to satisfy (3) and (4).

pattern mustReference_R(p, s, t) {
  find mustExist(p,s);
  find mustExist(t);
  S.R(s, t);
}

pattern mayReference_R(p, s, t) {
  /*1 */ find mayExist(p,s); find mayExist(p,t);
  /*2 */ find S(p,s); find T (p,t);
  /*3 */ count find mustReference_R(p, s, _) < {upper multiplicity of R});
  /*4.1*/ neg find mustContains(p,_,t);
  /*4.2*/ neg find mustTransitiveContains(p,t,s);
  /*5 */ {rules 3 and 4 for the inverse references}
} or {
  find mustReference_R(p, s, t);
}

Modal Indexing of Patterns

Newly created patterns are prefixed with must_ or may_ and a parameter p is added for the PartialModel object. For example, as illustrated below, must_noEntry(p,r) is the under-approximated version of noEntry(r).

1 // Original patterns
2 pattern noEntry(r : Region) {
3 neg find entryInRegion(r, _);}
4 pattern entryInRegion(r,e:Entry){
5 Region.vertices(r,e);}
6 // Must version
7 pattern must_noEntry(p,r)
8 {
9 find mustType_Region(p,r);
10 neg find may_entryInRegion
11 (p,r,_);
12 }
13 // May version
14 pattern may_noEntry(p,r)
15 {
16 find mayType_Region(p,r);
17 neg find must_entryInRegion
18 (p,r,_);
19 }
20 // Original pattern
21 pattern multipleEntry(r) {
22   find entryInRegion(r, e1);
23   find entryInRegion(r, e2);
24   e1 != e2; }
25 // Must version
26 pattern must_multipleEntry(p,r){
27   find must_entryInRegion(
28     p,r,e1);
29 find mustPattern_entryInRegion(
30   p,r,e2);
31 neg find mayEqual(p,e1,e2); }
32 // May version
33 pattern may_multipleEntry(p,r){
34   find may_entryInRegion(
35   p,r,e1);
36   find may_entryInRegion(
37   p,r,e2);
38   neg find mustEqual(p,e1,e2); }

The only remaining task is to replace constraints of the original match by calling the must or may variant of the corresponding constraint:

  • Existence: each variable is checked by mustExist or mayExist patterns.
  • Classifier Constraint: As mentioned at the base indexers, type constraints can be directly checked C(o).
  • Path Constraint: We split path expressions to single reference and at- tribute constraints, and replace all occurrences of a single R(s,t) constraint to either find mustReference_R(p,s,t) or find mayReference_R(p,s,t).
  • Equality Constraints: in case of equality constraints, we replace all a==b with find mustEqual(p,a,b) or find mayEqual(p,a,b). However, in case of inequality a!=b, the modality has to be changed to the dual:
    • Underapproximated a!=b is replaced by neg find mayEqual(p,a,b)
    • Overapproximated a!=b is replaced by neg find mustEqual(p,a,b) For example, the constraint e1!=e2 in line 24 of Figure 5 expresses that the two entries are different. In the must version of the pattern, it is replaced with neg find mayEqual(p,e1,e2), which excludes matches where the two entries can be mapped to the same element. However, in the may version of the pattern, it is replaced with neg find mustEqual(p,e1,e2), which excludes matches only where it is ensured that the two matches are equal.
  • Pattern Call Constraints: There are different rules to map pattern calls:
    • Positive call: a positively called pattern find patt(par) is mapped to find must_patt(p,par) or find may_patt(p,par). For example, the call find entryInRegion(r, e1); in line 22 of Figure 5 is replaced with find must_entryInRegion(p,r,e1) in the must variant of the pattern.
  • Negative call: In case of negative pattern call (neg find) the modality of the called pattern has to be changed to the opposite:
    • Underapproximation of neg find patt(par) replaced with neg find may_patt(p,par)
    • Overapproximation of neg find patt(par) replaced with neg find must_patt(p,par) For example, the negative pattern call neg find entryInRegion(r,_) in line 3 of Figure 5 is transformed to a negative may-pattern call neg find may_entryInRegion(p,r,_) constraint in the must version of the pattern, which forbids all possible matches where the entry can be in the checked region. Conversely, in the may version, it is transformed to neg find must_entryInRegion(p,r,_), which filters the matches only where it must be an entry in the region.

#Measurements

We carried out an initial scalability evaluation 1 of our approach using 3 models (with 157, 347 and 1765 objects, respectively) and 5 queries available from the open TrainBenchmark [2]. We generated randomly assigned MAVO annotations for 5% of the the model elements (e.g. with 7, 17, 88 uncertainties). We evaluated the performance of (1) each graph query individually for (2) both may- and must-patterns (may/must) using (3) two pattern matching strategies (incremental/local-search) with (4) open world or closed world assumption (open/closed) after an optional (5) fault injection step (valid/invalid) to introduce some constraint violations. We measured the execution time for evaluating the queries in seconds with a timeout of 2 minutes using a laptop computer (CPU: Intel Core-i5-m310M, MEM: 16GB, OS: Windows 10 Pro). Our experiments were executed 10 times and the median of execution time is reported in below:

References

[1] Famelis, M., Salay, R., Chechik, M.: Partial models: Towards modeling and reasoning with uncertainty. In: Proceedings of the 34th International Conference on Software Engineering. pp. 573–583. IEEE Press, Piscataway, NJ, USA (2012)

[2] Szárnyas, G., Semeráth, O., Ráth, I., Varró, D.: The TTC 2015 train benchmark case for incremental model validation. In: 8th Transformation Tool Contest, (STAF 2015). pp. 129–141 (2015)

Clone this wiki locally