diff options
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest')
-rw-r--r-- | Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem | 272 | ||||
-rw-r--r-- | Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp | 95 |
2 files changed, 56 insertions, 311 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem index 5792ceed..a0b5d6ea 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem | |||
@@ -1,7 +1,7 @@ | |||
1 | <?xml version="1.0" encoding="ASCII"?> | 1 | <?xml version="1.0" encoding="ASCII"?> |
2 | <language:LogicProblem xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:ecore2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/ecore2logicannotation" xmlns:language="http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" xmlns:language_1="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" xmlns:viatra2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/viatra2logicannotation"> | 2 | <language:LogicProblem xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:ecore2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/ecore2logicannotation" xmlns:language="http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" xmlns:language_1="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" xmlns:viatra2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/viatra2logicannotation"> |
3 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalElement class" subtypes="//@types.2" isAbstract="true"/> | 3 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalElement class" subtypes="//@types.2" isAbstract="true"/> |
4 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class" subtypes="//@types.10 //@types.11" isAbstract="true"/> | 4 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class"/> |
5 | <types xsi:type="language_1:TypeDeclaration" name="Function class" supertypes="//@types.0"/> | 5 | <types xsi:type="language_1:TypeDeclaration" name="Function class" supertypes="//@types.0"/> |
6 | <types xsi:type="language_1:TypeDeclaration" name="FAMTerminator class"/> | 6 | <types xsi:type="language_1:TypeDeclaration" name="FAMTerminator class"/> |
7 | <types xsi:type="language_1:TypeDeclaration" name="InformationLink class"/> | 7 | <types xsi:type="language_1:TypeDeclaration" name="InformationLink class"/> |
@@ -10,8 +10,6 @@ | |||
10 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalOutput class" supertypes="//@types.8"/> | 10 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalOutput class" supertypes="//@types.8"/> |
11 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalData class" subtypes="//@types.6 //@types.7" isAbstract="true"/> | 11 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalData class" subtypes="//@types.6 //@types.7" isAbstract="true"/> |
12 | <types xsi:type="language_1:TypeDefinition" name="FunctionType enum" elements="//@elements.0 //@elements.1 //@elements.2"/> | 12 | <types xsi:type="language_1:TypeDefinition" name="FunctionType enum" elements="//@elements.0 //@elements.1 //@elements.2"/> |
13 | <types xsi:type="language_1:TypeDefinition" name="FunctionalArchitectureModel class DefinedPart" supertypes="//@types.1" elements="//@elements.3"/> | ||
14 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class UndefinedPart" supertypes="//@types.1"/> | ||
15 | <assertions name="upperMultiplicity interface FunctionalElement" annotations="//@annotations.0"> | 13 | <assertions name="upperMultiplicity interface FunctionalElement" annotations="//@annotations.0"> |
16 | <value xsi:type="language_1:Forall"> | 14 | <value xsi:type="language_1:Forall"> |
17 | <quantifiedVariables name="src"> | 15 | <quantifiedVariables name="src"> |
@@ -496,7 +494,7 @@ | |||
496 | </expression> | 494 | </expression> |
497 | </value> | 495 | </value> |
498 | </assertions> | 496 | </assertions> |
499 | <assertions name="errorpattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.27"> | 497 | <assertions name="errorpattern ca mcgill ecse dslreasoner vampire queries terminatorAndInformation" annotations="//@annotations.20"> |
500 | <value xsi:type="language_1:Forall"> | 498 | <value xsi:type="language_1:Forall"> |
501 | <quantifiedVariables name="p0"> | 499 | <quantifiedVariables name="p0"> |
502 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | 500 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> |
@@ -505,7 +503,7 @@ | |||
505 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | 503 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> |
506 | </quantifiedVariables> | 504 | </quantifiedVariables> |
507 | <expression xsi:type="language_1:Not"> | 505 | <expression xsi:type="language_1:Not"> |
508 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22"> | 506 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15"> |
509 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.0"/> | 507 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.0"/> |
510 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.1"/> | 508 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.1"/> |
511 | </operand> | 509 | </operand> |
@@ -572,235 +570,7 @@ | |||
572 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | 570 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> |
573 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | 571 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> |
574 | </relations> | 572 | </relations> |
575 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam hasRoot" annotations="//@annotations.19"> | 573 | <relations xsi:type="language_1:RelationDefinition" name="pattern ca mcgill ecse dslreasoner vampire queries terminatorAndInformation" annotations="//@annotations.19"> |
576 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
577 | <variables name="parameter F"> | ||
578 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
579 | </variables> | ||
580 | <value xsi:type="language_1:Or"> | ||
581 | <operands xsi:type="language_1:Exists"> | ||
582 | <quantifiedVariables name="variable Model"> | ||
583 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
584 | </quantifiedVariables> | ||
585 | <expression xsi:type="language_1:And"> | ||
586 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19"> | ||
587 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/> | ||
588 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> | ||
589 | </operands> | ||
590 | </expression> | ||
591 | </operands> | ||
592 | </value> | ||
593 | </relations> | ||
594 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam hasInt" annotations="//@annotations.20"> | ||
595 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
596 | <variables name="parameter F"> | ||
597 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
598 | </variables> | ||
599 | <value xsi:type="language_1:Or"> | ||
600 | <operands xsi:type="language_1:Forall"> | ||
601 | <quantifiedVariables name="variable Child"> | ||
602 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
603 | </quantifiedVariables> | ||
604 | <quantifiedVariables name="variable Model"> | ||
605 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
606 | </quantifiedVariables> | ||
607 | <expression xsi:type="language_1:And"> | ||
608 | <operands xsi:type="language_1:InstanceOf"> | ||
609 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@variables.0"/> | ||
610 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
611 | </operands> | ||
612 | <operands xsi:type="language_1:Not"> | ||
613 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21"> | ||
614 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@value/@operands.0/@quantifiedVariables.0"/> | ||
615 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@variables.0"/> | ||
616 | </operand> | ||
617 | </operands> | ||
618 | <operands xsi:type="language_1:Not"> | ||
619 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19"> | ||
620 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@value/@operands.0/@quantifiedVariables.1"/> | ||
621 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@variables.0"/> | ||
622 | </operand> | ||
623 | </operands> | ||
624 | </expression> | ||
625 | </operands> | ||
626 | </value> | ||
627 | </relations> | ||
628 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam hasLeaf" annotations="//@annotations.21"> | ||
629 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
630 | <variables name="parameter F"> | ||
631 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
632 | </variables> | ||
633 | <value xsi:type="language_1:Or"> | ||
634 | <operands xsi:type="language_1:Exists"> | ||
635 | <quantifiedVariables name="variable Par"> | ||
636 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
637 | </quantifiedVariables> | ||
638 | <quantifiedVariables name="variable Child"> | ||
639 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
640 | </quantifiedVariables> | ||
641 | <expression xsi:type="language_1:And"> | ||
642 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21"> | ||
643 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.0"/> | ||
644 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.0/@quantifiedVariables.0"/> | ||
645 | </operands> | ||
646 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21"> | ||
647 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.0/@quantifiedVariables.1"/> | ||
648 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.0"/> | ||
649 | </operands> | ||
650 | </expression> | ||
651 | </operands> | ||
652 | </value> | ||
653 | </relations> | ||
654 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam model" annotations="//@annotations.22"> | ||
655 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | ||
656 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
657 | <variables name="parameter This"> | ||
658 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | ||
659 | </variables> | ||
660 | <variables name="parameter Target"> | ||
661 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
662 | </variables> | ||
663 | <value xsi:type="language_1:Or"> | ||
664 | <operands xsi:type="language_1:And"> | ||
665 | <operands xsi:type="language_1:InstanceOf"> | ||
666 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.0"/> | ||
667 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | ||
668 | </operands> | ||
669 | <operands xsi:type="language_1:InstanceOf"> | ||
670 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.1"/> | ||
671 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
672 | </operands> | ||
673 | </operands> | ||
674 | </value> | ||
675 | </relations> | ||
676 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam rootElements" annotations="//@annotations.23"> | ||
677 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
678 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
679 | <variables name="parameter Model"> | ||
680 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
681 | </variables> | ||
682 | <variables name="parameter Root"> | ||
683 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
684 | </variables> | ||
685 | <value xsi:type="language_1:Or"> | ||
686 | <operands xsi:type="language_1:And"> | ||
687 | <operands xsi:type="language_1:InstanceOf"> | ||
688 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.1"/> | ||
689 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
690 | </operands> | ||
691 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.3"> | ||
692 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
693 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.1"/> | ||
694 | </operands> | ||
695 | </operands> | ||
696 | </value> | ||
697 | </relations> | ||
698 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam type" annotations="//@annotations.24"> | ||
699 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
700 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | ||
701 | <variables name="parameter This"> | ||
702 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
703 | </variables> | ||
704 | <variables name="parameter Target"> | ||
705 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | ||
706 | </variables> | ||
707 | <value xsi:type="language_1:Or"> | ||
708 | <operands xsi:type="language_1:Exists"> | ||
709 | <quantifiedVariables name="variable Model"> | ||
710 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
711 | </quantifiedVariables> | ||
712 | <expression xsi:type="language_1:And"> | ||
713 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19"> | ||
714 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@value/@operands.0/@quantifiedVariables.0"/> | ||
715 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.0"/> | ||
716 | </operands> | ||
717 | <operands xsi:type="language_1:Equals"> | ||
718 | <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.1"/> | ||
719 | <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.0"/> | ||
720 | </operands> | ||
721 | </expression> | ||
722 | </operands> | ||
723 | <operands xsi:type="language_1:Forall"> | ||
724 | <quantifiedVariables name="variable Child"> | ||
725 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
726 | </quantifiedVariables> | ||
727 | <quantifiedVariables name="variable Model"> | ||
728 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
729 | </quantifiedVariables> | ||
730 | <expression xsi:type="language_1:And"> | ||
731 | <operands xsi:type="language_1:InstanceOf"> | ||
732 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.0"/> | ||
733 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
734 | </operands> | ||
735 | <operands xsi:type="language_1:Not"> | ||
736 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21"> | ||
737 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@value/@operands.1/@quantifiedVariables.0"/> | ||
738 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.0"/> | ||
739 | </operand> | ||
740 | </operands> | ||
741 | <operands xsi:type="language_1:Not"> | ||
742 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19"> | ||
743 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@value/@operands.1/@quantifiedVariables.1"/> | ||
744 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.0"/> | ||
745 | </operand> | ||
746 | </operands> | ||
747 | <operands xsi:type="language_1:Equals"> | ||
748 | <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.1"/> | ||
749 | <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.2"/> | ||
750 | </operands> | ||
751 | </expression> | ||
752 | </operands> | ||
753 | <operands xsi:type="language_1:Exists"> | ||
754 | <quantifiedVariables name="variable Par"> | ||
755 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
756 | </quantifiedVariables> | ||
757 | <quantifiedVariables name="variable Child"> | ||
758 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
759 | </quantifiedVariables> | ||
760 | <expression xsi:type="language_1:And"> | ||
761 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21"> | ||
762 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.0"/> | ||
763 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@value/@operands.2/@quantifiedVariables.0"/> | ||
764 | </operands> | ||
765 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21"> | ||
766 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@value/@operands.2/@quantifiedVariables.1"/> | ||
767 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.0"/> | ||
768 | </operands> | ||
769 | <operands xsi:type="language_1:Equals"> | ||
770 | <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.1"/> | ||
771 | <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.1"/> | ||
772 | </operands> | ||
773 | </expression> | ||
774 | </operands> | ||
775 | </value> | ||
776 | </relations> | ||
777 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam parent" annotations="//@annotations.25"> | ||
778 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
779 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
780 | <variables name="parameter Func"> | ||
781 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
782 | </variables> | ||
783 | <variables name="parameter Par"> | ||
784 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
785 | </variables> | ||
786 | <value xsi:type="language_1:Or"> | ||
787 | <operands xsi:type="language_1:And"> | ||
788 | <operands xsi:type="language_1:InstanceOf"> | ||
789 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21/@variables.0"/> | ||
790 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
791 | </operands> | ||
792 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.2"> | ||
793 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21/@variables.0"/> | ||
794 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21/@variables.1"/> | ||
795 | </operands> | ||
796 | <operands xsi:type="language_1:InstanceOf"> | ||
797 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21/@variables.1"/> | ||
798 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
799 | </operands> | ||
800 | </operands> | ||
801 | </value> | ||
802 | </relations> | ||
803 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.26"> | ||
804 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | 574 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> |
805 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | 575 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> |
806 | <variables name="parameter T"> | 576 | <variables name="parameter T"> |
@@ -816,12 +586,12 @@ | |||
816 | </quantifiedVariables> | 586 | </quantifiedVariables> |
817 | <expression xsi:type="language_1:And"> | 587 | <expression xsi:type="language_1:And"> |
818 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.11"> | 588 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.11"> |
819 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@value/@operands.0/@quantifiedVariables.0"/> | 589 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/> |
820 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@variables.1"/> | 590 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> |
821 | </operands> | 591 | </operands> |
822 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | 592 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> |
823 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@value/@operands.0/@quantifiedVariables.0"/> | 593 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/> |
824 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@variables.0"/> | 594 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> |
825 | </operands> | 595 | </operands> |
826 | </expression> | 596 | </expression> |
827 | </operands> | 597 | </operands> |
@@ -831,16 +601,12 @@ | |||
831 | </quantifiedVariables> | 601 | </quantifiedVariables> |
832 | <expression xsi:type="language_1:And"> | 602 | <expression xsi:type="language_1:And"> |
833 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.7"> | 603 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.7"> |
834 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@variables.1"/> | 604 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> |
835 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@value/@operands.1/@quantifiedVariables.0"/> | 605 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/> |
836 | </operands> | ||
837 | <operands xsi:type="language_1:InstanceOf"> | ||
838 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@value/@operands.1/@quantifiedVariables.0"/> | ||
839 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.6"/> | ||
840 | </operands> | 606 | </operands> |
841 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | 607 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> |
842 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@value/@operands.1/@quantifiedVariables.0"/> | 608 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/> |
843 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@variables.0"/> | 609 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> |
844 | </operands> | 610 | </operands> |
845 | </expression> | 611 | </expression> |
846 | </operands> | 612 | </operands> |
@@ -849,8 +615,7 @@ | |||
849 | <elements name="Root literal FunctionType" definedInType="//@types.9"/> | 615 | <elements name="Root literal FunctionType" definedInType="//@types.9"/> |
850 | <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/> | 616 | <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/> |
851 | <elements name="Leaf literal FunctionType" definedInType="//@types.9"/> | 617 | <elements name="Leaf literal FunctionType" definedInType="//@types.9"/> |
852 | <elements name="o 1" definedInType="//@types.10"/> | 618 | <containmentHierarchies typesOrderedInHierarchy="//@types.3 //@types.8 //@types.0 //@types.4 //@types.2 //@types.1 //@types.6 //@types.7 //@types.5" containmentRelations="//@relations.0 //@relations.3 //@relations.4 //@relations.8 //@relations.11 //@relations.12"/> |
853 | <containmentHierarchies typesOrderedInHierarchy="//@types.5 //@types.6 //@types.1 //@types.3 //@types.0 //@types.4 //@types.7 //@types.2 //@types.8 //@types.10 //@types.11" containmentRelations="//@relations.0 //@relations.3 //@relations.4 //@relations.8 //@relations.11 //@relations.12"/> | ||
854 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.0" relation="//@relations.0" upper="1"/> | 619 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.0" relation="//@relations.0" upper="1"/> |
855 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.1" relation="//@relations.1" lower="1"/> | 620 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.1" relation="//@relations.1" lower="1"/> |
856 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.2" relation="//@relations.1" upper="1"/> | 621 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.2" relation="//@relations.1" upper="1"/> |
@@ -870,13 +635,6 @@ | |||
870 | <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/> | 635 | <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/> |
871 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/> | 636 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/> |
872 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/> | 637 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/> |
873 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.15" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.hasRoot"/> | 638 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.15" patternFullyQualifiedName="ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation"/> |
874 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.16" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.hasInt"/> | 639 | <annotations xsi:type="viatra2logicannotations:TransformedViatraWellformednessConstraint" target="//@assertions.19" query="//@annotations.19"/> |
875 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.17" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.hasLeaf"/> | ||
876 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.18" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.model"/> | ||
877 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.19" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.rootElements"/> | ||
878 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.20" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.type"/> | ||
879 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.21" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.parent"/> | ||
880 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.22" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.terminatorAndInformation"/> | ||
881 | <annotations xsi:type="viatra2logicannotations:TransformedViatraWellformednessConstraint" target="//@assertions.19" query="//@annotations.26"/> | ||
882 | </language:LogicProblem> | 640 | </language:LogicProblem> |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp index 242c404c..1f220d6f 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp | |||
@@ -1,55 +1,42 @@ | |||
1 | % This is an initial Test Comment | 1 | % This is an initial Test Comment |
2 | fof ( typeDef_FunctionType_enum , axiom , ! [ A ] : ( type_FunctionType_enum ( A ) <=> ( A = "aRoot literal FunctionType" | ( A = "aIntermediate literal FunctionType" | A = "aLeaf literal FunctionType" ) ) ) ) . | 2 | fof ( typeDef_FunctionType_enum , axiom , ! [ A ] : ( t_FunctionType_enum ( A ) <=> ( e_Root_literal_FunctionType_FunctionType_enum ( A ) | ( e_Intermediate_literal_FunctionType_FunctionType_enum ( A ) | e_Leaf_literal_FunctionType_FunctionType_enum ( A ) ) ) ) ) . |
3 | fof ( typeDef_FunctionalArchitectureModel_class_DefinedPart , axiom , ! [ A ] : ( type_FunctionalArchitectureModel_class_DefinedPart ( A ) <=> A = "ao 1" ) ) . | 3 | fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( t_FunctionalData_class ( A ) & ( t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . |
4 | fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . | 4 | fof ( typeScope , axiom , ! [ A ] : ( object ( A ) <=> ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) . |
5 | fof ( compliance_interface_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_FunctionalInterface_class ( Var_1 ) ) ) ) . | 5 | fof ( typeUniqueness , axiom , o1 != o2 & ( o1 != o3 & ( o2 != o3 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & o4 != o5 ) ) ) ) ) ) ) ) ) . |
6 | fof ( compliance_model_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_model_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_FunctionalArchitectureModel_class ( Var_1 ) ) ) ) . | 6 | fof ( compliance_interface_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_FunctionalInterface_class ( Var_1 ) ) ) ) . |
7 | fof ( compliance_parent_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_parent_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_Function_class ( Var_1 ) ) ) ) . | 7 | fof ( compliance_model_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_model_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_FunctionalArchitectureModel_class ( Var_1 ) ) ) ) . |
8 | fof ( compliance_rootElements_reference_FunctionalArchitectureModel , axiom , ! [ Var_0 , Var_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( Var_0 , Var_1 ) => ( type_FunctionalArchitectureModel_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) . | 8 | fof ( compliance_parent_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_parent_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_Function_class ( Var_1 ) ) ) ) . |
9 | fof ( compliance_subElements_reference_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_subElements_reference_Function ( Var_0 , Var_1 ) => ( type_Function_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) . | 9 | fof ( compliance_rootElements_reference_FunctionalArchitectureModel , axiom , ! [ Var_0 , Var_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( Var_0 , Var_1 ) => ( t_FunctionalArchitectureModel_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) . |
10 | fof ( compliance_data_reference_FAMTerminator , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FAMTerminator ( Var_0 , Var_1 ) => ( type_FAMTerminator_class ( Var_0 ) & type_FunctionalData_class ( Var_1 ) ) ) ) . | 10 | fof ( compliance_subElements_reference_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_subElements_reference_Function ( Var_0 , Var_1 ) => ( t_Function_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) . |
11 | fof ( compliance_from_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_from_reference_InformationLink ( Var_0 , Var_1 ) => ( type_InformationLink_class ( Var_0 ) & type_FunctionalOutput_class ( Var_1 ) ) ) ) . | 11 | fof ( compliance_data_reference_FAMTerminator , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FAMTerminator ( Var_0 , Var_1 ) => ( t_FAMTerminator_class ( Var_0 ) & t_FunctionalData_class ( Var_1 ) ) ) ) . |
12 | fof ( compliance_to_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_to_reference_InformationLink ( Var_0 , Var_1 ) => ( type_InformationLink_class ( Var_0 ) & type_FunctionalInput_class ( Var_1 ) ) ) ) . | 12 | fof ( compliance_from_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_from_reference_InformationLink ( Var_0 , Var_1 ) => ( t_InformationLink_class ( Var_0 ) & t_FunctionalOutput_class ( Var_1 ) ) ) ) . |
13 | fof ( compliance_data_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( type_FunctionalInterface_class ( Var_0 ) & type_FunctionalData_class ( Var_1 ) ) ) ) . | 13 | fof ( compliance_to_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_to_reference_InformationLink ( Var_0 , Var_1 ) => ( t_InformationLink_class ( Var_0 ) & t_FunctionalInput_class ( Var_1 ) ) ) ) . |
14 | fof ( compliance_element_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_element_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( type_FunctionalInterface_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) . | 14 | fof ( compliance_data_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( t_FunctionalInterface_class ( Var_0 ) & t_FunctionalData_class ( Var_1 ) ) ) ) . |
15 | fof ( compliance_IncomingLinks_reference_FunctionalInput , axiom , ! [ Var_0 , Var_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( Var_0 , Var_1 ) => ( type_FunctionalInput_class ( Var_0 ) & type_InformationLink_class ( Var_1 ) ) ) ) . | 15 | fof ( compliance_element_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_element_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( t_FunctionalInterface_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) . |
16 | fof ( compliance_outgoingLinks_reference_FunctionalOutput , axiom , ! [ Var_0 , Var_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( Var_0 , Var_1 ) => ( type_FunctionalOutput_class ( Var_0 ) & type_InformationLink_class ( Var_1 ) ) ) ) . | 16 | fof ( compliance_IncomingLinks_reference_FunctionalInput , axiom , ! [ Var_0 , Var_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( Var_0 , Var_1 ) => ( t_FunctionalInput_class ( Var_0 ) & t_InformationLink_class ( Var_1 ) ) ) ) . |
17 | fof ( compliance_terminator_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_terminator_reference_FunctionalData ( Var_0 , Var_1 ) => ( type_FunctionalData_class ( Var_0 ) & type_FAMTerminator_class ( Var_1 ) ) ) ) . | 17 | fof ( compliance_outgoingLinks_reference_FunctionalOutput , axiom , ! [ Var_0 , Var_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( Var_0 , Var_1 ) => ( t_FunctionalOutput_class ( Var_0 ) & t_InformationLink_class ( Var_1 ) ) ) ) . |
18 | fof ( compliance_interface_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalData ( Var_0 , Var_1 ) => ( type_FunctionalData_class ( Var_0 ) & type_FunctionalInterface_class ( Var_1 ) ) ) ) . | 18 | fof ( compliance_terminator_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_terminator_reference_FunctionalData ( Var_0 , Var_1 ) => ( t_FunctionalData_class ( Var_0 ) & t_FAMTerminator_class ( Var_1 ) ) ) ) . |
19 | fof ( compliance_type_attribute_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_type_attribute_Function ( Var_0 , Var_1 ) => ( type_Function_class ( Var_0 ) & type_FunctionType_enum ( Var_1 ) ) ) ) . | 19 | fof ( compliance_interface_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalData ( Var_0 , Var_1 ) => ( t_FunctionalData_class ( Var_0 ) & t_FunctionalInterface_class ( Var_1 ) ) ) ) . |
20 | fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot , axiom , ! [ Var_parameter_F ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot ( Var_parameter_F ) => type_Function_class ( Var_parameter_F ) ) ) . | 20 | fof ( compliance_type_attribute_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_type_attribute_Function ( Var_0 , Var_1 ) => ( t_Function_class ( Var_0 ) & t_FunctionType_enum ( Var_1 ) ) ) ) . |
21 | fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot , axiom , ! [ Var_parameter_F ] : ( type_Function_class ( Var_parameter_F ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot ( Var_parameter_F ) <=> ? [ Var_variable_Model ] : ( type_FunctionalArchitectureModel_class ( Var_variable_Model ) & rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_F ) ) ) ) ) . | 21 | fof ( compliance_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) => ( t_FAMTerminator_class ( Var_parameter_T ) & t_InformationLink_class ( Var_parameter_I ) ) ) ) . |
22 | fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt , axiom , ! [ Var_parameter_F ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt ( Var_parameter_F ) => type_Function_class ( Var_parameter_F ) ) ) . | 22 | fof ( relation_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( ( t_FAMTerminator_class ( Var_parameter_T ) & t_InformationLink_class ( Var_parameter_I ) ) => ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( t_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , Var_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , Var_parameter_T ) ) ) | ? [ Var_variable_In ] : ( t_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( Var_parameter_I , Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , Var_parameter_T ) ) ) ) ) ) ) . |
23 | fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt , axiom , ! [ Var_parameter_F ] : ( type_Function_class ( Var_parameter_F ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt ( Var_parameter_F ) <=> ! [ Var_variable_Child , Var_variable_Model ] : ( ( type_Function_class ( Var_variable_Child ) & type_FunctionalArchitectureModel_class ( Var_variable_Model ) ) => ( type_Function_class ( Var_parameter_F ) & ( ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_F ) & ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_F ) ) ) ) ) ) ) . | 23 | fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . |
24 | fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf , axiom , ! [ Var_parameter_F ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf ( Var_parameter_F ) => type_Function_class ( Var_parameter_F ) ) ) . | 24 | fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ Var_src ] : ( t_FunctionalElement_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) ) ) ) . |
25 | fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf , axiom , ! [ Var_parameter_F ] : ( type_Function_class ( Var_parameter_F ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf ( Var_parameter_F ) <=> ? [ Var_variable_Par , Var_variable_Child ] : ( type_Function_class ( Var_variable_Par ) & ( type_Function_class ( Var_variable_Child ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_F , Var_variable_Par ) & rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_F ) ) ) ) ) ) ) . | 25 | fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & t_FunctionalArchitectureModel_class ( Var_trg_2 ) ) ) => ( ( rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . |
26 | fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model ( Var_parameter_This , Var_parameter_Target ) => ( type_FunctionalArchitectureModel_class ( Var_parameter_Target ) & type_FunctionalElement_class ( Var_parameter_This ) ) ) ) . | 26 | fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_Function_class ( Var_trg_1 ) & t_Function_class ( Var_trg_2 ) ) ) => ( ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_parent_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . |
27 | fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( ( type_FunctionalArchitectureModel_class ( Var_parameter_Target ) & type_FunctionalElement_class ( Var_parameter_This ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model ( Var_parameter_This , Var_parameter_Target ) <=> ( type_FunctionalElement_class ( Var_parameter_This ) & type_FunctionalArchitectureModel_class ( Var_parameter_Target ) ) ) ) ) . | 27 | fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FAMTerminator_class ( Var_src ) & ( t_FunctionalData_class ( Var_trg_1 ) & t_FunctionalData_class ( Var_trg_2 ) ) ) => ( ( rel_data_reference_FAMTerminator ( Var_src , Var_trg_1 ) & rel_data_reference_FAMTerminator ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . |
28 | fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements , axiom , ! [ Var_parameter_Model , Var_parameter_Root ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_parameter_Model , Var_parameter_Root ) => ( type_FunctionalArchitectureModel_class ( Var_parameter_Model ) & type_Function_class ( Var_parameter_Root ) ) ) ) . | 28 | fof ( upperMultiplicity_from_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_InformationLink_class ( Var_src ) & ( t_FunctionalOutput_class ( Var_trg_1 ) & t_FunctionalOutput_class ( Var_trg_2 ) ) ) => ( ( rel_from_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_from_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . |
29 | fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements , axiom , ! [ Var_parameter_Model , Var_parameter_Root ] : ( ( type_FunctionalArchitectureModel_class ( Var_parameter_Model ) & type_Function_class ( Var_parameter_Root ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_parameter_Model , Var_parameter_Root ) <=> ( type_Function_class ( Var_parameter_Root ) & rel_rootElements_reference_FunctionalArchitectureModel ( Var_parameter_Model , Var_parameter_Root ) ) ) ) ) . | 29 | fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ Var_src ] : ( t_InformationLink_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalInput_class ( Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) ) ) ) . |
30 | fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type ( Var_parameter_This , Var_parameter_Target ) => ( type_FunctionType_enum ( Var_parameter_Target ) & type_Function_class ( Var_parameter_This ) ) ) ) . | 30 | fof ( upperMultiplicity_to_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_InformationLink_class ( Var_src ) & ( t_FunctionalInput_class ( Var_trg_1 ) & t_FunctionalInput_class ( Var_trg_2 ) ) ) => ( ( rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . |
31 | fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( ( type_FunctionType_enum ( Var_parameter_Target ) & type_Function_class ( Var_parameter_This ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type ( Var_parameter_This , Var_parameter_Target ) <=> ( ? [ Var_variable_Model ] : ( type_FunctionalArchitectureModel_class ( Var_variable_Model ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_This ) & Var_parameter_Target = "aRoot literal FunctionType" ) ) | ( ! [ Var_variable_Child , Var_variable_Model ] : ( ( type_Function_class ( Var_variable_Child ) & type_FunctionalArchitectureModel_class ( Var_variable_Model ) ) => ( type_Function_class ( Var_parameter_This ) & ( ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_This ) & ( ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_This ) & Var_parameter_Target = "aLeaf literal FunctionType" ) ) ) ) | ? [ Var_variable_Par , Var_variable_Child ] : ( type_Function_class ( Var_variable_Par ) & ( type_Function_class ( Var_variable_Child ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_This , Var_variable_Par ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_This ) & Var_parameter_Target = "aIntermediate literal FunctionType" ) ) ) ) ) ) ) ) ) . | 31 | fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalInterface_class ( Var_src ) & ( t_FunctionalElement_class ( Var_trg_1 ) & t_FunctionalElement_class ( Var_trg_2 ) ) ) => ( ( rel_element_reference_FunctionalInterface ( Var_src , Var_trg_1 ) & rel_element_reference_FunctionalInterface ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . |
32 | fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent , axiom , ! [ Var_parameter_Func , Var_parameter_Par ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_Func , Var_parameter_Par ) => ( type_Function_class ( Var_parameter_Par ) & type_Function_class ( Var_parameter_Func ) ) ) ) . | 32 | fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalData_class ( Var_src ) & ( t_FAMTerminator_class ( Var_trg_1 ) & t_FAMTerminator_class ( Var_trg_2 ) ) ) => ( ( rel_terminator_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_terminator_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . |
33 | fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent , axiom , ! [ Var_parameter_Func , Var_parameter_Par ] : ( ( type_Function_class ( Var_parameter_Par ) & type_Function_class ( Var_parameter_Func ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_Func , Var_parameter_Par ) <=> ( type_Function_class ( Var_parameter_Func ) & ( rel_parent_reference_FunctionalElement ( Var_parameter_Func , Var_parameter_Par ) & type_Function_class ( Var_parameter_Par ) ) ) ) ) ) . | 33 | fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalData_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . |
34 | fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) => ( type_FAMTerminator_class ( Var_parameter_T ) & type_InformationLink_class ( Var_parameter_I ) ) ) ) . | 34 | fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalElement_class ( Var_src ) & t_FunctionalInterface_class ( Var_trg ) ) => ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_element_reference_FunctionalInterface ( Var_trg , Var_src ) ) ) ) . |
35 | fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( ( type_FAMTerminator_class ( Var_parameter_T ) & type_InformationLink_class ( Var_parameter_I ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( type_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , Var_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , Var_parameter_T ) ) ) | ? [ Var_variable_In ] : ( type_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( Var_parameter_I , Var_variable_In ) & ( type_FunctionalInput_class ( Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , Var_parameter_T ) ) ) ) ) ) ) ) . | 35 | fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalElement_class ( Var_src ) & t_Function_class ( Var_trg ) ) => ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_subElements_reference_Function ( Var_trg , Var_src ) ) ) ) . |
36 | fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_FunctionalInterface_class ( Var_trg_1 ) & type_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 36 | fof ( oppositeReference_data_FAMTerminator , axiom , ! [ Var_src , Var_trg ] : ( ( t_FAMTerminator_class ( Var_src ) & t_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FAMTerminator ( Var_src , Var_trg ) <=> rel_terminator_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) . |
37 | fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ Var_src ] : ( type_FunctionalElement_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionalArchitectureModel_class ( Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) ) ) ) . | 37 | fof ( oppositeReference_from_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( t_InformationLink_class ( Var_src ) & t_FunctionalOutput_class ( Var_trg ) ) => ( rel_from_reference_InformationLink ( Var_src , Var_trg ) <=> rel_outgoingLinks_reference_FunctionalOutput ( Var_trg , Var_src ) ) ) ) . |
38 | fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_FunctionalArchitectureModel_class ( Var_trg_1 ) & type_FunctionalArchitectureModel_class ( Var_trg_2 ) ) ) => ( ( rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 38 | fof ( oppositeReference_to_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( t_InformationLink_class ( Var_src ) & t_FunctionalInput_class ( Var_trg ) ) => ( rel_to_reference_InformationLink ( Var_src , Var_trg ) <=> rel_IncomingLinks_reference_FunctionalInput ( Var_trg , Var_src ) ) ) ) . |
39 | fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_Function_class ( Var_trg_1 ) & type_Function_class ( Var_trg_2 ) ) ) => ( ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_parent_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 39 | fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalInterface_class ( Var_src ) & t_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FunctionalInterface ( Var_src , Var_trg ) <=> rel_interface_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) . |
40 | fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FAMTerminator_class ( Var_src ) & ( type_FunctionalData_class ( Var_trg_1 ) & type_FunctionalData_class ( Var_trg_2 ) ) ) => ( ( rel_data_reference_FAMTerminator ( Var_src , Var_trg_1 ) & rel_data_reference_FAMTerminator ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 40 | fof ( lowerMultiplicity_type_Function , axiom , ! [ Var_src ] : ( t_Function_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionType_enum ( Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_1 ) ) ) ) . |
41 | fof ( upperMultiplicity_from_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_InformationLink_class ( Var_src ) & ( type_FunctionalOutput_class ( Var_trg_1 ) & type_FunctionalOutput_class ( Var_trg_2 ) ) ) => ( ( rel_from_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_from_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 41 | fof ( upperMultiplicity_type_Function , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_Function_class ( Var_src ) & ( t_FunctionType_enum ( Var_trg_1 ) & t_FunctionType_enum ( Var_trg_2 ) ) ) => ( ( rel_type_attribute_Function ( Var_src , Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . |
42 | fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ Var_src ] : ( type_InformationLink_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionalInput_class ( Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) ) ) ) . | 42 | fof ( errorpattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_p0 , Var_p1 ] : ( ( t_FAMTerminator_class ( Var_p0 ) & t_InformationLink_class ( Var_p1 ) ) => ~ rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_p0 , Var_p1 ) ) ) . |
43 | fof ( upperMultiplicity_to_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_InformationLink_class ( Var_src ) & ( type_FunctionalInput_class ( Var_trg_1 ) & type_FunctionalInput_class ( Var_trg_2 ) ) ) => ( ( rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | ||
44 | fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalInterface_class ( Var_src ) & ( type_FunctionalElement_class ( Var_trg_1 ) & type_FunctionalElement_class ( Var_trg_2 ) ) ) => ( ( rel_element_reference_FunctionalInterface ( Var_src , Var_trg_1 ) & rel_element_reference_FunctionalInterface ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | ||
45 | fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalData_class ( Var_src ) & ( type_FAMTerminator_class ( Var_trg_1 ) & type_FAMTerminator_class ( Var_trg_2 ) ) ) => ( ( rel_terminator_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_terminator_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | ||
46 | fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalData_class ( Var_src ) & ( type_FunctionalInterface_class ( Var_trg_1 ) & type_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | ||
47 | fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalElement_class ( Var_src ) & type_FunctionalInterface_class ( Var_trg ) ) => ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_element_reference_FunctionalInterface ( Var_trg , Var_src ) ) ) ) . | ||
48 | fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalElement_class ( Var_src ) & type_Function_class ( Var_trg ) ) => ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_subElements_reference_Function ( Var_trg , Var_src ) ) ) ) . | ||
49 | fof ( oppositeReference_data_FAMTerminator , axiom , ! [ Var_src , Var_trg ] : ( ( type_FAMTerminator_class ( Var_src ) & type_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FAMTerminator ( Var_src , Var_trg ) <=> rel_terminator_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) . | ||
50 | fof ( oppositeReference_from_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( type_InformationLink_class ( Var_src ) & type_FunctionalOutput_class ( Var_trg ) ) => ( rel_from_reference_InformationLink ( Var_src , Var_trg ) <=> rel_outgoingLinks_reference_FunctionalOutput ( Var_trg , Var_src ) ) ) ) . | ||
51 | fof ( oppositeReference_to_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( type_InformationLink_class ( Var_src ) & type_FunctionalInput_class ( Var_trg ) ) => ( rel_to_reference_InformationLink ( Var_src , Var_trg ) <=> rel_IncomingLinks_reference_FunctionalInput ( Var_trg , Var_src ) ) ) ) . | ||
52 | fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalInterface_class ( Var_src ) & type_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FunctionalInterface ( Var_src , Var_trg ) <=> rel_interface_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) . | ||
53 | fof ( lowerMultiplicity_type_Function , axiom , ! [ Var_src ] : ( type_Function_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionType_enum ( Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_1 ) ) ) ) . | ||
54 | fof ( upperMultiplicity_type_Function , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_Function_class ( Var_src ) & ( type_FunctionType_enum ( Var_trg_1 ) & type_FunctionType_enum ( Var_trg_2 ) ) ) => ( ( rel_type_attribute_Function ( Var_src , Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | ||
55 | fof ( errorpattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation , axiom , ! [ Var_p0 , Var_p1 ] : ( ( type_FAMTerminator_class ( Var_p0 ) & type_InformationLink_class ( Var_p1 ) ) => ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation ( Var_p0 , Var_p1 ) ) ) . | ||