diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-09-08 16:12:55 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:42:29 -0400 |
commit | 4aee5bcc86b9e6b515fbbdac030df42147be7dc1 (patch) | |
tree | ce9f8aa1cf0ab33d4304b9ce3a0abf4beb7b757a /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output | |
parent | VAMPIRE: complete first version of VampireModelInterpretation (diff) | |
download | VIATRA-Generator-4aee5bcc86b9e6b515fbbdac030df42147be7dc1.tar.gz VIATRA-Generator-4aee5bcc86b9e6b515fbbdac030df42147be7dc1.tar.zst VIATRA-Generator-4aee5bcc86b9e6b515fbbdac030df42147be7dc1.zip |
VAMPIRE: Implement wf constraint handling
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output')
-rw-r--r-- | Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem | 68 |
1 files changed, 66 insertions, 2 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 dcbb21eb..fe14bb31 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,5 +1,5 @@ | |||
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"> | 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" subtypes="//@types.10 //@types.11" isAbstract="true"/> |
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"/> |
@@ -496,6 +496,22 @@ | |||
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"> | ||
500 | <value xsi:type="language_1:Forall"> | ||
501 | <quantifiedVariables name="p0"> | ||
502 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | ||
503 | </quantifiedVariables> | ||
504 | <quantifiedVariables name="p1"> | ||
505 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | ||
506 | </quantifiedVariables> | ||
507 | <expression xsi:type="language_1:Not"> | ||
508 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15"> | ||
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"/> | ||
511 | </operand> | ||
512 | </expression> | ||
513 | </value> | ||
514 | </assertions> | ||
499 | <relations xsi:type="language_1:RelationDeclaration" name="interface reference FunctionalElement"> | 515 | <relations xsi:type="language_1:RelationDeclaration" name="interface reference FunctionalElement"> |
500 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | 516 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> |
501 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.5"/> | 517 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.5"/> |
@@ -556,11 +572,57 @@ | |||
556 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | 572 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> |
557 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | 573 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> |
558 | </relations> | 574 | </relations> |
575 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.19"> | ||
576 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | ||
577 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | ||
578 | <variables name="parameter T"> | ||
579 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | ||
580 | </variables> | ||
581 | <variables name="parameter I"> | ||
582 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | ||
583 | </variables> | ||
584 | <value xsi:type="language_1:Or"> | ||
585 | <operands xsi:type="language_1:Exists"> | ||
586 | <quantifiedVariables name="variable Out"> | ||
587 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.7"/> | ||
588 | </quantifiedVariables> | ||
589 | <expression xsi:type="language_1:And"> | ||
590 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.11"> | ||
591 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/> | ||
592 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | ||
593 | </operands> | ||
594 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | ||
595 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/> | ||
596 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> | ||
597 | </operands> | ||
598 | </expression> | ||
599 | </operands> | ||
600 | <operands xsi:type="language_1:Exists"> | ||
601 | <quantifiedVariables name="variable In"> | ||
602 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.6"/> | ||
603 | </quantifiedVariables> | ||
604 | <expression xsi:type="language_1:And"> | ||
605 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.7"> | ||
606 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | ||
607 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/> | ||
608 | </operands> | ||
609 | <operands xsi:type="language_1:InstanceOf"> | ||
610 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/> | ||
611 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.6"/> | ||
612 | </operands> | ||
613 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | ||
614 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/> | ||
615 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> | ||
616 | </operands> | ||
617 | </expression> | ||
618 | </operands> | ||
619 | </value> | ||
620 | </relations> | ||
559 | <elements name="Root literal FunctionType" definedInType="//@types.9"/> | 621 | <elements name="Root literal FunctionType" definedInType="//@types.9"/> |
560 | <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/> | 622 | <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/> |
561 | <elements name="Leaf literal FunctionType" definedInType="//@types.9"/> | 623 | <elements name="Leaf literal FunctionType" definedInType="//@types.9"/> |
562 | <elements name="o 1" definedInType="//@types.10"/> | 624 | <elements name="o 1" definedInType="//@types.10"/> |
563 | <containmentHierarchies typesOrderedInHierarchy="//@types.5 //@types.4 //@types.3 //@types.6 //@types.7 //@types.8 //@types.1 //@types.0 //@types.2 //@types.10 //@types.11" containmentRelations="//@relations.0 //@relations.3 //@relations.4 //@relations.8 //@relations.11 //@relations.12"/> | 625 | <containmentHierarchies typesOrderedInHierarchy="//@types.4 //@types.5 //@types.2 //@types.3 //@types.7 //@types.6 //@types.8 //@types.0 //@types.1 //@types.10 //@types.11" containmentRelations="//@relations.0 //@relations.3 //@relations.4 //@relations.8 //@relations.11 //@relations.12"/> |
564 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.0" relation="//@relations.0" upper="1"/> | 626 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.0" relation="//@relations.0" upper="1"/> |
565 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.1" relation="//@relations.1" lower="1"/> | 627 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.1" relation="//@relations.1" lower="1"/> |
566 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.2" relation="//@relations.1" upper="1"/> | 628 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.2" relation="//@relations.1" upper="1"/> |
@@ -580,4 +642,6 @@ | |||
580 | <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/> | 642 | <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/> |
581 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/> | 643 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/> |
582 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/> | 644 | <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"/> | ||
646 | <annotations xsi:type="viatra2logicannotations:TransformedViatraWellformednessConstraint" target="//@assertions.19" query="//@annotations.19"/> | ||
583 | </language:LogicProblem> | 647 | </language:LogicProblem> |