diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-05 13:37:02 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-05 13:37:02 -0500 |
commit | df12163128073296c4d811fa67b02e37ceb20179 (patch) | |
tree | 7509fdd478d6ff3d908d0ab5aa39ed9a8260f0b0 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner | |
parent | Begin handing of scope and fix type definitions. (diff) | |
download | VIATRA-Generator-df12163128073296c4d811fa67b02e37ceb20179.tar.gz VIATRA-Generator-df12163128073296c4d811fa67b02e37ceb20179.tar.zst VIATRA-Generator-df12163128073296c4d811fa67b02e37ceb20179.zip |
Implement type scope handling
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner')
7 files changed, 55 insertions, 42 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend index 54114189..18b3badd 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend | |||
@@ -6,6 +6,7 @@ import functionalarchitecture.FunctionalarchitecturePackage | |||
6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | 6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic |
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration |
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor | 8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult |
11 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | 12 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore |
@@ -22,9 +23,6 @@ import org.eclipse.emf.ecore.EObject | |||
22 | import org.eclipse.emf.ecore.EReference | 23 | import org.eclipse.emf.ecore.EReference |
23 | import org.eclipse.emf.ecore.resource.Resource | 24 | import org.eclipse.emf.ecore.resource.Resource |
24 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 25 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
25 | import hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns | ||
26 | import java.util.LinkedHashMap | ||
27 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor | ||
28 | 26 | ||
29 | class EcoreTest { | 27 | class EcoreTest { |
30 | def static void main(String[] args) { | 28 | def static void main(String[] args) { |
@@ -62,7 +60,7 @@ class EcoreTest { | |||
62 | reasoner = new VampireSolver | 60 | reasoner = new VampireSolver |
63 | val vampireConfig = new VampireSolverConfiguration => [ | 61 | val vampireConfig = new VampireSolverConfiguration => [ |
64 | //add configuration things, in config file first | 62 | //add configuration things, in config file first |
65 | it.writeToFile = true | 63 | it.documentationLevel = DocumentationLevel::FULL |
66 | ] | 64 | ] |
67 | 65 | ||
68 | solution = reasoner.solve(logicProblem, vampireConfig, workspace) | 66 | solution = reasoner.solve(logicProblem, vampireConfig, workspace) |
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 9ae00f8d..95bfd87a 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,8 +1,10 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns | ||
3 | import functionalarchitecture.FunctionalarchitecturePackage | 4 | import functionalarchitecture.FunctionalarchitecturePackage |
4 | import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns | ||
5 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 5 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
6 | import java.util.LinkedList | ||
7 | import org.eclipse.emf.ecore.EObject | ||
6 | import org.eclipse.emf.ecore.resource.Resource | 8 | import org.eclipse.emf.ecore.resource.Resource |
7 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 9 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
8 | 10 | ||
@@ -21,12 +23,12 @@ class FAMTest { | |||
21 | println("Input and output workspaces are created") | 23 | println("Input and output workspaces are created") |
22 | 24 | ||
23 | val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) | 25 | val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) |
24 | val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi") | 26 | val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel2.xmi") |
25 | val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) | 27 | val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) |
26 | 28 | ||
27 | println("DSL loaded") | 29 | println("DSL loaded") |
28 | 30 | ||
29 | GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) | 31 | GeneralTest.createAndSolveProblem(metamodel, new LinkedList<EObject>, queries, workspace) |
30 | } | 32 | } |
31 | 33 | ||
32 | 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 2c53d181..8a60f486 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 | |||
@@ -26,56 +26,74 @@ import org.eclipse.emf.ecore.EReference | |||
26 | import org.eclipse.emf.ecore.resource.Resource | 26 | import org.eclipse.emf.ecore.resource.Resource |
27 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 27 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
28 | import org.eclipse.viatra.query.runtime.api.IQueryGroup | 28 | import org.eclipse.viatra.query.runtime.api.IQueryGroup |
29 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver | ||
30 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
29 | 32 | ||
30 | class GeneralTest { | 33 | class GeneralTest { |
31 | def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List<EObject> partialModel, ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) { | 34 | def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List<EObject> partialModel, |
35 | ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) { | ||
32 | val Ecore2Logic ecore2Logic = new Ecore2Logic | 36 | val Ecore2Logic ecore2Logic = new Ecore2Logic |
33 | val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) | 37 | val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) |
34 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | 38 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) |
35 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | 39 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic |
36 | 40 | ||
37 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration()) | 41 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) |
38 | var problem = instanceModel2Logic.transform(modelGenerationProblem,partialModel).output | 42 | var problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output |
39 | problem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration).output | 43 | problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output |
40 | 44 | ||
41 | workspace.writeModel(problem, "Fam.logicproblem") | 45 | workspace.writeModel(problem, "Fam.logicproblem") |
42 | 46 | ||
43 | println("Problem created") | 47 | println("Problem created") |
44 | 48 | ||
45 | var LogicResult solution | 49 | var LogicResult solution |
46 | var LogicReasoner reasoner | 50 | var LogicReasoner reasoner |
51 | |||
47 | //* | 52 | //* |
48 | reasoner = new VampireSolver | 53 | reasoner = new VampireSolver |
49 | val vampireConfig = new VampireSolverConfiguration => [ | 54 | val vampireConfig = new VampireSolverConfiguration => [ |
50 | //add configuration things, in config file first | 55 | // add configuration things, in config file first |
51 | it.writeToFile = true | 56 | it.documentationLevel = DocumentationLevel::FULL |
57 | it.typeScopes.minNewElements = 5 | ||
52 | ] | 58 | ] |
59 | solution = reasoner.solve(problem, vampireConfig, workspace) | ||
53 | 60 | ||
54 | solution = reasoner.solve(problem, vampireConfig, workspace) | 61 | /*/ |
55 | 62 | ||
63 | reasoner = new AlloySolver | ||
64 | val alloyConfig = new AlloySolverConfiguration => [ | ||
65 | it.typeScopes.maxNewElements = 7 | ||
66 | it.typeScopes.minNewElements = 3 | ||
67 | it.solutionScope.numberOfRequiredSolution = 1 | ||
68 | it.typeScopes.maxNewIntegers = 0 | ||
69 | it.documentationLevel = DocumentationLevel::NORMAL | ||
70 | ] | ||
71 | solution = reasoner.solve(problem, alloyConfig, workspace) | ||
72 | //*/ | ||
73 | |||
56 | println("Problem solved") | 74 | println("Problem solved") |
57 | } | 75 | } |
58 | 76 | ||
59 | def static loadMetamodel(EPackage pckg) { | 77 | def static loadMetamodel(EPackage pckg) { |
60 | val List<EClass> classes = pckg.getEClassifiers.filter(EClass).toList | 78 | val List<EClass> classes = pckg.getEClassifiers.filter(EClass).toList |
61 | val List<EEnum> enums = pckg.getEClassifiers.filter(EEnum).toList | 79 | val List<EEnum> enums = pckg.getEClassifiers.filter(EEnum).toList |
62 | val List<EEnumLiteral> literals = enums.map[getELiterals].flatten.toList | 80 | val List<EEnumLiteral> literals = enums.map[getELiterals].flatten.toList |
63 | val List<EReference> references = classes.map[getEReferences].flatten.toList | 81 | val List<EReference> references = classes.map[getEReferences].flatten.toList |
64 | val List<EAttribute> attributes = classes.map[getEAttributes].flatten.toList | 82 | val List<EAttribute> attributes = classes.map[getEAttributes].flatten.toList |
65 | return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes) | 83 | return new EcoreMetamodelDescriptor(classes, #{}, false, enums, literals, references, attributes) |
66 | } | 84 | } |
67 | 85 | ||
68 | def static loadPartialModel(ReasonerWorkspace inputs, String path) { | 86 | def static loadPartialModel(ReasonerWorkspace inputs, String path) { |
69 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); | 87 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); |
70 | inputs.readModel(EObject,path).eResource.contents | 88 | inputs.readModel(EObject, path).eResource.contents |
71 | // inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList | 89 | // inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList |
72 | } | 90 | } |
73 | 91 | ||
74 | def static loadQueries(EcoreMetamodelDescriptor metamodel, IQueryGroup i) { | 92 | def static loadQueries(EcoreMetamodelDescriptor metamodel, IQueryGroup i) { |
75 | val patterns = i.specifications.toList | 93 | val patterns = i.specifications.toList |
76 | val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet | 94 | val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet |
77 | val derivedFeatures = emptyMap | 95 | val derivedFeatures = emptyMap |
78 | //NO DERIVED FEATURES | 96 | // NO DERIVED FEATURES |
79 | // val derivedFeatures = new LinkedHashMap | 97 | // val derivedFeatures = new LinkedHashMap |
80 | // derivedFeatures.put(i.type,metamodel.attributes.filter[it.name == "type"].head) | 98 | // derivedFeatures.put(i.type,metamodel.attributes.filter[it.name == "type"].head) |
81 | // derivedFeatures.put(i.model,metamodel.references.filter[it.name == "model"].head) | 99 | // derivedFeatures.put(i.model,metamodel.references.filter[it.name == "model"].head) |
@@ -86,4 +104,4 @@ class GeneralTest { | |||
86 | ) | 104 | ) |
87 | return res | 105 | return res |
88 | } | 106 | } |
89 | } \ No newline at end of file | 107 | } |
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 e4f6f87a..eb3f4b14 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,11 +1,11 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse |
2 | 2 | ||
3 | import functionalarchitecture.FunctionalarchitecturePackage | 3 | import functionalarchitecture.FunctionalarchitecturePackage |
4 | import hu.bme.mit.inf.dslreasoner.domains.y | ||
5 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 4 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
6 | import org.eclipse.emf.ecore.resource.Resource | 5 | import org.eclipse.emf.ecore.resource.Resource |
7 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 6 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
8 | import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage | 7 | import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage |
8 | import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.queries.YakinduPatterns | ||
9 | 9 | ||
10 | class YakinduTest { | 10 | class YakinduTest { |
11 | def static void main(String[] args) { | 11 | def static void main(String[] args) { |
@@ -23,11 +23,11 @@ class YakinduTest { | |||
23 | 23 | ||
24 | val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE) | 24 | val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE) |
25 | val partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi") | 25 | val partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi") |
26 | val queries = GeneralTest.loadQueries(metamodel, | 26 | // val queries = GeneralTest.loadQueries(metamodel, FamPa |
27 | 27 | ||
28 | println("DSL loaded") | 28 | println("DSL loaded") |
29 | 29 | ||
30 | GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) | 30 | // GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) |
31 | } | 31 | } |
32 | 32 | ||
33 | 33 | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql index 013d0419..60679874 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql | |||
@@ -1,4 +1,4 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.domains.fam | 1 | package ca.mcgill.ecse.dslreasoner.vampire.queries |
2 | 2 | ||
3 | import epackage "http://www.inf.mit.bme.hu/viatrasolver/example/fam" | 3 | import epackage "http://www.inf.mit.bme.hu/viatrasolver/example/fam" |
4 | 4 | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend index 15f9e1fe..40cb70a7 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend | |||
@@ -1,19 +1,17 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.test | 1 | package ca.mcgill.ecse.dslreasoner.vampire.test |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup | 3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage | 6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult |
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | ||
11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage | 13 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage |
15 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 14 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
16 | import java.util.Collections | ||
17 | import org.eclipse.emf.common.util.URI | 15 | import org.eclipse.emf.common.util.URI |
18 | import org.eclipse.emf.ecore.resource.Resource | 16 | import org.eclipse.emf.ecore.resource.Resource |
19 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl | 17 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl |
@@ -41,7 +39,7 @@ class MedicalSystem { | |||
41 | reasoner = new VampireSolver | 39 | reasoner = new VampireSolver |
42 | val vampireConfig = new VampireSolverConfiguration => [ | 40 | val vampireConfig = new VampireSolverConfiguration => [ |
43 | //add configuration things, in config file first | 41 | //add configuration things, in config file first |
44 | it.writeToFile = true | 42 | it.documentationLevel = DocumentationLevel::FULL |
45 | ] | 43 | ] |
46 | 44 | ||
47 | solution = reasoner.solve(root, vampireConfig, workspace) | 45 | solution = reasoner.solve(root, vampireConfig, workspace) |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend index 4fc81ad8..bbb14f1f 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend | |||
@@ -1,23 +1,19 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.test | 1 | package ca.mcgill.ecse.dslreasoner.vampire.test |
2 | 2 | ||
3 | |||
4 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup | 3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
5 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage | 6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage |
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult |
11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | ||
12 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
13 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage | 13 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage |
14 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 14 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
15 | import java.util.Collections | ||
16 | import org.eclipse.emf.common.util.URI | ||
17 | import org.eclipse.emf.ecore.resource.Resource | 15 | import org.eclipse.emf.ecore.resource.Resource |
18 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl | ||
19 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 16 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
20 | import java.io.File | ||
21 | 17 | ||
22 | class VampireTest { | 18 | class VampireTest { |
23 | 19 | ||
@@ -65,7 +61,8 @@ class VampireTest { | |||
65 | reasoner = new VampireSolver | 61 | reasoner = new VampireSolver |
66 | val vampireConfig = new VampireSolverConfiguration => [ | 62 | val vampireConfig = new VampireSolverConfiguration => [ |
67 | //add configuration things, in config file first | 63 | //add configuration things, in config file first |
68 | it.writeToFile = true | 64 | it.documentationLevel = DocumentationLevel::FULL |
65 | it.typeScopes.minNewElements = 4 | ||
69 | ] | 66 | ] |
70 | 67 | ||
71 | solution = reasoner.solve(problem, vampireConfig, workspace) | 68 | solution = reasoner.solve(problem, vampireConfig, workspace) |