diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-02-01 16:03:30 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:06:28 -0400 |
commit | 57e614aabedc176ba9965d0ca5e6daa23c5f4758 (patch) | |
tree | 16806454dff463419af99b14f6abfab3d1fa5291 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src | |
parent | FAM MM transformation works (diff) | |
download | VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.tar.gz VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.tar.zst VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.zip |
Fix FAM Test. Begin Grammar Fix.
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src')
9 files changed, 312 insertions, 14 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 new file mode 100644 index 00000000..54114189 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend | |||
@@ -0,0 +1,105 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
5 | import functionalarchitecture.FunctionalarchitecturePackage | ||
6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor | ||
9 | 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.logic2ecore.Logic2Ecore | ||
12 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | ||
14 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
15 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
16 | import java.util.List | ||
17 | import org.eclipse.emf.ecore.EAttribute | ||
18 | import org.eclipse.emf.ecore.EClass | ||
19 | import org.eclipse.emf.ecore.EEnum | ||
20 | import org.eclipse.emf.ecore.EEnumLiteral | ||
21 | import org.eclipse.emf.ecore.EObject | ||
22 | import org.eclipse.emf.ecore.EReference | ||
23 | import org.eclipse.emf.ecore.resource.Resource | ||
24 | 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 | |||
29 | class EcoreTest { | ||
30 | def static void main(String[] args) { | ||
31 | val inputs = new FileSystemWorkspace('''initialModels/''', "") | ||
32 | val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") | ||
33 | workspace.initAndClear | ||
34 | |||
35 | println("Input and output workspaces are created") | ||
36 | |||
37 | val metamodel = loadMetamodel() | ||
38 | val partialModel = loadPartialModel(inputs) | ||
39 | // val queries = loadQueries(metamodel) | ||
40 | |||
41 | println("DSL loaded") | ||
42 | |||
43 | val Ecore2Logic ecore2Logic = new Ecore2Logic | ||
44 | val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) | ||
45 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | ||
46 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | ||
47 | |||
48 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration()) | ||
49 | val modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem,partialModel) | ||
50 | // val validModelExtensionProblem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration) | ||
51 | |||
52 | val logicProblem = modelGenerationProblem.output | ||
53 | // val logicProblem = modelExtensionProblem.output | ||
54 | // val logicProblem = validModelExtensionProblem.output | ||
55 | |||
56 | |||
57 | println("Problem created") | ||
58 | |||
59 | var LogicResult solution | ||
60 | var LogicReasoner reasoner | ||
61 | //* | ||
62 | reasoner = new VampireSolver | ||
63 | val vampireConfig = new VampireSolverConfiguration => [ | ||
64 | //add configuration things, in config file first | ||
65 | it.writeToFile = true | ||
66 | ] | ||
67 | |||
68 | solution = reasoner.solve(logicProblem, vampireConfig, workspace) | ||
69 | |||
70 | println("Problem solved") | ||
71 | |||
72 | |||
73 | } | ||
74 | |||
75 | def private static loadMetamodel() { | ||
76 | val pckg = FunctionalarchitecturePackage.eINSTANCE | ||
77 | val List<EClass> classes = pckg.getEClassifiers.filter(EClass).toList | ||
78 | val List<EEnum> enums = pckg.getEClassifiers.filter(EEnum).toList | ||
79 | val List<EEnumLiteral> literals = enums.map[getELiterals].flatten.toList | ||
80 | val List<EReference> references = classes.map[getEReferences].flatten.toList | ||
81 | val List<EAttribute> attributes = classes.map[getEAttributes].flatten.toList | ||
82 | return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes) | ||
83 | } | ||
84 | |||
85 | def private static loadPartialModel(ReasonerWorkspace inputs) { | ||
86 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); | ||
87 | // inputs.readModel(EObject,"FunctionalArchitectureModel.xmi").eResource.allContents.toList | ||
88 | inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList | ||
89 | } | ||
90 | |||
91 | def private static loadQueries(EcoreMetamodelDescriptor metamodel) { | ||
92 | // val i = Patterns.instance | ||
93 | // val patterns = i.specifications.toList | ||
94 | // val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet | ||
95 | // val derivedFeatures = new LinkedHashMap | ||
96 | // derivedFeatures.put(i.type,metamodel.attributes.filter[it.name == "type"].head) | ||
97 | // derivedFeatures.put(i.model,metamodel.references.filter[it.name == "model"].head) | ||
98 | // val res = new ViatraQuerySetDescriptor( | ||
99 | // patterns, | ||
100 | // wfPatterns, | ||
101 | // derivedFeatures | ||
102 | // ) | ||
103 | // return res | ||
104 | } | ||
105 | } | ||
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 new file mode 100644 index 00000000..9ae00f8d --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend | |||
@@ -0,0 +1,33 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | ||
2 | |||
3 | import functionalarchitecture.FunctionalarchitecturePackage | ||
4 | import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns | ||
5 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
6 | import org.eclipse.emf.ecore.resource.Resource | ||
7 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
8 | |||
9 | class FAMTest { | ||
10 | def static void main(String[] args) { | ||
11 | //Workspace setup | ||
12 | val inputs = new FileSystemWorkspace('''initialModels/''', "") | ||
13 | val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") | ||
14 | workspace.initAndClear | ||
15 | |||
16 | //Logicproblem writing setup | ||
17 | val reg = Resource.Factory.Registry.INSTANCE | ||
18 | val map = reg.extensionToFactoryMap | ||
19 | map.put("logicproblem", new XMIResourceFactoryImpl) | ||
20 | |||
21 | println("Input and output workspaces are created") | ||
22 | |||
23 | val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) | ||
24 | val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi") | ||
25 | val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) | ||
26 | |||
27 | println("DSL loaded") | ||
28 | |||
29 | GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) | ||
30 | } | ||
31 | |||
32 | |||
33 | } | ||
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 new file mode 100644 index 00000000..363b9356 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend | |||
@@ -0,0 +1,33 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | ||
2 | |||
3 | import functionalarchitecture.FunctionalarchitecturePackage | ||
4 | import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns | ||
5 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
6 | import org.eclipse.emf.ecore.resource.Resource | ||
7 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
8 | |||
9 | class FileSystemTest { | ||
10 | def static void main(String[] args) { | ||
11 | //Workspace setup | ||
12 | val inputs = new FileSystemWorkspace('''initialModels/''', "") | ||
13 | val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") | ||
14 | workspace.initAndClear | ||
15 | |||
16 | //Logicproblem writing setup | ||
17 | val reg = Resource.Factory.Registry.INSTANCE | ||
18 | val map = reg.extensionToFactoryMap | ||
19 | map.put("logicproblem", new XMIResourceFactoryImpl) | ||
20 | |||
21 | println("Input and output workspaces are created") | ||
22 | |||
23 | val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) | ||
24 | val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi") | ||
25 | val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) | ||
26 | |||
27 | println("DSL loaded") | ||
28 | |||
29 | GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) | ||
30 | } | ||
31 | |||
32 | |||
33 | } | ||
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 new file mode 100644 index 00000000..2c53d181 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend | |||
@@ -0,0 +1,89 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
5 | import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns | ||
6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor | ||
9 | 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.logic2ecore.Logic2Ecore | ||
12 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | ||
13 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | ||
14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | ||
16 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
17 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
18 | import java.util.List | ||
19 | import org.eclipse.emf.ecore.EAttribute | ||
20 | import org.eclipse.emf.ecore.EClass | ||
21 | import org.eclipse.emf.ecore.EEnum | ||
22 | import org.eclipse.emf.ecore.EEnumLiteral | ||
23 | import org.eclipse.emf.ecore.EObject | ||
24 | import org.eclipse.emf.ecore.EPackage | ||
25 | import org.eclipse.emf.ecore.EReference | ||
26 | import org.eclipse.emf.ecore.resource.Resource | ||
27 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
28 | import org.eclipse.viatra.query.runtime.api.IQueryGroup | ||
29 | |||
30 | class GeneralTest { | ||
31 | def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List<EObject> partialModel, ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) { | ||
32 | val Ecore2Logic ecore2Logic = new Ecore2Logic | ||
33 | val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) | ||
34 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | ||
35 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | ||
36 | |||
37 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration()) | ||
38 | var problem = instanceModel2Logic.transform(modelGenerationProblem,partialModel).output | ||
39 | problem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration).output | ||
40 | |||
41 | workspace.writeModel(problem, "Fam.logicproblem") | ||
42 | |||
43 | println("Problem created") | ||
44 | |||
45 | var LogicResult solution | ||
46 | var LogicReasoner reasoner | ||
47 | //* | ||
48 | reasoner = new VampireSolver | ||
49 | val vampireConfig = new VampireSolverConfiguration => [ | ||
50 | //add configuration things, in config file first | ||
51 | it.writeToFile = true | ||
52 | ] | ||
53 | |||
54 | solution = reasoner.solve(problem, vampireConfig, workspace) | ||
55 | |||
56 | println("Problem solved") | ||
57 | } | ||
58 | |||
59 | def static loadMetamodel(EPackage pckg) { | ||
60 | val List<EClass> classes = pckg.getEClassifiers.filter(EClass).toList | ||
61 | val List<EEnum> enums = pckg.getEClassifiers.filter(EEnum).toList | ||
62 | val List<EEnumLiteral> literals = enums.map[getELiterals].flatten.toList | ||
63 | val List<EReference> references = classes.map[getEReferences].flatten.toList | ||
64 | val List<EAttribute> attributes = classes.map[getEAttributes].flatten.toList | ||
65 | return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes) | ||
66 | } | ||
67 | |||
68 | def static loadPartialModel(ReasonerWorkspace inputs, String path) { | ||
69 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); | ||
70 | inputs.readModel(EObject,path).eResource.contents | ||
71 | // inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList | ||
72 | } | ||
73 | |||
74 | def static loadQueries(EcoreMetamodelDescriptor metamodel, IQueryGroup i) { | ||
75 | val patterns = i.specifications.toList | ||
76 | val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet | ||
77 | val derivedFeatures = emptyMap | ||
78 | //NO DERIVED FEATURES | ||
79 | // val derivedFeatures = new LinkedHashMap | ||
80 | // derivedFeatures.put(i.type,metamodel.attributes.filter[it.name == "type"].head) | ||
81 | // derivedFeatures.put(i.model,metamodel.references.filter[it.name == "model"].head) | ||
82 | val res = new ViatraQuerySetDescriptor( | ||
83 | patterns, | ||
84 | wfPatterns, | ||
85 | derivedFeatures | ||
86 | ) | ||
87 | return res | ||
88 | } | ||
89 | } \ No newline at end of file | ||
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 new file mode 100644 index 00000000..e4f6f87a --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend | |||
@@ -0,0 +1,34 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | ||
2 | |||
3 | import functionalarchitecture.FunctionalarchitecturePackage | ||
4 | import hu.bme.mit.inf.dslreasoner.domains.y | ||
5 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
6 | import org.eclipse.emf.ecore.resource.Resource | ||
7 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
8 | import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage | ||
9 | |||
10 | class YakinduTest { | ||
11 | def static void main(String[] args) { | ||
12 | //Workspace setup | ||
13 | val inputs = new FileSystemWorkspace('''initialModels/''', "") | ||
14 | val workspace = new FileSystemWorkspace('''output/YakinduTest/''', "") | ||
15 | workspace.initAndClear | ||
16 | |||
17 | //Logicproblem writing setup | ||
18 | val reg = Resource.Factory.Registry.INSTANCE | ||
19 | val map = reg.extensionToFactoryMap | ||
20 | map.put("logicproblem", new XMIResourceFactoryImpl) | ||
21 | |||
22 | println("Input and output workspaces are created") | ||
23 | |||
24 | val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE) | ||
25 | val partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi") | ||
26 | val queries = GeneralTest.loadQueries(metamodel, | ||
27 | |||
28 | println("DSL loaded") | ||
29 | |||
30 | GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) | ||
31 | } | ||
32 | |||
33 | |||
34 | } | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/DslTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icseTests/FAMTest.xtend index a8b4dcfb..a8b4dcfb 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/DslTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icseTests/FAMTest.xtend | |||
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 ccc17617..15f9e1fe 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 | |||
@@ -22,11 +22,12 @@ import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | |||
22 | class MedicalSystem { | 22 | class MedicalSystem { |
23 | def static void main(String[] args) { | 23 | def static void main(String[] args) { |
24 | init() | 24 | init() |
25 | val workspace = new FileSystemWorkspace('''outputModels/''',"") | 25 | val workspace = new FileSystemWorkspace('''output/MedicalSystem/''',"") |
26 | workspace.initAndClear | 26 | workspace.initAndClear |
27 | val root = load() | 27 | val root = load() |
28 | println("Problem Loaded") | 28 | println("Problem Loaded") |
29 | 29 | ||
30 | |||
30 | // val rs = new ResourceSetImpl | 31 | // val rs = new ResourceSetImpl |
31 | // val logRes = rs.createResource(URI.createFileURI("vampireMidel.tptp")) | 32 | // val logRes = rs.createResource(URI.createFileURI("vampireMidel.tptp")) |
32 | // | 33 | // |
@@ -40,7 +41,7 @@ class MedicalSystem { | |||
40 | reasoner = new VampireSolver | 41 | reasoner = new VampireSolver |
41 | val vampireConfig = new VampireSolverConfiguration => [ | 42 | val vampireConfig = new VampireSolverConfiguration => [ |
42 | //add configuration things, in config file first | 43 | //add configuration things, in config file first |
43 | it.writeToFile = false | 44 | it.writeToFile = true |
44 | ] | 45 | ] |
45 | 46 | ||
46 | solution = reasoner.solve(root, vampireConfig, workspace) | 47 | solution = reasoner.solve(root, vampireConfig, workspace) |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend index 9d2235f0..f99f0a40 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend | |||
@@ -66,7 +66,7 @@ | |||
66 | // println("Problem created") | 66 | // println("Problem created") |
67 | // var LogicResult solution | 67 | // var LogicResult solution |
68 | // var LogicReasoner reasoner | 68 | // var LogicReasoner reasoner |
69 | // //* | 69 | // /* |
70 | // reasoner = new ViatraReasoner | 70 | // reasoner = new ViatraReasoner |
71 | // val viatraConfig = new ViatraReasonerConfiguration => [ | 71 | // val viatraConfig = new ViatraReasonerConfiguration => [ |
72 | // it.typeScopes.maxNewElements = 40 | 72 | // it.typeScopes.maxNewElements = 40 |
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 3d36bbf7..4fc81ad8 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 | |||
@@ -17,6 +17,7 @@ import org.eclipse.emf.common.util.URI | |||
17 | import org.eclipse.emf.ecore.resource.Resource | 17 | import org.eclipse.emf.ecore.resource.Resource |
18 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl | 18 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl |
19 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 19 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
20 | import java.io.File | ||
20 | 21 | ||
21 | class VampireTest { | 22 | class VampireTest { |
22 | 23 | ||
@@ -39,15 +40,11 @@ class VampireTest { | |||
39 | map.put("logicproblem", new XMIResourceFactoryImpl) | 40 | map.put("logicproblem", new XMIResourceFactoryImpl) |
40 | VampireLanguageStandaloneSetup.doSetup | 41 | VampireLanguageStandaloneSetup.doSetup |
41 | 42 | ||
42 | val workspace = new FileSystemWorkspace('''output/models/''',"") | 43 | val workspace = new FileSystemWorkspace('''output/VampireTest''',"") |
43 | workspace.initAndClear | 44 | workspace.initAndClear |
44 | 45 | ||
45 | // Load and create top level elements | 46 | //Storing the logicProblem |
46 | // Load source model | 47 | val filename = "problem.logicproblem" |
47 | val rs = new ResourceSetImpl | ||
48 | val logicURI = URI.createFileURI("output/files/logProb.logicproblem") | ||
49 | val logRes = rs.createResource(logicURI) | ||
50 | |||
51 | var LogicProblem problem = builder.createProblem | 48 | var LogicProblem problem = builder.createProblem |
52 | 49 | ||
53 | /* | 50 | /* |
@@ -56,8 +53,7 @@ class VampireTest { | |||
56 | rockPaperScisors(problem) | 53 | rockPaperScisors(problem) |
57 | //*/ | 54 | //*/ |
58 | 55 | ||
59 | logRes.contents.add(problem) | 56 | workspace.writeModel(problem, filename) |
60 | logRes.save(Collections.EMPTY_MAP) | ||
61 | 57 | ||
62 | //problem.add(Assertion( Y && X <=> X) ) | 58 | //problem.add(Assertion( Y && X <=> X) ) |
63 | 59 | ||
@@ -69,7 +65,7 @@ class VampireTest { | |||
69 | reasoner = new VampireSolver | 65 | reasoner = new VampireSolver |
70 | val vampireConfig = new VampireSolverConfiguration => [ | 66 | val vampireConfig = new VampireSolverConfiguration => [ |
71 | //add configuration things, in config file first | 67 | //add configuration things, in config file first |
72 | it.writeToFile = false | 68 | it.writeToFile = true |
73 | ] | 69 | ] |
74 | 70 | ||
75 | solution = reasoner.solve(problem, vampireConfig, workspace) | 71 | solution = reasoner.solve(problem, vampireConfig, workspace) |
@@ -88,6 +84,10 @@ class VampireTest { | |||
88 | 84 | ||
89 | } | 85 | } |
90 | 86 | ||
87 | def name() { | ||
88 | return this.class.simpleName | ||
89 | } | ||
90 | |||
91 | static def deMorgan(LogicProblem problem) { | 91 | static def deMorgan(LogicProblem problem) { |
92 | 92 | ||
93 | 93 | ||
@@ -144,7 +144,10 @@ class VampireTest { | |||
144 | //x.range | 144 | //x.range |
145 | Exists[ | 145 | Exists[ |
146 | val y = addVar("y",oldRPS) | 146 | val y = addVar("y",oldRPS) |
147 | beats2.call(x,y) | 147 | And(beats2.call(x,y), |
148 | x != y, | ||
149 | Not(beats2.call(y, x)) | ||
150 | ) | ||
148 | ] | 151 | ] |
149 | ])) | 152 | ])) |
150 | //*/ | 153 | //*/ |