aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-02-01 16:03:30 -0500
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-02-01 16:03:30 -0500
commit717916e99b2c8e7965fb31f4448b4336d8c2f19a (patch)
tree074c77b8465f1e47e7a28af2d95f79c1f5abaf86 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner
parentFAM MM transformation works (diff)
downloadVIATRA-Generator-717916e99b2c8e7965fb31f4448b4336d8c2f19a.tar.gz
VIATRA-Generator-717916e99b2c8e7965fb31f4448b4336d8c2f19a.tar.zst
VIATRA-Generator-717916e99b2c8e7965fb31f4448b4336d8c2f19a.zip
Fix FAM Test. Begin Grammar Fix.
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend105
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend33
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend33
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend89
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend34
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icseTests/FAMTest.xtend (renamed from Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/DslTest.xtend)0
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend5
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend2
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend25
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 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse
2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
5import functionalarchitecture.FunctionalarchitecturePackage
6import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
8import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
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.logic2ecore.Logic2Ecore
12import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
14import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
15import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
16import java.util.List
17import org.eclipse.emf.ecore.EAttribute
18import org.eclipse.emf.ecore.EClass
19import org.eclipse.emf.ecore.EEnum
20import org.eclipse.emf.ecore.EEnumLiteral
21import org.eclipse.emf.ecore.EObject
22import org.eclipse.emf.ecore.EReference
23import org.eclipse.emf.ecore.resource.Resource
24import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
25import hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns
26import java.util.LinkedHashMap
27import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
28
29class 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 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse
2
3import functionalarchitecture.FunctionalarchitecturePackage
4import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns
5import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
6import org.eclipse.emf.ecore.resource.Resource
7import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
8
9class 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 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse
2
3import functionalarchitecture.FunctionalarchitecturePackage
4import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns
5import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
6import org.eclipse.emf.ecore.resource.Resource
7import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
8
9class 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 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse
2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
5import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns
6import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
8import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
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.logic2ecore.Logic2Ecore
12import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
13import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
14import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
15import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
16import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
17import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
18import java.util.List
19import org.eclipse.emf.ecore.EAttribute
20import org.eclipse.emf.ecore.EClass
21import org.eclipse.emf.ecore.EEnum
22import org.eclipse.emf.ecore.EEnumLiteral
23import org.eclipse.emf.ecore.EObject
24import org.eclipse.emf.ecore.EPackage
25import org.eclipse.emf.ecore.EReference
26import org.eclipse.emf.ecore.resource.Resource
27import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
28import org.eclipse.viatra.query.runtime.api.IQueryGroup
29
30class 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 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse
2
3import functionalarchitecture.FunctionalarchitecturePackage
4import hu.bme.mit.inf.dslreasoner.domains.y
5import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
6import org.eclipse.emf.ecore.resource.Resource
7import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
8import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage
9
10class 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
22class MedicalSystem { 22class 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
17import org.eclipse.emf.ecore.resource.Resource 17import org.eclipse.emf.ecore.resource.Resource
18import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl 18import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl
19import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 19import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
20import java.io.File
20 21
21class VampireTest { 22class 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 //*/
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 07:47:06 +0000