aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test
diff options
context:
space:
mode:
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF3
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem2
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp50
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml10
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend97
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend99
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend117
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend98
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbinbin6358 -> 6358 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbinbin4068 -> 6825 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbinbin4115 -> 6088 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbinbin8623 -> 6456 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbinbin4054 -> 6042 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java107
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java102
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java107
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java99
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbinbin4997 -> 4997 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbinbin687 -> 687 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbinbin6500 -> 6500 bytes
20 files changed, 567 insertions, 324 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF
index 1995ee52..2ea274a4 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF
@@ -4,7 +4,8 @@ Bundle-Name: Test
4Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.test;singleton:=true 4Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.test;singleton:=true
5Bundle-Version: 1.0.0.qualifier 5Bundle-Version: 1.0.0.qualifier
6Export-Package: ca.mcgill.ecse.dslreasoner.vampire.queries 6Export-Package: ca.mcgill.ecse.dslreasoner.vampire.queries
7Require-Bundle: org.eclipse.emf.ecore, 7Require-Bundle: org.eclipse.viatra.addon.querybasedfeatures.runtime,
8 org.eclipse.emf.ecore,
8 org.eclipse.viatra.query.runtime.rete, 9 org.eclipse.viatra.query.runtime.rete,
9 org.eclipse.viatra.query.runtime.localsearch, 10 org.eclipse.viatra.query.runtime.localsearch,
10 com.google.guava, 11 com.google.guava,
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 85e09a0a..18e58ab0 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
@@ -557,7 +557,7 @@
557 <elements name="Root literal FunctionType" definedInType="//@types.9"/> 557 <elements name="Root literal FunctionType" definedInType="//@types.9"/>
558 <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/> 558 <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/>
559 <elements name="Leaf literal FunctionType" definedInType="//@types.9"/> 559 <elements name="Leaf literal FunctionType" definedInType="//@types.9"/>
560 <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"/> 560 <containmentHierarchies typesOrderedInHierarchy="//@types.8 //@types.5 //@types.4 //@types.6 //@types.1 //@types.7 //@types.3 //@types.2 //@types.0" containmentRelations="//@relations.0 //@relations.3 //@relations.4 //@relations.8 //@relations.11 //@relations.12"/>
561 <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.0" relation="//@relations.0" upper="1"/> 561 <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.0" relation="//@relations.0" upper="1"/>
562 <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.1" relation="//@relations.1" lower="1"/> 562 <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.1" relation="//@relations.1" lower="1"/>
563 <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.2" relation="//@relations.1" upper="1"/> 563 <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.2" relation="//@relations.1" upper="1"/>
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 b4bb6700..3d49d42c 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
@@ -4,41 +4,21 @@ fof ( enumScope_FunctionType_Root , axiom , ! [ A ] : ( A = eo1 <=> e_Root_Funct
4fof ( enumScope_FunctionType_Intermediate , axiom , ! [ A ] : ( A = eo2 <=> e_Intermediate_FunctionType ( A ) ) ) . 4fof ( enumScope_FunctionType_Intermediate , axiom , ! [ A ] : ( A = eo2 <=> e_Intermediate_FunctionType ( A ) ) ) .
5fof ( enumScope_FunctionType_Leaf , axiom , ! [ A ] : ( A = eo3 <=> e_Leaf_FunctionType ( A ) ) ) . 5fof ( enumScope_FunctionType_Leaf , axiom , ! [ A ] : ( A = eo3 <=> e_Leaf_FunctionType ( A ) ) ) .
6fof ( notObjectHandler , axiom , ! [ A ] : ( ~ object ( A ) <=> ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) ) ) . 6fof ( notObjectHandler , axiom , ! [ A ] : ( ~ object ( A ) <=> ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) ) ) .
7fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FAMTerminator ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . 7fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalOutput ( A ) & ( t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
8fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = eo1 | ( A = eo2 | A = eo3 ) ) ) ) ) ) => object ( A ) ) ) . 8fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = eo1 | ( A = eo2 | A = eo3 ) ) ) ) ) ) => object ( A ) ) ) .
9fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = eo1 | ( A = eo2 | ( A = eo3 | ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | ( A = o6 | ( A = o7 | ( A = o8 | ( A = o9 | ( A = o10 | ( A = o11 | ( A = o12 | ( A = o13 | ( A = o14 | ( A = o15 | ( A = o16 | ( A = o17 | ( A = o18 | ( A = o19 | ( A = o20 | ( A = o21 | ( A = o22 | ( A = o23 | ( A = o24 | A = o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . 9fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = eo1 | ( A = eo2 | ( A = eo3 | ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) ) ) ) .
10fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o2 | A = o3 ) => ( t_FunctionalInterface ( A ) & object ( A ) ) ) ) . 10fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( A = o2 => ( t_Function ( A ) & object ( A ) ) ) ) .
11fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( A = o4 => ( t_Function ( A ) & object ( A ) ) ) ) . 11fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( ( A = o3 | ( A = o4 | A = o5 ) ) => ( t_FunctionalOutput ( A ) & object ( A ) ) ) ) .
12fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( ( A = o5 | ( A = o6 | A = o7 ) ) => ( t_FunctionalOutput ( A ) & object ( A ) ) ) ) . 12fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o6 | A = o7 ) => ( t_FunctionalInterface ( A ) & object ( A ) ) ) ) .
13fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( ( t_Function ( A ) & object ( A ) ) => ( A = o4 | ( A = o8 | ( A = o9 | ( A = o10 | A = o11 ) ) ) ) ) ) . 13fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( ( t_Function ( A ) & object ( A ) ) => A = o2 ) ) .
14fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( ( t_FunctionalOutput ( A ) & object ( A ) ) => ( A = o5 | ( A = o6 | ( A = o7 | A = o8 ) ) ) ) ) . 14fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( ( t_FunctionalOutput ( A ) & object ( A ) ) => ( A = o3 | ( A = o4 | A = o5 ) ) ) ) .
15fof ( t_uniqueness_eo1 , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo1 != o1 & ( eo1 != o2 & ( eo1 != o3 & ( eo1 != o4 & ( eo1 != o5 & ( eo1 != o6 & ( eo1 != o7 & ( eo1 != o8 & ( eo1 != o9 & ( eo1 != o10 & ( eo1 != o11 & ( eo1 != o12 & ( eo1 != o13 & ( eo1 != o14 & ( eo1 != o15 & ( eo1 != o16 & ( eo1 != o17 & ( eo1 != o18 & ( eo1 != o19 & ( eo1 != o20 & ( eo1 != o21 & ( eo1 != o22 & ( eo1 != o23 & ( eo1 != o24 & eo1 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . 15fof ( t_uniqueness_eo1 , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo1 != o1 & ( eo1 != o2 & ( eo1 != o3 & ( eo1 != o4 & eo1 != o5 ) ) ) ) ) ) .
16fof ( t_uniqueness_eo2 , axiom , eo2 != eo3 & ( eo2 != o1 & ( eo2 != o2 & ( eo2 != o3 & ( eo2 != o4 & ( eo2 != o5 & ( eo2 != o6 & ( eo2 != o7 & ( eo2 != o8 & ( eo2 != o9 & ( eo2 != o10 & ( eo2 != o11 & ( eo2 != o12 & ( eo2 != o13 & ( eo2 != o14 & ( eo2 != o15 & ( eo2 != o16 & ( eo2 != o17 & ( eo2 != o18 & ( eo2 != o19 & ( eo2 != o20 & ( eo2 != o21 & ( eo2 != o22 & ( eo2 != o23 & ( eo2 != o24 & eo2 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . 16fof ( t_uniqueness_eo2 , axiom , eo2 != eo3 & ( eo2 != o1 & ( eo2 != o2 & ( eo2 != o3 & ( eo2 != o4 & eo2 != o5 ) ) ) ) ) .
17fof ( t_uniqueness_eo3 , axiom , eo3 != o1 & ( eo3 != o2 & ( eo3 != o3 & ( eo3 != o4 & ( eo3 != o5 & ( eo3 != o6 & ( eo3 != o7 & ( eo3 != o8 & ( eo3 != o9 & ( eo3 != o10 & ( eo3 != o11 & ( eo3 != o12 & ( eo3 != o13 & ( eo3 != o14 & ( eo3 != o15 & ( eo3 != o16 & ( eo3 != o17 & ( eo3 != o18 & ( eo3 != o19 & ( eo3 != o20 & ( eo3 != o21 & ( eo3 != o22 & ( eo3 != o23 & ( eo3 != o24 & eo3 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . 17fof ( t_uniqueness_eo3 , axiom , eo3 != o1 & ( eo3 != o2 & ( eo3 != o3 & ( eo3 != o4 & eo3 != o5 ) ) ) ) .
18fof ( t_uniqueness_o1 , axiom , o1 != o2 & ( o1 != o3 & ( o1 != o4 & ( o1 != o5 & ( o1 != o6 & ( o1 != o7 & ( o1 != o8 & ( o1 != o9 & ( o1 != o10 & ( o1 != o11 & ( o1 != o12 & ( o1 != o13 & ( o1 != o14 & ( o1 != o15 & ( o1 != o16 & ( o1 != o17 & ( o1 != o18 & ( o1 != o19 & ( o1 != o20 & ( o1 != o21 & ( o1 != o22 & ( o1 != o23 & ( o1 != o24 & o1 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . 18fof ( t_uniqueness_o1 , axiom , o1 != o2 & ( o1 != o3 & ( o1 != o4 & o1 != o5 ) ) ) .
19fof ( t_uniqueness_o2 , axiom , o2 != o3 & ( o2 != o4 & ( o2 != o5 & ( o2 != o6 & ( o2 != o7 & ( o2 != o8 & ( o2 != o9 & ( o2 != o10 & ( o2 != o11 & ( o2 != o12 & ( o2 != o13 & ( o2 != o14 & ( o2 != o15 & ( o2 != o16 & ( o2 != o17 & ( o2 != o18 & ( o2 != o19 & ( o2 != o20 & ( o2 != o21 & ( o2 != o22 & ( o2 != o23 & ( o2 != o24 & o2 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . 19fof ( t_uniqueness_o2 , axiom , o2 != o3 & ( o2 != o4 & o2 != o5 ) ) .
20fof ( t_uniqueness_o3 , axiom , o3 != o4 & ( o3 != o5 & ( o3 != o6 & ( o3 != o7 & ( o3 != o8 & ( o3 != o9 & ( o3 != o10 & ( o3 != o11 & ( o3 != o12 & ( o3 != o13 & ( o3 != o14 & ( o3 != o15 & ( o3 != o16 & ( o3 != o17 & ( o3 != o18 & ( o3 != o19 & ( o3 != o20 & ( o3 != o21 & ( o3 != o22 & ( o3 != o23 & ( o3 != o24 & o3 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . 20fof ( t_uniqueness_o3 , axiom , o3 != o4 & o3 != o5 ) .
21fof ( t_uniqueness_o4 , axiom , o4 != o5 & ( o4 != o6 & ( o4 != o7 & ( o4 != o8 & ( o4 != o9 & ( o4 != o10 & ( o4 != o11 & ( o4 != o12 & ( o4 != o13 & ( o4 != o14 & ( o4 != o15 & ( o4 != o16 & ( o4 != o17 & ( o4 != o18 & ( o4 != o19 & ( o4 != o20 & ( o4 != o21 & ( o4 != o22 & ( o4 != o23 & ( o4 != o24 & o4 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . 21fof ( t_uniqueness_o4 , axiom , o4 != o5 ) .
22fof ( t_uniqueness_o5 , axiom , o5 != o6 & ( o5 != o7 & ( o5 != o8 & ( o5 != o9 & ( o5 != o10 & ( o5 != o11 & ( o5 != o12 & ( o5 != o13 & ( o5 != o14 & ( o5 != o15 & ( o5 != o16 & ( o5 != o17 & ( o5 != o18 & ( o5 != o19 & ( o5 != o20 & ( o5 != o21 & ( o5 != o22 & ( o5 != o23 & ( o5 != o24 & o5 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
23fof ( t_uniqueness_o6 , axiom , o6 != o7 & ( o6 != o8 & ( o6 != o9 & ( o6 != o10 & ( o6 != o11 & ( o6 != o12 & ( o6 != o13 & ( o6 != o14 & ( o6 != o15 & ( o6 != o16 & ( o6 != o17 & ( o6 != o18 & ( o6 != o19 & ( o6 != o20 & ( o6 != o21 & ( o6 != o22 & ( o6 != o23 & ( o6 != o24 & o6 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
24fof ( t_uniqueness_o7 , axiom , o7 != o8 & ( o7 != o9 & ( o7 != o10 & ( o7 != o11 & ( o7 != o12 & ( o7 != o13 & ( o7 != o14 & ( o7 != o15 & ( o7 != o16 & ( o7 != o17 & ( o7 != o18 & ( o7 != o19 & ( o7 != o20 & ( o7 != o21 & ( o7 != o22 & ( o7 != o23 & ( o7 != o24 & o7 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
25fof ( t_uniqueness_o8 , axiom , o8 != o9 & ( o8 != o10 & ( o8 != o11 & ( o8 != o12 & ( o8 != o13 & ( o8 != o14 & ( o8 != o15 & ( o8 != o16 & ( o8 != o17 & ( o8 != o18 & ( o8 != o19 & ( o8 != o20 & ( o8 != o21 & ( o8 != o22 & ( o8 != o23 & ( o8 != o24 & o8 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
26fof ( t_uniqueness_o9 , axiom , o9 != o10 & ( o9 != o11 & ( o9 != o12 & ( o9 != o13 & ( o9 != o14 & ( o9 != o15 & ( o9 != o16 & ( o9 != o17 & ( o9 != o18 & ( o9 != o19 & ( o9 != o20 & ( o9 != o21 & ( o9 != o22 & ( o9 != o23 & ( o9 != o24 & o9 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
27fof ( t_uniqueness_o10 , axiom , o10 != o11 & ( o10 != o12 & ( o10 != o13 & ( o10 != o14 & ( o10 != o15 & ( o10 != o16 & ( o10 != o17 & ( o10 != o18 & ( o10 != o19 & ( o10 != o20 & ( o10 != o21 & ( o10 != o22 & ( o10 != o23 & ( o10 != o24 & o10 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
28fof ( t_uniqueness_o11 , axiom , o11 != o12 & ( o11 != o13 & ( o11 != o14 & ( o11 != o15 & ( o11 != o16 & ( o11 != o17 & ( o11 != o18 & ( o11 != o19 & ( o11 != o20 & ( o11 != o21 & ( o11 != o22 & ( o11 != o23 & ( o11 != o24 & o11 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) .
29fof ( t_uniqueness_o12 , axiom , o12 != o13 & ( o12 != o14 & ( o12 != o15 & ( o12 != o16 & ( o12 != o17 & ( o12 != o18 & ( o12 != o19 & ( o12 != o20 & ( o12 != o21 & ( o12 != o22 & ( o12 != o23 & ( o12 != o24 & o12 != o25 ) ) ) ) ) ) ) ) ) ) ) ) .
30fof ( t_uniqueness_o13 , axiom , o13 != o14 & ( o13 != o15 & ( o13 != o16 & ( o13 != o17 & ( o13 != o18 & ( o13 != o19 & ( o13 != o20 & ( o13 != o21 & ( o13 != o22 & ( o13 != o23 & ( o13 != o24 & o13 != o25 ) ) ) ) ) ) ) ) ) ) ) .
31fof ( t_uniqueness_o14 , axiom , o14 != o15 & ( o14 != o16 & ( o14 != o17 & ( o14 != o18 & ( o14 != o19 & ( o14 != o20 & ( o14 != o21 & ( o14 != o22 & ( o14 != o23 & ( o14 != o24 & o14 != o25 ) ) ) ) ) ) ) ) ) ) .
32fof ( t_uniqueness_o15 , axiom , o15 != o16 & ( o15 != o17 & ( o15 != o18 & ( o15 != o19 & ( o15 != o20 & ( o15 != o21 & ( o15 != o22 & ( o15 != o23 & ( o15 != o24 & o15 != o25 ) ) ) ) ) ) ) ) ) .
33fof ( t_uniqueness_o16 , axiom , o16 != o17 & ( o16 != o18 & ( o16 != o19 & ( o16 != o20 & ( o16 != o21 & ( o16 != o22 & ( o16 != o23 & ( o16 != o24 & o16 != o25 ) ) ) ) ) ) ) ) .
34fof ( t_uniqueness_o17 , axiom , o17 != o18 & ( o17 != o19 & ( o17 != o20 & ( o17 != o21 & ( o17 != o22 & ( o17 != o23 & ( o17 != o24 & o17 != o25 ) ) ) ) ) ) ) .
35fof ( t_uniqueness_o18 , axiom , o18 != o19 & ( o18 != o20 & ( o18 != o21 & ( o18 != o22 & ( o18 != o23 & ( o18 != o24 & o18 != o25 ) ) ) ) ) ) .
36fof ( t_uniqueness_o19 , axiom , o19 != o20 & ( o19 != o21 & ( o19 != o22 & ( o19 != o23 & ( o19 != o24 & o19 != o25 ) ) ) ) ) .
37fof ( t_uniqueness_o20 , axiom , o20 != o21 & ( o20 != o22 & ( o20 != o23 & ( o20 != o24 & o20 != o25 ) ) ) ) .
38fof ( t_uniqueness_o21 , axiom , o21 != o22 & ( o21 != o23 & ( o21 != o24 & o21 != o25 ) ) ) .
39fof ( t_uniqueness_o22 , axiom , o22 != o23 & ( o22 != o24 & o22 != o25 ) ) .
40fof ( t_uniqueness_o23 , axiom , o23 != o24 & o23 != o25 ) .
41fof ( t_uniqueness_o24 , axiom , o24 != o25 ) .
42fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . 22fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
43fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) . 23fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) .
44fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) . 24fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) .
@@ -64,8 +44,8 @@ fof ( containment_noDup_r_terminator_FunctionalData , axiom , ? [ A , B ] : ( r_
64fof ( containment_t_FunctionalElement , axiom , ! [ A ] : ( t_FunctionalElement ( A ) => ? [ B ] : ( ( r_rootElements_FunctionalArchitectureModel ( B , A ) & ~ r_subElements_Function ( B , A ) ) | ( ~ r_rootElements_FunctionalArchitectureModel ( B , A ) & r_subElements_Function ( B , A ) ) ) ) ) . 44fof ( containment_t_FunctionalElement , axiom , ! [ A ] : ( t_FunctionalElement ( A ) => ? [ B ] : ( ( r_rootElements_FunctionalArchitectureModel ( B , A ) & ~ r_subElements_Function ( B , A ) ) | ( ~ r_rootElements_FunctionalArchitectureModel ( B , A ) & r_subElements_Function ( B , A ) ) ) ) ) .
65fof ( containment_t_FunctionalData , axiom , ! [ A ] : ( t_FunctionalData ( A ) => ? [ B ] : r_data_FunctionalInterface ( B , A ) ) ) . 45fof ( containment_t_FunctionalData , axiom , ! [ A ] : ( t_FunctionalData ( A ) => ? [ B ] : r_data_FunctionalInterface ( B , A ) ) ) .
66fof ( containment_t_InformationLink , axiom , ! [ A ] : ( t_InformationLink ( A ) => ? [ B ] : r_outgoingLinks_FunctionalOutput ( B , A ) ) ) . 46fof ( containment_t_InformationLink , axiom , ! [ A ] : ( t_InformationLink ( A ) => ? [ B ] : r_outgoingLinks_FunctionalOutput ( B , A ) ) ) .
67fof ( containment_t_FAMTerminator , axiom , ! [ A ] : ( t_FAMTerminator ( A ) => ? [ B ] : r_terminator_FunctionalData ( B , A ) ) ) .
68fof ( containment_t_FunctionalInterface , axiom , ! [ A ] : ( t_FunctionalInterface ( A ) => ? [ B ] : r_interface_FunctionalElement ( B , A ) ) ) . 47fof ( containment_t_FunctionalInterface , axiom , ! [ A ] : ( t_FunctionalInterface ( A ) => ? [ B ] : r_interface_FunctionalElement ( B , A ) ) ) .
48fof ( containment_t_FAMTerminator , axiom , ! [ A ] : ( t_FAMTerminator ( A ) => ? [ B ] : r_terminator_FunctionalData ( B , A ) ) ) .
69fof ( containment_noCycle_1 , axiom , ~ ? [ V1 ] : ( r_interface_FunctionalElement ( V1 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V1 ) | ( r_subElements_Function ( V1 , V1 ) | ( r_data_FunctionalInterface ( V1 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V1 ) | r_terminator_FunctionalData ( V1 , V1 ) ) ) ) ) ) ) . 49fof ( containment_noCycle_1 , axiom , ~ ? [ V1 ] : ( r_interface_FunctionalElement ( V1 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V1 ) | ( r_subElements_Function ( V1 , V1 ) | ( r_data_FunctionalInterface ( V1 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V1 ) | r_terminator_FunctionalData ( V1 , V1 ) ) ) ) ) ) ) .
70fof ( containment_noCycle_2 , axiom , ~ ? [ V1 , V2 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V2 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V1 ) | ( r_subElements_Function ( V2 , V1 ) | ( r_data_FunctionalInterface ( V2 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V1 ) | r_terminator_FunctionalData ( V2 , V1 ) ) ) ) ) ) ) ) . 50fof ( containment_noCycle_2 , axiom , ~ ? [ V1 , V2 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V2 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V1 ) | ( r_subElements_Function ( V2 , V1 ) | ( r_data_FunctionalInterface ( V2 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V1 ) | r_terminator_FunctionalData ( V2 , V1 ) ) ) ) ) ) ) ) .
71fof ( containment_noCycle_3 , axiom , ~ ? [ V1 , V2 , V3 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V2 , V3 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V3 ) | ( r_subElements_Function ( V2 , V3 ) | ( r_data_FunctionalInterface ( V2 , V3 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V3 ) | r_terminator_FunctionalData ( V2 , V3 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V3 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V3 , V1 ) | ( r_subElements_Function ( V3 , V1 ) | ( r_data_FunctionalInterface ( V3 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V3 , V1 ) | r_terminator_FunctionalData ( V3 , V1 ) ) ) ) ) ) ) ) ) . 51fof ( containment_noCycle_3 , axiom , ~ ? [ V1 , V2 , V3 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V2 , V3 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V3 ) | ( r_subElements_Function ( V2 , V3 ) | ( r_data_FunctionalInterface ( V2 , V3 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V3 ) | r_terminator_FunctionalData ( V2 , V3 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V3 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V3 , V1 ) | ( r_subElements_Function ( V3 , V1 ) | ( r_data_FunctionalInterface ( V3 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V3 , V1 ) | r_terminator_FunctionalData ( V3 , V1 ) ) ) ) ) ) ) ) ) .
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml
index 38efb459..3770f0af 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml
@@ -4,4 +4,14 @@
4 <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation"/> 4 <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation"/>
5 </group> 5 </group>
6 </extension> 6 </extension>
7 <extension id="ca.mcgill.ecse.dslreasoner.vampire.queries.FileSystemPatterns" point="org.eclipse.viatra.query.runtime.queryspecification">
8 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:ca.mcgill.ecse.dslreasoner.vampire.queries.FileSystemPatterns" id="ca.mcgill.ecse.dslreasoner.vampire.queries.FileSystemPatterns">
9 <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.patternContent"/>
10 <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.live"/>
11 <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.contentInNotLive"/>
12 </group>
13 </extension>
14 <extension id="extension.derived.ca.mcgill.ecse.dslreasoner.vampire.queries.live" point="org.eclipse.viatra.query.runtime.base.wellbehaving.derived.features">
15 <wellbehaving-derived-feature classifier-name="FileSystem" feature-name="live" package-nsUri="FileSystemMetamodel"/>
16 </extension>
7</plugin> 17</plugin>
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
index ef2e0c2f..f66ad93c 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
@@ -1,36 +1,115 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse 1package ca.mcgill.ecse.dslreasoner.vampire.icse
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns 3import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
6import functionalarchitecture.Function
7import functionalarchitecture.FunctionalInterface
8import functionalarchitecture.FunctionalOutput
4import functionalarchitecture.FunctionalarchitecturePackage 9import functionalarchitecture.FunctionalarchitecturePackage
10import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
11import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
13import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
14import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
15import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
16import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
5import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 17import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
6import java.util.LinkedList 18import java.util.HashMap
7import org.eclipse.emf.ecore.EObject
8import org.eclipse.emf.ecore.resource.Resource 19import org.eclipse.emf.ecore.resource.Resource
9import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 20import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
10 21
11class FAMTest { 22class FAMTest {
12 def static void main(String[] args) { 23 def static void main(String[] args) {
13 //Workspace setup 24 val Ecore2Logic ecore2Logic = new Ecore2Logic
25 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
26 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
27
28 // Workspace setup
14 val inputs = new FileSystemWorkspace('''initialModels/''', "") 29 val inputs = new FileSystemWorkspace('''initialModels/''', "")
15 val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") 30 val workspace = new FileSystemWorkspace('''output/FAMTest/''', "")
16 workspace.initAndClear 31 workspace.initAndClear
17 32
18 //Logicproblem writing setup 33 // Logicproblem writing setup
19 val reg = Resource.Factory.Registry.INSTANCE 34 val reg = Resource.Factory.Registry.INSTANCE
20 val map = reg.extensionToFactoryMap 35 val map = reg.extensionToFactoryMap
21 map.put("logicproblem", new XMIResourceFactoryImpl) 36 map.put("logicproblem", new XMIResourceFactoryImpl)
22
23 37
24 println("Input and output workspaces are created") 38 println("Input and output workspaces are created")
25 39
40 // Load DSL
26 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) 41 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE)
27 val partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi") 42 val partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi")
28 val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) 43 val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance)
29 44
30 println("DSL loaded") 45 println("DSL loaded")
46
47 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
48 var problem = modelGenerationProblem.output
49// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
50// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
51 workspace.writeModel(problem, "Fam.logicproblem")
52
53 println("Problem created")
54
55 //Start Time
56 var startTime = System.currentTimeMillis
57
58 var LogicReasoner reasoner
59 // *
60 reasoner = new VampireSolver
61
62 // /////////////////////////////////////////////////////
63 // Minimum Scope
64 val classMapMin = new HashMap<Class, Integer>
65 classMapMin.put(Function, 1)
66 classMapMin.put(FunctionalInterface, 2)
67 classMapMin.put(FunctionalOutput, 3)
31 68
32 GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) 69 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace)
70
71 // Maximum Scope
72 val classMapMax = new HashMap<Class, Integer>
73 classMapMax.put(Function, 5)
74 classMapMax.put(FunctionalInterface, 2)
75 classMapMax.put(FunctionalOutput, 4)
76
77 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace)
78
79 // Define Config File
80 val vampireConfig = new VampireSolverConfiguration => [
81 // add configuration things, in config file first
82 it.documentationLevel = DocumentationLevel::FULL
83
84 it.typeScopes.minNewElements = 4
85 it.typeScopes.maxNewElements = 5
86 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin
87 if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax
88 it.contCycleLevel = 5
89 it.uniquenessDuplicates = false
90 ]
91
92 var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace)
93
94 /*/
95 *
96 * reasoner = new AlloySolver
97 * val alloyConfig = new AlloySolverConfiguration => [
98 * it.typeScopes.maxNewElements = 7
99 * it.typeScopes.minNewElements = 3
100 * it.solutionScope.numberOfRequiredSolution = 1
101 * it.typeScopes.maxNewIntegers = 0
102 * it.documentationLevel = DocumentationLevel::NORMAL
103 * ]
104 * solution = reasoner.solve(problem, alloyConfig, workspace)
105 //*/
106 // /////////////////////////////////////////////////////
107
108 var totalTimeMin = (System.currentTimeMillis - startTime) / 60000
109 var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60
110
111 println("Problem solved")
112 println("Time was: " + totalTimeMin + ":" + totalTimeSec)
33 } 113 }
34 114
35
36} 115}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend
index 363b9356..50639577 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend
@@ -1,33 +1,108 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse 1package ca.mcgill.ecse.dslreasoner.vampire.icse
2 2
3import functionalarchitecture.FunctionalarchitecturePackage 3import ca.mcgill.ecse.dslreasoner.vampire.queries
4import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns 4import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.filesystemPackage
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
9import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
10import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
11import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
12import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
5import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 14import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
15import java.util.HashMap
6import org.eclipse.emf.ecore.resource.Resource 16import org.eclipse.emf.ecore.resource.Resource
7import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 17import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
8 18
9class FileSystemTest { 19class FileSystemTest {
10 def static void main(String[] args) { 20 def static void main(String[] args) {
11 //Workspace setup 21 val Ecore2Logic ecore2Logic = new Ecore2Logic
22 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
23 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
24
25 // Workspace setup
12 val inputs = new FileSystemWorkspace('''initialModels/''', "") 26 val inputs = new FileSystemWorkspace('''initialModels/''', "")
13 val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") 27 val workspace = new FileSystemWorkspace('''output/FAMTest/''', "")
14 workspace.initAndClear 28 workspace.initAndClear
15 29
16 //Logicproblem writing setup 30 // Logicproblem writing setup
17 val reg = Resource.Factory.Registry.INSTANCE 31 val reg = Resource.Factory.Registry.INSTANCE
18 val map = reg.extensionToFactoryMap 32 val map = reg.extensionToFactoryMap
19 map.put("logicproblem", new XMIResourceFactoryImpl) 33 map.put("logicproblem", new XMIResourceFactoryImpl)
20 34
21 println("Input and output workspaces are created") 35 println("Input and output workspaces are created")
22 36
23 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) 37 val metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE)
24 val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi") 38 val partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi")
25 val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) 39 //val queries = GeneralTest.loadQueries(metamodel, FileSystemPatterns.instance)
26 40
27 println("DSL loaded") 41 println("DSL loaded")
28 42
29 GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) 43 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
44 var problem = modelGenerationProblem.output
45// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
46// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
47 workspace.writeModel(problem, "Fam.logicproblem")
48
49 println("Problem created")
50
51 // Start Time
52 var startTime = System.currentTimeMillis
53
54 var LogicReasoner reasoner
55 // *
56 reasoner = new VampireSolver
57
58 // /////////////////////////////////////////////////////
59 // Minimum Scope
60 val classMapMin = new HashMap<Class, Integer>
61// classMapMin.put(Function, 1)
62// classMapMin.put(FunctionalInterface, 2)
63// classMapMin.put(FunctionalOutput, 3)
64 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace)
65
66 // Maximum Scope
67 val classMapMax = new HashMap<Class, Integer>
68// classMapMax.put(Function, 5)
69// classMapMax.put(FunctionalInterface, 2)
70// classMapMax.put(FunctionalOutput, 4)
71 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace)
72
73 // Define Config File
74 val vampireConfig = new VampireSolverConfiguration => [
75 // add configuration things, in config file first
76 it.documentationLevel = DocumentationLevel::FULL
77
78 it.typeScopes.minNewElements = 4
79 it.typeScopes.maxNewElements = 5
80 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin
81 if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax
82 it.contCycleLevel = 5
83 it.uniquenessDuplicates = false
84 ]
85
86 var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace)
87
88 /*/
89 *
90 * reasoner = new AlloySolver
91 * val alloyConfig = new AlloySolverConfiguration => [
92 * it.typeScopes.maxNewElements = 7
93 * it.typeScopes.minNewElements = 3
94 * it.solutionScope.numberOfRequiredSolution = 1
95 * it.typeScopes.maxNewIntegers = 0
96 * it.documentationLevel = DocumentationLevel::NORMAL
97 * ]
98 * solution = reasoner.solve(problem, alloyConfig, workspace)
99 //*/
100 // /////////////////////////////////////////////////////
101 var totalTimeMin = (System.currentTimeMillis - startTime) / 60000
102 var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60
103
104 println("Problem solved")
105 println("Time was: " + totalTimeMin + ":" + totalTimeSec)
30 } 106 }
31 107
32
33} 108}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
index 949abe87..89375801 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
@@ -1,25 +1,14 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse 1package ca.mcgill.ecse.dslreasoner.vampire.icse
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
6import functionalarchitecture.Function
7import functionalarchitecture.FunctionalInterface
8import functionalarchitecture.FunctionalOutput
9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic 3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
10import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration 4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
11import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor 5import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type 6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
14import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
15import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
16import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
17import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor 7import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
19import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
20import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 8import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
21import java.util.HashMap 9import java.util.HashMap
22import java.util.List 10import java.util.List
11import java.util.Map
23import org.eclipse.emf.ecore.EAttribute 12import org.eclipse.emf.ecore.EAttribute
24import org.eclipse.emf.ecore.EClass 13import org.eclipse.emf.ecore.EClass
25import org.eclipse.emf.ecore.EEnum 14import org.eclipse.emf.ecore.EEnum
@@ -30,100 +19,18 @@ import org.eclipse.emf.ecore.EReference
30import org.eclipse.emf.ecore.resource.Resource 19import org.eclipse.emf.ecore.resource.Resource
31import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 20import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
32import org.eclipse.viatra.query.runtime.api.IQueryGroup 21import org.eclipse.viatra.query.runtime.api.IQueryGroup
33import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
34 22
35class GeneralTest { 23class GeneralTest {
36 def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List<EObject> partialModel, 24 def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel, Ecore2Logic e2l, Ecore2Logic_Trace trace) {
37 ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) { 25 val typeMap = new HashMap<Type, Integer>
38 val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE 26 val listMap = metamodel.classes.toMap[s|s.name]
39 val Ecore2Logic ecore2Logic = new Ecore2Logic
40 val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic)
41 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
42 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
43
44 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
45 var problem = modelGenerationProblem.output
46// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
47// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
48 workspace.writeModel(problem, "Fam.logicproblem")
49
50 println("Problem created")
51
52 var startTime = System.currentTimeMillis
53
54 var LogicResult solution
55 var LogicReasoner reasoner
56
57 // *
58 reasoner = new VampireSolver
59
60 // Setting up scope
61 val typeMapMin = new HashMap<Type, Integer>
62 val typeMapMax = new HashMap<Type, Integer>
63 val list2MapMin = metamodel.classes.toMap[s|s.name]
64 val list2MapMax = metamodel.classes.toMap[s|s.name]
65
66 // Minimum Scope
67 typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace,
68 list2MapMin.get(Function.simpleName)
69 ), 1)
70 typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace,
71 list2MapMin.get(FunctionalInterface.simpleName)
72 ), 2)
73 typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace,
74 list2MapMin.get(FunctionalOutput.simpleName)
75 ), 3)
76
77 // Maximum Scope
78 typeMapMax.put(ecore2Logic.TypeofEClass(
79 modelGenerationProblem.trace,
80 list2MapMax.get(Function.simpleName)
81 ), 5)
82 typeMapMax.put(ecore2Logic.TypeofEClass(
83 modelGenerationProblem.trace,
84 list2MapMax.get(FunctionalInterface.simpleName)
85 ), 2)
86 typeMapMax.put(ecore2Logic.TypeofEClass(
87 modelGenerationProblem.trace,
88 list2MapMax.get(FunctionalOutput.simpleName)
89 ), 4)
90
91 // Configuration
92 val vampireConfig = new VampireSolverConfiguration => [
93 // add configuration things, in config file first
94 it.documentationLevel = DocumentationLevel::FULL
95 it.typeScopes.minNewElements = 4
96 it.typeScopes.maxNewElements = 25
97 it.typeScopes.minNewElementsByType = typeMapMin
98 it.typeScopes.maxNewElementsByType = typeMapMax
99 it.contCycleLevel = 5
100 it.uniquenessDuplicates = false
101 ]
102 solution = reasoner.solve(problem, vampireConfig, workspace)
103
104 /*/
105 *
106 * reasoner = new AlloySolver
107 * val alloyConfig = new AlloySolverConfiguration => [
108 * it.typeScopes.maxNewElements = 7
109 * it.typeScopes.minNewElements = 3
110 * it.solutionScope.numberOfRequiredSolution = 1
111 * it.typeScopes.maxNewIntegers = 0
112 * it.documentationLevel = DocumentationLevel::NORMAL
113 * ]
114 * solution = reasoner.solve(problem, alloyConfig, workspace)
115 //*/
116
117
118 var totalTimeMin = (System.currentTimeMillis - startTime)/60000
119 var totalTimeSec = ((System.currentTimeMillis - startTime)/1000)% 60
120
121 println("Problem solved")
122 println("Time was: " + totalTimeMin + ":" + totalTimeSec)
123
124
125
126 27
28 for (Class elem : classMap.keySet) {
29 typeMap.put(e2l.TypeofEClass(
30 trace, listMap.get(elem.simpleName)
31 ), classMap.get(elem))
32 }
33 return typeMap
127 } 34 }
128 35
129 def static loadMetamodel(EPackage pckg) { 36 def static loadMetamodel(EPackage pckg) {
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
index eb3f4b14..1fac968b 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
@@ -1,34 +1,108 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse 1package ca.mcgill.ecse.dslreasoner.vampire.icse
2 2
3import functionalarchitecture.FunctionalarchitecturePackage 3import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
6import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
8import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
9import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
10import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
11import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
4import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 13import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
14import java.util.HashMap
5import org.eclipse.emf.ecore.resource.Resource 15import org.eclipse.emf.ecore.resource.Resource
6import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 16import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
7import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage
8import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.queries.YakinduPatterns
9 17
10class YakinduTest { 18class YakinduTest {
11 def static void main(String[] args) { 19 def static void main(String[] args) {
12 //Workspace setup 20 val Ecore2Logic ecore2Logic = new Ecore2Logic
21 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
22 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
23
24 // Workspace setup
13 val inputs = new FileSystemWorkspace('''initialModels/''', "") 25 val inputs = new FileSystemWorkspace('''initialModels/''', "")
14 val workspace = new FileSystemWorkspace('''output/YakinduTest/''', "") 26 val workspace = new FileSystemWorkspace('''output/YakinduTest/''', "")
15 workspace.initAndClear 27 workspace.initAndClear
16 28
17 //Logicproblem writing setup 29 // Logicproblem writing setup
18 val reg = Resource.Factory.Registry.INSTANCE 30 val reg = Resource.Factory.Registry.INSTANCE
19 val map = reg.extensionToFactoryMap 31 val map = reg.extensionToFactoryMap
20 map.put("logicproblem", new XMIResourceFactoryImpl) 32 map.put("logicproblem", new XMIResourceFactoryImpl)
21 33
22 println("Input and output workspaces are created") 34 println("Input and output workspaces are created")
23 35
24 val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE) 36 val metamodel = GeneralTest.loadMetamodel(yakinduPackage.eINSTANCE)
25 val partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi") 37 val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/yakinduinstance.xmi")
26// val queries = GeneralTest.loadQueries(metamodel, FamPa 38// val queries = GeneralTest.loadQueries(metamodel, FamPa
39 val queries = null
27 40
28 println("DSL loaded") 41 println("DSL loaded")
29 42
30// GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) 43 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
44 var problem = modelGenerationProblem.output
45// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
46// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
47 workspace.writeModel(problem, "Yakindu.logicproblem")
48
49 println("Problem created")
50
51 // Start Time
52 var startTime = System.currentTimeMillis
53
54 var LogicReasoner reasoner
55 // *
56 reasoner = new VampireSolver
57
58 // /////////////////////////////////////////////////////
59 // Minimum Scope
60 val classMapMin = new HashMap<Class, Integer>
61// classMapMin.put(Function, 1)
62// classMapMin.put(FunctionalInterface, 2)
63// classMapMin.put(FunctionalOutput, 3)
64 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace)
65
66 // Maximum Scope
67 val classMapMax = new HashMap<Class, Integer>
68// classMapMax.put(Function, 5)
69// classMapMax.put(FunctionalInterface, 2)
70// classMapMax.put(FunctionalOutput, 4)
71 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace)
72
73 // Define Config File
74 val vampireConfig = new VampireSolverConfiguration => [
75 // add configuration things, in config file first
76 it.documentationLevel = DocumentationLevel::FULL
77
78 it.typeScopes.minNewElements = 20
79 it.typeScopes.maxNewElements = 30
80 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin
81 if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax
82 it.contCycleLevel = 5
83 it.uniquenessDuplicates = false
84 ]
85
86 var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace)
87
88 /*/
89 *
90 * reasoner = new AlloySolver
91 * val alloyConfig = new AlloySolverConfiguration => [
92 * it.typeScopes.maxNewElements = 7
93 * it.typeScopes.minNewElements = 3
94 * it.solutionScope.numberOfRequiredSolution = 1
95 * it.typeScopes.maxNewIntegers = 0
96 * it.documentationLevel = DocumentationLevel::NORMAL
97 * ]
98 * solution = reasoner.solve(problem, alloyConfig, workspace)
99 //*/
100 // /////////////////////////////////////////////////////
101 var totalTimeMin = (System.currentTimeMillis - startTime) / 60000
102 var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60
103
104 println("Problem solved")
105 println("Time was: " + totalTimeMin + ":" + totalTimeSec)
31 } 106 }
32 107
33
34} 108}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
index 7f92eba4..55d90ac7 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
index 67bf34bd..8eeb2d28 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
index 093855d8..ab6aaf6e 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
index 2df2ba62..cd75a66c 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
index 0c97e8d1..1b920064 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
index 7b4bb578..5fc2a391 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
@@ -2,37 +2,110 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse;
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; 3import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;
4import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns; 4import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
7import functionalarchitecture.Function;
8import functionalarchitecture.FunctionalOutput;
5import functionalarchitecture.FunctionalarchitecturePackage; 9import functionalarchitecture.FunctionalarchitecturePackage;
10import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;
11import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration;
12import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace;
6import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; 13import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;
14import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
15import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
16import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
18import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
19import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
20import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;
7import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; 21import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor;
22import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic;
8import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; 23import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
24import java.util.HashMap;
9import java.util.Map; 25import java.util.Map;
10import org.eclipse.emf.common.util.EList; 26import org.eclipse.emf.common.util.EList;
11import org.eclipse.emf.ecore.EObject; 27import org.eclipse.emf.ecore.EObject;
12import org.eclipse.emf.ecore.resource.Resource; 28import org.eclipse.emf.ecore.resource.Resource;
13import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; 29import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
14import org.eclipse.xtend2.lib.StringConcatenation; 30import org.eclipse.xtend2.lib.StringConcatenation;
31import org.eclipse.xtext.xbase.lib.Exceptions;
15import org.eclipse.xtext.xbase.lib.InputOutput; 32import org.eclipse.xtext.xbase.lib.InputOutput;
33import org.eclipse.xtext.xbase.lib.ObjectExtensions;
34import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
16 35
17@SuppressWarnings("all") 36@SuppressWarnings("all")
18public class FAMTest { 37public class FAMTest {
19 public static void main(final String[] args) { 38 public static void main(final String[] args) {
20 StringConcatenation _builder = new StringConcatenation(); 39 try {
21 _builder.append("initialModels/"); 40 final Ecore2Logic ecore2Logic = new Ecore2Logic();
22 final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); 41 final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic);
23 StringConcatenation _builder_1 = new StringConcatenation(); 42 final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();
24 _builder_1.append("output/FAMTest/"); 43 StringConcatenation _builder = new StringConcatenation();
25 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); 44 _builder.append("initialModels/");
26 workspace.initAndClear(); 45 final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), "");
27 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; 46 StringConcatenation _builder_1 = new StringConcatenation();
28 final Map<String, Object> map = reg.getExtensionToFactoryMap(); 47 _builder_1.append("output/FAMTest/");
29 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); 48 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), "");
30 map.put("logicproblem", _xMIResourceFactoryImpl); 49 workspace.initAndClear();
31 InputOutput.<String>println("Input and output workspaces are created"); 50 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;
32 final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE); 51 final Map<String, Object> map = reg.getExtensionToFactoryMap();
33 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi"); 52 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();
34 final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance()); 53 map.put("logicproblem", _xMIResourceFactoryImpl);
35 InputOutput.<String>println("DSL loaded"); 54 InputOutput.<String>println("Input and output workspaces are created");
36 GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace); 55 final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE);
56 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi");
57 final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance());
58 InputOutput.<String>println("DSL loaded");
59 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();
60 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);
61 LogicProblem problem = modelGenerationProblem.getOutput();
62 workspace.writeModel(problem, "Fam.logicproblem");
63 InputOutput.<String>println("Problem created");
64 long startTime = System.currentTimeMillis();
65 LogicReasoner reasoner = null;
66 VampireSolver _vampireSolver = new VampireSolver();
67 reasoner = _vampireSolver;
68 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();
69 classMapMin.put(Function.class, Integer.valueOf(1));
70 classMapMin.put(functionalarchitecture.FunctionalInterface.class, Integer.valueOf(2));
71 classMapMin.put(FunctionalOutput.class, Integer.valueOf(3));
72 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
73 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();
74 classMapMax.put(Function.class, Integer.valueOf(5));
75 classMapMax.put(functionalarchitecture.FunctionalInterface.class, Integer.valueOf(2));
76 classMapMax.put(FunctionalOutput.class, Integer.valueOf(4));
77 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
78 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
79 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
80 it.documentationLevel = DocumentationLevel.FULL;
81 it.typeScopes.minNewElements = 4;
82 it.typeScopes.maxNewElements = 5;
83 int _size = typeMapMin.size();
84 boolean _notEquals = (_size != 0);
85 if (_notEquals) {
86 it.typeScopes.minNewElementsByType = typeMapMin;
87 }
88 int _size_1 = typeMapMin.size();
89 boolean _notEquals_1 = (_size_1 != 0);
90 if (_notEquals_1) {
91 it.typeScopes.maxNewElementsByType = typeMapMax;
92 }
93 it.contCycleLevel = 5;
94 it.uniquenessDuplicates = false;
95 };
96 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
97 LogicResult solution = reasoner.solve(problem, vampireConfig, workspace);
98 long _currentTimeMillis = System.currentTimeMillis();
99 long _minus = (_currentTimeMillis - startTime);
100 long totalTimeMin = (_minus / 60000);
101 long _currentTimeMillis_1 = System.currentTimeMillis();
102 long _minus_1 = (_currentTimeMillis_1 - startTime);
103 long _divide = (_minus_1 / 1000);
104 long totalTimeSec = (_divide % 60);
105 InputOutput.<String>println("Problem solved");
106 InputOutput.<String>println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec)));
107 } catch (Throwable _e) {
108 throw Exceptions.sneakyThrow(_e);
109 }
37 } 110 }
38} 111}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java
index 5994b4b4..eedec995 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java
@@ -1,38 +1,100 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse; 1package ca.mcgill.ecse.dslreasoner.vampire.icse;
2 2
3import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.filesystemPackage;
3import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; 4import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;
4import functionalarchitecture.FunctionalarchitecturePackage; 5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
5import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns; 6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;
8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration;
9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace;
6import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; 10import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;
7import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; 11import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
13import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
15import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
16import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
17import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic;
8import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; 19import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
20import java.util.HashMap;
9import java.util.Map; 21import java.util.Map;
10import org.eclipse.emf.common.util.EList; 22import org.eclipse.emf.common.util.EList;
11import org.eclipse.emf.ecore.EObject; 23import org.eclipse.emf.ecore.EObject;
12import org.eclipse.emf.ecore.resource.Resource; 24import org.eclipse.emf.ecore.resource.Resource;
13import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; 25import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
14import org.eclipse.xtend2.lib.StringConcatenation; 26import org.eclipse.xtend2.lib.StringConcatenation;
27import org.eclipse.xtext.xbase.lib.Exceptions;
15import org.eclipse.xtext.xbase.lib.InputOutput; 28import org.eclipse.xtext.xbase.lib.InputOutput;
29import org.eclipse.xtext.xbase.lib.ObjectExtensions;
30import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
16 31
17@SuppressWarnings("all") 32@SuppressWarnings("all")
18public class FileSystemTest { 33public class FileSystemTest {
19 public static void main(final String[] args) { 34 public static void main(final String[] args) {
20 StringConcatenation _builder = new StringConcatenation(); 35 try {
21 _builder.append("initialModels/"); 36 final Ecore2Logic ecore2Logic = new Ecore2Logic();
22 final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); 37 final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic);
23 StringConcatenation _builder_1 = new StringConcatenation(); 38 final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();
24 _builder_1.append("output/FAMTest/"); 39 StringConcatenation _builder = new StringConcatenation();
25 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); 40 _builder.append("initialModels/");
26 workspace.initAndClear(); 41 final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), "");
27 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; 42 StringConcatenation _builder_1 = new StringConcatenation();
28 final Map<String, Object> map = reg.getExtensionToFactoryMap(); 43 _builder_1.append("output/FAMTest/");
29 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); 44 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), "");
30 map.put("logicproblem", _xMIResourceFactoryImpl); 45 workspace.initAndClear();
31 InputOutput.<String>println("Input and output workspaces are created"); 46 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;
32 final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE); 47 final Map<String, Object> map = reg.getExtensionToFactoryMap();
33 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi"); 48 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();
34 final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance()); 49 map.put("logicproblem", _xMIResourceFactoryImpl);
35 InputOutput.<String>println("DSL loaded"); 50 InputOutput.<String>println("Input and output workspaces are created");
36 GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace); 51 final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE);
52 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi");
53 InputOutput.<String>println("DSL loaded");
54 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();
55 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);
56 LogicProblem problem = modelGenerationProblem.getOutput();
57 workspace.writeModel(problem, "Fam.logicproblem");
58 InputOutput.<String>println("Problem created");
59 long startTime = System.currentTimeMillis();
60 LogicReasoner reasoner = null;
61 VampireSolver _vampireSolver = new VampireSolver();
62 reasoner = _vampireSolver;
63 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();
64 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
65 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();
66 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
67 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
68 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
69 it.documentationLevel = DocumentationLevel.FULL;
70 it.typeScopes.minNewElements = 4;
71 it.typeScopes.maxNewElements = 5;
72 int _size = typeMapMin.size();
73 boolean _notEquals = (_size != 0);
74 if (_notEquals) {
75 it.typeScopes.minNewElementsByType = typeMapMin;
76 }
77 int _size_1 = typeMapMin.size();
78 boolean _notEquals_1 = (_size_1 != 0);
79 if (_notEquals_1) {
80 it.typeScopes.maxNewElementsByType = typeMapMax;
81 }
82 it.contCycleLevel = 5;
83 it.uniquenessDuplicates = false;
84 };
85 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
86 LogicResult solution = reasoner.solve(problem, vampireConfig, workspace);
87 long _currentTimeMillis = System.currentTimeMillis();
88 long _minus = (_currentTimeMillis - startTime);
89 long totalTimeMin = (_minus / 60000);
90 long _currentTimeMillis_1 = System.currentTimeMillis();
91 long _minus_1 = (_currentTimeMillis_1 - startTime);
92 long _divide = (_minus_1 / 1000);
93 long totalTimeSec = (_divide % 60);
94 InputOutput.<String>println("Problem solved");
95 InputOutput.<String>println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec)));
96 } catch (Throwable _e) {
97 throw Exceptions.sneakyThrow(_e);
98 }
37 } 99 }
38} 100}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
index 0150ef1d..0bb8f76e 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
@@ -1,27 +1,12 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse; 1package ca.mcgill.ecse.dslreasoner.vampire.icse;
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
6import com.google.common.base.Objects; 3import com.google.common.base.Objects;
7import com.google.common.collect.Iterables; 4import com.google.common.collect.Iterables;
8import functionalarchitecture.Function;
9import functionalarchitecture.FunctionalOutput;
10import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; 5import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;
11import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration;
12import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; 6import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace;
13import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; 7import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;
14import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
15import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
16import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; 8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
18import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
19import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
20import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore;
21import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;
22import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; 9import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor;
23import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic;
24import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
25import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; 10import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
26import java.util.Collections; 11import java.util.Collections;
27import java.util.HashMap; 12import java.util.HashMap;
@@ -43,94 +28,24 @@ import org.eclipse.viatra.query.runtime.api.IQueryGroup;
43import org.eclipse.viatra.query.runtime.api.IQuerySpecification; 28import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
44import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; 29import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation;
45import org.eclipse.xtext.xbase.lib.CollectionLiterals; 30import org.eclipse.xtext.xbase.lib.CollectionLiterals;
46import org.eclipse.xtext.xbase.lib.Exceptions;
47import org.eclipse.xtext.xbase.lib.Extension;
48import org.eclipse.xtext.xbase.lib.Functions.Function1; 31import org.eclipse.xtext.xbase.lib.Functions.Function1;
49import org.eclipse.xtext.xbase.lib.InputOutput;
50import org.eclipse.xtext.xbase.lib.IterableExtensions; 32import org.eclipse.xtext.xbase.lib.IterableExtensions;
51import org.eclipse.xtext.xbase.lib.ListExtensions; 33import org.eclipse.xtext.xbase.lib.ListExtensions;
52import org.eclipse.xtext.xbase.lib.ObjectExtensions;
53import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
54 34
55@SuppressWarnings("all") 35@SuppressWarnings("all")
56public class GeneralTest { 36public class GeneralTest {
57 public static String createAndSolveProblem(final EcoreMetamodelDescriptor metamodel, final List<EObject> partialModel, final ViatraQuerySetDescriptor queries, final FileSystemWorkspace workspace) { 37 public static Map<Type, Integer> getTypeMap(final Map<Class, Integer> classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) {
58 try { 38 final HashMap<Type, Integer> typeMap = new HashMap<Type, Integer>();
59 String _xblockexpression = null; 39 final Function1<EClass, String> _function = (EClass s) -> {
60 { 40 return s.getName();
61 @Extension 41 };
62 final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; 42 final Map<String, EClass> listMap = IterableExtensions.<String, EClass>toMap(metamodel.getClasses(), _function);
63 final Ecore2Logic ecore2Logic = new Ecore2Logic(); 43 Set<Class> _keySet = classMap.keySet();
64 final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic); 44 for (final Class elem : _keySet) {
65 final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); 45 typeMap.put(
66 final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); 46 e2l.TypeofEClass(trace, listMap.get(elem.getSimpleName())), classMap.get(elem));
67 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();
68 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);
69 LogicProblem problem = modelGenerationProblem.getOutput();
70 workspace.writeModel(problem, "Fam.logicproblem");
71 InputOutput.<String>println("Problem created");
72 long startTime = System.currentTimeMillis();
73 LogicResult solution = null;
74 LogicReasoner reasoner = null;
75 VampireSolver _vampireSolver = new VampireSolver();
76 reasoner = _vampireSolver;
77 final HashMap<Type, Integer> typeMapMin = new HashMap<Type, Integer>();
78 final HashMap<Type, Integer> typeMapMax = new HashMap<Type, Integer>();
79 final Function1<EClass, String> _function = (EClass s) -> {
80 return s.getName();
81 };
82 final Map<String, EClass> list2MapMin = IterableExtensions.<String, EClass>toMap(metamodel.getClasses(), _function);
83 final Function1<EClass, String> _function_1 = (EClass s) -> {
84 return s.getName();
85 };
86 final Map<String, EClass> list2MapMax = IterableExtensions.<String, EClass>toMap(metamodel.getClasses(), _function_1);
87 typeMapMin.put(
88 ecore2Logic.TypeofEClass(modelGenerationProblem.getTrace(),
89 list2MapMin.get(Function.class.getSimpleName())), Integer.valueOf(1));
90 typeMapMin.put(
91 ecore2Logic.TypeofEClass(modelGenerationProblem.getTrace(),
92 list2MapMin.get(functionalarchitecture.FunctionalInterface.class.getSimpleName())), Integer.valueOf(2));
93 typeMapMin.put(
94 ecore2Logic.TypeofEClass(modelGenerationProblem.getTrace(),
95 list2MapMin.get(FunctionalOutput.class.getSimpleName())), Integer.valueOf(3));
96 typeMapMax.put(
97 ecore2Logic.TypeofEClass(
98 modelGenerationProblem.getTrace(),
99 list2MapMax.get(Function.class.getSimpleName())), Integer.valueOf(5));
100 typeMapMax.put(
101 ecore2Logic.TypeofEClass(
102 modelGenerationProblem.getTrace(),
103 list2MapMax.get(functionalarchitecture.FunctionalInterface.class.getSimpleName())), Integer.valueOf(2));
104 typeMapMax.put(
105 ecore2Logic.TypeofEClass(
106 modelGenerationProblem.getTrace(),
107 list2MapMax.get(FunctionalOutput.class.getSimpleName())), Integer.valueOf(4));
108 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
109 final Procedure1<VampireSolverConfiguration> _function_2 = (VampireSolverConfiguration it) -> {
110 it.documentationLevel = DocumentationLevel.FULL;
111 it.typeScopes.minNewElements = 4;
112 it.typeScopes.maxNewElements = 25;
113 it.typeScopes.minNewElementsByType = typeMapMin;
114 it.typeScopes.maxNewElementsByType = typeMapMax;
115 it.contCycleLevel = 5;
116 it.uniquenessDuplicates = false;
117 };
118 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function_2);
119 solution = reasoner.solve(problem, vampireConfig, workspace);
120 long _currentTimeMillis = System.currentTimeMillis();
121 long _minus = (_currentTimeMillis - startTime);
122 long totalTimeMin = (_minus / 60000);
123 long _currentTimeMillis_1 = System.currentTimeMillis();
124 long _minus_1 = (_currentTimeMillis_1 - startTime);
125 long _divide = (_minus_1 / 1000);
126 long totalTimeSec = (_divide % 60);
127 InputOutput.<String>println("Problem solved");
128 _xblockexpression = InputOutput.<String>println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec)));
129 }
130 return _xblockexpression;
131 } catch (Throwable _e) {
132 throw Exceptions.sneakyThrow(_e);
133 } 47 }
48 return typeMap;
134 } 49 }
135 50
136 public static EcoreMetamodelDescriptor loadMetamodel(final EPackage pckg) { 51 public static EcoreMetamodelDescriptor loadMetamodel(final EPackage pckg) {
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
index bea4e8a6..81079764 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
@@ -1,34 +1,101 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse; 1package ca.mcgill.ecse.dslreasoner.vampire.icse;
2 2
3import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage;
3import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; 4import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;
4import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage; 5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;
8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration;
9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace;
5import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; 10import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;
11import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
13import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
15import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
16import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
17import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic;
6import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; 19import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
20import java.util.HashMap;
7import java.util.Map; 21import java.util.Map;
8import org.eclipse.emf.common.util.EList; 22import org.eclipse.emf.common.util.EList;
9import org.eclipse.emf.ecore.EObject; 23import org.eclipse.emf.ecore.EObject;
10import org.eclipse.emf.ecore.resource.Resource; 24import org.eclipse.emf.ecore.resource.Resource;
11import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; 25import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
12import org.eclipse.xtend2.lib.StringConcatenation; 26import org.eclipse.xtend2.lib.StringConcatenation;
27import org.eclipse.xtext.xbase.lib.Exceptions;
13import org.eclipse.xtext.xbase.lib.InputOutput; 28import org.eclipse.xtext.xbase.lib.InputOutput;
29import org.eclipse.xtext.xbase.lib.ObjectExtensions;
30import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
14 31
15@SuppressWarnings("all") 32@SuppressWarnings("all")
16public class YakinduTest { 33public class YakinduTest {
17 public static void main(final String[] args) { 34 public static void main(final String[] args) {
18 StringConcatenation _builder = new StringConcatenation(); 35 try {
19 _builder.append("initialModels/"); 36 final Ecore2Logic ecore2Logic = new Ecore2Logic();
20 final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); 37 final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic);
21 StringConcatenation _builder_1 = new StringConcatenation(); 38 final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();
22 _builder_1.append("output/YakinduTest/"); 39 StringConcatenation _builder = new StringConcatenation();
23 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); 40 _builder.append("initialModels/");
24 workspace.initAndClear(); 41 final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), "");
25 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; 42 StringConcatenation _builder_1 = new StringConcatenation();
26 final Map<String, Object> map = reg.getExtensionToFactoryMap(); 43 _builder_1.append("output/YakinduTest/");
27 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); 44 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), "");
28 map.put("logicproblem", _xMIResourceFactoryImpl); 45 workspace.initAndClear();
29 InputOutput.<String>println("Input and output workspaces are created"); 46 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;
30 final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE); 47 final Map<String, Object> map = reg.getExtensionToFactoryMap();
31 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi"); 48 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();
32 InputOutput.<String>println("DSL loaded"); 49 map.put("logicproblem", _xMIResourceFactoryImpl);
50 InputOutput.<String>println("Input and output workspaces are created");
51 final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(yakinduPackage.eINSTANCE);
52 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/yakinduinstance.xmi");
53 final Object queries = null;
54 InputOutput.<String>println("DSL loaded");
55 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();
56 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);
57 LogicProblem problem = modelGenerationProblem.getOutput();
58 workspace.writeModel(problem, "Yakindu.logicproblem");
59 InputOutput.<String>println("Problem created");
60 long startTime = System.currentTimeMillis();
61 LogicReasoner reasoner = null;
62 VampireSolver _vampireSolver = new VampireSolver();
63 reasoner = _vampireSolver;
64 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();
65 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
66 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();
67 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
68 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
69 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
70 it.documentationLevel = DocumentationLevel.FULL;
71 it.typeScopes.minNewElements = 20;
72 it.typeScopes.maxNewElements = 30;
73 int _size = typeMapMin.size();
74 boolean _notEquals = (_size != 0);
75 if (_notEquals) {
76 it.typeScopes.minNewElementsByType = typeMapMin;
77 }
78 int _size_1 = typeMapMin.size();
79 boolean _notEquals_1 = (_size_1 != 0);
80 if (_notEquals_1) {
81 it.typeScopes.maxNewElementsByType = typeMapMax;
82 }
83 it.contCycleLevel = 5;
84 it.uniquenessDuplicates = false;
85 };
86 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
87 LogicResult solution = reasoner.solve(problem, vampireConfig, workspace);
88 long _currentTimeMillis = System.currentTimeMillis();
89 long _minus = (_currentTimeMillis - startTime);
90 long totalTimeMin = (_minus / 60000);
91 long _currentTimeMillis_1 = System.currentTimeMillis();
92 long _minus_1 = (_currentTimeMillis_1 - startTime);
93 long _divide = (_minus_1 / 1000);
94 long totalTimeSec = (_divide % 60);
95 InputOutput.<String>println("Problem solved");
96 InputOutput.<String>println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec)));
97 } catch (Throwable _e) {
98 throw Exceptions.sneakyThrow(_e);
99 }
33 } 100 }
34} 101}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
index c0481fd8..29f8df00 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
index 53dc2a03..72d33e5d 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
index 6c84f917..e9c4c0a4 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
Binary files differ
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-26 11:44:02 +0000