Consistency of Conditional Graph Grammars
AGG 1.2.0 supports a consistency control mechanism which is able to check if a given graph satisfies certain consistency conditions specified for a graph grammar.
Consistency conditions describe basic properties of graphs as e.g. the existence of certain elements, independent of a particular rule. We propose a transformation of global consistency conditions into post application conditions for individual rules. A so-constructed rule is applicable to a consistent graph if and only if the derived graph is consistent, too. A graph grammar is consistent if the start graph satisfies the consistency conditions and the rules preserve this property.
In AGG, consistency conditions are defined on the basis of graphical consistency constraints.
A graphical consistency constraint is a total injective morphism c : P -> C , the left graph P called premise and the right graph C conclusion. A graphical consistency constraint is satisfied by a graph G, if for all total injective morphisms p : P -> G there is a total injective morphisms q : C -> G such that q o c = p . If CC is a set of graphical consistency constraints, we say that G satisfies CC , if G satisfies all constraints in CC. .
The post application conditions generated from graphical consistency constraints ensure consistency of a graph grammar during rule application.
Note: If you use attributed graph grammar please do not forget to set all attribute members of the graph objects in all atomic consistency constraints :
- use variables or constants in the left-hand side of a constraint
- use variables or constants ( no expressions ) in the right-hand side of a constraint
- you can use attribute conditions to define relations between variables
The translation of consistency constraints into post conditions might cause problems for rules with attribute conditions.
Graphical user interfaces
In the following, we consider menus to create graphical constraints, formulas or post application conditions and to check consistency of a graph grammar. To create an atomic graphical constraint use :
- menu item New Atomic Constraint of File menu
- menu item New Atomic Constraint of GraGra popupmenu
An atomic constraint can contain more as one conclusions. Default size of conclusions is 1. To create more conclusions use menu item New Conclusion of Atomic Constraint popupmenu.
The left , right graphs and morphism of an atomic constraint will be edited like a rule.
Atomic Constraint popupmenu.
To create a constraint (formula) use :
- menu item New Constraint of File menu
- menu item New Constraint of GraGra popupmenu
We can define a boolean formula using atomic consistency constraints as variables.
To edit a formula use menu item Edit of Constraint popupmenu. You get a formula editor.
Constraint (formula) popupmenu.
The formula editor shown here contains atomic constraints in ''Carrousel`` example shown below.
File menu and GraGra popupmenu are shown here.
File menu and GraGra popupmenu
To generate post application conditions
- from all atomic constraints for all rules at the same time
use menu item Create Post Conditions from menu Analyzer / Consistency Check
- from all atomic constraints for an espesial rule
use menu item Create Post Conditions from Rule popupmenu
- from an espesial atomic constraint for all rules
use menu item Create Post Conditions from Atomic Constraint popupmenu
- from an espesial atomic constraint for an espesial rule - NOT JET IMPLEMENTED
To check consistency of a graph grammar use :
- menu item Check Atomics of Analyzer / Consistency Check menu or GraGra popupmenu
- menu item Check Constraints of Analyzer / Consistency Check menu or GraGra popupmenu
- menu item Check Graph of Atomic Constraint popupmenu or Constraint popupmenu
Consistency Check menu.
Sample Consistency Checking in AGG
Let us consider graph grammar "MerryGoRound" as an example for consistency checking.
The grammar is stored in "carrousel.ggx" .
The carrousel is modeled by a node of type 'carrousel` .
Each boat modeled by a node of type 'boat` is connected by a blue edge to the carrousel node. People on the carrousel are modeled by nodes of types 'child` and 'adult` , connected by black edges to the boat they are sitting in.
We use flags 'stop' and 'go' modeled by a red rectangle node and black rectangle node respectively. The flags are connected by blue edges to the carrousel node.
Additionally, we have two consistency conditions. The first condition ensures that whenever there is a child in a boat of the carrousel, there is an adult in this boat, too. The second condition ensures that whenever there is an adult in a boat ,there is a child in this boat, too. In this case the carrousel may start to move, i.e. the 'stop' flag on top may be replaced by a 'go' flag.
The type graph of the grammar is shown in Figure 1.
Figure 1. The carrousel type graph.
The consistency constraints: Child and Adult
The first atomic consistency constraint Child is shown in Figure 2.
Figure 2. Atomic consistency constraint Child
The second atomic consistency constraint Adult is shown in Figure 3.
Figure 3. Atomic consistency constraint Adult
Additionally, we can define a boolean formula using the atomic consistency constraints just defined as variables.
The formula will be defined in editor shown in Figure 4.
Figure 4. Formula editor
The start graph of the grammar is shown in Figure 5.
Figure 5. The carrousel graph.
Now the Rules: SetPair, SetChild, SetAdult, Go, Stop, Empty
The first rule SetPair with tree NACs ensures that only a pair of one child and one adult can enter an empty boat.
The rule is shown in Figure 6.
Figure 6. Rule SetPair
The NACs of rule SetPair are shown in Figure 7.
Figure 7. NACs of rule SetPair
The rule SetChild with a NAC ensures that a child can only enter a boat without another child.
Figure 8. Rule SetChild
We generate two post application conditions fromChild and fromAdult from consistency constraints Child and Adult
to ensure that a child can only enter a boat with an adult.
Post application conditions of the rule SetChild
The rule SetAdult with a NAC ensures that an adult can only enter a boat without another adult.
Figure 9. Rule SetAdult
We also generate two post application conditions from consistency constraints
to ensure that an adult can only enter a boat with a child.
Post application conditions of the rule SetAdult
The rule Go can be applied if and only if each boat contains a child and an adult or is empty.
This is ensured through post application conditions generated from consistency constraints.
An example of an atomic post application condition is shown in Figure 10a. Rule Go is shown in Figure 10.
Figure 10. Rule Go
Now an example of a post application condition of the rule Go.
An atomic of the post application condition fromChild is shown in Figure 10a.
Figure 10a. Overlap 1 : An atomic of the post application condition fromChild
The rule Stop is shown in Figure 11.
Figure 11. Rule Stop
The rule Empty is shown in Figure 12.
Figure 12. Rule Empty
Consistency of conditional graph grammars is described in: Ensuring Consistency of Conditional Graph Grammars - A Constructive Approach - by Reiko Heckel and Annika Wagner, 1995 . Modellierung und Nachweis der Konsistenz von verteilten Transaktionsmodellen für Datenbanksysteme mit algebraischen Graphgrammatiken by Manuel Koch (in German).
Bericht-Nr. 96-36. Forschungsberichte des Fachbereichs Informatik an der Technischen Universität Berlin.
Konzeption und Implementierung eines Verfahrens zum Nachweis der Konsistenz in einer attributierten Graphgrammatik
Diploma thesis of Michael Matz (in German)