aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated
diff options
context:
space:
mode:
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated2925
1 files changed, 2925 insertions, 0 deletions
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
index 5ac9e1dc..f2e524ab 100644
--- 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
@@ -26323,3 +26323,2928 @@ pattern refineRelation_incomingTransitions_reference_Vertex_and_target_reference
26323 find mayInRelationincomingTransitions_reference_Vertex(problem,interpretation,from,to); 26323 find mayInRelationincomingTransitions_reference_Vertex(problem,interpretation,from,to);
26324 neg find mustInRelationincomingTransitions_reference_Vertex(problem,interpretation,from,to); 26324 neg find mustInRelationincomingTransitions_reference_Vertex(problem,interpretation,from,to);
26325} 26325}
26326import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage"
26327import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"
26328import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"
26329
26330//////////
26331// 0. Util
26332//////////
26333private pattern interpretation(problem:LogicProblem, interpretation:PartialInterpretation) {
26334 PartialInterpretation.problem(interpretation,problem);
26335}
26336
26337/////////////////////////
26338// 0.1 Existence
26339/////////////////////////
26340private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26341 find interpretation(problem,interpretation);
26342 LogicProblem.elements(problem,element);
26343} or {
26344 find interpretation(problem,interpretation);
26345 PartialInterpretation.newElements(interpretation,element);
26346}
26347
26348private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26349 find mustExist(problem,interpretation,element);
26350} or {
26351 find interpretation(problem,interpretation);
26352 neg find elementCloseWorld(element);
26353 PartialInterpretation.openWorldElements(interpretation,element);
26354}
26355
26356private pattern elementCloseWorld(element:DefinedElement) {
26357 PartialInterpretation.openWorldElements(i,element);
26358 PartialInterpretation.maxNewElements(i,0);
26359} or {
26360 Scope.targetTypeInterpretation(scope,interpretation);
26361 PartialTypeInterpratation.elements(interpretation,element);
26362 Scope.maxNewElements(scope,0);
26363}
26364
26365////////////////////////
26366// 0.2 Equivalence
26367////////////////////////
26368pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) {
26369 find mayExist(problem,interpretation,a);
26370 find mayExist(problem,interpretation,b);
26371 a == b;
26372}
26373
26374////////////////////////
26375// 0.3 Required Patterns by TypeIndexer
26376////////////////////////
26377private pattern typeInterpretation(problem:LogicProblem, interpretation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) {
26378 find interpretation(problem,interpretation);
26379 LogicProblem.types(problem,type);
26380 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
26381 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26382}
26383
26384private pattern directInstanceOf(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, type:Type) {
26385 find interpretation(problem,interpretation);
26386 LogicProblem.types(problem,type);
26387 TypeDefinition.elements(type,element);
26388} or {
26389 find interpretation(problem,interpretation);
26390 find typeInterpretation(problem,interpretation,type,typeInterpretation);
26391 PartialComplexTypeInterpretation.elements(typeInterpretation,element);
26392}
26393
26394private pattern isPrimitive(element: PrimitiveElement) {
26395 PrimitiveElement(element);
26396}
26397
26398//////////
26399// 1. Problem-Specific Base Indexers
26400//////////
26401// 1.1 Type Indexers
26402//////////
26403// 1.1.1 primitive Type Indexers
26404//////////
26405
26406//////////
26407// 1.1.2 domain-specific Type Indexers
26408//////////
26409/**
26410 * An element must be an instance of type "Pseudostate class".
26411 */
26412private pattern mustInstanceOfPseudostate_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26413 Type.name(type,"Pseudostate class");
26414 find directInstanceOf(problem,interpretation,element,type);
26415}
26416private pattern scopeDisallowsNewPseudostate_class(problem:LogicProblem, interpretation:PartialInterpretation) {
26417 find interpretation(problem,interpretation);
26418 PartialInterpretation.scopes(interpretation,scope);
26419 Scope.targetTypeInterpretation(scope,typeInterpretation);
26420 Scope.maxNewElements(scope,0);
26421 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26422 Type.name(type,"Pseudostate class");
26423}
26424
26425/**
26426 * An element may be an instance of type "Pseudostate class".
26427 */
26428private pattern mayInstanceOfPseudostate_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26429{
26430 find interpretation(problem,interpretation);
26431 PartialInterpretation.newElements(interpretation,element);
26432 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26433 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26434 neg find mustInstanceOfEntry_class(problem,interpretation,element);
26435 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26436 neg find mustInstanceOfChoice_class(problem,interpretation,element);
26437 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
26438 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
26439 neg find mustInstanceOfExit_class(problem,interpretation,element);
26440 neg find scopeDisallowsNewPseudostate_class(problem, interpretation);
26441 neg find isPrimitive(element);
26442} or {
26443 find interpretation(problem,interpretation);
26444 PartialInterpretation.openWorldElements(interpretation,element);
26445 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26446 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26447 neg find mustInstanceOfEntry_class(problem,interpretation,element);
26448 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26449 neg find mustInstanceOfChoice_class(problem,interpretation,element);
26450 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
26451 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
26452 neg find mustInstanceOfExit_class(problem,interpretation,element);
26453 neg find scopeDisallowsNewPseudostate_class(problem, interpretation);
26454 neg find isPrimitive(element);
26455} or
26456{ find mustInstanceOfPseudostate_class(problem,interpretation,element); }
26457/**
26458 * An element must be an instance of type "Vertex class".
26459 */
26460private pattern mustInstanceOfVertex_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26461 Type.name(type,"Vertex class");
26462 find directInstanceOf(problem,interpretation,element,type);
26463}
26464private pattern scopeDisallowsNewVertex_class(problem:LogicProblem, interpretation:PartialInterpretation) {
26465 find interpretation(problem,interpretation);
26466 PartialInterpretation.scopes(interpretation,scope);
26467 Scope.targetTypeInterpretation(scope,typeInterpretation);
26468 Scope.maxNewElements(scope,0);
26469 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26470 Type.name(type,"Vertex class");
26471}
26472
26473/**
26474 * An element may be an instance of type "Vertex class".
26475 */
26476private pattern mayInstanceOfVertex_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26477{
26478 find interpretation(problem,interpretation);
26479 PartialInterpretation.newElements(interpretation,element);
26480 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
26481 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26482 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26483 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26484 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
26485 neg find scopeDisallowsNewVertex_class(problem, interpretation);
26486 neg find isPrimitive(element);
26487} or {
26488 find interpretation(problem,interpretation);
26489 PartialInterpretation.openWorldElements(interpretation,element);
26490 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
26491 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26492 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26493 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26494 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
26495 neg find scopeDisallowsNewVertex_class(problem, interpretation);
26496 neg find isPrimitive(element);
26497} or
26498{ find mustInstanceOfVertex_class(problem,interpretation,element); }
26499/**
26500 * An element must be an instance of type "Region class".
26501 */
26502private pattern mustInstanceOfRegion_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26503 Type.name(type,"Region class");
26504 find directInstanceOf(problem,interpretation,element,type);
26505}
26506private pattern scopeDisallowsNewRegion_class(problem:LogicProblem, interpretation:PartialInterpretation) {
26507 find interpretation(problem,interpretation);
26508 PartialInterpretation.scopes(interpretation,scope);
26509 Scope.targetTypeInterpretation(scope,typeInterpretation);
26510 Scope.maxNewElements(scope,0);
26511 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26512 Type.name(type,"Region class");
26513}
26514
26515/**
26516 * An element may be an instance of type "Region class".
26517 */
26518private pattern mayInstanceOfRegion_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26519{
26520 find interpretation(problem,interpretation);
26521 PartialInterpretation.newElements(interpretation,element);
26522 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26523 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26524 neg find mustInstanceOfVertex_class(problem,interpretation,element);
26525 neg find scopeDisallowsNewRegion_class(problem, interpretation);
26526 neg find isPrimitive(element);
26527} or {
26528 find interpretation(problem,interpretation);
26529 PartialInterpretation.openWorldElements(interpretation,element);
26530 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26531 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26532 neg find mustInstanceOfVertex_class(problem,interpretation,element);
26533 neg find scopeDisallowsNewRegion_class(problem, interpretation);
26534 neg find isPrimitive(element);
26535} or
26536{ find mustInstanceOfRegion_class(problem,interpretation,element); }
26537/**
26538 * An element must be an instance of type "Transition class".
26539 */
26540private pattern mustInstanceOfTransition_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26541 Type.name(type,"Transition class");
26542 find directInstanceOf(problem,interpretation,element,type);
26543}
26544private pattern scopeDisallowsNewTransition_class(problem:LogicProblem, interpretation:PartialInterpretation) {
26545 find interpretation(problem,interpretation);
26546 PartialInterpretation.scopes(interpretation,scope);
26547 Scope.targetTypeInterpretation(scope,typeInterpretation);
26548 Scope.maxNewElements(scope,0);
26549 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26550 Type.name(type,"Transition class");
26551}
26552
26553/**
26554 * An element may be an instance of type "Transition class".
26555 */
26556private pattern mayInstanceOfTransition_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26557{
26558 find interpretation(problem,interpretation);
26559 PartialInterpretation.newElements(interpretation,element);
26560 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26561 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26562 neg find mustInstanceOfVertex_class(problem,interpretation,element);
26563 neg find scopeDisallowsNewTransition_class(problem, interpretation);
26564 neg find isPrimitive(element);
26565} or {
26566 find interpretation(problem,interpretation);
26567 PartialInterpretation.openWorldElements(interpretation,element);
26568 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26569 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26570 neg find mustInstanceOfVertex_class(problem,interpretation,element);
26571 neg find scopeDisallowsNewTransition_class(problem, interpretation);
26572 neg find isPrimitive(element);
26573} or
26574{ find mustInstanceOfTransition_class(problem,interpretation,element); }
26575/**
26576 * An element must be an instance of type "Statechart class".
26577 */
26578private pattern mustInstanceOfStatechart_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26579 Type.name(type,"Statechart class");
26580 find directInstanceOf(problem,interpretation,element,type);
26581}
26582private pattern scopeDisallowsNewStatechart_class(problem:LogicProblem, interpretation:PartialInterpretation) {
26583 find interpretation(problem,interpretation);
26584 PartialInterpretation.scopes(interpretation,scope);
26585 Scope.targetTypeInterpretation(scope,typeInterpretation);
26586 Scope.maxNewElements(scope,0);
26587 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26588 Type.name(type,"Statechart class");
26589}
26590
26591/**
26592 * An element may be an instance of type "Statechart class".
26593 */
26594private pattern mayInstanceOfStatechart_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26595{
26596 find interpretation(problem,interpretation);
26597 PartialInterpretation.newElements(interpretation,element);
26598 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26599 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26600 neg find mustInstanceOfVertex_class(problem,interpretation,element);
26601 neg find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element);
26602 neg find scopeDisallowsNewStatechart_class(problem, interpretation);
26603 neg find isPrimitive(element);
26604} or {
26605 find interpretation(problem,interpretation);
26606 PartialInterpretation.openWorldElements(interpretation,element);
26607 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26608 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26609 neg find mustInstanceOfVertex_class(problem,interpretation,element);
26610 neg find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element);
26611 neg find scopeDisallowsNewStatechart_class(problem, interpretation);
26612 neg find isPrimitive(element);
26613} or
26614{ find mustInstanceOfStatechart_class(problem,interpretation,element); }
26615/**
26616 * An element must be an instance of type "Entry class".
26617 */
26618private pattern mustInstanceOfEntry_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26619 Type.name(type,"Entry class");
26620 find directInstanceOf(problem,interpretation,element,type);
26621}
26622private pattern scopeDisallowsNewEntry_class(problem:LogicProblem, interpretation:PartialInterpretation) {
26623 find interpretation(problem,interpretation);
26624 PartialInterpretation.scopes(interpretation,scope);
26625 Scope.targetTypeInterpretation(scope,typeInterpretation);
26626 Scope.maxNewElements(scope,0);
26627 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26628 Type.name(type,"Entry class");
26629}
26630
26631/**
26632 * An element may be an instance of type "Entry class".
26633 */
26634private pattern mayInstanceOfEntry_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26635{
26636 find interpretation(problem,interpretation);
26637 PartialInterpretation.newElements(interpretation,element);
26638 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26639 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26640 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26641 neg find mustInstanceOfChoice_class(problem,interpretation,element);
26642 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
26643 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
26644 neg find mustInstanceOfExit_class(problem,interpretation,element);
26645 neg find scopeDisallowsNewEntry_class(problem, interpretation);
26646 neg find isPrimitive(element);
26647} or {
26648 find interpretation(problem,interpretation);
26649 PartialInterpretation.openWorldElements(interpretation,element);
26650 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26651 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26652 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26653 neg find mustInstanceOfChoice_class(problem,interpretation,element);
26654 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
26655 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
26656 neg find mustInstanceOfExit_class(problem,interpretation,element);
26657 neg find scopeDisallowsNewEntry_class(problem, interpretation);
26658 neg find isPrimitive(element);
26659} or
26660{ find mustInstanceOfEntry_class(problem,interpretation,element); }
26661/**
26662 * An element must be an instance of type "Synchronization class".
26663 */
26664private pattern mustInstanceOfSynchronization_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26665 Type.name(type,"Synchronization class");
26666 find directInstanceOf(problem,interpretation,element,type);
26667}
26668private pattern scopeDisallowsNewSynchronization_class(problem:LogicProblem, interpretation:PartialInterpretation) {
26669 find interpretation(problem,interpretation);
26670 PartialInterpretation.scopes(interpretation,scope);
26671 Scope.targetTypeInterpretation(scope,typeInterpretation);
26672 Scope.maxNewElements(scope,0);
26673 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26674 Type.name(type,"Synchronization class");
26675}
26676
26677/**
26678 * An element may be an instance of type "Synchronization class".
26679 */
26680private pattern mayInstanceOfSynchronization_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26681{
26682 find interpretation(problem,interpretation);
26683 PartialInterpretation.newElements(interpretation,element);
26684 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26685 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26686 neg find mustInstanceOfEntry_class(problem,interpretation,element);
26687 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26688 neg find mustInstanceOfChoice_class(problem,interpretation,element);
26689 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
26690 neg find mustInstanceOfExit_class(problem,interpretation,element);
26691 neg find scopeDisallowsNewSynchronization_class(problem, interpretation);
26692 neg find isPrimitive(element);
26693} or {
26694 find interpretation(problem,interpretation);
26695 PartialInterpretation.openWorldElements(interpretation,element);
26696 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26697 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26698 neg find mustInstanceOfEntry_class(problem,interpretation,element);
26699 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26700 neg find mustInstanceOfChoice_class(problem,interpretation,element);
26701 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
26702 neg find mustInstanceOfExit_class(problem,interpretation,element);
26703 neg find scopeDisallowsNewSynchronization_class(problem, interpretation);
26704 neg find isPrimitive(element);
26705} or
26706{ find mustInstanceOfSynchronization_class(problem,interpretation,element); }
26707/**
26708 * An element must be an instance of type "State class".
26709 */
26710private pattern mustInstanceOfState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26711 Type.name(type,"State class");
26712 find directInstanceOf(problem,interpretation,element,type);
26713}
26714private pattern scopeDisallowsNewState_class(problem:LogicProblem, interpretation:PartialInterpretation) {
26715 find interpretation(problem,interpretation);
26716 PartialInterpretation.scopes(interpretation,scope);
26717 Scope.targetTypeInterpretation(scope,typeInterpretation);
26718 Scope.maxNewElements(scope,0);
26719 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26720 Type.name(type,"State class");
26721}
26722
26723/**
26724 * An element may be an instance of type "State class".
26725 */
26726private pattern mayInstanceOfState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26727{
26728 find interpretation(problem,interpretation);
26729 PartialInterpretation.newElements(interpretation,element);
26730 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
26731 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26732 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
26733 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26734 neg find mustInstanceOfFinalState_class(problem,interpretation,element);
26735 neg find scopeDisallowsNewState_class(problem, interpretation);
26736 neg find isPrimitive(element);
26737} or {
26738 find interpretation(problem,interpretation);
26739 PartialInterpretation.openWorldElements(interpretation,element);
26740 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
26741 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26742 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
26743 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26744 neg find mustInstanceOfFinalState_class(problem,interpretation,element);
26745 neg find scopeDisallowsNewState_class(problem, interpretation);
26746 neg find isPrimitive(element);
26747} or
26748{ find mustInstanceOfState_class(problem,interpretation,element); }
26749/**
26750 * An element must be an instance of type "RegularState class".
26751 */
26752private pattern mustInstanceOfRegularState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26753 Type.name(type,"RegularState class");
26754 find directInstanceOf(problem,interpretation,element,type);
26755}
26756private pattern scopeDisallowsNewRegularState_class(problem:LogicProblem, interpretation:PartialInterpretation) {
26757 find interpretation(problem,interpretation);
26758 PartialInterpretation.scopes(interpretation,scope);
26759 Scope.targetTypeInterpretation(scope,typeInterpretation);
26760 Scope.maxNewElements(scope,0);
26761 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26762 Type.name(type,"RegularState class");
26763}
26764
26765/**
26766 * An element may be an instance of type "RegularState class".
26767 */
26768private pattern mayInstanceOfRegularState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26769{
26770 find interpretation(problem,interpretation);
26771 PartialInterpretation.newElements(interpretation,element);
26772 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
26773 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26774 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26775 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26776 neg find mustInstanceOfFinalState_class(problem,interpretation,element);
26777 neg find scopeDisallowsNewRegularState_class(problem, interpretation);
26778 neg find isPrimitive(element);
26779} or {
26780 find interpretation(problem,interpretation);
26781 PartialInterpretation.openWorldElements(interpretation,element);
26782 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
26783 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26784 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26785 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26786 neg find mustInstanceOfFinalState_class(problem,interpretation,element);
26787 neg find scopeDisallowsNewRegularState_class(problem, interpretation);
26788 neg find isPrimitive(element);
26789} or
26790{ find mustInstanceOfRegularState_class(problem,interpretation,element); }
26791/**
26792 * An element must be an instance of type "CompositeElement class".
26793 */
26794private pattern mustInstanceOfCompositeElement_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26795 Type.name(type,"CompositeElement class");
26796 find directInstanceOf(problem,interpretation,element,type);
26797}
26798private pattern scopeDisallowsNewCompositeElement_class(problem:LogicProblem, interpretation:PartialInterpretation) {
26799 find interpretation(problem,interpretation);
26800 PartialInterpretation.scopes(interpretation,scope);
26801 Scope.targetTypeInterpretation(scope,typeInterpretation);
26802 Scope.maxNewElements(scope,0);
26803 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26804 Type.name(type,"CompositeElement class");
26805}
26806
26807/**
26808 * An element may be an instance of type "CompositeElement class".
26809 */
26810private pattern mayInstanceOfCompositeElement_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26811{
26812 find interpretation(problem,interpretation);
26813 PartialInterpretation.newElements(interpretation,element);
26814 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26815 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
26816 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26817 neg find mustInstanceOfVertex_class(problem,interpretation,element);
26818 neg find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element);
26819 neg find scopeDisallowsNewCompositeElement_class(problem, interpretation);
26820 neg find isPrimitive(element);
26821} or {
26822 find interpretation(problem,interpretation);
26823 PartialInterpretation.openWorldElements(interpretation,element);
26824 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26825 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
26826 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26827 neg find mustInstanceOfVertex_class(problem,interpretation,element);
26828 neg find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element);
26829 neg find scopeDisallowsNewCompositeElement_class(problem, interpretation);
26830 neg find isPrimitive(element);
26831} or
26832{ find mustInstanceOfCompositeElement_class(problem,interpretation,element); }
26833/**
26834 * An element must be an instance of type "Choice class".
26835 */
26836private pattern mustInstanceOfChoice_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26837 Type.name(type,"Choice class");
26838 find directInstanceOf(problem,interpretation,element,type);
26839}
26840private pattern scopeDisallowsNewChoice_class(problem:LogicProblem, interpretation:PartialInterpretation) {
26841 find interpretation(problem,interpretation);
26842 PartialInterpretation.scopes(interpretation,scope);
26843 Scope.targetTypeInterpretation(scope,typeInterpretation);
26844 Scope.maxNewElements(scope,0);
26845 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26846 Type.name(type,"Choice class");
26847}
26848
26849/**
26850 * An element may be an instance of type "Choice class".
26851 */
26852private pattern mayInstanceOfChoice_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26853{
26854 find interpretation(problem,interpretation);
26855 PartialInterpretation.newElements(interpretation,element);
26856 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26857 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26858 neg find mustInstanceOfEntry_class(problem,interpretation,element);
26859 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26860 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
26861 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
26862 neg find mustInstanceOfExit_class(problem,interpretation,element);
26863 neg find scopeDisallowsNewChoice_class(problem, interpretation);
26864 neg find isPrimitive(element);
26865} or {
26866 find interpretation(problem,interpretation);
26867 PartialInterpretation.openWorldElements(interpretation,element);
26868 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26869 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26870 neg find mustInstanceOfEntry_class(problem,interpretation,element);
26871 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26872 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
26873 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
26874 neg find mustInstanceOfExit_class(problem,interpretation,element);
26875 neg find scopeDisallowsNewChoice_class(problem, interpretation);
26876 neg find isPrimitive(element);
26877} or
26878{ find mustInstanceOfChoice_class(problem,interpretation,element); }
26879/**
26880 * An element must be an instance of type "Exit class".
26881 */
26882private pattern mustInstanceOfExit_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26883 Type.name(type,"Exit class");
26884 find directInstanceOf(problem,interpretation,element,type);
26885}
26886private pattern scopeDisallowsNewExit_class(problem:LogicProblem, interpretation:PartialInterpretation) {
26887 find interpretation(problem,interpretation);
26888 PartialInterpretation.scopes(interpretation,scope);
26889 Scope.targetTypeInterpretation(scope,typeInterpretation);
26890 Scope.maxNewElements(scope,0);
26891 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26892 Type.name(type,"Exit class");
26893}
26894
26895/**
26896 * An element may be an instance of type "Exit class".
26897 */
26898private pattern mayInstanceOfExit_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26899{
26900 find interpretation(problem,interpretation);
26901 PartialInterpretation.newElements(interpretation,element);
26902 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26903 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26904 neg find mustInstanceOfEntry_class(problem,interpretation,element);
26905 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26906 neg find mustInstanceOfChoice_class(problem,interpretation,element);
26907 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
26908 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
26909 neg find scopeDisallowsNewExit_class(problem, interpretation);
26910 neg find isPrimitive(element);
26911} or {
26912 find interpretation(problem,interpretation);
26913 PartialInterpretation.openWorldElements(interpretation,element);
26914 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26915 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26916 neg find mustInstanceOfEntry_class(problem,interpretation,element);
26917 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26918 neg find mustInstanceOfChoice_class(problem,interpretation,element);
26919 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
26920 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
26921 neg find scopeDisallowsNewExit_class(problem, interpretation);
26922 neg find isPrimitive(element);
26923} or
26924{ find mustInstanceOfExit_class(problem,interpretation,element); }
26925/**
26926 * An element must be an instance of type "FinalState class".
26927 */
26928private pattern mustInstanceOfFinalState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26929 Type.name(type,"FinalState class");
26930 find directInstanceOf(problem,interpretation,element,type);
26931}
26932private pattern scopeDisallowsNewFinalState_class(problem:LogicProblem, interpretation:PartialInterpretation) {
26933 find interpretation(problem,interpretation);
26934 PartialInterpretation.scopes(interpretation,scope);
26935 Scope.targetTypeInterpretation(scope,typeInterpretation);
26936 Scope.maxNewElements(scope,0);
26937 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26938 Type.name(type,"FinalState class");
26939}
26940
26941/**
26942 * An element may be an instance of type "FinalState class".
26943 */
26944private pattern mayInstanceOfFinalState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26945{
26946 find interpretation(problem,interpretation);
26947 PartialInterpretation.newElements(interpretation,element);
26948 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
26949 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26950 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26951 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26952 neg find scopeDisallowsNewFinalState_class(problem, interpretation);
26953 neg find isPrimitive(element);
26954} or {
26955 find interpretation(problem,interpretation);
26956 PartialInterpretation.openWorldElements(interpretation,element);
26957 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
26958 neg find mustInstanceOfTransition_class(problem,interpretation,element);
26959 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
26960 neg find mustInstanceOfRegion_class(problem,interpretation,element);
26961 neg find scopeDisallowsNewFinalState_class(problem, interpretation);
26962 neg find isPrimitive(element);
26963} or
26964{ find mustInstanceOfFinalState_class(problem,interpretation,element); }
26965/**
26966 * An element must be an instance of type "Statechart class DefinedPart".
26967 */
26968private pattern mustInstanceOfStatechart_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26969 Type.name(type,"Statechart class DefinedPart");
26970 find directInstanceOf(problem,interpretation,element,type);
26971}
26972private pattern scopeDisallowsNewStatechart_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation) {
26973 find interpretation(problem,interpretation);
26974 PartialInterpretation.scopes(interpretation,scope);
26975 Scope.targetTypeInterpretation(scope,typeInterpretation);
26976 Scope.maxNewElements(scope,0);
26977 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26978 Type.name(type,"Statechart class DefinedPart");
26979}
26980
26981/**
26982 * An element may be an instance of type "Statechart class DefinedPart".
26983 */
26984private pattern mayInstanceOfStatechart_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
26985{ find mustInstanceOfStatechart_class_DefinedPart(problem,interpretation,element); }
26986/**
26987 * An element must be an instance of type "Statechart class UndefinedPart".
26988 */
26989private pattern mustInstanceOfStatechart_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
26990 Type.name(type,"Statechart class UndefinedPart");
26991 find directInstanceOf(problem,interpretation,element,type);
26992}
26993private pattern scopeDisallowsNewStatechart_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation) {
26994 find interpretation(problem,interpretation);
26995 PartialInterpretation.scopes(interpretation,scope);
26996 Scope.targetTypeInterpretation(scope,typeInterpretation);
26997 Scope.maxNewElements(scope,0);
26998 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
26999 Type.name(type,"Statechart class UndefinedPart");
27000}
27001
27002/**
27003 * An element may be an instance of type "Statechart class UndefinedPart".
27004 */
27005private pattern mayInstanceOfStatechart_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
27006{
27007 find interpretation(problem,interpretation);
27008 PartialInterpretation.newElements(interpretation,element);
27009 neg find mustInstanceOfTransition_class(problem,interpretation,element);
27010 neg find mustInstanceOfRegion_class(problem,interpretation,element);
27011 neg find mustInstanceOfVertex_class(problem,interpretation,element);
27012 neg find scopeDisallowsNewStatechart_class_UndefinedPart(problem, interpretation);
27013 neg find isPrimitive(element);
27014} or {
27015 find interpretation(problem,interpretation);
27016 PartialInterpretation.openWorldElements(interpretation,element);
27017 neg find mustInstanceOfTransition_class(problem,interpretation,element);
27018 neg find mustInstanceOfRegion_class(problem,interpretation,element);
27019 neg find mustInstanceOfVertex_class(problem,interpretation,element);
27020 neg find scopeDisallowsNewStatechart_class_UndefinedPart(problem, interpretation);
27021 neg find isPrimitive(element);
27022} or
27023{ find mustInstanceOfStatechart_class_UndefinedPart(problem,interpretation,element); }
27024/**
27025 * An element must be an instance of type "CompositeElement class DefinedPart".
27026 */
27027private pattern mustInstanceOfCompositeElement_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
27028 Type.name(type,"CompositeElement class DefinedPart");
27029 find directInstanceOf(problem,interpretation,element,type);
27030}
27031private pattern scopeDisallowsNewCompositeElement_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation) {
27032 find interpretation(problem,interpretation);
27033 PartialInterpretation.scopes(interpretation,scope);
27034 Scope.targetTypeInterpretation(scope,typeInterpretation);
27035 Scope.maxNewElements(scope,0);
27036 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
27037 Type.name(type,"CompositeElement class DefinedPart");
27038}
27039
27040/**
27041 * An element may be an instance of type "CompositeElement class DefinedPart".
27042 */
27043private pattern mayInstanceOfCompositeElement_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
27044{ find mustInstanceOfCompositeElement_class_DefinedPart(problem,interpretation,element); }
27045/**
27046 * An element must be an instance of type "CompositeElement class UndefinedPart".
27047 */
27048private pattern mustInstanceOfCompositeElement_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
27049 Type.name(type,"CompositeElement class UndefinedPart");
27050 find directInstanceOf(problem,interpretation,element,type);
27051}
27052private pattern scopeDisallowsNewCompositeElement_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation) {
27053 find interpretation(problem,interpretation);
27054 PartialInterpretation.scopes(interpretation,scope);
27055 Scope.targetTypeInterpretation(scope,typeInterpretation);
27056 Scope.maxNewElements(scope,0);
27057 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
27058 Type.name(type,"CompositeElement class UndefinedPart");
27059}
27060
27061/**
27062 * An element may be an instance of type "CompositeElement class UndefinedPart".
27063 */
27064private pattern mayInstanceOfCompositeElement_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
27065{
27066 find interpretation(problem,interpretation);
27067 PartialInterpretation.newElements(interpretation,element);
27068 neg find mustInstanceOfTransition_class(problem,interpretation,element);
27069 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
27070 neg find mustInstanceOfRegion_class(problem,interpretation,element);
27071 neg find mustInstanceOfVertex_class(problem,interpretation,element);
27072 neg find scopeDisallowsNewCompositeElement_class_UndefinedPart(problem, interpretation);
27073 neg find isPrimitive(element);
27074} or {
27075 find interpretation(problem,interpretation);
27076 PartialInterpretation.openWorldElements(interpretation,element);
27077 neg find mustInstanceOfTransition_class(problem,interpretation,element);
27078 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
27079 neg find mustInstanceOfRegion_class(problem,interpretation,element);
27080 neg find mustInstanceOfVertex_class(problem,interpretation,element);
27081 neg find scopeDisallowsNewCompositeElement_class_UndefinedPart(problem, interpretation);
27082 neg find isPrimitive(element);
27083} or
27084{ find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element); }
27085
27086//////////
27087// 1.2 Relation Declaration Indexers
27088//////////
27089/**
27090 * Matcher for detecting tuples t where []incomingTransitions reference Vertex(source,target)
27091 */
27092private pattern mustInRelationincomingTransitions_reference_Vertex(
27093 problem:LogicProblem, interpretation:PartialInterpretation,
27094 source: DefinedElement, target:DefinedElement)
27095{
27096 find interpretation(problem,interpretation);
27097 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
27098 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"incomingTransitions reference Vertex");
27099 PartialRelationInterpretation.relationlinks(relationIterpretation,link);
27100 BinaryElementRelationLink.param1(link,source);
27101 BinaryElementRelationLink.param2(link,target);
27102}
27103/**
27104 * Matcher for detecting tuples t where <>incomingTransitions reference Vertex(source,target)
27105 */
27106private pattern mayInRelationincomingTransitions_reference_Vertex(
27107 problem:LogicProblem, interpretation:PartialInterpretation,
27108 source: DefinedElement, target:DefinedElement)
27109{
27110 find interpretation(problem,interpretation);
27111 // The two endpoint of the link have to exist
27112 find mayExist(problem, interpretation, source);
27113 find mayExist(problem, interpretation, target);
27114 // Type consistency
27115 find mayInstanceOfVertex_class(problem,interpretation,source);
27116 find mayInstanceOfTransition_class(problem,interpretation,target);
27117 // There are "numberOfExistingReferences" currently existing instances of the reference to the target,
27118 // the upper bound of the opposite reference multiplicity should be considered.
27119 numberOfExistingOppositeReferences == count find mustInRelationtarget_reference_Transition(problem,interpretation,target,_);
27120 check(numberOfExistingOppositeReferences < 1);
27121} or {
27122 find mustInRelationincomingTransitions_reference_Vertex(problem,interpretation,source,target);
27123}
27124/**
27125 * Matcher for detecting tuples t where []outgoingTransitions reference Vertex(source,target)
27126 */
27127private pattern mustInRelationoutgoingTransitions_reference_Vertex(
27128 problem:LogicProblem, interpretation:PartialInterpretation,
27129 source: DefinedElement, target:DefinedElement)
27130{
27131 find interpretation(problem,interpretation);
27132 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
27133 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"outgoingTransitions reference Vertex");
27134 PartialRelationInterpretation.relationlinks(relationIterpretation,link);
27135 BinaryElementRelationLink.param1(link,source);
27136 BinaryElementRelationLink.param2(link,target);
27137}
27138/**
27139 * Matcher for detecting tuples t where <>outgoingTransitions reference Vertex(source,target)
27140 */
27141private pattern mayInRelationoutgoingTransitions_reference_Vertex(
27142 problem:LogicProblem, interpretation:PartialInterpretation,
27143 source: DefinedElement, target:DefinedElement)
27144{
27145 find interpretation(problem,interpretation);
27146 // The two endpoint of the link have to exist
27147 find mayExist(problem, interpretation, source);
27148 find mayExist(problem, interpretation, target);
27149 // Type consistency
27150 find mayInstanceOfVertex_class(problem,interpretation,source);
27151 find mayInstanceOfTransition_class(problem,interpretation,target);
27152 // There are "numberOfExistingReferences" currently existing instances of the reference to the target,
27153 // the upper bound of the opposite reference multiplicity should be considered.
27154 numberOfExistingOppositeReferences == count find mustInRelationsource_reference_Transition(problem,interpretation,target,_);
27155 check(numberOfExistingOppositeReferences < 1);
27156 // The reference is containment, then a new reference cannot be create if:
27157 // 1. Multiple parents
27158 neg find mustContains4(problem,interpretation,_,target);
27159 // 2. Circle in the containment hierarchy
27160 neg find mustTransitiveContains(source,target);
27161} or {
27162 find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,source,target);
27163}
27164/**
27165 * Matcher for detecting tuples t where []vertices reference Region(source,target)
27166 */
27167private pattern mustInRelationvertices_reference_Region(
27168 problem:LogicProblem, interpretation:PartialInterpretation,
27169 source: DefinedElement, target:DefinedElement)
27170{
27171 find interpretation(problem,interpretation);
27172 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
27173 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"vertices reference Region");
27174 PartialRelationInterpretation.relationlinks(relationIterpretation,link);
27175 BinaryElementRelationLink.param1(link,source);
27176 BinaryElementRelationLink.param2(link,target);
27177}
27178/**
27179 * Matcher for detecting tuples t where <>vertices reference Region(source,target)
27180 */
27181private pattern mayInRelationvertices_reference_Region(
27182 problem:LogicProblem, interpretation:PartialInterpretation,
27183 source: DefinedElement, target:DefinedElement)
27184{
27185 find interpretation(problem,interpretation);
27186 // The two endpoint of the link have to exist
27187 find mayExist(problem, interpretation, source);
27188 find mayExist(problem, interpretation, target);
27189 // Type consistency
27190 find mayInstanceOfRegion_class(problem,interpretation,source);
27191 find mayInstanceOfVertex_class(problem,interpretation,target);
27192 // The reference is containment, then a new reference cannot be create if:
27193 // 1. Multiple parents
27194 neg find mustContains4(problem,interpretation,_,target);
27195 // 2. Circle in the containment hierarchy
27196 neg find mustTransitiveContains(source,target);
27197} or {
27198 find mustInRelationvertices_reference_Region(problem,interpretation,source,target);
27199}
27200/**
27201 * Matcher for detecting tuples t where []target reference Transition(source,target)
27202 */
27203private pattern mustInRelationtarget_reference_Transition(
27204 problem:LogicProblem, interpretation:PartialInterpretation,
27205 source: DefinedElement, target:DefinedElement)
27206{
27207 find interpretation(problem,interpretation);
27208 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
27209 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"target reference Transition");
27210 PartialRelationInterpretation.relationlinks(relationIterpretation,link);
27211 BinaryElementRelationLink.param1(link,source);
27212 BinaryElementRelationLink.param2(link,target);
27213}
27214/**
27215 * Matcher for detecting tuples t where <>target reference Transition(source,target)
27216 */
27217private pattern mayInRelationtarget_reference_Transition(
27218 problem:LogicProblem, interpretation:PartialInterpretation,
27219 source: DefinedElement, target:DefinedElement)
27220{
27221 find interpretation(problem,interpretation);
27222 // The two endpoint of the link have to exist
27223 find mayExist(problem, interpretation, source);
27224 find mayExist(problem, interpretation, target);
27225 // Type consistency
27226 find mayInstanceOfTransition_class(problem,interpretation,source);
27227 find mayInstanceOfVertex_class(problem,interpretation,target);
27228 // There are "numberOfExistingReferences" currently existing instances of the reference from the source,
27229 // the upper bound of the multiplicity should be considered.
27230 numberOfExistingReferences == count find mustInRelationtarget_reference_Transition(problem,interpretation,source,_);
27231 check(numberOfExistingReferences < 1);
27232} or {
27233 find mustInRelationtarget_reference_Transition(problem,interpretation,source,target);
27234}
27235/**
27236 * Matcher for detecting tuples t where []source reference Transition(source,target)
27237 */
27238private pattern mustInRelationsource_reference_Transition(
27239 problem:LogicProblem, interpretation:PartialInterpretation,
27240 source: DefinedElement, target:DefinedElement)
27241{
27242 find interpretation(problem,interpretation);
27243 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
27244 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"source reference Transition");
27245 PartialRelationInterpretation.relationlinks(relationIterpretation,link);
27246 BinaryElementRelationLink.param1(link,source);
27247 BinaryElementRelationLink.param2(link,target);
27248}
27249/**
27250 * Matcher for detecting tuples t where <>source reference Transition(source,target)
27251 */
27252private pattern mayInRelationsource_reference_Transition(
27253 problem:LogicProblem, interpretation:PartialInterpretation,
27254 source: DefinedElement, target:DefinedElement)
27255{
27256 find interpretation(problem,interpretation);
27257 // The two endpoint of the link have to exist
27258 find mayExist(problem, interpretation, source);
27259 find mayExist(problem, interpretation, target);
27260 // Type consistency
27261 find mayInstanceOfTransition_class(problem,interpretation,source);
27262 find mayInstanceOfVertex_class(problem,interpretation,target);
27263 // There are "numberOfExistingReferences" currently existing instances of the reference from the source,
27264 // the upper bound of the multiplicity should be considered.
27265 numberOfExistingReferences == count find mustInRelationsource_reference_Transition(problem,interpretation,source,_);
27266 check(numberOfExistingReferences < 1);
27267 // The eOpposite of the reference is containment, then a referene cannot be created if
27268 // 1. Multiple parents
27269 neg find mustContains4(problem,interpretation,source,_);
27270 // 2. Circle in the containment hierarchy
27271 neg find mustTransitiveContains(source,target);
27272} or {
27273 find mustInRelationsource_reference_Transition(problem,interpretation,source,target);
27274}
27275/**
27276 * Matcher for detecting tuples t where []regions reference CompositeElement(source,target)
27277 */
27278private pattern mustInRelationregions_reference_CompositeElement(
27279 problem:LogicProblem, interpretation:PartialInterpretation,
27280 source: DefinedElement, target:DefinedElement)
27281{
27282 find interpretation(problem,interpretation);
27283 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
27284 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"regions reference CompositeElement");
27285 PartialRelationInterpretation.relationlinks(relationIterpretation,link);
27286 BinaryElementRelationLink.param1(link,source);
27287 BinaryElementRelationLink.param2(link,target);
27288}
27289/**
27290 * Matcher for detecting tuples t where <>regions reference CompositeElement(source,target)
27291 */
27292private pattern mayInRelationregions_reference_CompositeElement(
27293 problem:LogicProblem, interpretation:PartialInterpretation,
27294 source: DefinedElement, target:DefinedElement)
27295{
27296 find interpretation(problem,interpretation);
27297 // The two endpoint of the link have to exist
27298 find mayExist(problem, interpretation, source);
27299 find mayExist(problem, interpretation, target);
27300 // Type consistency
27301 find mayInstanceOfCompositeElement_class(problem,interpretation,source);
27302 find mayInstanceOfRegion_class(problem,interpretation,target);
27303 // The reference is containment, then a new reference cannot be create if:
27304 // 1. Multiple parents
27305 neg find mustContains4(problem,interpretation,_,target);
27306 // 2. Circle in the containment hierarchy
27307 neg find mustTransitiveContains(source,target);
27308} or {
27309 find mustInRelationregions_reference_CompositeElement(problem,interpretation,source,target);
27310}
27311
27312//////////
27313// 1.3 Relation Definition Indexers
27314//////////
27315// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries entryInRegion
27316private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_entryInRegion(
27317 problem:LogicProblem, interpretation:PartialInterpretation,
27318 var_r1, var_e1)
27319{
27320 find interpretation(problem,interpretation);
27321 find mustInstanceOfRegion_class(problem,interpretation,var_r1);
27322 find mustInstanceOfEntry_class(problem,interpretation,var_e1);
27323 // r1 is exported
27324 // e1 is exported
27325 find mustInstanceOfRegion_class(problem,interpretation,var_r1);
27326 find mustInRelationvertices_reference_Region(problem,interpretation,var_r1,var_virtual0);
27327 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
27328 var_virtual0 == var_e1;
27329}
27330private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_entryInRegion(
27331 problem:LogicProblem, interpretation:PartialInterpretation,
27332 var_r1, var_e1)
27333{
27334 find interpretation(problem,interpretation);
27335 find mayInstanceOfRegion_class(problem,interpretation,var_r1);
27336 find mayInstanceOfEntry_class(problem,interpretation,var_e1);
27337 // r1 is exported
27338 // e1 is exported
27339 find mayInstanceOfRegion_class(problem,interpretation,var_r1);
27340 find mayInRelationvertices_reference_Region(problem,interpretation,var_r1,var_virtual0);
27341 find mayInstanceOfVertex_class(problem,interpretation,var_virtual0);
27342 find mayEquivalent(problem, interpretation, var_virtual0, var_e1);
27343}
27344private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_entryInRegion(
27345 problem:LogicProblem, interpretation:PartialInterpretation,
27346 var_r1, var_e1)
27347{
27348 find interpretation(problem,interpretation);
27349 find mustInstanceOfRegion_class(problem,interpretation,var_r1);
27350 find mustInstanceOfEntry_class(problem,interpretation,var_e1);
27351 // r1 is exported
27352 // e1 is exported
27353 find mustInstanceOfRegion_class(problem,interpretation,var_r1);
27354 find mustInRelationvertices_reference_Region(problem,interpretation,var_r1,var_virtual0);
27355 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
27356 var_virtual0 == var_e1;
27357}
27358// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries noEntryInRegion
27359private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noEntryInRegion(
27360 problem:LogicProblem, interpretation:PartialInterpretation,
27361 var_r1)
27362{
27363 find interpretation(problem,interpretation);
27364 find mustInstanceOfRegion_class(problem,interpretation,var_r1);
27365 // r1 is exported
27366 neg find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_entryInRegion(problem,interpretation,var_r1,_var__0);
27367}
27368private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noEntryInRegion(
27369 problem:LogicProblem, interpretation:PartialInterpretation,
27370 var_r1)
27371{
27372 find interpretation(problem,interpretation);
27373 find mayInstanceOfRegion_class(problem,interpretation,var_r1);
27374 // r1 is exported
27375 neg find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_entryInRegion(problem,interpretation,var_r1,_var__0);
27376}
27377private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noEntryInRegion(
27378 problem:LogicProblem, interpretation:PartialInterpretation,
27379 var_r1)
27380{
27381 find interpretation(problem,interpretation);
27382 find mustInstanceOfRegion_class(problem,interpretation,var_r1);
27383 // r1 is exported
27384 neg find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_entryInRegion(problem,interpretation,var_r1,_var__0);
27385}
27386// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries multipleEntryInRegion
27387private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleEntryInRegion(
27388 problem:LogicProblem, interpretation:PartialInterpretation,
27389 var_r)
27390{
27391 find interpretation(problem,interpretation);
27392 find mustInstanceOfRegion_class(problem,interpretation,var_r);
27393 // r is exported
27394 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_entryInRegion(problem,interpretation,var_r,var_e1);
27395 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_entryInRegion(problem,interpretation,var_r,var_e2);
27396 neg find mayEquivalent(problem, interpretation, var_e1, var_e2);
27397}
27398private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleEntryInRegion(
27399 problem:LogicProblem, interpretation:PartialInterpretation,
27400 var_r)
27401{
27402 find interpretation(problem,interpretation);
27403 find mayInstanceOfRegion_class(problem,interpretation,var_r);
27404 // r is exported
27405 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_entryInRegion(problem,interpretation,var_r,var_e1);
27406 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_entryInRegion(problem,interpretation,var_r,var_e2);
27407 var_e1 != var_e2;
27408}
27409private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleEntryInRegion(
27410 problem:LogicProblem, interpretation:PartialInterpretation,
27411 var_r)
27412{
27413 find interpretation(problem,interpretation);
27414 find mustInstanceOfRegion_class(problem,interpretation,var_r);
27415 // r is exported
27416 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_entryInRegion(problem,interpretation,var_r,var_e1);
27417 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_entryInRegion(problem,interpretation,var_r,var_e2);
27418 var_e1 != var_e2;
27419}
27420// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries transition
27421private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(
27422 problem:LogicProblem, interpretation:PartialInterpretation,
27423 var_t, var_src, var_trg)
27424{
27425 find interpretation(problem,interpretation);
27426 find mustInstanceOfTransition_class(problem,interpretation,var_t);
27427 find mustInstanceOfVertex_class(problem,interpretation,var_src);
27428 find mustInstanceOfVertex_class(problem,interpretation,var_trg);
27429 // t is exported
27430 // src is exported
27431 // trg is exported
27432 find mustInstanceOfTransition_class(problem,interpretation,var_t);
27433 find mustInRelationsource_reference_Transition(problem,interpretation,var_t,var_virtual0);
27434 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
27435 var_virtual0 == var_src;
27436 find mustInstanceOfTransition_class(problem,interpretation,var_t);
27437 find mustInRelationtarget_reference_Transition(problem,interpretation,var_t,var_virtual1);
27438 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
27439 var_virtual1 == var_trg;
27440}
27441private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(
27442 problem:LogicProblem, interpretation:PartialInterpretation,
27443 var_t, var_src, var_trg)
27444{
27445 find interpretation(problem,interpretation);
27446 find mayInstanceOfTransition_class(problem,interpretation,var_t);
27447 find mayInstanceOfVertex_class(problem,interpretation,var_src);
27448 find mayInstanceOfVertex_class(problem,interpretation,var_trg);
27449 // t is exported
27450 // src is exported
27451 // trg is exported
27452 find mayInstanceOfTransition_class(problem,interpretation,var_t);
27453 find mayInRelationsource_reference_Transition(problem,interpretation,var_t,var_virtual0);
27454 find mayInstanceOfVertex_class(problem,interpretation,var_virtual0);
27455 find mayEquivalent(problem, interpretation, var_virtual0, var_src);
27456 find mayInstanceOfTransition_class(problem,interpretation,var_t);
27457 find mayInRelationtarget_reference_Transition(problem,interpretation,var_t,var_virtual1);
27458 find mayInstanceOfVertex_class(problem,interpretation,var_virtual1);
27459 find mayEquivalent(problem, interpretation, var_virtual1, var_trg);
27460}
27461private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(
27462 problem:LogicProblem, interpretation:PartialInterpretation,
27463 var_t, var_src, var_trg)
27464{
27465 find interpretation(problem,interpretation);
27466 find mustInstanceOfTransition_class(problem,interpretation,var_t);
27467 find mustInstanceOfVertex_class(problem,interpretation,var_src);
27468 find mustInstanceOfVertex_class(problem,interpretation,var_trg);
27469 // t is exported
27470 // src is exported
27471 // trg is exported
27472 find mustInstanceOfTransition_class(problem,interpretation,var_t);
27473 find mustInRelationsource_reference_Transition(problem,interpretation,var_t,var_virtual0);
27474 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
27475 var_virtual0 == var_src;
27476 find mustInstanceOfTransition_class(problem,interpretation,var_t);
27477 find mustInRelationtarget_reference_Transition(problem,interpretation,var_t,var_virtual1);
27478 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
27479 var_virtual1 == var_trg;
27480}
27481// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries incomingToEntry
27482private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_incomingToEntry(
27483 problem:LogicProblem, interpretation:PartialInterpretation,
27484 var_t, var_e)
27485{
27486 find interpretation(problem,interpretation);
27487 find mustInstanceOfTransition_class(problem,interpretation,var_t);
27488 find mustInstanceOfEntry_class(problem,interpretation,var_e);
27489 // t is exported
27490 // e is exported
27491 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t,_var__0,var_e);
27492}
27493private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_incomingToEntry(
27494 problem:LogicProblem, interpretation:PartialInterpretation,
27495 var_t, var_e)
27496{
27497 find interpretation(problem,interpretation);
27498 find mayInstanceOfTransition_class(problem,interpretation,var_t);
27499 find mayInstanceOfEntry_class(problem,interpretation,var_e);
27500 // t is exported
27501 // e is exported
27502 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t,_var__0,var_e);
27503}
27504private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_incomingToEntry(
27505 problem:LogicProblem, interpretation:PartialInterpretation,
27506 var_t, var_e)
27507{
27508 find interpretation(problem,interpretation);
27509 find mustInstanceOfTransition_class(problem,interpretation,var_t);
27510 find mustInstanceOfEntry_class(problem,interpretation,var_e);
27511 // t is exported
27512 // e is exported
27513 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t,_var__0,var_e);
27514}
27515// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries noOutgoingTransitionFromEntry
27516private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noOutgoingTransitionFromEntry(
27517 problem:LogicProblem, interpretation:PartialInterpretation,
27518 var_e)
27519{
27520 find interpretation(problem,interpretation);
27521 find mustInstanceOfEntry_class(problem,interpretation,var_e);
27522 // e is exported
27523 neg find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_e,_var__1);
27524}
27525private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noOutgoingTransitionFromEntry(
27526 problem:LogicProblem, interpretation:PartialInterpretation,
27527 var_e)
27528{
27529 find interpretation(problem,interpretation);
27530 find mayInstanceOfEntry_class(problem,interpretation,var_e);
27531 // e is exported
27532 neg find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_e,_var__1);
27533}
27534private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noOutgoingTransitionFromEntry(
27535 problem:LogicProblem, interpretation:PartialInterpretation,
27536 var_e)
27537{
27538 find interpretation(problem,interpretation);
27539 find mustInstanceOfEntry_class(problem,interpretation,var_e);
27540 // e is exported
27541 neg find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_e,_var__1);
27542}
27543// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries multipleTransitionFromEntry
27544private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleTransitionFromEntry(
27545 problem:LogicProblem, interpretation:PartialInterpretation,
27546 var_e, var_t1, var_t2)
27547{
27548 find interpretation(problem,interpretation);
27549 find mustInstanceOfEntry_class(problem,interpretation,var_e);
27550 find mustInstanceOfTransition_class(problem,interpretation,var_t1);
27551 find mustInstanceOfTransition_class(problem,interpretation,var_t2);
27552 // e is exported
27553 // t1 is exported
27554 // t2 is exported
27555 find mustInstanceOfEntry_class(problem,interpretation,var_e);
27556 find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,var_e,var_virtual0);
27557 find mustInstanceOfTransition_class(problem,interpretation,var_virtual0);
27558 var_virtual0 == var_t1;
27559 find mustInstanceOfEntry_class(problem,interpretation,var_e);
27560 find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,var_e,var_virtual1);
27561 find mustInstanceOfTransition_class(problem,interpretation,var_virtual1);
27562 var_virtual1 == var_t2;
27563 neg find mayEquivalent(problem, interpretation, var_t1, var_t2);
27564}
27565private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleTransitionFromEntry(
27566 problem:LogicProblem, interpretation:PartialInterpretation,
27567 var_e, var_t1, var_t2)
27568{
27569 find interpretation(problem,interpretation);
27570 find mayInstanceOfEntry_class(problem,interpretation,var_e);
27571 find mayInstanceOfTransition_class(problem,interpretation,var_t1);
27572 find mayInstanceOfTransition_class(problem,interpretation,var_t2);
27573 // e is exported
27574 // t1 is exported
27575 // t2 is exported
27576 find mayInstanceOfEntry_class(problem,interpretation,var_e);
27577 find mayInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,var_e,var_virtual0);
27578 find mayInstanceOfTransition_class(problem,interpretation,var_virtual0);
27579 find mayEquivalent(problem, interpretation, var_virtual0, var_t1);
27580 find mayInstanceOfEntry_class(problem,interpretation,var_e);
27581 find mayInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,var_e,var_virtual1);
27582 find mayInstanceOfTransition_class(problem,interpretation,var_virtual1);
27583 find mayEquivalent(problem, interpretation, var_virtual1, var_t2);
27584 var_t1 != var_t2;
27585}
27586private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleTransitionFromEntry(
27587 problem:LogicProblem, interpretation:PartialInterpretation,
27588 var_e, var_t1, var_t2)
27589{
27590 find interpretation(problem,interpretation);
27591 find mustInstanceOfEntry_class(problem,interpretation,var_e);
27592 find mustInstanceOfTransition_class(problem,interpretation,var_t1);
27593 find mustInstanceOfTransition_class(problem,interpretation,var_t2);
27594 // e is exported
27595 // t1 is exported
27596 // t2 is exported
27597 find mustInstanceOfEntry_class(problem,interpretation,var_e);
27598 find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,var_e,var_virtual0);
27599 find mustInstanceOfTransition_class(problem,interpretation,var_virtual0);
27600 var_virtual0 == var_t1;
27601 find mustInstanceOfEntry_class(problem,interpretation,var_e);
27602 find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,var_e,var_virtual1);
27603 find mustInstanceOfTransition_class(problem,interpretation,var_virtual1);
27604 var_virtual1 == var_t2;
27605 var_t1 != var_t2;
27606}
27607// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries outgoingFromExit
27608private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromExit(
27609 problem:LogicProblem, interpretation:PartialInterpretation,
27610 var_t, var_e)
27611{
27612 find interpretation(problem,interpretation);
27613 find mustInstanceOfTransition_class(problem,interpretation,var_t);
27614 find mustInstanceOfExit_class(problem,interpretation,var_e);
27615 // t is exported
27616 // e is exported
27617 find mustInstanceOfExit_class(problem,interpretation,var_e);
27618 find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,var_e,var_virtual0);
27619 find mustInstanceOfTransition_class(problem,interpretation,var_virtual0);
27620 var_virtual0 == var_t;
27621}
27622private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromExit(
27623 problem:LogicProblem, interpretation:PartialInterpretation,
27624 var_t, var_e)
27625{
27626 find interpretation(problem,interpretation);
27627 find mayInstanceOfTransition_class(problem,interpretation,var_t);
27628 find mayInstanceOfExit_class(problem,interpretation,var_e);
27629 // t is exported
27630 // e is exported
27631 find mayInstanceOfExit_class(problem,interpretation,var_e);
27632 find mayInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,var_e,var_virtual0);
27633 find mayInstanceOfTransition_class(problem,interpretation,var_virtual0);
27634 find mayEquivalent(problem, interpretation, var_virtual0, var_t);
27635}
27636private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromExit(
27637 problem:LogicProblem, interpretation:PartialInterpretation,
27638 var_t, var_e)
27639{
27640 find interpretation(problem,interpretation);
27641 find mustInstanceOfTransition_class(problem,interpretation,var_t);
27642 find mustInstanceOfExit_class(problem,interpretation,var_e);
27643 // t is exported
27644 // e is exported
27645 find mustInstanceOfExit_class(problem,interpretation,var_e);
27646 find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,var_e,var_virtual0);
27647 find mustInstanceOfTransition_class(problem,interpretation,var_virtual0);
27648 var_virtual0 == var_t;
27649}
27650// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries outgoingFromFinal
27651private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromFinal(
27652 problem:LogicProblem, interpretation:PartialInterpretation,
27653 var_t, var_f)
27654{
27655 find interpretation(problem,interpretation);
27656 find mustInstanceOfTransition_class(problem,interpretation,var_t);
27657 find mustInstanceOfFinalState_class(problem,interpretation,var_f);
27658 // t is exported
27659 // f is exported
27660 find mustInstanceOfFinalState_class(problem,interpretation,var_f);
27661 find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,var_f,var_virtual0);
27662 find mustInstanceOfTransition_class(problem,interpretation,var_virtual0);
27663 var_virtual0 == var_t;
27664}
27665private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromFinal(
27666 problem:LogicProblem, interpretation:PartialInterpretation,
27667 var_t, var_f)
27668{
27669 find interpretation(problem,interpretation);
27670 find mayInstanceOfTransition_class(problem,interpretation,var_t);
27671 find mayInstanceOfFinalState_class(problem,interpretation,var_f);
27672 // t is exported
27673 // f is exported
27674 find mayInstanceOfFinalState_class(problem,interpretation,var_f);
27675 find mayInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,var_f,var_virtual0);
27676 find mayInstanceOfTransition_class(problem,interpretation,var_virtual0);
27677 find mayEquivalent(problem, interpretation, var_virtual0, var_t);
27678}
27679private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromFinal(
27680 problem:LogicProblem, interpretation:PartialInterpretation,
27681 var_t, var_f)
27682{
27683 find interpretation(problem,interpretation);
27684 find mustInstanceOfTransition_class(problem,interpretation,var_t);
27685 find mustInstanceOfFinalState_class(problem,interpretation,var_f);
27686 // t is exported
27687 // f is exported
27688 find mustInstanceOfFinalState_class(problem,interpretation,var_f);
27689 find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,var_f,var_virtual0);
27690 find mustInstanceOfTransition_class(problem,interpretation,var_virtual0);
27691 var_virtual0 == var_t;
27692}
27693// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries noStateInRegion
27694private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noStateInRegion(
27695 problem:LogicProblem, interpretation:PartialInterpretation,
27696 var_region)
27697{
27698 find interpretation(problem,interpretation);
27699 find mustInstanceOfRegion_class(problem,interpretation,var_region);
27700 // region is exported
27701 neg find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_StateInRegion(problem,interpretation,var_region,_var__0);
27702}
27703private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noStateInRegion(
27704 problem:LogicProblem, interpretation:PartialInterpretation,
27705 var_region)
27706{
27707 find interpretation(problem,interpretation);
27708 find mayInstanceOfRegion_class(problem,interpretation,var_region);
27709 // region is exported
27710 neg find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_StateInRegion(problem,interpretation,var_region,_var__0);
27711}
27712private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noStateInRegion(
27713 problem:LogicProblem, interpretation:PartialInterpretation,
27714 var_region)
27715{
27716 find interpretation(problem,interpretation);
27717 find mustInstanceOfRegion_class(problem,interpretation,var_region);
27718 // region is exported
27719 neg find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_StateInRegion(problem,interpretation,var_region,_var__0);
27720}
27721// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries StateInRegion
27722private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_StateInRegion(
27723 problem:LogicProblem, interpretation:PartialInterpretation,
27724 var_region, var_state)
27725{
27726 find interpretation(problem,interpretation);
27727 find mustInstanceOfRegion_class(problem,interpretation,var_region);
27728 find mustInstanceOfState_class(problem,interpretation,var_state);
27729 // region is exported
27730 // state is exported
27731 find mustInstanceOfRegion_class(problem,interpretation,var_region);
27732 find mustInRelationvertices_reference_Region(problem,interpretation,var_region,var_virtual0);
27733 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
27734 var_virtual0 == var_state;
27735}
27736private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_StateInRegion(
27737 problem:LogicProblem, interpretation:PartialInterpretation,
27738 var_region, var_state)
27739{
27740 find interpretation(problem,interpretation);
27741 find mayInstanceOfRegion_class(problem,interpretation,var_region);
27742 find mayInstanceOfState_class(problem,interpretation,var_state);
27743 // region is exported
27744 // state is exported
27745 find mayInstanceOfRegion_class(problem,interpretation,var_region);
27746 find mayInRelationvertices_reference_Region(problem,interpretation,var_region,var_virtual0);
27747 find mayInstanceOfVertex_class(problem,interpretation,var_virtual0);
27748 find mayEquivalent(problem, interpretation, var_virtual0, var_state);
27749}
27750private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_StateInRegion(
27751 problem:LogicProblem, interpretation:PartialInterpretation,
27752 var_region, var_state)
27753{
27754 find interpretation(problem,interpretation);
27755 find mustInstanceOfRegion_class(problem,interpretation,var_region);
27756 find mustInstanceOfState_class(problem,interpretation,var_state);
27757 // region is exported
27758 // state is exported
27759 find mustInstanceOfRegion_class(problem,interpretation,var_region);
27760 find mustInRelationvertices_reference_Region(problem,interpretation,var_region,var_virtual0);
27761 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
27762 var_virtual0 == var_state;
27763}
27764// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries choiceHasNoOutgoing
27765private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoOutgoing(
27766 problem:LogicProblem, interpretation:PartialInterpretation,
27767 var_c)
27768{
27769 find interpretation(problem,interpretation);
27770 find mustInstanceOfChoice_class(problem,interpretation,var_c);
27771 // c is exported
27772 neg find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_c,_var__1);
27773}
27774private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoOutgoing(
27775 problem:LogicProblem, interpretation:PartialInterpretation,
27776 var_c)
27777{
27778 find interpretation(problem,interpretation);
27779 find mayInstanceOfChoice_class(problem,interpretation,var_c);
27780 // c is exported
27781 neg find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_c,_var__1);
27782}
27783private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoOutgoing(
27784 problem:LogicProblem, interpretation:PartialInterpretation,
27785 var_c)
27786{
27787 find interpretation(problem,interpretation);
27788 find mustInstanceOfChoice_class(problem,interpretation,var_c);
27789 // c is exported
27790 neg find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_c,_var__1);
27791}
27792// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries choiceHasNoIncoming
27793private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoIncoming(
27794 problem:LogicProblem, interpretation:PartialInterpretation,
27795 var_c)
27796{
27797 find interpretation(problem,interpretation);
27798 find mustInstanceOfChoice_class(problem,interpretation,var_c);
27799 // c is exported
27800 neg find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,_var__1,var_c);
27801}
27802private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoIncoming(
27803 problem:LogicProblem, interpretation:PartialInterpretation,
27804 var_c)
27805{
27806 find interpretation(problem,interpretation);
27807 find mayInstanceOfChoice_class(problem,interpretation,var_c);
27808 // c is exported
27809 neg find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,_var__1,var_c);
27810}
27811private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoIncoming(
27812 problem:LogicProblem, interpretation:PartialInterpretation,
27813 var_c)
27814{
27815 find interpretation(problem,interpretation);
27816 find mustInstanceOfChoice_class(problem,interpretation,var_c);
27817 // c is exported
27818 neg find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,_var__1,var_c);
27819}
27820// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries synchHasNoOutgoing
27821private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoOutgoing(
27822 problem:LogicProblem, interpretation:PartialInterpretation,
27823 var_s)
27824{
27825 find interpretation(problem,interpretation);
27826 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
27827 // s is exported
27828 neg find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_s,_var__1);
27829}
27830private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoOutgoing(
27831 problem:LogicProblem, interpretation:PartialInterpretation,
27832 var_s)
27833{
27834 find interpretation(problem,interpretation);
27835 find mayInstanceOfSynchronization_class(problem,interpretation,var_s);
27836 // s is exported
27837 neg find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_s,_var__1);
27838}
27839private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoOutgoing(
27840 problem:LogicProblem, interpretation:PartialInterpretation,
27841 var_s)
27842{
27843 find interpretation(problem,interpretation);
27844 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
27845 // s is exported
27846 neg find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_s,_var__1);
27847}
27848// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries synchHasNoIncoming
27849private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoIncoming(
27850 problem:LogicProblem, interpretation:PartialInterpretation,
27851 var_s)
27852{
27853 find interpretation(problem,interpretation);
27854 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
27855 // s is exported
27856 neg find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,_var__1,var_s);
27857}
27858private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoIncoming(
27859 problem:LogicProblem, interpretation:PartialInterpretation,
27860 var_s)
27861{
27862 find interpretation(problem,interpretation);
27863 find mayInstanceOfSynchronization_class(problem,interpretation,var_s);
27864 // s is exported
27865 neg find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,_var__1,var_s);
27866}
27867private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoIncoming(
27868 problem:LogicProblem, interpretation:PartialInterpretation,
27869 var_s)
27870{
27871 find interpretation(problem,interpretation);
27872 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
27873 // s is exported
27874 neg find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,_var__1,var_s);
27875}
27876// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries SynchronizedIncomingInSameRegion
27877private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedIncomingInSameRegion(
27878 problem:LogicProblem, interpretation:PartialInterpretation,
27879 var_s, var_v1, var_v2)
27880{
27881 find interpretation(problem,interpretation);
27882 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
27883 find mustInstanceOfVertex_class(problem,interpretation,var_v1);
27884 find mustInstanceOfVertex_class(problem,interpretation,var_v2);
27885 // s is exported
27886 // v1 is exported
27887 // v2 is exported
27888 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t1,var_v1,var_s);
27889 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t2,var_v2,var_s);
27890 neg find mayEquivalent(problem, interpretation, var_t1, var_t2);
27891 find mustInstanceOfRegion_class(problem,interpretation,var_r);
27892 find mustInRelationvertices_reference_Region(problem,interpretation,var_r,var_virtual0);
27893 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
27894 var_virtual0 == var_v1;
27895 find mustInstanceOfRegion_class(problem,interpretation,var_r);
27896 find mustInRelationvertices_reference_Region(problem,interpretation,var_r,var_virtual1);
27897 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
27898 var_virtual1 == var_v2;
27899}or{
27900 find interpretation(problem,interpretation);
27901 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
27902 find mustInstanceOfVertex_class(problem,interpretation,var_v1);
27903 find mustInstanceOfVertex_class(problem,interpretation,var_v2);
27904 // s is exported
27905 // v1 is exported
27906 // v2 is exported
27907 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t1,var_s,var_v1);
27908 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t2,var_s,var_v2);
27909 neg find mayEquivalent(problem, interpretation, var_t1, var_t2);
27910 find mustInstanceOfRegion_class(problem,interpretation,var_r);
27911 find mustInRelationvertices_reference_Region(problem,interpretation,var_r,var_virtual0);
27912 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
27913 var_virtual0 == var_v1;
27914 find mustInstanceOfRegion_class(problem,interpretation,var_r);
27915 find mustInRelationvertices_reference_Region(problem,interpretation,var_r,var_virtual1);
27916 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
27917 var_virtual1 == var_v2;
27918}
27919private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedIncomingInSameRegion(
27920 problem:LogicProblem, interpretation:PartialInterpretation,
27921 var_s, var_v1, var_v2)
27922{
27923 find interpretation(problem,interpretation);
27924 find mayInstanceOfSynchronization_class(problem,interpretation,var_s);
27925 find mayInstanceOfVertex_class(problem,interpretation,var_v1);
27926 find mayInstanceOfVertex_class(problem,interpretation,var_v2);
27927 // s is exported
27928 // v1 is exported
27929 // v2 is exported
27930 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t1,var_v1,var_s);
27931 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t2,var_v2,var_s);
27932 var_t1 != var_t2;
27933 find mayInstanceOfRegion_class(problem,interpretation,var_r);
27934 find mayInRelationvertices_reference_Region(problem,interpretation,var_r,var_virtual0);
27935 find mayInstanceOfVertex_class(problem,interpretation,var_virtual0);
27936 find mayEquivalent(problem, interpretation, var_virtual0, var_v1);
27937 find mayInstanceOfRegion_class(problem,interpretation,var_r);
27938 find mayInRelationvertices_reference_Region(problem,interpretation,var_r,var_virtual1);
27939 find mayInstanceOfVertex_class(problem,interpretation,var_virtual1);
27940 find mayEquivalent(problem, interpretation, var_virtual1, var_v2);
27941}or{
27942 find interpretation(problem,interpretation);
27943 find mayInstanceOfSynchronization_class(problem,interpretation,var_s);
27944 find mayInstanceOfVertex_class(problem,interpretation,var_v1);
27945 find mayInstanceOfVertex_class(problem,interpretation,var_v2);
27946 // s is exported
27947 // v1 is exported
27948 // v2 is exported
27949 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t1,var_s,var_v1);
27950 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t2,var_s,var_v2);
27951 var_t1 != var_t2;
27952 find mayInstanceOfRegion_class(problem,interpretation,var_r);
27953 find mayInRelationvertices_reference_Region(problem,interpretation,var_r,var_virtual0);
27954 find mayInstanceOfVertex_class(problem,interpretation,var_virtual0);
27955 find mayEquivalent(problem, interpretation, var_virtual0, var_v1);
27956 find mayInstanceOfRegion_class(problem,interpretation,var_r);
27957 find mayInRelationvertices_reference_Region(problem,interpretation,var_r,var_virtual1);
27958 find mayInstanceOfVertex_class(problem,interpretation,var_virtual1);
27959 find mayEquivalent(problem, interpretation, var_virtual1, var_v2);
27960}
27961private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedIncomingInSameRegion(
27962 problem:LogicProblem, interpretation:PartialInterpretation,
27963 var_s, var_v1, var_v2)
27964{
27965 find interpretation(problem,interpretation);
27966 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
27967 find mustInstanceOfVertex_class(problem,interpretation,var_v1);
27968 find mustInstanceOfVertex_class(problem,interpretation,var_v2);
27969 // s is exported
27970 // v1 is exported
27971 // v2 is exported
27972 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t1,var_v1,var_s);
27973 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t2,var_v2,var_s);
27974 var_t1 != var_t2;
27975 find mustInstanceOfRegion_class(problem,interpretation,var_r);
27976 find mustInRelationvertices_reference_Region(problem,interpretation,var_r,var_virtual0);
27977 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
27978 var_virtual0 == var_v1;
27979 find mustInstanceOfRegion_class(problem,interpretation,var_r);
27980 find mustInRelationvertices_reference_Region(problem,interpretation,var_r,var_virtual1);
27981 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
27982 var_virtual1 == var_v2;
27983}or{
27984 find interpretation(problem,interpretation);
27985 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
27986 find mustInstanceOfVertex_class(problem,interpretation,var_v1);
27987 find mustInstanceOfVertex_class(problem,interpretation,var_v2);
27988 // s is exported
27989 // v1 is exported
27990 // v2 is exported
27991 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t1,var_s,var_v1);
27992 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,var_t2,var_s,var_v2);
27993 var_t1 != var_t2;
27994 find mustInstanceOfRegion_class(problem,interpretation,var_r);
27995 find mustInRelationvertices_reference_Region(problem,interpretation,var_r,var_virtual0);
27996 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
27997 var_virtual0 == var_v1;
27998 find mustInstanceOfRegion_class(problem,interpretation,var_r);
27999 find mustInRelationvertices_reference_Region(problem,interpretation,var_r,var_virtual1);
28000 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
28001 var_virtual1 == var_v2;
28002}
28003// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries notSynchronizingStates
28004private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_notSynchronizingStates(
28005 problem:LogicProblem, interpretation:PartialInterpretation,
28006 var_s)
28007{
28008 find interpretation(problem,interpretation);
28009 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28010 // s is exported
28011 neg find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleOutgoingTrainsition(problem,interpretation,var_s);
28012 neg find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleIncomingTrainsition(problem,interpretation,var_s);
28013}
28014private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_notSynchronizingStates(
28015 problem:LogicProblem, interpretation:PartialInterpretation,
28016 var_s)
28017{
28018 find interpretation(problem,interpretation);
28019 find mayInstanceOfSynchronization_class(problem,interpretation,var_s);
28020 // s is exported
28021 neg find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleOutgoingTrainsition(problem,interpretation,var_s);
28022 neg find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleIncomingTrainsition(problem,interpretation,var_s);
28023}
28024private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_notSynchronizingStates(
28025 problem:LogicProblem, interpretation:PartialInterpretation,
28026 var_s)
28027{
28028 find interpretation(problem,interpretation);
28029 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28030 // s is exported
28031 neg find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleOutgoingTrainsition(problem,interpretation,var_s);
28032 neg find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleIncomingTrainsition(problem,interpretation,var_s);
28033}
28034// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries hasMultipleOutgoingTrainsition
28035private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleOutgoingTrainsition(
28036 problem:LogicProblem, interpretation:PartialInterpretation,
28037 var_v)
28038{
28039 find interpretation(problem,interpretation);
28040 find mustInstanceOfSynchronization_class(problem,interpretation,var_v);
28041 // v is exported
28042 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_v,var_trg1);
28043 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__1,var_v,var_trg2);
28044 neg find mayEquivalent(problem, interpretation, var_trg1, var_trg2);
28045}
28046private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleOutgoingTrainsition(
28047 problem:LogicProblem, interpretation:PartialInterpretation,
28048 var_v)
28049{
28050 find interpretation(problem,interpretation);
28051 find mayInstanceOfSynchronization_class(problem,interpretation,var_v);
28052 // v is exported
28053 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_v,var_trg1);
28054 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__1,var_v,var_trg2);
28055 var_trg1 != var_trg2;
28056}
28057private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleOutgoingTrainsition(
28058 problem:LogicProblem, interpretation:PartialInterpretation,
28059 var_v)
28060{
28061 find interpretation(problem,interpretation);
28062 find mustInstanceOfSynchronization_class(problem,interpretation,var_v);
28063 // v is exported
28064 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_v,var_trg1);
28065 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__1,var_v,var_trg2);
28066 var_trg1 != var_trg2;
28067}
28068// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries hasMultipleIncomingTrainsition
28069private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleIncomingTrainsition(
28070 problem:LogicProblem, interpretation:PartialInterpretation,
28071 var_v)
28072{
28073 find interpretation(problem,interpretation);
28074 find mustInstanceOfSynchronization_class(problem,interpretation,var_v);
28075 // v is exported
28076 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_src1,var_v);
28077 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__1,var_src2,var_v);
28078 neg find mayEquivalent(problem, interpretation, var_src1, var_src2);
28079}
28080private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleIncomingTrainsition(
28081 problem:LogicProblem, interpretation:PartialInterpretation,
28082 var_v)
28083{
28084 find interpretation(problem,interpretation);
28085 find mayInstanceOfSynchronization_class(problem,interpretation,var_v);
28086 // v is exported
28087 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_src1,var_v);
28088 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__1,var_src2,var_v);
28089 var_src1 != var_src2;
28090}
28091private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleIncomingTrainsition(
28092 problem:LogicProblem, interpretation:PartialInterpretation,
28093 var_v)
28094{
28095 find interpretation(problem,interpretation);
28096 find mustInstanceOfSynchronization_class(problem,interpretation,var_v);
28097 // v is exported
28098 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_src1,var_v);
28099 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__1,var_src2,var_v);
28100 var_src1 != var_src2;
28101}
28102// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries SynchronizedRegionsAreNotSiblings
28103private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionsAreNotSiblings(
28104 problem:LogicProblem, interpretation:PartialInterpretation,
28105 var_s, var_v1, var_v2)
28106{
28107 find interpretation(problem,interpretation);
28108 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28109 find mustInstanceOfVertex_class(problem,interpretation,var_v1);
28110 find mustInstanceOfVertex_class(problem,interpretation,var_v2);
28111 // s is exported
28112 // v1 is exported
28113 // v2 is exported
28114 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_v1,var_s);
28115 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__1,var_v2,var_s);
28116 find mustInstanceOfCompositeElement_class(problem,interpretation,var_r1);
28117 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_r1,var_virtual0);
28118 find mustInstanceOfRegion_class(problem,interpretation,var_virtual0);
28119 find mustInRelationvertices_reference_Region(problem,interpretation,var_virtual0,var_virtual1);
28120 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
28121 var_virtual1 == var_v1;
28122 find mustInstanceOfCompositeElement_class(problem,interpretation,var_r2);
28123 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_r2,var_virtual2);
28124 find mustInstanceOfRegion_class(problem,interpretation,var_virtual2);
28125 find mustInRelationvertices_reference_Region(problem,interpretation,var_virtual2,var_virtual3);
28126 find mustInstanceOfVertex_class(problem,interpretation,var_virtual3);
28127 var_virtual3 == var_v2;
28128 neg find mayEquivalent(problem, interpretation, var_r1, var_r2);
28129}or{
28130 find interpretation(problem,interpretation);
28131 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28132 find mustInstanceOfVertex_class(problem,interpretation,var_v1);
28133 find mustInstanceOfVertex_class(problem,interpretation,var_v2);
28134 // s is exported
28135 // v1 is exported
28136 // v2 is exported
28137 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_s,var_v1);
28138 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__1,var_s,var_v2);
28139 find mustInstanceOfCompositeElement_class(problem,interpretation,var_r1);
28140 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_r1,var_virtual0);
28141 find mustInstanceOfRegion_class(problem,interpretation,var_virtual0);
28142 find mustInRelationvertices_reference_Region(problem,interpretation,var_virtual0,var_virtual1);
28143 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
28144 var_virtual1 == var_v1;
28145 find mustInstanceOfCompositeElement_class(problem,interpretation,var_r2);
28146 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_r2,var_virtual2);
28147 find mustInstanceOfRegion_class(problem,interpretation,var_virtual2);
28148 find mustInRelationvertices_reference_Region(problem,interpretation,var_virtual2,var_virtual3);
28149 find mustInstanceOfVertex_class(problem,interpretation,var_virtual3);
28150 var_virtual3 == var_v2;
28151 neg find mayEquivalent(problem, interpretation, var_r1, var_r2);
28152}
28153private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionsAreNotSiblings(
28154 problem:LogicProblem, interpretation:PartialInterpretation,
28155 var_s, var_v1, var_v2)
28156{
28157 find interpretation(problem,interpretation);
28158 find mayInstanceOfSynchronization_class(problem,interpretation,var_s);
28159 find mayInstanceOfVertex_class(problem,interpretation,var_v1);
28160 find mayInstanceOfVertex_class(problem,interpretation,var_v2);
28161 // s is exported
28162 // v1 is exported
28163 // v2 is exported
28164 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_v1,var_s);
28165 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__1,var_v2,var_s);
28166 find mayInstanceOfCompositeElement_class(problem,interpretation,var_r1);
28167 find mayInRelationregions_reference_CompositeElement(problem,interpretation,var_r1,var_virtual0);
28168 find mayInstanceOfRegion_class(problem,interpretation,var_virtual0);
28169 find mayInRelationvertices_reference_Region(problem,interpretation,var_virtual0,var_virtual1);
28170 find mayInstanceOfVertex_class(problem,interpretation,var_virtual1);
28171 find mayEquivalent(problem, interpretation, var_virtual1, var_v1);
28172 find mayInstanceOfCompositeElement_class(problem,interpretation,var_r2);
28173 find mayInRelationregions_reference_CompositeElement(problem,interpretation,var_r2,var_virtual2);
28174 find mayInstanceOfRegion_class(problem,interpretation,var_virtual2);
28175 find mayInRelationvertices_reference_Region(problem,interpretation,var_virtual2,var_virtual3);
28176 find mayInstanceOfVertex_class(problem,interpretation,var_virtual3);
28177 find mayEquivalent(problem, interpretation, var_virtual3, var_v2);
28178 var_r1 != var_r2;
28179}or{
28180 find interpretation(problem,interpretation);
28181 find mayInstanceOfSynchronization_class(problem,interpretation,var_s);
28182 find mayInstanceOfVertex_class(problem,interpretation,var_v1);
28183 find mayInstanceOfVertex_class(problem,interpretation,var_v2);
28184 // s is exported
28185 // v1 is exported
28186 // v2 is exported
28187 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_s,var_v1);
28188 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__1,var_s,var_v2);
28189 find mayInstanceOfCompositeElement_class(problem,interpretation,var_r1);
28190 find mayInRelationregions_reference_CompositeElement(problem,interpretation,var_r1,var_virtual0);
28191 find mayInstanceOfRegion_class(problem,interpretation,var_virtual0);
28192 find mayInRelationvertices_reference_Region(problem,interpretation,var_virtual0,var_virtual1);
28193 find mayInstanceOfVertex_class(problem,interpretation,var_virtual1);
28194 find mayEquivalent(problem, interpretation, var_virtual1, var_v1);
28195 find mayInstanceOfCompositeElement_class(problem,interpretation,var_r2);
28196 find mayInRelationregions_reference_CompositeElement(problem,interpretation,var_r2,var_virtual2);
28197 find mayInstanceOfRegion_class(problem,interpretation,var_virtual2);
28198 find mayInRelationvertices_reference_Region(problem,interpretation,var_virtual2,var_virtual3);
28199 find mayInstanceOfVertex_class(problem,interpretation,var_virtual3);
28200 find mayEquivalent(problem, interpretation, var_virtual3, var_v2);
28201 var_r1 != var_r2;
28202}
28203private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionsAreNotSiblings(
28204 problem:LogicProblem, interpretation:PartialInterpretation,
28205 var_s, var_v1, var_v2)
28206{
28207 find interpretation(problem,interpretation);
28208 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28209 find mustInstanceOfVertex_class(problem,interpretation,var_v1);
28210 find mustInstanceOfVertex_class(problem,interpretation,var_v2);
28211 // s is exported
28212 // v1 is exported
28213 // v2 is exported
28214 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_v1,var_s);
28215 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__1,var_v2,var_s);
28216 find mustInstanceOfCompositeElement_class(problem,interpretation,var_r1);
28217 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_r1,var_virtual0);
28218 find mustInstanceOfRegion_class(problem,interpretation,var_virtual0);
28219 find mustInRelationvertices_reference_Region(problem,interpretation,var_virtual0,var_virtual1);
28220 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
28221 var_virtual1 == var_v1;
28222 find mustInstanceOfCompositeElement_class(problem,interpretation,var_r2);
28223 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_r2,var_virtual2);
28224 find mustInstanceOfRegion_class(problem,interpretation,var_virtual2);
28225 find mustInRelationvertices_reference_Region(problem,interpretation,var_virtual2,var_virtual3);
28226 find mustInstanceOfVertex_class(problem,interpretation,var_virtual3);
28227 var_virtual3 == var_v2;
28228 var_r1 != var_r2;
28229}or{
28230 find interpretation(problem,interpretation);
28231 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28232 find mustInstanceOfVertex_class(problem,interpretation,var_v1);
28233 find mustInstanceOfVertex_class(problem,interpretation,var_v2);
28234 // s is exported
28235 // v1 is exported
28236 // v2 is exported
28237 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_s,var_v1);
28238 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__1,var_s,var_v2);
28239 find mustInstanceOfCompositeElement_class(problem,interpretation,var_r1);
28240 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_r1,var_virtual0);
28241 find mustInstanceOfRegion_class(problem,interpretation,var_virtual0);
28242 find mustInRelationvertices_reference_Region(problem,interpretation,var_virtual0,var_virtual1);
28243 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
28244 var_virtual1 == var_v1;
28245 find mustInstanceOfCompositeElement_class(problem,interpretation,var_r2);
28246 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_r2,var_virtual2);
28247 find mustInstanceOfRegion_class(problem,interpretation,var_virtual2);
28248 find mustInRelationvertices_reference_Region(problem,interpretation,var_virtual2,var_virtual3);
28249 find mustInstanceOfVertex_class(problem,interpretation,var_virtual3);
28250 var_virtual3 == var_v2;
28251 var_r1 != var_r2;
28252}
28253// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries child
28254private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_child(
28255 problem:LogicProblem, interpretation:PartialInterpretation,
28256 var_parent, var_child)
28257{
28258 find interpretation(problem,interpretation);
28259 find mustInstanceOfCompositeElement_class(problem,interpretation,var_parent);
28260 find mustInstanceOfVertex_class(problem,interpretation,var_child);
28261 // parent is exported
28262 // child is exported
28263 find mustInstanceOfCompositeElement_class(problem,interpretation,var_parent);
28264 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_parent,var_virtual0);
28265 find mustInstanceOfRegion_class(problem,interpretation,var_virtual0);
28266 find mustInRelationvertices_reference_Region(problem,interpretation,var_virtual0,var_virtual1);
28267 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
28268 var_virtual1 == var_child;
28269}
28270private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_child(
28271 problem:LogicProblem, interpretation:PartialInterpretation,
28272 var_parent, var_child)
28273{
28274 find interpretation(problem,interpretation);
28275 find mayInstanceOfCompositeElement_class(problem,interpretation,var_parent);
28276 find mayInstanceOfVertex_class(problem,interpretation,var_child);
28277 // parent is exported
28278 // child is exported
28279 find mayInstanceOfCompositeElement_class(problem,interpretation,var_parent);
28280 find mayInRelationregions_reference_CompositeElement(problem,interpretation,var_parent,var_virtual0);
28281 find mayInstanceOfRegion_class(problem,interpretation,var_virtual0);
28282 find mayInRelationvertices_reference_Region(problem,interpretation,var_virtual0,var_virtual1);
28283 find mayInstanceOfVertex_class(problem,interpretation,var_virtual1);
28284 find mayEquivalent(problem, interpretation, var_virtual1, var_child);
28285}
28286private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_child(
28287 problem:LogicProblem, interpretation:PartialInterpretation,
28288 var_parent, var_child)
28289{
28290 find interpretation(problem,interpretation);
28291 find mustInstanceOfCompositeElement_class(problem,interpretation,var_parent);
28292 find mustInstanceOfVertex_class(problem,interpretation,var_child);
28293 // parent is exported
28294 // child is exported
28295 find mustInstanceOfCompositeElement_class(problem,interpretation,var_parent);
28296 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_parent,var_virtual0);
28297 find mustInstanceOfRegion_class(problem,interpretation,var_virtual0);
28298 find mustInRelationvertices_reference_Region(problem,interpretation,var_virtual0,var_virtual1);
28299 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
28300 var_virtual1 == var_child;
28301}
28302// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries SynchronizedRegionDoesNotHaveMultipleRegions
28303private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionDoesNotHaveMultipleRegions(
28304 problem:LogicProblem, interpretation:PartialInterpretation,
28305 var_s, var_v)
28306{
28307 find interpretation(problem,interpretation);
28308 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28309 find mustInstanceOfVertex_class(problem,interpretation,var_v);
28310 // s is exported
28311 // v is exported
28312 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_v,var_s);
28313 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_child(problem,interpretation,var_c,var_v);
28314 neg find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleRegions(problem,interpretation,var_c);
28315}or{
28316 find interpretation(problem,interpretation);
28317 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28318 find mustInstanceOfVertex_class(problem,interpretation,var_v);
28319 // s is exported
28320 // v is exported
28321 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_s,var_v);
28322 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_child(problem,interpretation,var_c,var_v);
28323 neg find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleRegions(problem,interpretation,var_c);
28324}
28325private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionDoesNotHaveMultipleRegions(
28326 problem:LogicProblem, interpretation:PartialInterpretation,
28327 var_s, var_v)
28328{
28329 find interpretation(problem,interpretation);
28330 find mayInstanceOfSynchronization_class(problem,interpretation,var_s);
28331 find mayInstanceOfVertex_class(problem,interpretation,var_v);
28332 // s is exported
28333 // v is exported
28334 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_v,var_s);
28335 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_child(problem,interpretation,var_c,var_v);
28336 neg find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleRegions(problem,interpretation,var_c);
28337}or{
28338 find interpretation(problem,interpretation);
28339 find mayInstanceOfSynchronization_class(problem,interpretation,var_s);
28340 find mayInstanceOfVertex_class(problem,interpretation,var_v);
28341 // s is exported
28342 // v is exported
28343 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_s,var_v);
28344 find mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_child(problem,interpretation,var_c,var_v);
28345 neg find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleRegions(problem,interpretation,var_c);
28346}
28347private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionDoesNotHaveMultipleRegions(
28348 problem:LogicProblem, interpretation:PartialInterpretation,
28349 var_s, var_v)
28350{
28351 find interpretation(problem,interpretation);
28352 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28353 find mustInstanceOfVertex_class(problem,interpretation,var_v);
28354 // s is exported
28355 // v is exported
28356 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_v,var_s);
28357 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_child(problem,interpretation,var_c,var_v);
28358 neg find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleRegions(problem,interpretation,var_c);
28359}or{
28360 find interpretation(problem,interpretation);
28361 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28362 find mustInstanceOfVertex_class(problem,interpretation,var_v);
28363 // s is exported
28364 // v is exported
28365 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_transition(problem,interpretation,_var__0,var_s,var_v);
28366 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_child(problem,interpretation,var_c,var_v);
28367 neg find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleRegions(problem,interpretation,var_c);
28368}
28369// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries hasMultipleRegions
28370private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleRegions(
28371 problem:LogicProblem, interpretation:PartialInterpretation,
28372 var_composite)
28373{
28374 find interpretation(problem,interpretation);
28375 find mustInstanceOfCompositeElement_class(problem,interpretation,var_composite);
28376 // composite is exported
28377 find mustInstanceOfCompositeElement_class(problem,interpretation,var_composite);
28378 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_composite,var_virtual0);
28379 find mustInstanceOfRegion_class(problem,interpretation,var_virtual0);
28380 var_virtual0 == var_region1;
28381 find mustInstanceOfCompositeElement_class(problem,interpretation,var_composite);
28382 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_composite,var_virtual1);
28383 find mustInstanceOfRegion_class(problem,interpretation,var_virtual1);
28384 var_virtual1 == var_region2;
28385 neg find mayEquivalent(problem, interpretation, var_region1, var_region2);
28386}
28387private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleRegions(
28388 problem:LogicProblem, interpretation:PartialInterpretation,
28389 var_composite)
28390{
28391 find interpretation(problem,interpretation);
28392 find mayInstanceOfCompositeElement_class(problem,interpretation,var_composite);
28393 // composite is exported
28394 find mayInstanceOfCompositeElement_class(problem,interpretation,var_composite);
28395 find mayInRelationregions_reference_CompositeElement(problem,interpretation,var_composite,var_virtual0);
28396 find mayInstanceOfRegion_class(problem,interpretation,var_virtual0);
28397 find mayEquivalent(problem, interpretation, var_virtual0, var_region1);
28398 find mayInstanceOfCompositeElement_class(problem,interpretation,var_composite);
28399 find mayInRelationregions_reference_CompositeElement(problem,interpretation,var_composite,var_virtual1);
28400 find mayInstanceOfRegion_class(problem,interpretation,var_virtual1);
28401 find mayEquivalent(problem, interpretation, var_virtual1, var_region2);
28402 var_region1 != var_region2;
28403}
28404private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_hasMultipleRegions(
28405 problem:LogicProblem, interpretation:PartialInterpretation,
28406 var_composite)
28407{
28408 find interpretation(problem,interpretation);
28409 find mustInstanceOfCompositeElement_class(problem,interpretation,var_composite);
28410 // composite is exported
28411 find mustInstanceOfCompositeElement_class(problem,interpretation,var_composite);
28412 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_composite,var_virtual0);
28413 find mustInstanceOfRegion_class(problem,interpretation,var_virtual0);
28414 var_virtual0 == var_region1;
28415 find mustInstanceOfCompositeElement_class(problem,interpretation,var_composite);
28416 find mustInRelationregions_reference_CompositeElement(problem,interpretation,var_composite,var_virtual1);
28417 find mustInstanceOfRegion_class(problem,interpretation,var_virtual1);
28418 var_virtual1 == var_region2;
28419 var_region1 != var_region2;
28420}
28421// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries synchThree
28422private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchThree(
28423 problem:LogicProblem, interpretation:PartialInterpretation,
28424 var_s)
28425{
28426 find interpretation(problem,interpretation);
28427 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28428 // s is exported
28429 find mustInstanceOfTransition_class(problem,interpretation,var_t1);
28430 find mustInRelationtarget_reference_Transition(problem,interpretation,var_t1,var_virtual0);
28431 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
28432 var_virtual0 == var_s;
28433 find mustInstanceOfTransition_class(problem,interpretation,var_t2);
28434 find mustInRelationtarget_reference_Transition(problem,interpretation,var_t2,var_virtual1);
28435 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
28436 var_virtual1 == var_s;
28437 find mustInstanceOfTransition_class(problem,interpretation,var_t3);
28438 find mustInRelationtarget_reference_Transition(problem,interpretation,var_t3,var_virtual2);
28439 find mustInstanceOfVertex_class(problem,interpretation,var_virtual2);
28440 var_virtual2 == var_s;
28441 neg find mayEquivalent(problem, interpretation, var_t1, var_t2);
28442 neg find mayEquivalent(problem, interpretation, var_t2, var_t3);
28443 neg find mayEquivalent(problem, interpretation, var_t1, var_t3);
28444}or{
28445 find interpretation(problem,interpretation);
28446 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28447 // s is exported
28448 find mustInstanceOfTransition_class(problem,interpretation,var_t1);
28449 find mustInRelationsource_reference_Transition(problem,interpretation,var_t1,var_virtual0);
28450 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
28451 var_virtual0 == var_s;
28452 find mustInstanceOfTransition_class(problem,interpretation,var_t2);
28453 find mustInRelationsource_reference_Transition(problem,interpretation,var_t2,var_virtual1);
28454 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
28455 var_virtual1 == var_s;
28456 find mustInstanceOfTransition_class(problem,interpretation,var_t3);
28457 find mustInRelationsource_reference_Transition(problem,interpretation,var_t3,var_virtual2);
28458 find mustInstanceOfVertex_class(problem,interpretation,var_virtual2);
28459 var_virtual2 == var_s;
28460 neg find mayEquivalent(problem, interpretation, var_t1, var_t2);
28461 neg find mayEquivalent(problem, interpretation, var_t2, var_t3);
28462 neg find mayEquivalent(problem, interpretation, var_t1, var_t3);
28463}
28464private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchThree(
28465 problem:LogicProblem, interpretation:PartialInterpretation,
28466 var_s)
28467{
28468 find interpretation(problem,interpretation);
28469 find mayInstanceOfSynchronization_class(problem,interpretation,var_s);
28470 // s is exported
28471 find mayInstanceOfTransition_class(problem,interpretation,var_t1);
28472 find mayInRelationtarget_reference_Transition(problem,interpretation,var_t1,var_virtual0);
28473 find mayInstanceOfVertex_class(problem,interpretation,var_virtual0);
28474 find mayEquivalent(problem, interpretation, var_virtual0, var_s);
28475 find mayInstanceOfTransition_class(problem,interpretation,var_t2);
28476 find mayInRelationtarget_reference_Transition(problem,interpretation,var_t2,var_virtual1);
28477 find mayInstanceOfVertex_class(problem,interpretation,var_virtual1);
28478 find mayEquivalent(problem, interpretation, var_virtual1, var_s);
28479 find mayInstanceOfTransition_class(problem,interpretation,var_t3);
28480 find mayInRelationtarget_reference_Transition(problem,interpretation,var_t3,var_virtual2);
28481 find mayInstanceOfVertex_class(problem,interpretation,var_virtual2);
28482 find mayEquivalent(problem, interpretation, var_virtual2, var_s);
28483 var_t1 != var_t2;
28484 var_t2 != var_t3;
28485 var_t1 != var_t3;
28486}or{
28487 find interpretation(problem,interpretation);
28488 find mayInstanceOfSynchronization_class(problem,interpretation,var_s);
28489 // s is exported
28490 find mayInstanceOfTransition_class(problem,interpretation,var_t1);
28491 find mayInRelationsource_reference_Transition(problem,interpretation,var_t1,var_virtual0);
28492 find mayInstanceOfVertex_class(problem,interpretation,var_virtual0);
28493 find mayEquivalent(problem, interpretation, var_virtual0, var_s);
28494 find mayInstanceOfTransition_class(problem,interpretation,var_t2);
28495 find mayInRelationsource_reference_Transition(problem,interpretation,var_t2,var_virtual1);
28496 find mayInstanceOfVertex_class(problem,interpretation,var_virtual1);
28497 find mayEquivalent(problem, interpretation, var_virtual1, var_s);
28498 find mayInstanceOfTransition_class(problem,interpretation,var_t3);
28499 find mayInRelationsource_reference_Transition(problem,interpretation,var_t3,var_virtual2);
28500 find mayInstanceOfVertex_class(problem,interpretation,var_virtual2);
28501 find mayEquivalent(problem, interpretation, var_virtual2, var_s);
28502 var_t1 != var_t2;
28503 var_t2 != var_t3;
28504 var_t1 != var_t3;
28505}
28506private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchThree(
28507 problem:LogicProblem, interpretation:PartialInterpretation,
28508 var_s)
28509{
28510 find interpretation(problem,interpretation);
28511 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28512 // s is exported
28513 find mustInstanceOfTransition_class(problem,interpretation,var_t1);
28514 find mustInRelationtarget_reference_Transition(problem,interpretation,var_t1,var_virtual0);
28515 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
28516 var_virtual0 == var_s;
28517 find mustInstanceOfTransition_class(problem,interpretation,var_t2);
28518 find mustInRelationtarget_reference_Transition(problem,interpretation,var_t2,var_virtual1);
28519 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
28520 var_virtual1 == var_s;
28521 find mustInstanceOfTransition_class(problem,interpretation,var_t3);
28522 find mustInRelationtarget_reference_Transition(problem,interpretation,var_t3,var_virtual2);
28523 find mustInstanceOfVertex_class(problem,interpretation,var_virtual2);
28524 var_virtual2 == var_s;
28525 var_t1 != var_t2;
28526 var_t2 != var_t3;
28527 var_t1 != var_t3;
28528}or{
28529 find interpretation(problem,interpretation);
28530 find mustInstanceOfSynchronization_class(problem,interpretation,var_s);
28531 // s is exported
28532 find mustInstanceOfTransition_class(problem,interpretation,var_t1);
28533 find mustInRelationsource_reference_Transition(problem,interpretation,var_t1,var_virtual0);
28534 find mustInstanceOfVertex_class(problem,interpretation,var_virtual0);
28535 var_virtual0 == var_s;
28536 find mustInstanceOfTransition_class(problem,interpretation,var_t2);
28537 find mustInRelationsource_reference_Transition(problem,interpretation,var_t2,var_virtual1);
28538 find mustInstanceOfVertex_class(problem,interpretation,var_virtual1);
28539 var_virtual1 == var_s;
28540 find mustInstanceOfTransition_class(problem,interpretation,var_t3);
28541 find mustInRelationsource_reference_Transition(problem,interpretation,var_t3,var_virtual2);
28542 find mustInstanceOfVertex_class(problem,interpretation,var_virtual2);
28543 var_virtual2 == var_s;
28544 var_t1 != var_t2;
28545 var_t2 != var_t3;
28546 var_t1 != var_t3;
28547}
28548// Must, May and Current queries for pattern ca mcgill ecse dslreasoner standalone test yakindu queries twoSynch
28549private pattern mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_twoSynch(
28550 problem:LogicProblem, interpretation:PartialInterpretation,
28551 var_s1, var_s2)
28552{
28553 find interpretation(problem,interpretation);
28554 find mustInstanceOfSynchronization_class(problem,interpretation,var_s1);
28555 find mustInstanceOfSynchronization_class(problem,interpretation,var_s2);
28556 // s1 is exported
28557 // s2 is exported
28558 find mustInstanceOfSynchronization_class(problem,interpretation,var_s1);
28559 find mustInstanceOfSynchronization_class(problem,interpretation,var_s2);
28560 neg find mayEquivalent(problem, interpretation, var_s1, var_s2);
28561}
28562private pattern mayInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_twoSynch(
28563 problem:LogicProblem, interpretation:PartialInterpretation,
28564 var_s1, var_s2)
28565{
28566 find interpretation(problem,interpretation);
28567 find mayInstanceOfSynchronization_class(problem,interpretation,var_s1);
28568 find mayInstanceOfSynchronization_class(problem,interpretation,var_s2);
28569 // s1 is exported
28570 // s2 is exported
28571 find mayInstanceOfSynchronization_class(problem,interpretation,var_s1);
28572 find mayInstanceOfSynchronization_class(problem,interpretation,var_s2);
28573 var_s1 != var_s2;
28574}
28575private pattern currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_twoSynch(
28576 problem:LogicProblem, interpretation:PartialInterpretation,
28577 var_s1, var_s2)
28578{
28579 find interpretation(problem,interpretation);
28580 find mustInstanceOfSynchronization_class(problem,interpretation,var_s1);
28581 find mustInstanceOfSynchronization_class(problem,interpretation,var_s2);
28582 // s1 is exported
28583 // s2 is exported
28584 find mustInstanceOfSynchronization_class(problem,interpretation,var_s1);
28585 find mustInstanceOfSynchronization_class(problem,interpretation,var_s2);
28586 var_s1 != var_s2;
28587}
28588
28589//////////
28590// 1.4 Containment Indexer
28591//////////
28592private pattern mustContains2(source: DefinedElement, target: DefinedElement) {
28593 find mustContains4(_,_,source,target);
28594}
28595
28596private pattern mustContains4(problem:LogicProblem, interpretation:PartialInterpretation,
28597 source: DefinedElement, target: DefinedElement)
28598 { find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,source,target); }or
28599
28600 { find mustInRelationvertices_reference_Region(problem,interpretation,source,target); }or
28601
28602 { find mustInRelationregions_reference_CompositeElement(problem,interpretation,source,target); }
28603
28604private pattern mustTransitiveContains(source,target) {
28605 find mustContains2+(source,target);
28606}
28607
28608//////////
28609// 2. Invalidation Indexers
28610//////////
28611// 2.1 Invalidated by WF Queries
28612//////////
28613pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noEntryInRegion(problem:LogicProblem, interpretation:PartialInterpretation,
28614 var_r1)
28615{
28616 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noEntryInRegion(problem,interpretation,var_r1);
28617}
28618pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleEntryInRegion(problem:LogicProblem, interpretation:PartialInterpretation,
28619 var_r)
28620{
28621 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleEntryInRegion(problem,interpretation,var_r);
28622}
28623pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_incomingToEntry(problem:LogicProblem, interpretation:PartialInterpretation,
28624 var_t, var_e)
28625{
28626 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_incomingToEntry(problem,interpretation,var_t,var_e);
28627}
28628pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noOutgoingTransitionFromEntry(problem:LogicProblem, interpretation:PartialInterpretation,
28629 var_e)
28630{
28631 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noOutgoingTransitionFromEntry(problem,interpretation,var_e);
28632}
28633pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleTransitionFromEntry(problem:LogicProblem, interpretation:PartialInterpretation,
28634 var_e, var_t1, var_t2)
28635{
28636 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleTransitionFromEntry(problem,interpretation,var_e,var_t1,var_t2);
28637}
28638pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromExit(problem:LogicProblem, interpretation:PartialInterpretation,
28639 var_t, var_e)
28640{
28641 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromExit(problem,interpretation,var_t,var_e);
28642}
28643pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromFinal(problem:LogicProblem, interpretation:PartialInterpretation,
28644 var_t, var_f)
28645{
28646 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromFinal(problem,interpretation,var_t,var_f);
28647}
28648pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noStateInRegion(problem:LogicProblem, interpretation:PartialInterpretation,
28649 var_region)
28650{
28651 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noStateInRegion(problem,interpretation,var_region);
28652}
28653pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoOutgoing(problem:LogicProblem, interpretation:PartialInterpretation,
28654 var_c)
28655{
28656 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoOutgoing(problem,interpretation,var_c);
28657}
28658pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoIncoming(problem:LogicProblem, interpretation:PartialInterpretation,
28659 var_c)
28660{
28661 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoIncoming(problem,interpretation,var_c);
28662}
28663pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoOutgoing(problem:LogicProblem, interpretation:PartialInterpretation,
28664 var_s)
28665{
28666 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoOutgoing(problem,interpretation,var_s);
28667}
28668pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoIncoming(problem:LogicProblem, interpretation:PartialInterpretation,
28669 var_s)
28670{
28671 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoIncoming(problem,interpretation,var_s);
28672}
28673pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedIncomingInSameRegion(problem:LogicProblem, interpretation:PartialInterpretation,
28674 var_s, var_v1, var_v2)
28675{
28676 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedIncomingInSameRegion(problem,interpretation,var_s,var_v1,var_v2);
28677}
28678pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_notSynchronizingStates(problem:LogicProblem, interpretation:PartialInterpretation,
28679 var_s)
28680{
28681 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_notSynchronizingStates(problem,interpretation,var_s);
28682}
28683pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionsAreNotSiblings(problem:LogicProblem, interpretation:PartialInterpretation,
28684 var_s, var_v1, var_v2)
28685{
28686 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionsAreNotSiblings(problem,interpretation,var_s,var_v1,var_v2);
28687}
28688pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionDoesNotHaveMultipleRegions(problem:LogicProblem, interpretation:PartialInterpretation,
28689 var_s, var_v)
28690{
28691 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionDoesNotHaveMultipleRegions(problem,interpretation,var_s,var_v);
28692}
28693pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchThree(problem:LogicProblem, interpretation:PartialInterpretation,
28694 var_s)
28695{
28696 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchThree(problem,interpretation,var_s);
28697}
28698pattern invalidatedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_twoSynch(problem:LogicProblem, interpretation:PartialInterpretation,
28699 var_s1, var_s2)
28700{
28701 find mustInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_twoSynch(problem,interpretation,var_s1,var_s2);
28702}
28703
28704//////////
28705// 3. Unfinishedness Indexers
28706//////////
28707// 3.1 Unfinishedness Measured by Multiplicity
28708//////////
28709pattern unfinishedLowerMultiplicity_target_reference_Transition(problem:LogicProblem, interpretation:PartialInterpretation, relationIterpretation:PartialRelationInterpretation, object:DefinedElement,missingMultiplicity) {
28710 find interpretation(problem,interpretation);
28711 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
28712 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"target reference Transition");
28713 find mustInstanceOfTransition_class(problem,interpretation,object);
28714 numberOfExistingReferences == count find mustInRelationtarget_reference_Transition(problem,interpretation,object,_);
28715 check(numberOfExistingReferences < 1);
28716 missingMultiplicity == eval(1-numberOfExistingReferences);
28717}
28718
28719//////////
28720// 3.2 Unfinishedness Measured by WF Queries
28721//////////
28722pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noEntryInRegion(problem:LogicProblem, interpretation:PartialInterpretation,
28723 var_r1)
28724{
28725 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noEntryInRegion(problem,interpretation,var_r1);
28726}
28727pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleEntryInRegion(problem:LogicProblem, interpretation:PartialInterpretation,
28728 var_r)
28729{
28730 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleEntryInRegion(problem,interpretation,var_r);
28731}
28732pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_incomingToEntry(problem:LogicProblem, interpretation:PartialInterpretation,
28733 var_t, var_e)
28734{
28735 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_incomingToEntry(problem,interpretation,var_t,var_e);
28736}
28737pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noOutgoingTransitionFromEntry(problem:LogicProblem, interpretation:PartialInterpretation,
28738 var_e)
28739{
28740 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noOutgoingTransitionFromEntry(problem,interpretation,var_e);
28741}
28742pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleTransitionFromEntry(problem:LogicProblem, interpretation:PartialInterpretation,
28743 var_e, var_t1, var_t2)
28744{
28745 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_multipleTransitionFromEntry(problem,interpretation,var_e,var_t1,var_t2);
28746}
28747pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromExit(problem:LogicProblem, interpretation:PartialInterpretation,
28748 var_t, var_e)
28749{
28750 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromExit(problem,interpretation,var_t,var_e);
28751}
28752pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromFinal(problem:LogicProblem, interpretation:PartialInterpretation,
28753 var_t, var_f)
28754{
28755 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_outgoingFromFinal(problem,interpretation,var_t,var_f);
28756}
28757pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noStateInRegion(problem:LogicProblem, interpretation:PartialInterpretation,
28758 var_region)
28759{
28760 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_noStateInRegion(problem,interpretation,var_region);
28761}
28762pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoOutgoing(problem:LogicProblem, interpretation:PartialInterpretation,
28763 var_c)
28764{
28765 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoOutgoing(problem,interpretation,var_c);
28766}
28767pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoIncoming(problem:LogicProblem, interpretation:PartialInterpretation,
28768 var_c)
28769{
28770 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_choiceHasNoIncoming(problem,interpretation,var_c);
28771}
28772pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoOutgoing(problem:LogicProblem, interpretation:PartialInterpretation,
28773 var_s)
28774{
28775 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoOutgoing(problem,interpretation,var_s);
28776}
28777pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoIncoming(problem:LogicProblem, interpretation:PartialInterpretation,
28778 var_s)
28779{
28780 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchHasNoIncoming(problem,interpretation,var_s);
28781}
28782pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedIncomingInSameRegion(problem:LogicProblem, interpretation:PartialInterpretation,
28783 var_s, var_v1, var_v2)
28784{
28785 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedIncomingInSameRegion(problem,interpretation,var_s,var_v1,var_v2);
28786}
28787pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_notSynchronizingStates(problem:LogicProblem, interpretation:PartialInterpretation,
28788 var_s)
28789{
28790 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_notSynchronizingStates(problem,interpretation,var_s);
28791}
28792pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionsAreNotSiblings(problem:LogicProblem, interpretation:PartialInterpretation,
28793 var_s, var_v1, var_v2)
28794{
28795 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionsAreNotSiblings(problem,interpretation,var_s,var_v1,var_v2);
28796}
28797pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionDoesNotHaveMultipleRegions(problem:LogicProblem, interpretation:PartialInterpretation,
28798 var_s, var_v)
28799{
28800 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_SynchronizedRegionDoesNotHaveMultipleRegions(problem,interpretation,var_s,var_v);
28801}
28802pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchThree(problem:LogicProblem, interpretation:PartialInterpretation,
28803 var_s)
28804{
28805 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_synchThree(problem,interpretation,var_s);
28806}
28807pattern unfinishedBy_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_twoSynch(problem:LogicProblem, interpretation:PartialInterpretation,
28808 var_s1, var_s2)
28809{
28810 find currentInRelation_pattern_ca_mcgill_ecse_dslreasoner_standalone_test_yakindu_queries_twoSynch(problem,interpretation,var_s1,var_s2);
28811}
28812
28813//////////
28814// 4. Refinement Indexers
28815//////////
28816// 4.1 Object constructors
28817//////////
28818private pattern hasElementInContainment(problem:LogicProblem, interpretation:PartialInterpretation)
28819{
28820 find interpretation(problem,interpretation);
28821 find mustInstanceOfState_class(problem,interpretation,root);
28822 find mustExist(problem, interpretation, root);
28823}or{
28824 find interpretation(problem,interpretation);
28825 find mustInstanceOfRegion_class(problem,interpretation,root);
28826 find mustExist(problem, interpretation, root);
28827}or{
28828 find interpretation(problem,interpretation);
28829 find mustInstanceOfStatechart_class(problem,interpretation,root);
28830 find mustExist(problem, interpretation, root);
28831}or{
28832 find interpretation(problem,interpretation);
28833 find mustInstanceOfSynchronization_class(problem,interpretation,root);
28834 find mustExist(problem, interpretation, root);
28835}or{
28836 find interpretation(problem,interpretation);
28837 find mustInstanceOfChoice_class(problem,interpretation,root);
28838 find mustExist(problem, interpretation, root);
28839}or{
28840 find interpretation(problem,interpretation);
28841 find mustInstanceOfVertex_class(problem,interpretation,root);
28842 find mustExist(problem, interpretation, root);
28843}or{
28844 find interpretation(problem,interpretation);
28845 find mustInstanceOfRegularState_class(problem,interpretation,root);
28846 find mustExist(problem, interpretation, root);
28847}or{
28848 find interpretation(problem,interpretation);
28849 find mustInstanceOfEntry_class(problem,interpretation,root);
28850 find mustExist(problem, interpretation, root);
28851}or{
28852 find interpretation(problem,interpretation);
28853 find mustInstanceOfPseudostate_class(problem,interpretation,root);
28854 find mustExist(problem, interpretation, root);
28855}or{
28856 find interpretation(problem,interpretation);
28857 find mustInstanceOfFinalState_class(problem,interpretation,root);
28858 find mustExist(problem, interpretation, root);
28859}or{
28860 find interpretation(problem,interpretation);
28861 find mustInstanceOfExit_class(problem,interpretation,root);
28862 find mustExist(problem, interpretation, root);
28863}or{
28864 find interpretation(problem,interpretation);
28865 find mustInstanceOfTransition_class(problem,interpretation,root);
28866 find mustExist(problem, interpretation, root);
28867}or{
28868 find interpretation(problem,interpretation);
28869 find mustInstanceOfCompositeElement_class(problem,interpretation,root);
28870 find mustExist(problem, interpretation, root);
28871}or{
28872 find interpretation(problem,interpretation);
28873 find mustInstanceOfStatechart_class_DefinedPart(problem,interpretation,root);
28874 find mustExist(problem, interpretation, root);
28875}or{
28876 find interpretation(problem,interpretation);
28877 find mustInstanceOfStatechart_class_UndefinedPart(problem,interpretation,root);
28878 find mustExist(problem, interpretation, root);
28879}or{
28880 find interpretation(problem,interpretation);
28881 find mustInstanceOfCompositeElement_class_DefinedPart(problem,interpretation,root);
28882 find mustExist(problem, interpretation, root);
28883}or{
28884 find interpretation(problem,interpretation);
28885 find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,root);
28886 find mustExist(problem, interpretation, root);
28887}
28888pattern createObject_Transition_class_by_outgoingTransitions_reference_Vertex_with_source_reference_Transition(
28889 problem:LogicProblem, interpretation:PartialInterpretation,
28890 relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
28891 container:DefinedElement)
28892{
28893 find interpretation(problem,interpretation);
28894 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
28895 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Transition class");
28896 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
28897 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"outgoingTransitions reference Vertex");
28898 PartialInterpretation.partialrelationinterpretation(interpretation,inverseInterpretation);
28899 PartialRelationInterpretation.interpretationOf.name(inverseInterpretation,"source reference Transition");
28900 find mustInstanceOfVertex_class(problem,interpretation,container);
28901 find mayInstanceOfTransition_class(problem,interpretation,newObject);
28902 find mayInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,container,newObject);
28903 find mustExist(problem, interpretation, container);
28904 neg find mustExist(problem, interpretation, newObject);
28905}
28906pattern createObject_Transition_class(
28907 problem:LogicProblem, interpretation:PartialInterpretation,
28908 typeInterpretation:PartialComplexTypeInterpretation)
28909{
28910 find interpretation(problem,interpretation);
28911 neg find hasElementInContainment(problem,interpretation);
28912 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
28913 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Transition class");
28914 find mayInstanceOfTransition_class(problem,interpretation,newObject);
28915 find mayExist(problem, interpretation, newObject);
28916 neg find mustExist(problem, interpretation, newObject);
28917}
28918pattern createObject_Entry_class_by_vertices_reference_Region(
28919 problem:LogicProblem, interpretation:PartialInterpretation,
28920 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
28921 container:DefinedElement)
28922{
28923 find interpretation(problem,interpretation);
28924 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
28925 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Entry class");
28926 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
28927 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
28928 find mustInstanceOfRegion_class(problem,interpretation,container);
28929 find mayInstanceOfEntry_class(problem,interpretation,newObject);
28930 find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
28931 find mustExist(problem, interpretation, container);
28932 neg find mustExist(problem, interpretation, newObject);
28933}
28934pattern createObject_Entry_class(
28935 problem:LogicProblem, interpretation:PartialInterpretation,
28936 typeInterpretation:PartialComplexTypeInterpretation)
28937{
28938 find interpretation(problem,interpretation);
28939 neg find hasElementInContainment(problem,interpretation);
28940 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
28941 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Entry class");
28942 find mayInstanceOfEntry_class(problem,interpretation,newObject);
28943 find mayExist(problem, interpretation, newObject);
28944 neg find mustExist(problem, interpretation, newObject);
28945}
28946pattern createObject_Region_class_by_regions_reference_CompositeElement(
28947 problem:LogicProblem, interpretation:PartialInterpretation,
28948 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
28949 container:DefinedElement)
28950{
28951 find interpretation(problem,interpretation);
28952 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
28953 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Region class");
28954 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
28955 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"regions reference CompositeElement");
28956 find mustInstanceOfCompositeElement_class(problem,interpretation,container);
28957 find mayInstanceOfRegion_class(problem,interpretation,newObject);
28958 find mayInRelationregions_reference_CompositeElement(problem,interpretation,container,newObject);
28959 find mustExist(problem, interpretation, container);
28960 neg find mustExist(problem, interpretation, newObject);
28961}
28962pattern createObject_Region_class(
28963 problem:LogicProblem, interpretation:PartialInterpretation,
28964 typeInterpretation:PartialComplexTypeInterpretation)
28965{
28966 find interpretation(problem,interpretation);
28967 neg find hasElementInContainment(problem,interpretation);
28968 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
28969 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Region class");
28970 find mayInstanceOfRegion_class(problem,interpretation,newObject);
28971 find mayExist(problem, interpretation, newObject);
28972 neg find mustExist(problem, interpretation, newObject);
28973}
28974pattern createObject_Choice_class_by_vertices_reference_Region(
28975 problem:LogicProblem, interpretation:PartialInterpretation,
28976 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
28977 container:DefinedElement)
28978{
28979 find interpretation(problem,interpretation);
28980 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
28981 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Choice class");
28982 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
28983 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
28984 find mustInstanceOfRegion_class(problem,interpretation,container);
28985 find mayInstanceOfChoice_class(problem,interpretation,newObject);
28986 find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
28987 find mustExist(problem, interpretation, container);
28988 neg find mustExist(problem, interpretation, newObject);
28989}
28990pattern createObject_Choice_class(
28991 problem:LogicProblem, interpretation:PartialInterpretation,
28992 typeInterpretation:PartialComplexTypeInterpretation)
28993{
28994 find interpretation(problem,interpretation);
28995 neg find hasElementInContainment(problem,interpretation);
28996 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
28997 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Choice class");
28998 find mayInstanceOfChoice_class(problem,interpretation,newObject);
28999 find mayExist(problem, interpretation, newObject);
29000 neg find mustExist(problem, interpretation, newObject);
29001}
29002pattern createObject_Synchronization_class_by_vertices_reference_Region(
29003 problem:LogicProblem, interpretation:PartialInterpretation,
29004 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
29005 container:DefinedElement)
29006{
29007 find interpretation(problem,interpretation);
29008 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
29009 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Synchronization class");
29010 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
29011 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
29012 find mustInstanceOfRegion_class(problem,interpretation,container);
29013 find mayInstanceOfSynchronization_class(problem,interpretation,newObject);
29014 find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
29015 find mustExist(problem, interpretation, container);
29016 neg find mustExist(problem, interpretation, newObject);
29017}
29018pattern createObject_Synchronization_class(
29019 problem:LogicProblem, interpretation:PartialInterpretation,
29020 typeInterpretation:PartialComplexTypeInterpretation)
29021{
29022 find interpretation(problem,interpretation);
29023 neg find hasElementInContainment(problem,interpretation);
29024 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
29025 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Synchronization class");
29026 find mayInstanceOfSynchronization_class(problem,interpretation,newObject);
29027 find mayExist(problem, interpretation, newObject);
29028 neg find mustExist(problem, interpretation, newObject);
29029}
29030pattern createObject_Statechart_class_UndefinedPart(
29031 problem:LogicProblem, interpretation:PartialInterpretation,
29032 typeInterpretation:PartialComplexTypeInterpretation)
29033{
29034 find interpretation(problem,interpretation);
29035 neg find hasElementInContainment(problem,interpretation);
29036 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
29037 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Statechart class UndefinedPart");
29038 find mayInstanceOfStatechart_class_UndefinedPart(problem,interpretation,newObject);
29039 find mayExist(problem, interpretation, newObject);
29040 neg find mustExist(problem, interpretation, newObject);
29041}
29042pattern createObject_State_class_by_vertices_reference_Region(
29043 problem:LogicProblem, interpretation:PartialInterpretation,
29044 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
29045 container:DefinedElement)
29046{
29047 find interpretation(problem,interpretation);
29048 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
29049 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"State class");
29050 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
29051 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
29052 find mustInstanceOfRegion_class(problem,interpretation,container);
29053 find mayInstanceOfState_class(problem,interpretation,newObject);
29054 find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
29055 find mustExist(problem, interpretation, container);
29056 neg find mustExist(problem, interpretation, newObject);
29057}
29058pattern createObject_State_class(
29059 problem:LogicProblem, interpretation:PartialInterpretation,
29060 typeInterpretation:PartialComplexTypeInterpretation)
29061{
29062 find interpretation(problem,interpretation);
29063 neg find hasElementInContainment(problem,interpretation);
29064 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
29065 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"State class");
29066 find mayInstanceOfState_class(problem,interpretation,newObject);
29067 find mayExist(problem, interpretation, newObject);
29068 neg find mustExist(problem, interpretation, newObject);
29069}
29070pattern createObject_Exit_class_by_vertices_reference_Region(
29071 problem:LogicProblem, interpretation:PartialInterpretation,
29072 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
29073 container:DefinedElement)
29074{
29075 find interpretation(problem,interpretation);
29076 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
29077 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Exit class");
29078 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
29079 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
29080 find mustInstanceOfRegion_class(problem,interpretation,container);
29081 find mayInstanceOfExit_class(problem,interpretation,newObject);
29082 find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
29083 find mustExist(problem, interpretation, container);
29084 neg find mustExist(problem, interpretation, newObject);
29085}
29086pattern createObject_Exit_class(
29087 problem:LogicProblem, interpretation:PartialInterpretation,
29088 typeInterpretation:PartialComplexTypeInterpretation)
29089{
29090 find interpretation(problem,interpretation);
29091 neg find hasElementInContainment(problem,interpretation);
29092 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
29093 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Exit class");
29094 find mayInstanceOfExit_class(problem,interpretation,newObject);
29095 find mayExist(problem, interpretation, newObject);
29096 neg find mustExist(problem, interpretation, newObject);
29097}
29098pattern createObject_FinalState_class_by_vertices_reference_Region(
29099 problem:LogicProblem, interpretation:PartialInterpretation,
29100 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
29101 container:DefinedElement)
29102{
29103 find interpretation(problem,interpretation);
29104 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
29105 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"FinalState class");
29106 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
29107 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
29108 find mustInstanceOfRegion_class(problem,interpretation,container);
29109 find mayInstanceOfFinalState_class(problem,interpretation,newObject);
29110 find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
29111 find mustExist(problem, interpretation, container);
29112 neg find mustExist(problem, interpretation, newObject);
29113}
29114pattern createObject_FinalState_class(
29115 problem:LogicProblem, interpretation:PartialInterpretation,
29116 typeInterpretation:PartialComplexTypeInterpretation)
29117{
29118 find interpretation(problem,interpretation);
29119 neg find hasElementInContainment(problem,interpretation);
29120 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
29121 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"FinalState class");
29122 find mayInstanceOfFinalState_class(problem,interpretation,newObject);
29123 find mayExist(problem, interpretation, newObject);
29124 neg find mustExist(problem, interpretation, newObject);
29125}
29126
29127//////////
29128// 4.2 Type refinement
29129//////////
29130pattern refineTypeTo_Transition_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
29131 find interpretation(problem,interpretation);
29132 PartialInterpretation.newElements(interpretation,element);
29133 find mayInstanceOfTransition_class(problem,interpretation,element);
29134 neg find mustInstanceOfTransition_class(problem,interpretation,element);
29135 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
29136 neg find mustInstanceOfRegion_class(problem,interpretation,element);
29137 neg find mustInstanceOfVertex_class(problem,interpretation,element);
29138}
29139pattern refineTypeTo_Entry_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
29140 find interpretation(problem,interpretation);
29141 PartialInterpretation.newElements(interpretation,element);
29142 find mayInstanceOfEntry_class(problem,interpretation,element);
29143 neg find mustInstanceOfTransition_class(problem,interpretation,element);
29144 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
29145 neg find mustInstanceOfEntry_class(problem,interpretation,element);
29146 neg find mustInstanceOfRegion_class(problem,interpretation,element);
29147 neg find mustInstanceOfChoice_class(problem,interpretation,element);
29148 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
29149 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
29150 neg find mustInstanceOfExit_class(problem,interpretation,element);
29151}
29152pattern refineTypeTo_Region_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
29153 find interpretation(problem,interpretation);
29154 PartialInterpretation.newElements(interpretation,element);
29155 find mayInstanceOfRegion_class(problem,interpretation,element);
29156 neg find mustInstanceOfTransition_class(problem,interpretation,element);
29157 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
29158 neg find mustInstanceOfRegion_class(problem,interpretation,element);
29159 neg find mustInstanceOfVertex_class(problem,interpretation,element);
29160}
29161pattern refineTypeTo_Choice_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
29162 find interpretation(problem,interpretation);
29163 PartialInterpretation.newElements(interpretation,element);
29164 find mayInstanceOfChoice_class(problem,interpretation,element);
29165 neg find mustInstanceOfTransition_class(problem,interpretation,element);
29166 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
29167 neg find mustInstanceOfEntry_class(problem,interpretation,element);
29168 neg find mustInstanceOfRegion_class(problem,interpretation,element);
29169 neg find mustInstanceOfChoice_class(problem,interpretation,element);
29170 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
29171 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
29172 neg find mustInstanceOfExit_class(problem,interpretation,element);
29173}
29174pattern refineTypeTo_Synchronization_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
29175 find interpretation(problem,interpretation);
29176 PartialInterpretation.newElements(interpretation,element);
29177 find mayInstanceOfSynchronization_class(problem,interpretation,element);
29178 neg find mustInstanceOfTransition_class(problem,interpretation,element);
29179 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
29180 neg find mustInstanceOfEntry_class(problem,interpretation,element);
29181 neg find mustInstanceOfRegion_class(problem,interpretation,element);
29182 neg find mustInstanceOfChoice_class(problem,interpretation,element);
29183 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
29184 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
29185 neg find mustInstanceOfExit_class(problem,interpretation,element);
29186}
29187pattern refineTypeTo_Statechart_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
29188 find interpretation(problem,interpretation);
29189 PartialInterpretation.newElements(interpretation,element);
29190 find mayInstanceOfStatechart_class_UndefinedPart(problem,interpretation,element);
29191 neg find mustInstanceOfTransition_class(problem,interpretation,element);
29192 neg find mustInstanceOfRegion_class(problem,interpretation,element);
29193 neg find mustInstanceOfVertex_class(problem,interpretation,element);
29194 neg find mustInstanceOfStatechart_class_UndefinedPart(problem,interpretation,element);
29195}
29196pattern refineTypeTo_State_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
29197 find interpretation(problem,interpretation);
29198 PartialInterpretation.newElements(interpretation,element);
29199 find mayInstanceOfState_class(problem,interpretation,element);
29200 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
29201 neg find mustInstanceOfTransition_class(problem,interpretation,element);
29202 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
29203 neg find mustInstanceOfRegion_class(problem,interpretation,element);
29204 neg find mustInstanceOfState_class(problem,interpretation,element);
29205 neg find mustInstanceOfFinalState_class(problem,interpretation,element);
29206}
29207pattern refineTypeTo_Exit_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
29208 find interpretation(problem,interpretation);
29209 PartialInterpretation.newElements(interpretation,element);
29210 find mayInstanceOfExit_class(problem,interpretation,element);
29211 neg find mustInstanceOfTransition_class(problem,interpretation,element);
29212 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
29213 neg find mustInstanceOfEntry_class(problem,interpretation,element);
29214 neg find mustInstanceOfRegion_class(problem,interpretation,element);
29215 neg find mustInstanceOfChoice_class(problem,interpretation,element);
29216 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
29217 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
29218 neg find mustInstanceOfExit_class(problem,interpretation,element);
29219}
29220pattern refineTypeTo_FinalState_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
29221 find interpretation(problem,interpretation);
29222 PartialInterpretation.newElements(interpretation,element);
29223 find mayInstanceOfFinalState_class(problem,interpretation,element);
29224 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
29225 neg find mustInstanceOfTransition_class(problem,interpretation,element);
29226 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
29227 neg find mustInstanceOfRegion_class(problem,interpretation,element);
29228 neg find mustInstanceOfFinalState_class(problem,interpretation,element);
29229}
29230
29231//////////
29232// 4.3 Relation refinement
29233//////////
29234pattern refineRelation_incomingTransitions_reference_Vertex_and_target_reference_Transition(
29235 problem:LogicProblem, interpretation:PartialInterpretation,
29236 relationIterpretation:PartialRelationInterpretation, oppositeInterpretation:PartialRelationInterpretation,
29237 from: DefinedElement, to: DefinedElement)
29238{
29239 find interpretation(problem,interpretation);
29240 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
29241 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"incomingTransitions reference Vertex");
29242 PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation);
29243 PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"target reference Transition");
29244 find mustExist(problem, interpretation, from);
29245 find mustExist(problem, interpretation, to);
29246 find mustInstanceOfVertex_class(problem,interpretation,from);
29247 find mustInstanceOfTransition_class(problem,interpretation,to);
29248 find mayInRelationincomingTransitions_reference_Vertex(problem,interpretation,from,to);
29249 neg find mustInRelationincomingTransitions_reference_Vertex(problem,interpretation,from,to);
29250}
generated by cgit v1.2.3-54-g00ecf (git 2.45.1) at 2024-05-28 04:08:54 +0000