VAMPIRE: last commit

author: ArenBabikian <aren.babikian@mail.mcgill.ca> 2020-02-03 15:20:02 -0500
committer: ArenBabikian <aren.babikian@mail.mcgill.ca> 2020-06-07 19:44:44 -0400
commit: 8e461ef60f59a2cb57ddca31a0b785c1b046e63a (patch)
tree: ff27d80e7fc391a155fe70c0bd46d6da028c4b37 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output
parent: VAMPIRE: Further Post-submission updates (diff)
download: VIATRA-Generator-8e461ef60f59a2cb57ddca31a0b785c1b046e63a.tar.gz
VIATRA-Generator-8e461ef60f59a2cb57ddca31a0b785c1b046e63a.tar.zst
VIATRA-Generator-8e461ef60f59a2cb57ddca31a0b785c1b046e63a.zip
1 files changed, 57 insertions, 5 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 f86a2f3c..48991faa 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 @@
 <?xml version="1.0" encoding="ASCII"?>
 <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">
  <types xsi:type="language_1:TypeDeclaration" name="FunctionalElement class" subtypes="//@types.2" isAbstract="true"/>
-  <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class" subtypes="//@types.10 //@types.11" isAbstract="true"/>
+  <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class"/>
  <types xsi:type="language_1:TypeDeclaration" name="Function class" supertypes="//@types.0"/>
  <types xsi:type="language_1:TypeDeclaration" name="FAMTerminator class"/>
  <types xsi:type="language_1:TypeDeclaration" name="InformationLink class"/>
@@ -10,8 +10,6 @@
  <types xsi:type="language_1:TypeDeclaration" name="FunctionalOutput class" supertypes="//@types.8"/>
  <types xsi:type="language_1:TypeDeclaration" name="FunctionalData class" subtypes="//@types.6 //@types.7" isAbstract="true"/>
  <types xsi:type="language_1:TypeDefinition" name="FunctionType enum" elements="//@elements.0 //@elements.1 //@elements.2"/>
-  <types xsi:type="language_1:TypeDefinition" name="FunctionalArchitectureModel class DefinedPart" supertypes="//@types.1" elements="//@elements.3"/>
-  <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class UndefinedPart" supertypes="//@types.1"/>
  <assertions name="upperMultiplicity interface FunctionalElement" annotations="//@annotations.0">
    <value xsi:type="language_1:Forall">
      <quantifiedVariables name="src">
@@ -496,6 +494,55 @@
      </expression>
    </value>
  </assertions>
+  <assertions name="lowerMultiplicity value FunctionalData" annotations="//@annotations.19">
+    <value xsi:type="language_1:Forall">
+      <quantifiedVariables name="src">
+        <range xsi:type="language_1:ComplexTypeReference" referred="//@types.8"/>
+      </quantifiedVariables>
+      <expression xsi:type="language_1:Exists">
+        <quantifiedVariables name="trg 1">
+          <range xsi:type="language_1:IntTypeReference"/>
+        </quantifiedVariables>
+        <expression xsi:type="language_1:And">
+          <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15">
+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.0"/>
+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@expression/@quantifiedVariables.0"/>
+          </operands>
+        </expression>
+      </expression>
+    </value>
+  </assertions>
+  <assertions name="upperMultiplicity value FunctionalData" annotations="//@annotations.20">
+    <value xsi:type="language_1:Forall">
+      <quantifiedVariables name="src">
+        <range xsi:type="language_1:ComplexTypeReference" referred="//@types.8"/>
+      </quantifiedVariables>
+      <quantifiedVariables name="trg 1">
+        <range xsi:type="language_1:IntTypeReference"/>
+      </quantifiedVariables>
+      <quantifiedVariables name="trg 2">
+        <range xsi:type="language_1:IntTypeReference"/>
+      </quantifiedVariables>
+      <expression xsi:type="language_1:Impl">
+        <leftOperand xsi:type="language_1:And">
+          <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15">
+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.20/@value/@quantifiedVariables.0"/>
+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.20/@value/@quantifiedVariables.1"/>
+          </operands>
+          <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15">
+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.20/@value/@quantifiedVariables.0"/>
+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.20/@value/@quantifiedVariables.2"/>
+          </operands>
+        </leftOperand>
+        <rightOperand xsi:type="language_1:Not">
+          <operand xsi:type="language_1:Distinct">
+            <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.20/@value/@quantifiedVariables.1"/>
+            <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.20/@value/@quantifiedVariables.2"/>
+          </operand>
+        </rightOperand>
+      </expression>
+    </value>
+  </assertions>
  <relations xsi:type="language_1:RelationDeclaration" name="interface reference FunctionalElement">
    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/>
    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.5"/>
@@ -556,11 +603,14 @@
    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>
    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/>
  </relations>
+  <relations xsi:type="language_1:RelationDeclaration" name="value attribute FunctionalData">
+    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.8"/>
+    <parameters xsi:type="language_1:IntTypeReference"/>
+  </relations>
  <elements name="Root literal FunctionType" definedInType="//@types.9"/>
  <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/>
  <elements name="Leaf literal FunctionType" definedInType="//@types.9"/>
-  <elements name="o 1" definedInType="//@types.10"/>
+  <containmentHierarchies typesOrderedInHierarchy="//@types.2 //@types.3 //@types.4 //@types.7 //@types.0 //@types.6 //@types.1 //@types.5 //@types.8" containmentRelations="//@relations.0 //@relations.3 //@relations.4 //@relations.8 //@relations.11 //@relations.12"/>
-  <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"/>
  <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.0" relation="//@relations.0" upper="1"/>
  <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.1" relation="//@relations.1" lower="1"/>
  <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.2" relation="//@relations.1" upper="1"/>
@@ -580,4 +630,6 @@
  <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/>
  <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/>
  <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/>
+  <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.19" relation="//@relations.15" lower="1"/>
+  <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.20" relation="//@relations.15" upper="1"/>
 </language:LogicProblem>
author	ArenBabikian <aren.babikian@mail.mcgill.ca>	2020-02-03 15:20:02 -0500
committer	ArenBabikian <aren.babikian@mail.mcgill.ca>	2020-06-07 19:44:44 -0400
commit	8e461ef60f59a2cb57ddca31a0b785c1b046e63a (patch)
tree	ff27d80e7fc391a155fe70c0bd46d6da028c4b37 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output
parent	VAMPIRE: Further Post-submission updates (diff)
download	VIATRA-Generator-8e461ef60f59a2cb57ddca31a0b785c1b046e63a.tar.gz VIATRA-Generator-8e461ef60f59a2cb57ddca31a0b785c1b046e63a.tar.zst VIATRA-Generator-8e461ef60f59a2cb57ddca31a0b785c1b046e63a.zip

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 f86a2f3c..48991faa 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">	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">
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,6 +494,55 @@
496	</expression>	494	</expression>
497	</value>	495	</value>
498	</assertions>	496	</assertions>
		497	<assertions name="lowerMultiplicity value FunctionalData" annotations="//@annotations.19">
		498	<value xsi:type="language_1:Forall">
		499	<quantifiedVariables name="src">
		500	<range xsi:type="language_1:ComplexTypeReference" referred="//@types.8"/>
		501	</quantifiedVariables>
		502	<expression xsi:type="language_1:Exists">
		503	<quantifiedVariables name="trg 1">
		504	<range xsi:type="language_1:IntTypeReference"/>
		505	</quantifiedVariables>
		506	<expression xsi:type="language_1:And">
		507	<operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15">
		508	<parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.0"/>
		509	<parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@expression/@quantifiedVariables.0"/>
		510	</operands>
		511	</expression>
		512	</expression>
		513	</value>
		514	</assertions>
		515	<assertions name="upperMultiplicity value FunctionalData" annotations="//@annotations.20">
		516	<value xsi:type="language_1:Forall">
		517	<quantifiedVariables name="src">
		518	<range xsi:type="language_1:ComplexTypeReference" referred="//@types.8"/>
		519	</quantifiedVariables>
		520	<quantifiedVariables name="trg 1">
		521	<range xsi:type="language_1:IntTypeReference"/>
		522	</quantifiedVariables>
		523	<quantifiedVariables name="trg 2">
		524	<range xsi:type="language_1:IntTypeReference"/>
		525	</quantifiedVariables>
		526	<expression xsi:type="language_1:Impl">
		527	<leftOperand xsi:type="language_1:And">
		528	<operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15">
		529	<parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.20/@value/@quantifiedVariables.0"/>
		530	<parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.20/@value/@quantifiedVariables.1"/>
		531	</operands>
		532	<operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15">
		533	<parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.20/@value/@quantifiedVariables.0"/>
		534	<parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.20/@value/@quantifiedVariables.2"/>
		535	</operands>
		536	</leftOperand>
		537	<rightOperand xsi:type="language_1:Not">
		538	<operand xsi:type="language_1:Distinct">
		539	<operands xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.20/@value/@quantifiedVariables.1"/>
		540	<operands xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.20/@value/@quantifiedVariables.2"/>
		541	</operand>
		542	</rightOperand>
		543	</expression>
		544	</value>
		545	</assertions>
499	<relations xsi:type="language_1:RelationDeclaration" name="interface reference FunctionalElement">	546	<relations xsi:type="language_1:RelationDeclaration" name="interface reference FunctionalElement">
500	<parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/>	547	<parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/>
501	<parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.5"/>	548	<parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.5"/>
@@ -556,11 +603,14 @@
556	<parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>	603	<parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>
557	<parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/>	604	<parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/>
558	</relations>	605	</relations>
		606	<relations xsi:type="language_1:RelationDeclaration" name="value attribute FunctionalData">
		607	<parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.8"/>
		608	<parameters xsi:type="language_1:IntTypeReference"/>
		609	</relations>
559	<elements name="Root literal FunctionType" definedInType="//@types.9"/>	610	<elements name="Root literal FunctionType" definedInType="//@types.9"/>
560	<elements name="Intermediate literal FunctionType" definedInType="//@types.9"/>	611	<elements name="Intermediate literal FunctionType" definedInType="//@types.9"/>
561	<elements name="Leaf literal FunctionType" definedInType="//@types.9"/>	612	<elements name="Leaf literal FunctionType" definedInType="//@types.9"/>
562	<elements name="o 1" definedInType="//@types.10"/>	613	<containmentHierarchies typesOrderedInHierarchy="//@types.2 //@types.3 //@types.4 //@types.7 //@types.0 //@types.6 //@types.1 //@types.5 //@types.8" containmentRelations="//@relations.0 //@relations.3 //@relations.4 //@relations.8 //@relations.11 //@relations.12"/>
563	<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"/>	614	<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"/>	615	<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"/>	616	<annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.2" relation="//@relations.1" upper="1"/>
@@ -580,4 +630,6 @@
580	<annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/>	630	<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"/>	631	<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"/>	632	<annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/>
		633	<annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.19" relation="//@relations.15" lower="1"/>
		634	<annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.20" relation="//@relations.15" upper="1"/>
583	</language:LogicProblem>	635	</language:LogicProblem>