Granular Conflict Analysis for Transformation Rules with Application Conditions
摘要
Conflict and dependency analysis is an important static analysis tool for gaining an overview of potential interactions of graph transformation rules. The analysis is based on critical pairs, which represent conflicting transformations in a minimal context. For many applications, however, the computation of complete critical pairs is unnecessarily complex. Instead, the crucial information about a conflicting pair of transformations is already contained in much smaller structures, called conflict reasons or disabling essences in existing research. So far, these structures have only been introduced for plain rules; in practical scenarios, however, transformation rules are regularly equipped with (application) conditions. In this paper, we fill this gap by lifting the computation of disabling essences to rules with conditions. It turns out that the situation is much more complex than for plain rules, where a pair of transformations is in conflict if and only if a non-trivial disabling essence embeds into the pair. However, we can show that, for every conflicting pair of transformations via rules with conditions, there is a disabling essence that embeds into this pair. For the special case of negative application conditions we can even show that a disabling essence is embeddable if and only if the transformation pair is in conflict. We work within the general context of adhesive HLR categories, which include several types of graph-like structures.