aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-03-07 17:29:18 -0500
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-03-07 17:29:18 -0500
commit63cb743dacb8cd374777ba87783cbb96416d32e8 (patch)
treefee66ffc353ee9706c4bc333bb5092751f766051 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test
parentFix Enum handling for Paradox Integration (diff)
downloadVIATRA-Generator-63cb743dacb8cd374777ba87783cbb96416d32e8.tar.gz
VIATRA-Generator-63cb743dacb8cd374777ba87783cbb96416d32e8.tar.zst
VIATRA-Generator-63cb743dacb8cd374777ba87783cbb96416d32e8.zip
Improve TypeScope handling
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FaModel.xmi7
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp7
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend4
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend22
-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.xtendbinbin4155 -> 4068 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbinbin4115 -> 4115 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbinbin7580 -> 7398 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbinbin4054 -> 4054 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java6
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java7
-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
14 files changed, 37 insertions, 16 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FaModel.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FaModel.xmi
new file mode 100644
index 00000000..cef17e1b
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FaModel.xmi
@@ -0,0 +1,7 @@
1<?xml version="1.0" encoding="UTF-8"?>
2<functionalarchitecture:FunctionalArchitectureModel
3 xmi:version="2.0"
4 xmlns:xmi="http://www.omg.org/XMI"
5 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
6 xmlns:functionalarchitecture="http://www.inf.mit.bme.hu/viatrasolver/example/fam"
7 xsi:schemaLocation="http://www.inf.mit.bme.hu/viatrasolver/example/fam FAM/FamMetamodel.ecore"/>
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 a3b9c865..f55667e4 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
@@ -1,9 +1,10 @@
1% This is an initial Test Comment 1% This is an initial Test Comment
2fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) . 2fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) .
3fof ( enumScope_FunctionType , axiom , e_Root_FunctionType ( eo1 ) & ( ~ e_Intermediate_FunctionType ( eo1 ) & ( ~ e_Leaf_FunctionType ( eo1 ) & ( e_Intermediate_FunctionType ( eo2 ) & ( ~ e_Root_FunctionType ( eo2 ) & ( ~ e_Leaf_FunctionType ( eo2 ) & ( e_Leaf_FunctionType ( eo3 ) & ( ~ e_Root_FunctionType ( eo3 ) & ~ e_Intermediate_FunctionType ( eo3 ) ) ) ) ) ) ) ) ) . 3fof ( enumScope_FunctionType , axiom , e_Root_FunctionType ( eo1 ) & ( ~ e_Intermediate_FunctionType ( eo1 ) & ( ~ e_Leaf_FunctionType ( eo1 ) & ( e_Intermediate_FunctionType ( eo2 ) & ( ~ e_Root_FunctionType ( eo2 ) & ( ~ e_Leaf_FunctionType ( eo2 ) & ( e_Leaf_FunctionType ( eo3 ) & ( ~ e_Root_FunctionType ( eo3 ) & ~ e_Intermediate_FunctionType ( eo3 ) ) ) ) ) ) ) ) ) .
4fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FunctionalData ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & t_Function ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . 4fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( ~ t_FunctionType ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
5fof ( typeScope , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) => object ( A ) ) ) . 5fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | A = o3 ) ) => object ( A ) ) ) .
6fof ( typeUniqueness , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo2 != eo3 & ( eo1 != o1 & ( eo2 != o1 & ( eo3 != o1 & ( eo1 != o2 & ( eo2 != o2 & ( eo3 != o2 & ( o1 != o2 & ( eo1 != o3 & ( eo2 != o3 & ( eo3 != o3 & ( o1 != o3 & ( o2 != o3 & ( eo1 != o4 & ( eo2 != o4 & ( eo3 != o4 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( eo1 != o5 & ( eo2 != o5 & ( eo3 != o5 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & o4 != o5 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . 6fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | A = o6 ) ) ) ) ) ) ) .
7fof ( typeUniqueness , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo2 != eo3 & ( eo1 != o1 & ( eo2 != o1 & ( eo3 != o1 & ( eo1 != o2 & ( eo2 != o2 & ( eo3 != o2 & ( o1 != o2 & ( eo1 != o3 & ( eo2 != o3 & ( eo3 != o3 & ( o1 != o3 & ( o2 != o3 & ( eo1 != o4 & ( eo2 != o4 & ( eo3 != o4 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( eo1 != o5 & ( eo2 != o5 & ( eo3 != o5 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & ( o4 != o5 & ( eo1 != o6 & ( eo2 != o6 & ( eo3 != o6 & ( o1 != o6 & ( o2 != o6 & ( o3 != o6 & ( o4 != o6 & o5 != o6 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
7fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . 8fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
8fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) . 9fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) .
9fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) . 10fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) .
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 95bfd87a..a9314376 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
@@ -23,12 +23,12 @@ class FAMTest {
23 println("Input and output workspaces are created") 23 println("Input and output workspaces are created")
24 24
25 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) 25 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE)
26 val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel2.xmi") 26 val partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi")
27 val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) 27 val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance)
28 28
29 println("DSL loaded") 29 println("DSL loaded")
30 30
31 GeneralTest.createAndSolveProblem(metamodel, new LinkedList<EObject>, queries, workspace) 31 GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace)
32 } 32 }
33 33
34 34
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 20ad6119..40e305aa 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
@@ -2,19 +2,23 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver 3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration 4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
5import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns 5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
6import functionalarchitecture.Function
6import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic 7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration 8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
8import 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
9import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner 12import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
10import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult 14import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
11import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore 15import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
12import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic 16import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
13import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
14import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor 17import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
15import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic 18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
16import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 19import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
17import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 20import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
21import java.util.HashMap
18import java.util.List 22import java.util.List
19import org.eclipse.emf.ecore.EAttribute 23import org.eclipse.emf.ecore.EAttribute
20import org.eclipse.emf.ecore.EClass 24import org.eclipse.emf.ecore.EClass
@@ -26,13 +30,12 @@ import org.eclipse.emf.ecore.EReference
26import org.eclipse.emf.ecore.resource.Resource 30import org.eclipse.emf.ecore.resource.Resource
27import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 31import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
28import org.eclipse.viatra.query.runtime.api.IQueryGroup 32import org.eclipse.viatra.query.runtime.api.IQueryGroup
29import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver 33import org.eclipse.emf.ecore.EClassifier
30import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
31import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
32 34
33class GeneralTest { 35class GeneralTest {
34 def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List<EObject> partialModel, 36 def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List<EObject> partialModel,
35 ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) { 37 ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) {
38 val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
36 val Ecore2Logic ecore2Logic = new Ecore2Logic 39 val Ecore2Logic ecore2Logic = new Ecore2Logic
37 val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) 40 val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic)
38 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) 41 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
@@ -52,10 +55,17 @@ class GeneralTest {
52 55
53 //* 56 //*
54 reasoner = new VampireSolver 57 reasoner = new VampireSolver
58// val typeMap = new HashMap<Type, Integer>
59// val n = Function.simpleName
60// val classif = factory.vampireLanguagePackage.getEClassifier(n) as EClass
61// val x = ecore2Logic.TypeofEClass(modelGenerationProblem.trace, classif)
62// typeMap.put(x, 3)
55 val vampireConfig = new VampireSolverConfiguration => [ 63 val vampireConfig = new VampireSolverConfiguration => [
56 // add configuration things, in config file first 64 // add configuration things, in config file first
57 it.documentationLevel = DocumentationLevel::FULL 65 it.documentationLevel = DocumentationLevel::FULL
58 it.typeScopes.minNewElements = 5 66 it.typeScopes.minNewElements = 3
67 it.typeScopes.maxNewElements = 6
68// it.typeScopes.minNewElementsByType = typeMap
59 ] 69 ]
60 solution = reasoner.solve(problem, vampireConfig, workspace) 70 solution = reasoner.solve(problem, vampireConfig, workspace)
61 71
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 c9fd4467..620541af 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 9ded2f72..38c38fcd 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 2c84c402..dbe2934c 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 120f7cbb..86f98ad3 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 8364a369..91e71b1b 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 dd061008..7b4bb578 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
@@ -6,7 +6,6 @@ import functionalarchitecture.FunctionalarchitecturePackage;
6import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; 6import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;
7import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; 7import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor;
8import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; 8import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
9import java.util.LinkedList;
10import java.util.Map; 9import java.util.Map;
11import org.eclipse.emf.common.util.EList; 10import org.eclipse.emf.common.util.EList;
12import org.eclipse.emf.ecore.EObject; 11import org.eclipse.emf.ecore.EObject;
@@ -31,10 +30,9 @@ public class FAMTest {
31 map.put("logicproblem", _xMIResourceFactoryImpl); 30 map.put("logicproblem", _xMIResourceFactoryImpl);
32 InputOutput.<String>println("Input and output workspaces are created"); 31 InputOutput.<String>println("Input and output workspaces are created");
33 final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE); 32 final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE);
34 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel2.xmi"); 33 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi");
35 final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance()); 34 final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance());
36 InputOutput.<String>println("DSL loaded"); 35 InputOutput.<String>println("DSL loaded");
37 LinkedList<EObject> _linkedList = new LinkedList<EObject>(); 36 GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace);
38 GeneralTest.createAndSolveProblem(metamodel, _linkedList, queries, workspace);
39 } 37 }
40} 38}
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 5e4df399..c902bd10 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
@@ -2,6 +2,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse;
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; 3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; 4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
5import com.google.common.base.Objects; 6import com.google.common.base.Objects;
6import com.google.common.collect.Iterables; 7import com.google.common.collect.Iterables;
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; 8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;
@@ -39,6 +40,7 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
39import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; 40import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation;
40import org.eclipse.xtext.xbase.lib.CollectionLiterals; 41import org.eclipse.xtext.xbase.lib.CollectionLiterals;
41import org.eclipse.xtext.xbase.lib.Exceptions; 42import org.eclipse.xtext.xbase.lib.Exceptions;
43import org.eclipse.xtext.xbase.lib.Extension;
42import org.eclipse.xtext.xbase.lib.Functions.Function1; 44import org.eclipse.xtext.xbase.lib.Functions.Function1;
43import org.eclipse.xtext.xbase.lib.InputOutput; 45import org.eclipse.xtext.xbase.lib.InputOutput;
44import org.eclipse.xtext.xbase.lib.IterableExtensions; 46import org.eclipse.xtext.xbase.lib.IterableExtensions;
@@ -52,6 +54,8 @@ public class GeneralTest {
52 try { 54 try {
53 String _xblockexpression = null; 55 String _xblockexpression = null;
54 { 56 {
57 @Extension
58 final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
55 final Ecore2Logic ecore2Logic = new Ecore2Logic(); 59 final Ecore2Logic ecore2Logic = new Ecore2Logic();
56 final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic); 60 final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic);
57 final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); 61 final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic);
@@ -68,7 +72,8 @@ public class GeneralTest {
68 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); 72 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
69 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { 73 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
70 it.documentationLevel = DocumentationLevel.FULL; 74 it.documentationLevel = DocumentationLevel.FULL;
71 it.typeScopes.minNewElements = 5; 75 it.typeScopes.minNewElements = 3;
76 it.typeScopes.maxNewElements = 6;
72 }; 77 };
73 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); 78 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
74 solution = reasoner.solve(problem, vampireConfig, workspace); 79 solution = reasoner.solve(problem, vampireConfig, workspace);
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 3669124b..2fac977d 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 a6a6e1b8..1c3ec2f4 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 71eec0ad..d479a2aa 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