From f1d9a50a3be2bfabc6091d51e120ca63ac1ab2d4 Mon Sep 17 00:00:00 2001
From: ArenBabikian <aren.babikian@mail.mcgill.ca>
Date: Fri, 15 Feb 2019 12:42:15 -0500
Subject: Set up #19

---
 .../yakindu/debug/generated3valued.vql_deactivated | 1472 ++++++++++++++++++++
 1 file changed, 1472 insertions(+)
 create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated

(limited to 'Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated')

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated b/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated
new file mode 100644
index 00000000..6d8fc404
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated
@@ -0,0 +1,1472 @@
+import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage"
+import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"
+import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"
+
+//////////
+// 0. Util
+//////////
+private pattern interpretation(problem:LogicProblem, interpretation:PartialInterpretation) {
+	PartialInterpretation.problem(interpretation,problem);
+}
+	
+/////////////////////////
+// 0.1 Existence
+/////////////////////////
+private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	find interpretation(problem,interpretation);
+	LogicProblem.elements(problem,element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+}
+
+private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+    find mustExist(problem,interpretation,element);
+} or {
+    find interpretation(problem,interpretation);
+    neg find elementCloseWorld(element);
+    PartialInterpretation.openWorldElements(interpretation,element);
+}
+
+private pattern elementCloseWorld(element:DefinedElement) {
+	PartialInterpretation.openWorldElements(i,element);
+    PartialInterpretation.maxNewElements(i,0);
+} or {
+	Scope.targetTypeInterpretation(scope,interpretation);
+	PartialTypeInterpratation.elements(interpretation,element);
+	Scope.maxNewElements(scope,0);
+}
+
+////////////////////////
+// 0.2 Equivalence
+////////////////////////
+pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) {
+	find mayExist(problem,interpretation,a);
+	find mayExist(problem,interpretation,b);
+	a == b;
+}
+
+////////////////////////
+// 0.3 Required Patterns by TypeIndexer
+////////////////////////
+private pattern typeInterpretation(problem:LogicProblem, interpretation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) {
+	find interpretation(problem,interpretation);
+	LogicProblem.types(problem,type);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+}
+
+private pattern directInstanceOf(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, type:Type) {
+	find interpretation(problem,interpretation);
+	LogicProblem.types(problem,type);
+	TypeDefinition.elements(type,element);
+} or {
+	find interpretation(problem,interpretation);
+	find typeInterpretation(problem,interpretation,type,typeInterpretation);
+	PartialComplexTypeInterpretation.elements(typeInterpretation,element);
+}
+
+private pattern isPrimitive(element: PrimitiveElement) {
+	PrimitiveElement(element);
+}
+
+//////////
+// 1. Problem-Specific Base Indexers
+//////////
+// 1.1 Type Indexers
+//////////
+// 1.1.1 primitive Type Indexers
+//////////
+
+//////////
+// 1.1.2 domain-specific Type Indexers
+//////////
+/**
+ * An element must be an instance of type "Pseudostate class".
+ */
+private pattern mustInstanceOfPseudostate_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"Pseudostate class");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewPseudostate_class(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"Pseudostate class");
+}
+
+/**
+ * An element may be an instance of type "Pseudostate class".
+ */
+private pattern mayInstanceOfPseudostate_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfExit_class(problem,interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfChoice_class(problem,interpretation,element);
+	neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfEntry_class(problem,interpretation,element);
+	neg find scopeDisallowsNewPseudostate_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfExit_class(problem,interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfChoice_class(problem,interpretation,element);
+	neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfEntry_class(problem,interpretation,element);
+	neg find scopeDisallowsNewPseudostate_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfPseudostate_class(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "Vertex class".
+ */
+private pattern mustInstanceOfVertex_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"Vertex class");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewVertex_class(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"Vertex class");
+}
+
+/**
+ * An element may be an instance of type "Vertex class".
+ */
+private pattern mayInstanceOfVertex_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find scopeDisallowsNewVertex_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find scopeDisallowsNewVertex_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfVertex_class(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "Region class".
+ */
+private pattern mustInstanceOfRegion_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"Region class");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewRegion_class(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"Region class");
+}
+
+/**
+ * An element may be an instance of type "Region class".
+ */
+private pattern mayInstanceOfRegion_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+	neg find scopeDisallowsNewRegion_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+	neg find scopeDisallowsNewRegion_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfRegion_class(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "Transition class".
+ */
+private pattern mustInstanceOfTransition_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"Transition class");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewTransition_class(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"Transition class");
+}
+
+/**
+ * An element may be an instance of type "Transition class".
+ */
+private pattern mayInstanceOfTransition_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+	neg find scopeDisallowsNewTransition_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+	neg find scopeDisallowsNewTransition_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfTransition_class(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "Statechart class".
+ */
+private pattern mustInstanceOfStatechart_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"Statechart class");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewStatechart_class(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"Statechart class");
+}
+
+/**
+ * An element may be an instance of type "Statechart class".
+ */
+private pattern mayInstanceOfStatechart_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element);
+	neg find scopeDisallowsNewStatechart_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element);
+	neg find scopeDisallowsNewStatechart_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfStatechart_class(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "Entry class".
+ */
+private pattern mustInstanceOfEntry_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"Entry class");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewEntry_class(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"Entry class");
+}
+
+/**
+ * An element may be an instance of type "Entry class".
+ */
+private pattern mayInstanceOfEntry_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfExit_class(problem,interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfChoice_class(problem,interpretation,element);
+	neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find scopeDisallowsNewEntry_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfExit_class(problem,interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfChoice_class(problem,interpretation,element);
+	neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find scopeDisallowsNewEntry_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfEntry_class(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "Synchronization class".
+ */
+private pattern mustInstanceOfSynchronization_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"Synchronization class");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewSynchronization_class(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"Synchronization class");
+}
+
+/**
+ * An element may be an instance of type "Synchronization class".
+ */
+private pattern mayInstanceOfSynchronization_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfExit_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfChoice_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfEntry_class(problem,interpretation,element);
+	neg find scopeDisallowsNewSynchronization_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfExit_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfChoice_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfEntry_class(problem,interpretation,element);
+	neg find scopeDisallowsNewSynchronization_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfSynchronization_class(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "State class".
+ */
+private pattern mustInstanceOfState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"State class");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewState_class(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"State class");
+}
+
+/**
+ * An element may be an instance of type "State class".
+ */
+private pattern mayInstanceOfState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfFinalState_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
+	neg find mustInstanceOfStatechart_class(problem,interpretation,element);
+	neg find scopeDisallowsNewState_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfFinalState_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
+	neg find mustInstanceOfStatechart_class(problem,interpretation,element);
+	neg find scopeDisallowsNewState_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfState_class(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "RegularState class".
+ */
+private pattern mustInstanceOfRegularState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"RegularState class");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewRegularState_class(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"RegularState class");
+}
+
+/**
+ * An element may be an instance of type "RegularState class".
+ */
+private pattern mayInstanceOfRegularState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfFinalState_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find scopeDisallowsNewRegularState_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfFinalState_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find scopeDisallowsNewRegularState_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfRegularState_class(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "CompositeElement class".
+ */
+private pattern mustInstanceOfCompositeElement_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"CompositeElement class");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewCompositeElement_class(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"CompositeElement class");
+}
+
+/**
+ * An element may be an instance of type "CompositeElement class".
+ */
+private pattern mayInstanceOfCompositeElement_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfStatechart_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+	neg find scopeDisallowsNewCompositeElement_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfStatechart_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+	neg find scopeDisallowsNewCompositeElement_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfCompositeElement_class(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "Choice class".
+ */
+private pattern mustInstanceOfChoice_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"Choice class");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewChoice_class(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"Choice class");
+}
+
+/**
+ * An element may be an instance of type "Choice class".
+ */
+private pattern mayInstanceOfChoice_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfExit_class(problem,interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfEntry_class(problem,interpretation,element);
+	neg find scopeDisallowsNewChoice_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfExit_class(problem,interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfEntry_class(problem,interpretation,element);
+	neg find scopeDisallowsNewChoice_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfChoice_class(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "Exit class".
+ */
+private pattern mustInstanceOfExit_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"Exit class");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewExit_class(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"Exit class");
+}
+
+/**
+ * An element may be an instance of type "Exit class".
+ */
+private pattern mayInstanceOfExit_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfChoice_class(problem,interpretation,element);
+	neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfEntry_class(problem,interpretation,element);
+	neg find scopeDisallowsNewExit_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfChoice_class(problem,interpretation,element);
+	neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfEntry_class(problem,interpretation,element);
+	neg find scopeDisallowsNewExit_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfExit_class(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "FinalState class".
+ */
+private pattern mustInstanceOfFinalState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"FinalState class");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewFinalState_class(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"FinalState class");
+}
+
+/**
+ * An element may be an instance of type "FinalState class".
+ */
+private pattern mayInstanceOfFinalState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find scopeDisallowsNewFinalState_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find scopeDisallowsNewFinalState_class(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfFinalState_class(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "Statechart class DefinedPart".
+ */
+private pattern mustInstanceOfStatechart_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"Statechart class DefinedPart");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewStatechart_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"Statechart class DefinedPart");
+}
+
+/**
+ * An element may be an instance of type "Statechart class DefinedPart".
+ */
+private pattern mayInstanceOfStatechart_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{ find mustInstanceOfStatechart_class_DefinedPart(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "Statechart class UndefinedPart".
+ */
+private pattern mustInstanceOfStatechart_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"Statechart class UndefinedPart");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewStatechart_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"Statechart class UndefinedPart");
+}
+
+/**
+ * An element may be an instance of type "Statechart class UndefinedPart".
+ */
+private pattern mayInstanceOfStatechart_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+	neg find scopeDisallowsNewStatechart_class_UndefinedPart(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+	neg find scopeDisallowsNewStatechart_class_UndefinedPart(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfStatechart_class_UndefinedPart(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "CompositeElement class DefinedPart".
+ */
+private pattern mustInstanceOfCompositeElement_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"CompositeElement class DefinedPart");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewCompositeElement_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"CompositeElement class DefinedPart");
+}
+
+/**
+ * An element may be an instance of type "CompositeElement class DefinedPart".
+ */
+private pattern mayInstanceOfCompositeElement_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{ find mustInstanceOfCompositeElement_class_DefinedPart(problem,interpretation,element); }
+/**
+ * An element must be an instance of type "CompositeElement class UndefinedPart".
+ */
+private pattern mustInstanceOfCompositeElement_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+	Type.name(type,"CompositeElement class UndefinedPart");
+	find directInstanceOf(problem,interpretation,element,type);
+}
+private pattern scopeDisallowsNewCompositeElement_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.scopes(interpretation,scope);
+	Scope.targetTypeInterpretation(scope,typeInterpretation);
+	Scope.maxNewElements(scope,0);
+	PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
+	Type.name(type,"CompositeElement class UndefinedPart");
+}
+
+/**
+ * An element may be an instance of type "CompositeElement class UndefinedPart".
+ */
+private pattern mayInstanceOfCompositeElement_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfStatechart_class(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+	neg find scopeDisallowsNewCompositeElement_class_UndefinedPart(problem, interpretation);
+	neg find isPrimitive(element);
+} or {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.openWorldElements(interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfStatechart_class(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+	neg find scopeDisallowsNewCompositeElement_class_UndefinedPart(problem, interpretation);
+	neg find isPrimitive(element);
+} or
+{ find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element); }
+
+//////////
+// 1.2 Relation Declaration Indexers
+//////////
+/**
+ * Matcher for detecting tuples t where []incomingTransitions reference Vertex(source,target)
+ */
+private pattern mustInRelationincomingTransitions_reference_Vertex(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	source: DefinedElement, target:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"incomingTransitions reference Vertex");
+	PartialRelationInterpretation.relationlinks(relationIterpretation,link);
+	BinaryElementRelationLink.param1(link,source);
+	BinaryElementRelationLink.param2(link,target);
+}
+/**
+ * Matcher for detecting tuples t where <>incomingTransitions reference Vertex(source,target)
+ */
+private pattern mayInRelationincomingTransitions_reference_Vertex(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	source: DefinedElement, target:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	// The two endpoint of the link have to exist
+	find mayExist(problem, interpretation, source);
+	find mayExist(problem, interpretation, target);
+	// Type consistency
+	find mayInstanceOfVertex_class(problem,interpretation,source);
+	find mayInstanceOfTransition_class(problem,interpretation,target);
+	// There are "numberOfExistingReferences" currently existing instances of the reference to the target,
+	// the upper bound of the opposite reference multiplicity should be considered.
+	numberOfExistingOppositeReferences == count find mustInRelationtarget_reference_Transition(problem,interpretation,target,_);
+	check(numberOfExistingOppositeReferences < 1);
+} or {
+	find mustInRelationincomingTransitions_reference_Vertex(problem,interpretation,source,target);
+}
+/**
+ * Matcher for detecting tuples t where []outgoingTransitions reference Vertex(source,target)
+ */
+private pattern mustInRelationoutgoingTransitions_reference_Vertex(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	source: DefinedElement, target:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"outgoingTransitions reference Vertex");
+	PartialRelationInterpretation.relationlinks(relationIterpretation,link);
+	BinaryElementRelationLink.param1(link,source);
+	BinaryElementRelationLink.param2(link,target);
+}
+/**
+ * Matcher for detecting tuples t where <>outgoingTransitions reference Vertex(source,target)
+ */
+private pattern mayInRelationoutgoingTransitions_reference_Vertex(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	source: DefinedElement, target:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	// The two endpoint of the link have to exist
+	find mayExist(problem, interpretation, source);
+	find mayExist(problem, interpretation, target);
+	// Type consistency
+	find mayInstanceOfVertex_class(problem,interpretation,source);
+	find mayInstanceOfTransition_class(problem,interpretation,target);
+	// There are "numberOfExistingReferences" currently existing instances of the reference to the target,
+	// the upper bound of the opposite reference multiplicity should be considered.
+	numberOfExistingOppositeReferences == count find mustInRelationsource_reference_Transition(problem,interpretation,target,_);
+	check(numberOfExistingOppositeReferences < 1);
+	// The reference is containment, then a new reference cannot be create if:
+	// 1. Multiple parents
+	neg find mustContains4(problem,interpretation,_,target);
+	// 2. Circle in the containment hierarchy
+	neg find mustTransitiveContains(source,target);
+} or {
+	find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,source,target);
+}
+/**
+ * Matcher for detecting tuples t where []vertices reference Region(source,target)
+ */
+private pattern mustInRelationvertices_reference_Region(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	source: DefinedElement, target:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"vertices reference Region");
+	PartialRelationInterpretation.relationlinks(relationIterpretation,link);
+	BinaryElementRelationLink.param1(link,source);
+	BinaryElementRelationLink.param2(link,target);
+}
+/**
+ * Matcher for detecting tuples t where <>vertices reference Region(source,target)
+ */
+private pattern mayInRelationvertices_reference_Region(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	source: DefinedElement, target:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	// The two endpoint of the link have to exist
+	find mayExist(problem, interpretation, source);
+	find mayExist(problem, interpretation, target);
+	// Type consistency
+	find mayInstanceOfRegion_class(problem,interpretation,source);
+	find mayInstanceOfVertex_class(problem,interpretation,target);
+	// The reference is containment, then a new reference cannot be create if:
+	// 1. Multiple parents
+	neg find mustContains4(problem,interpretation,_,target);
+	// 2. Circle in the containment hierarchy
+	neg find mustTransitiveContains(source,target);
+} or {
+	find mustInRelationvertices_reference_Region(problem,interpretation,source,target);
+}
+/**
+ * Matcher for detecting tuples t where []target reference Transition(source,target)
+ */
+private pattern mustInRelationtarget_reference_Transition(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	source: DefinedElement, target:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"target reference Transition");
+	PartialRelationInterpretation.relationlinks(relationIterpretation,link);
+	BinaryElementRelationLink.param1(link,source);
+	BinaryElementRelationLink.param2(link,target);
+}
+/**
+ * Matcher for detecting tuples t where <>target reference Transition(source,target)
+ */
+private pattern mayInRelationtarget_reference_Transition(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	source: DefinedElement, target:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	// The two endpoint of the link have to exist
+	find mayExist(problem, interpretation, source);
+	find mayExist(problem, interpretation, target);
+	// Type consistency
+	find mayInstanceOfTransition_class(problem,interpretation,source);
+	find mayInstanceOfVertex_class(problem,interpretation,target);
+	// There are "numberOfExistingReferences" currently existing instances of the reference from the source,
+	// the upper bound of the multiplicity should be considered.
+	numberOfExistingReferences == count find mustInRelationtarget_reference_Transition(problem,interpretation,source,_);
+	check(numberOfExistingReferences < 1);
+} or {
+	find mustInRelationtarget_reference_Transition(problem,interpretation,source,target);
+}
+/**
+ * Matcher for detecting tuples t where []source reference Transition(source,target)
+ */
+private pattern mustInRelationsource_reference_Transition(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	source: DefinedElement, target:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"source reference Transition");
+	PartialRelationInterpretation.relationlinks(relationIterpretation,link);
+	BinaryElementRelationLink.param1(link,source);
+	BinaryElementRelationLink.param2(link,target);
+}
+/**
+ * Matcher for detecting tuples t where <>source reference Transition(source,target)
+ */
+private pattern mayInRelationsource_reference_Transition(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	source: DefinedElement, target:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	// The two endpoint of the link have to exist
+	find mayExist(problem, interpretation, source);
+	find mayExist(problem, interpretation, target);
+	// Type consistency
+	find mayInstanceOfTransition_class(problem,interpretation,source);
+	find mayInstanceOfVertex_class(problem,interpretation,target);
+	// There are "numberOfExistingReferences" currently existing instances of the reference from the source,
+	// the upper bound of the multiplicity should be considered.
+	numberOfExistingReferences == count find mustInRelationsource_reference_Transition(problem,interpretation,source,_);
+	check(numberOfExistingReferences < 1);
+	// The eOpposite of the reference is containment, then a referene cannot be created if
+	// 1. Multiple parents
+	neg find mustContains4(problem,interpretation,source,_);
+	// 2. Circle in the containment hierarchy
+	neg find mustTransitiveContains(source,target);
+} or {
+	find mustInRelationsource_reference_Transition(problem,interpretation,source,target);
+}
+/**
+ * Matcher for detecting tuples t where []regions reference CompositeElement(source,target)
+ */
+private pattern mustInRelationregions_reference_CompositeElement(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	source: DefinedElement, target:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"regions reference CompositeElement");
+	PartialRelationInterpretation.relationlinks(relationIterpretation,link);
+	BinaryElementRelationLink.param1(link,source);
+	BinaryElementRelationLink.param2(link,target);
+}
+/**
+ * Matcher for detecting tuples t where <>regions reference CompositeElement(source,target)
+ */
+private pattern mayInRelationregions_reference_CompositeElement(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	source: DefinedElement, target:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	// The two endpoint of the link have to exist
+	find mayExist(problem, interpretation, source);
+	find mayExist(problem, interpretation, target);
+	// Type consistency
+	find mayInstanceOfCompositeElement_class(problem,interpretation,source);
+	find mayInstanceOfRegion_class(problem,interpretation,target);
+	// The reference is containment, then a new reference cannot be create if:
+	// 1. Multiple parents
+	neg find mustContains4(problem,interpretation,_,target);
+	// 2. Circle in the containment hierarchy
+	neg find mustTransitiveContains(source,target);
+} or {
+	find mustInRelationregions_reference_CompositeElement(problem,interpretation,source,target);
+}
+
+//////////
+// 1.3 Relation Definition Indexers
+//////////
+
+//////////
+// 1.4 Containment Indexer
+//////////
+private pattern mustContains2(source: DefinedElement, target: DefinedElement) {
+	find mustContains4(_,_,source,target);
+}
+	
+private pattern mustContains4(problem:LogicProblem, interpretation:PartialInterpretation,
+	source: DefinedElement, target: DefinedElement)
+	{ find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,source,target); }or
+	
+	{ find mustInRelationvertices_reference_Region(problem,interpretation,source,target); }or
+	
+	{ find mustInRelationregions_reference_CompositeElement(problem,interpretation,source,target); }
+
+private pattern mustTransitiveContains(source,target) {
+	find mustContains2+(source,target);
+}
+
+//////////
+// 2. Invalidation Indexers
+//////////
+// 2.1 Invalidated by WF Queries
+//////////
+
+//////////
+// 3. Unfinishedness Indexers
+//////////
+// 3.1 Unfinishedness Measured by Multiplicity
+//////////
+pattern unfinishedLowerMultiplicity_target_reference_Transition(problem:LogicProblem, interpretation:PartialInterpretation, relationIterpretation:PartialRelationInterpretation, object:DefinedElement,missingMultiplicity) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"target reference Transition");
+	find mustInstanceOfTransition_class(problem,interpretation,object);
+	numberOfExistingReferences == count find mustInRelationtarget_reference_Transition(problem,interpretation,object,_);
+	check(numberOfExistingReferences < 1);
+	missingMultiplicity == eval(1-numberOfExistingReferences);
+}
+
+//////////
+// 3.2 Unfinishedness Measured by WF Queries
+//////////
+
+//////////
+// 4. Refinement Indexers
+//////////
+// 4.1 Object constructors
+//////////
+private pattern hasElementInContainment(problem:LogicProblem, interpretation:PartialInterpretation)
+{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfPseudostate_class(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfCompositeElement_class(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfTransition_class(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfState_class(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfSynchronization_class(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfEntry_class(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfRegularState_class(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfChoice_class(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfVertex_class(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfStatechart_class(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfExit_class(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfFinalState_class(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfRegion_class(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfStatechart_class_DefinedPart(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfStatechart_class_UndefinedPart(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfCompositeElement_class_DefinedPart(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}or{
+	find interpretation(problem,interpretation);
+	find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,root);
+	find mustExist(problem, interpretation, root);
+}
+pattern createObject_Exit_class_by_vertices_reference_Region(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
+	container:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Exit class");
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
+	find mustInstanceOfRegion_class(problem,interpretation,container);
+	find mayInstanceOfExit_class(problem,interpretation,newObject);
+	find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
+	find mustExist(problem, interpretation, container);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_Exit_class(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	typeInterpretation:PartialComplexTypeInterpretation)
+{
+	find interpretation(problem,interpretation);
+	neg find hasElementInContainment(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Exit class");
+	find mayInstanceOfExit_class(problem,interpretation,newObject);
+	find mayExist(problem, interpretation, newObject);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_FinalState_class_by_vertices_reference_Region(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
+	container:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"FinalState class");
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
+	find mustInstanceOfRegion_class(problem,interpretation,container);
+	find mayInstanceOfFinalState_class(problem,interpretation,newObject);
+	find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
+	find mustExist(problem, interpretation, container);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_FinalState_class(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	typeInterpretation:PartialComplexTypeInterpretation)
+{
+	find interpretation(problem,interpretation);
+	neg find hasElementInContainment(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"FinalState class");
+	find mayInstanceOfFinalState_class(problem,interpretation,newObject);
+	find mayExist(problem, interpretation, newObject);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_Transition_class_by_outgoingTransitions_reference_Vertex_with_source_reference_Transition(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
+	container:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Transition class");
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"outgoingTransitions reference Vertex");
+	PartialInterpretation.partialrelationinterpretation(interpretation,inverseInterpretation);
+	PartialRelationInterpretation.interpretationOf.name(inverseInterpretation,"source reference Transition");
+	find mustInstanceOfVertex_class(problem,interpretation,container);
+	find mayInstanceOfTransition_class(problem,interpretation,newObject);
+	find mayInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,container,newObject);
+	find mustExist(problem, interpretation, container);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_Transition_class(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	typeInterpretation:PartialComplexTypeInterpretation)
+{
+	find interpretation(problem,interpretation);
+	neg find hasElementInContainment(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Transition class");
+	find mayInstanceOfTransition_class(problem,interpretation,newObject);
+	find mayExist(problem, interpretation, newObject);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_Region_class_by_regions_reference_CompositeElement(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
+	container:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Region class");
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"regions reference CompositeElement");
+	find mustInstanceOfCompositeElement_class(problem,interpretation,container);
+	find mayInstanceOfRegion_class(problem,interpretation,newObject);
+	find mayInRelationregions_reference_CompositeElement(problem,interpretation,container,newObject);
+	find mustExist(problem, interpretation, container);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_Region_class(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	typeInterpretation:PartialComplexTypeInterpretation)
+{
+	find interpretation(problem,interpretation);
+	neg find hasElementInContainment(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Region class");
+	find mayInstanceOfRegion_class(problem,interpretation,newObject);
+	find mayExist(problem, interpretation, newObject);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_Choice_class_by_vertices_reference_Region(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
+	container:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Choice class");
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
+	find mustInstanceOfRegion_class(problem,interpretation,container);
+	find mayInstanceOfChoice_class(problem,interpretation,newObject);
+	find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
+	find mustExist(problem, interpretation, container);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_Choice_class(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	typeInterpretation:PartialComplexTypeInterpretation)
+{
+	find interpretation(problem,interpretation);
+	neg find hasElementInContainment(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Choice class");
+	find mayInstanceOfChoice_class(problem,interpretation,newObject);
+	find mayExist(problem, interpretation, newObject);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_Synchronization_class_by_vertices_reference_Region(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
+	container:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Synchronization class");
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
+	find mustInstanceOfRegion_class(problem,interpretation,container);
+	find mayInstanceOfSynchronization_class(problem,interpretation,newObject);
+	find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
+	find mustExist(problem, interpretation, container);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_Synchronization_class(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	typeInterpretation:PartialComplexTypeInterpretation)
+{
+	find interpretation(problem,interpretation);
+	neg find hasElementInContainment(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Synchronization class");
+	find mayInstanceOfSynchronization_class(problem,interpretation,newObject);
+	find mayExist(problem, interpretation, newObject);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_Statechart_class_UndefinedPart(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	typeInterpretation:PartialComplexTypeInterpretation)
+{
+	find interpretation(problem,interpretation);
+	neg find hasElementInContainment(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Statechart class UndefinedPart");
+	find mayInstanceOfStatechart_class_UndefinedPart(problem,interpretation,newObject);
+	find mayExist(problem, interpretation, newObject);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_Entry_class_by_vertices_reference_Region(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
+	container:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Entry class");
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
+	find mustInstanceOfRegion_class(problem,interpretation,container);
+	find mayInstanceOfEntry_class(problem,interpretation,newObject);
+	find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
+	find mustExist(problem, interpretation, container);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_Entry_class(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	typeInterpretation:PartialComplexTypeInterpretation)
+{
+	find interpretation(problem,interpretation);
+	neg find hasElementInContainment(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Entry class");
+	find mayInstanceOfEntry_class(problem,interpretation,newObject);
+	find mayExist(problem, interpretation, newObject);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_State_class_by_vertices_reference_Region(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
+	container:DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"State class");
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
+	find mustInstanceOfRegion_class(problem,interpretation,container);
+	find mayInstanceOfState_class(problem,interpretation,newObject);
+	find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
+	find mustExist(problem, interpretation, container);
+	neg find mustExist(problem, interpretation, newObject);
+}
+pattern createObject_State_class(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	typeInterpretation:PartialComplexTypeInterpretation)
+{
+	find interpretation(problem,interpretation);
+	neg find hasElementInContainment(problem,interpretation);
+	PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
+	PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"State class");
+	find mayInstanceOfState_class(problem,interpretation,newObject);
+	find mayExist(problem, interpretation, newObject);
+	neg find mustExist(problem, interpretation, newObject);
+}
+
+//////////
+// 4.2 Type refinement
+//////////
+pattern refineTypeTo_Exit_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	find mayInstanceOfExit_class(problem,interpretation,element);
+	neg find mustInstanceOfExit_class(problem,interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfChoice_class(problem,interpretation,element);
+	neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfEntry_class(problem,interpretation,element);
+}
+pattern refineTypeTo_FinalState_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	find mayInstanceOfFinalState_class(problem,interpretation,element);
+	neg find mustInstanceOfFinalState_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+}
+pattern refineTypeTo_Transition_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	find mayInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+}
+pattern refineTypeTo_Region_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	find mayInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+}
+pattern refineTypeTo_Choice_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	find mayInstanceOfChoice_class(problem,interpretation,element);
+	neg find mustInstanceOfExit_class(problem,interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfChoice_class(problem,interpretation,element);
+	neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfEntry_class(problem,interpretation,element);
+}
+pattern refineTypeTo_Synchronization_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	find mayInstanceOfSynchronization_class(problem,interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfExit_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfChoice_class(problem,interpretation,element);
+	neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfEntry_class(problem,interpretation,element);
+}
+pattern refineTypeTo_Statechart_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	find mayInstanceOfStatechart_class_UndefinedPart(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfStatechart_class_UndefinedPart(problem,interpretation,element);
+	neg find mustInstanceOfVertex_class(problem,interpretation,element);
+}
+pattern refineTypeTo_Entry_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	find mayInstanceOfEntry_class(problem,interpretation,element);
+	neg find mustInstanceOfExit_class(problem,interpretation,element);
+	neg find mustInstanceOfRegularState_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfChoice_class(problem,interpretation,element);
+	neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
+	neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
+	neg find mustInstanceOfEntry_class(problem,interpretation,element);
+}
+pattern refineTypeTo_State_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
+	find interpretation(problem,interpretation);
+	PartialInterpretation.newElements(interpretation,element);
+	find mayInstanceOfState_class(problem,interpretation,element);
+	neg find mustInstanceOfFinalState_class(problem,interpretation,element);
+	neg find mustInstanceOfRegion_class(problem,interpretation,element);
+	neg find mustInstanceOfTransition_class(problem,interpretation,element);
+	neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
+	neg find mustInstanceOfStatechart_class(problem,interpretation,element);
+	neg find mustInstanceOfState_class(problem,interpretation,element);
+}
+
+//////////
+// 4.3 Relation refinement
+//////////
+pattern refineRelation_incomingTransitions_reference_Vertex_and_target_reference_Transition(
+	problem:LogicProblem, interpretation:PartialInterpretation,
+	relationIterpretation:PartialRelationInterpretation, oppositeInterpretation:PartialRelationInterpretation,
+	from: DefinedElement, to: DefinedElement)
+{
+	find interpretation(problem,interpretation);
+	PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
+	PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"incomingTransitions reference Vertex");
+	PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation);
+	PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"target reference Transition");
+	find mustExist(problem, interpretation, from);
+	find mustExist(problem, interpretation, to);
+	find mustInstanceOfVertex_class(problem,interpretation,from);
+	find mustInstanceOfTransition_class(problem,interpretation,to);
+	find mayInRelationincomingTransitions_reference_Vertex(problem,interpretation,from,to);
+	neg find mustInRelationincomingTransitions_reference_Vertex(problem,interpretation,from,to);
+}
-- 
cgit v1.2.3-54-g00ecf