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