diff options
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem')
-rw-r--r-- | Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem | 181 |
1 files changed, 165 insertions, 16 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 fe14bb31..226150e8 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 | |||
@@ -496,7 +496,7 @@ | |||
496 | </expression> | 496 | </expression> |
497 | </value> | 497 | </value> |
498 | </assertions> | 498 | </assertions> |
499 | <assertions name="errorpattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.20"> | 499 | <assertions name="errorpattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.24"> |
500 | <value xsi:type="language_1:Forall"> | 500 | <value xsi:type="language_1:Forall"> |
501 | <quantifiedVariables name="p0"> | 501 | <quantifiedVariables name="p0"> |
502 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | 502 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> |
@@ -505,7 +505,7 @@ | |||
505 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | 505 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> |
506 | </quantifiedVariables> | 506 | </quantifiedVariables> |
507 | <expression xsi:type="language_1:Not"> | 507 | <expression xsi:type="language_1:Not"> |
508 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15"> | 508 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17"> |
509 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.0"/> | 509 | <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"/> | 510 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.1"/> |
511 | </operand> | 511 | </operand> |
@@ -572,7 +572,51 @@ | |||
572 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | 572 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> |
573 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | 573 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> |
574 | </relations> | 574 | </relations> |
575 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.19"> | 575 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam rootElements" annotations="//@annotations.19"> |
576 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
577 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
578 | <variables name="parameter Model"> | ||
579 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
580 | </variables> | ||
581 | <variables name="parameter Root"> | ||
582 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
583 | </variables> | ||
584 | <value xsi:type="language_1:Or"> | ||
585 | <operands xsi:type="language_1:And"> | ||
586 | <operands xsi:type="language_1:InstanceOf"> | ||
587 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | ||
588 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
589 | </operands> | ||
590 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.3"> | ||
591 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> | ||
592 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | ||
593 | </operands> | ||
594 | </operands> | ||
595 | </value> | ||
596 | </relations> | ||
597 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam model" annotations="//@annotations.20"> | ||
598 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | ||
599 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
600 | <variables name="parameter This"> | ||
601 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | ||
602 | </variables> | ||
603 | <variables name="parameter Target"> | ||
604 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
605 | </variables> | ||
606 | <value xsi:type="language_1:Or"> | ||
607 | <operands 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.0"/> | ||
611 | </operands> | ||
612 | <operands xsi:type="language_1:InstanceOf"> | ||
613 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@variables.1"/> | ||
614 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
615 | </operands> | ||
616 | </operands> | ||
617 | </value> | ||
618 | </relations> | ||
619 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.21"> | ||
576 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | 620 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> |
577 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | 621 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> |
578 | <variables name="parameter T"> | 622 | <variables name="parameter T"> |
@@ -588,12 +632,12 @@ | |||
588 | </quantifiedVariables> | 632 | </quantifiedVariables> |
589 | <expression xsi:type="language_1:And"> | 633 | <expression xsi:type="language_1:And"> |
590 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.11"> | 634 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.11"> |
591 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/> | 635 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.0/@quantifiedVariables.0"/> |
592 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | 636 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.1"/> |
593 | </operands> | 637 | </operands> |
594 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | 638 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> |
595 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/> | 639 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.0/@quantifiedVariables.0"/> |
596 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> | 640 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.0"/> |
597 | </operands> | 641 | </operands> |
598 | </expression> | 642 | </expression> |
599 | </operands> | 643 | </operands> |
@@ -603,16 +647,117 @@ | |||
603 | </quantifiedVariables> | 647 | </quantifiedVariables> |
604 | <expression xsi:type="language_1:And"> | 648 | <expression xsi:type="language_1:And"> |
605 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.7"> | 649 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.7"> |
606 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | 650 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.1"/> |
607 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/> | 651 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.1/@quantifiedVariables.0"/> |
652 | </operands> | ||
653 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | ||
654 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.1/@quantifiedVariables.0"/> | ||
655 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.0"/> | ||
656 | </operands> | ||
657 | </expression> | ||
658 | </operands> | ||
659 | </value> | ||
660 | </relations> | ||
661 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam parent" annotations="//@annotations.22"> | ||
662 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
663 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
664 | <variables name="parameter Func"> | ||
665 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
666 | </variables> | ||
667 | <variables name="parameter Par"> | ||
668 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
669 | </variables> | ||
670 | <value xsi:type="language_1:Or"> | ||
671 | <operands xsi:type="language_1:And"> | ||
672 | <operands xsi:type="language_1:InstanceOf"> | ||
673 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.0"/> | ||
674 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
675 | </operands> | ||
676 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.2"> | ||
677 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.0"/> | ||
678 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.1"/> | ||
679 | </operands> | ||
680 | <operands xsi:type="language_1:InstanceOf"> | ||
681 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.1"/> | ||
682 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
683 | </operands> | ||
684 | </operands> | ||
685 | </value> | ||
686 | </relations> | ||
687 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam type" annotations="//@annotations.23"> | ||
688 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
689 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | ||
690 | <variables name="parameter This"> | ||
691 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
692 | </variables> | ||
693 | <variables name="parameter Target"> | ||
694 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | ||
695 | </variables> | ||
696 | <value xsi:type="language_1:Or"> | ||
697 | <operands xsi:type="language_1:Exists"> | ||
698 | <quantifiedVariables name="variable Model"> | ||
699 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
700 | </quantifiedVariables> | ||
701 | <expression xsi:type="language_1:And"> | ||
702 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15"> | ||
703 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.0/@quantifiedVariables.0"/> | ||
704 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
705 | </operands> | ||
706 | <operands xsi:type="language_1:Equals"> | ||
707 | <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.1"/> | ||
708 | <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.0"/> | ||
608 | </operands> | 709 | </operands> |
710 | </expression> | ||
711 | </operands> | ||
712 | <operands xsi:type="language_1:Forall"> | ||
713 | <quantifiedVariables name="variable Child"> | ||
714 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
715 | </quantifiedVariables> | ||
716 | <quantifiedVariables name="variable Model"> | ||
717 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
718 | </quantifiedVariables> | ||
719 | <expression xsi:type="language_1:And"> | ||
609 | <operands xsi:type="language_1:InstanceOf"> | 720 | <operands xsi:type="language_1:InstanceOf"> |
610 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/> | 721 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> |
611 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.6"/> | 722 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> |
612 | </operands> | 723 | </operands> |
613 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | 724 | <operands xsi:type="language_1:Not"> |
614 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/> | 725 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18"> |
615 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> | 726 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.1/@quantifiedVariables.0"/> |
727 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
728 | </operand> | ||
729 | </operands> | ||
730 | <operands xsi:type="language_1:Not"> | ||
731 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15"> | ||
732 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.1/@quantifiedVariables.1"/> | ||
733 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
734 | </operand> | ||
735 | </operands> | ||
736 | <operands xsi:type="language_1:Equals"> | ||
737 | <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.1"/> | ||
738 | <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.2"/> | ||
739 | </operands> | ||
740 | </expression> | ||
741 | </operands> | ||
742 | <operands xsi:type="language_1:Exists"> | ||
743 | <quantifiedVariables name="variable Par"> | ||
744 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
745 | </quantifiedVariables> | ||
746 | <quantifiedVariables name="variable Child"> | ||
747 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
748 | </quantifiedVariables> | ||
749 | <expression xsi:type="language_1:And"> | ||
750 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18"> | ||
751 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
752 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.2/@quantifiedVariables.0"/> | ||
753 | </operands> | ||
754 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18"> | ||
755 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.2/@quantifiedVariables.1"/> | ||
756 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
757 | </operands> | ||
758 | <operands xsi:type="language_1:Equals"> | ||
759 | <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.1"/> | ||
760 | <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.1"/> | ||
616 | </operands> | 761 | </operands> |
617 | </expression> | 762 | </expression> |
618 | </operands> | 763 | </operands> |
@@ -642,6 +787,10 @@ | |||
642 | <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/> | 787 | <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/> |
643 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/> | 788 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/> |
644 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/> | 789 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/> |
645 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.15" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.terminatorAndInformation"/> | 790 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.15" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.rootElements"/> |
646 | <annotations xsi:type="viatra2logicannotations:TransformedViatraWellformednessConstraint" target="//@assertions.19" query="//@annotations.19"/> | 791 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.16" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.model"/> |
792 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.17" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.terminatorAndInformation"/> | ||
793 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.18" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.parent"/> | ||
794 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.19" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.type"/> | ||
795 | <annotations xsi:type="viatra2logicannotations:TransformedViatraWellformednessConstraint" target="//@assertions.19" query="//@annotations.21"/> | ||
647 | </language:LogicProblem> | 796 | </language:LogicProblem> |