aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse
diff options
context:
space:
mode:
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend97
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend99
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend117
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend98
4 files changed, 273 insertions, 138 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
index ef2e0c2f..f66ad93c 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
@@ -1,36 +1,115 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse 1package ca.mcgill.ecse.dslreasoner.vampire.icse
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns 3import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
6import functionalarchitecture.Function
7import functionalarchitecture.FunctionalInterface
8import functionalarchitecture.FunctionalOutput
4import functionalarchitecture.FunctionalarchitecturePackage 9import functionalarchitecture.FunctionalarchitecturePackage
10import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
11import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
13import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
14import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
15import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
16import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
5import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 17import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
6import java.util.LinkedList 18import java.util.HashMap
7import org.eclipse.emf.ecore.EObject
8import org.eclipse.emf.ecore.resource.Resource 19import org.eclipse.emf.ecore.resource.Resource
9import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 20import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
10 21
11class FAMTest { 22class FAMTest {
12 def static void main(String[] args) { 23 def static void main(String[] args) {
13 //Workspace setup 24 val Ecore2Logic ecore2Logic = new Ecore2Logic
25 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
26 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
27
28 // Workspace setup
14 val inputs = new FileSystemWorkspace('''initialModels/''', "") 29 val inputs = new FileSystemWorkspace('''initialModels/''', "")
15 val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") 30 val workspace = new FileSystemWorkspace('''output/FAMTest/''', "")
16 workspace.initAndClear 31 workspace.initAndClear
17 32
18 //Logicproblem writing setup 33 // Logicproblem writing setup
19 val reg = Resource.Factory.Registry.INSTANCE 34 val reg = Resource.Factory.Registry.INSTANCE
20 val map = reg.extensionToFactoryMap 35 val map = reg.extensionToFactoryMap
21 map.put("logicproblem", new XMIResourceFactoryImpl) 36 map.put("logicproblem", new XMIResourceFactoryImpl)
22
23 37
24 println("Input and output workspaces are created") 38 println("Input and output workspaces are created")
25 39
40 // Load DSL
26 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) 41 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE)
27 val partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi") 42 val partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi")
28 val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) 43 val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance)
29 44
30 println("DSL loaded") 45 println("DSL loaded")
46
47 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
48 var problem = modelGenerationProblem.output
49// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
50// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
51 workspace.writeModel(problem, "Fam.logicproblem")
52
53 println("Problem created")
54
55 //Start Time
56 var startTime = System.currentTimeMillis
57
58 var LogicReasoner reasoner
59 // *
60 reasoner = new VampireSolver
61
62 // /////////////////////////////////////////////////////
63 // Minimum Scope
64 val classMapMin = new HashMap<Class, Integer>
65 classMapMin.put(Function, 1)
66 classMapMin.put(FunctionalInterface, 2)
67 classMapMin.put(FunctionalOutput, 3)
31 68
32 GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) 69 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace)
70
71 // Maximum Scope
72 val classMapMax = new HashMap<Class, Integer>
73 classMapMax.put(Function, 5)
74 classMapMax.put(FunctionalInterface, 2)
75 classMapMax.put(FunctionalOutput, 4)
76
77 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace)
78
79 // Define Config File
80 val vampireConfig = new VampireSolverConfiguration => [
81 // add configuration things, in config file first
82 it.documentationLevel = DocumentationLevel::FULL
83
84 it.typeScopes.minNewElements = 4
85 it.typeScopes.maxNewElements = 5
86 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin
87 if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax
88 it.contCycleLevel = 5
89 it.uniquenessDuplicates = false
90 ]
91
92 var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace)
93
94 /*/
95 *
96 * reasoner = new AlloySolver
97 * val alloyConfig = new AlloySolverConfiguration => [
98 * it.typeScopes.maxNewElements = 7
99 * it.typeScopes.minNewElements = 3
100 * it.solutionScope.numberOfRequiredSolution = 1
101 * it.typeScopes.maxNewIntegers = 0
102 * it.documentationLevel = DocumentationLevel::NORMAL
103 * ]
104 * solution = reasoner.solve(problem, alloyConfig, workspace)
105 //*/
106 // /////////////////////////////////////////////////////
107
108 var totalTimeMin = (System.currentTimeMillis - startTime) / 60000
109 var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60
110
111 println("Problem solved")
112 println("Time was: " + totalTimeMin + ":" + totalTimeSec)
33 } 113 }
34 114
35
36} 115}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend
index 363b9356..50639577 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend
@@ -1,33 +1,108 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse 1package ca.mcgill.ecse.dslreasoner.vampire.icse
2 2
3import functionalarchitecture.FunctionalarchitecturePackage 3import ca.mcgill.ecse.dslreasoner.vampire.queries
4import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns 4import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.filesystemPackage
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
9import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
10import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
11import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
12import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
5import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 14import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
15import java.util.HashMap
6import org.eclipse.emf.ecore.resource.Resource 16import org.eclipse.emf.ecore.resource.Resource
7import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 17import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
8 18
9class FileSystemTest { 19class FileSystemTest {
10 def static void main(String[] args) { 20 def static void main(String[] args) {
11 //Workspace setup 21 val Ecore2Logic ecore2Logic = new Ecore2Logic
22 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
23 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
24
25 // Workspace setup
12 val inputs = new FileSystemWorkspace('''initialModels/''', "") 26 val inputs = new FileSystemWorkspace('''initialModels/''', "")
13 val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") 27 val workspace = new FileSystemWorkspace('''output/FAMTest/''', "")
14 workspace.initAndClear 28 workspace.initAndClear
15 29
16 //Logicproblem writing setup 30 // Logicproblem writing setup
17 val reg = Resource.Factory.Registry.INSTANCE 31 val reg = Resource.Factory.Registry.INSTANCE
18 val map = reg.extensionToFactoryMap 32 val map = reg.extensionToFactoryMap
19 map.put("logicproblem", new XMIResourceFactoryImpl) 33 map.put("logicproblem", new XMIResourceFactoryImpl)
20 34
21 println("Input and output workspaces are created") 35 println("Input and output workspaces are created")
22 36
23 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) 37 val metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE)
24 val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi") 38 val partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi")
25 val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) 39 //val queries = GeneralTest.loadQueries(metamodel, FileSystemPatterns.instance)
26 40
27 println("DSL loaded") 41 println("DSL loaded")
28 42
29 GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) 43 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
44 var problem = modelGenerationProblem.output
45// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
46// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
47 workspace.writeModel(problem, "Fam.logicproblem")
48
49 println("Problem created")
50
51 // Start Time
52 var startTime = System.currentTimeMillis
53
54 var LogicReasoner reasoner
55 // *
56 reasoner = new VampireSolver
57
58 // /////////////////////////////////////////////////////
59 // Minimum Scope
60 val classMapMin = new HashMap<Class, Integer>
61// classMapMin.put(Function, 1)
62// classMapMin.put(FunctionalInterface, 2)
63// classMapMin.put(FunctionalOutput, 3)
64 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace)
65
66 // Maximum Scope
67 val classMapMax = new HashMap<Class, Integer>
68// classMapMax.put(Function, 5)
69// classMapMax.put(FunctionalInterface, 2)
70// classMapMax.put(FunctionalOutput, 4)
71 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace)
72
73 // Define Config File
74 val vampireConfig = new VampireSolverConfiguration => [
75 // add configuration things, in config file first
76 it.documentationLevel = DocumentationLevel::FULL
77
78 it.typeScopes.minNewElements = 4
79 it.typeScopes.maxNewElements = 5
80 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin
81 if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax
82 it.contCycleLevel = 5
83 it.uniquenessDuplicates = false
84 ]
85
86 var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace)
87
88 /*/
89 *
90 * reasoner = new AlloySolver
91 * val alloyConfig = new AlloySolverConfiguration => [
92 * it.typeScopes.maxNewElements = 7
93 * it.typeScopes.minNewElements = 3
94 * it.solutionScope.numberOfRequiredSolution = 1
95 * it.typeScopes.maxNewIntegers = 0
96 * it.documentationLevel = DocumentationLevel::NORMAL
97 * ]
98 * solution = reasoner.solve(problem, alloyConfig, workspace)
99 //*/
100 // /////////////////////////////////////////////////////
101 var totalTimeMin = (System.currentTimeMillis - startTime) / 60000
102 var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60
103
104 println("Problem solved")
105 println("Time was: " + totalTimeMin + ":" + totalTimeSec)
30 } 106 }
31 107
32
33} 108}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
index 949abe87..89375801 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
@@ -1,25 +1,14 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse 1package ca.mcgill.ecse.dslreasoner.vampire.icse
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
6import functionalarchitecture.Function
7import functionalarchitecture.FunctionalInterface
8import functionalarchitecture.FunctionalOutput
9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic 3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
10import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration 4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
11import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor 5import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type 6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
14import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
15import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
16import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
17import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor 7import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
19import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
20import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 8import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
21import java.util.HashMap 9import java.util.HashMap
22import java.util.List 10import java.util.List
11import java.util.Map
23import org.eclipse.emf.ecore.EAttribute 12import org.eclipse.emf.ecore.EAttribute
24import org.eclipse.emf.ecore.EClass 13import org.eclipse.emf.ecore.EClass
25import org.eclipse.emf.ecore.EEnum 14import org.eclipse.emf.ecore.EEnum
@@ -30,100 +19,18 @@ import org.eclipse.emf.ecore.EReference
30import org.eclipse.emf.ecore.resource.Resource 19import org.eclipse.emf.ecore.resource.Resource
31import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 20import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
32import org.eclipse.viatra.query.runtime.api.IQueryGroup 21import org.eclipse.viatra.query.runtime.api.IQueryGroup
33import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
34 22
35class GeneralTest { 23class GeneralTest {
36 def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List<EObject> partialModel, 24 def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel, Ecore2Logic e2l, Ecore2Logic_Trace trace) {
37 ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) { 25 val typeMap = new HashMap<Type, Integer>
38 val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE 26 val listMap = metamodel.classes.toMap[s|s.name]
39 val Ecore2Logic ecore2Logic = new Ecore2Logic
40 val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic)
41 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
42 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
43
44 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
45 var problem = modelGenerationProblem.output
46// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
47// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
48 workspace.writeModel(problem, "Fam.logicproblem")
49
50 println("Problem created")
51
52 var startTime = System.currentTimeMillis
53
54 var LogicResult solution
55 var LogicReasoner reasoner
56
57 // *
58 reasoner = new VampireSolver
59
60 // Setting up scope
61 val typeMapMin = new HashMap<Type, Integer>
62 val typeMapMax = new HashMap<Type, Integer>
63 val list2MapMin = metamodel.classes.toMap[s|s.name]
64 val list2MapMax = metamodel.classes.toMap[s|s.name]
65
66 // Minimum Scope
67 typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace,
68 list2MapMin.get(Function.simpleName)
69 ), 1)
70 typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace,
71 list2MapMin.get(FunctionalInterface.simpleName)
72 ), 2)
73 typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace,
74 list2MapMin.get(FunctionalOutput.simpleName)
75 ), 3)
76
77 // Maximum Scope
78 typeMapMax.put(ecore2Logic.TypeofEClass(
79 modelGenerationProblem.trace,
80 list2MapMax.get(Function.simpleName)
81 ), 5)
82 typeMapMax.put(ecore2Logic.TypeofEClass(
83 modelGenerationProblem.trace,
84 list2MapMax.get(FunctionalInterface.simpleName)
85 ), 2)
86 typeMapMax.put(ecore2Logic.TypeofEClass(
87 modelGenerationProblem.trace,
88 list2MapMax.get(FunctionalOutput.simpleName)
89 ), 4)
90
91 // Configuration
92 val vampireConfig = new VampireSolverConfiguration => [
93 // add configuration things, in config file first
94 it.documentationLevel = DocumentationLevel::FULL
95 it.typeScopes.minNewElements = 4
96 it.typeScopes.maxNewElements = 25
97 it.typeScopes.minNewElementsByType = typeMapMin
98 it.typeScopes.maxNewElementsByType = typeMapMax
99 it.contCycleLevel = 5
100 it.uniquenessDuplicates = false
101 ]
102 solution = reasoner.solve(problem, vampireConfig, workspace)
103
104 /*/
105 *
106 * reasoner = new AlloySolver
107 * val alloyConfig = new AlloySolverConfiguration => [
108 * it.typeScopes.maxNewElements = 7
109 * it.typeScopes.minNewElements = 3
110 * it.solutionScope.numberOfRequiredSolution = 1
111 * it.typeScopes.maxNewIntegers = 0
112 * it.documentationLevel = DocumentationLevel::NORMAL
113 * ]
114 * solution = reasoner.solve(problem, alloyConfig, workspace)
115 //*/
116
117
118 var totalTimeMin = (System.currentTimeMillis - startTime)/60000
119 var totalTimeSec = ((System.currentTimeMillis - startTime)/1000)% 60
120
121 println("Problem solved")
122 println("Time was: " + totalTimeMin + ":" + totalTimeSec)
123
124
125
126 27
28 for (Class elem : classMap.keySet) {
29 typeMap.put(e2l.TypeofEClass(
30 trace, listMap.get(elem.simpleName)
31 ), classMap.get(elem))
32 }
33 return typeMap
127 } 34 }
128 35
129 def static loadMetamodel(EPackage pckg) { 36 def static loadMetamodel(EPackage pckg) {
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
index eb3f4b14..1fac968b 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
@@ -1,34 +1,108 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse 1package ca.mcgill.ecse.dslreasoner.vampire.icse
2 2
3import functionalarchitecture.FunctionalarchitecturePackage 3import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
6import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
8import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
9import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
10import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
11import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
4import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 13import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
14import java.util.HashMap
5import org.eclipse.emf.ecore.resource.Resource 15import org.eclipse.emf.ecore.resource.Resource
6import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 16import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
7import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage
8import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.queries.YakinduPatterns
9 17
10class YakinduTest { 18class YakinduTest {
11 def static void main(String[] args) { 19 def static void main(String[] args) {
12 //Workspace setup 20 val Ecore2Logic ecore2Logic = new Ecore2Logic
21 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
22 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
23
24 // Workspace setup
13 val inputs = new FileSystemWorkspace('''initialModels/''', "") 25 val inputs = new FileSystemWorkspace('''initialModels/''', "")
14 val workspace = new FileSystemWorkspace('''output/YakinduTest/''', "") 26 val workspace = new FileSystemWorkspace('''output/YakinduTest/''', "")
15 workspace.initAndClear 27 workspace.initAndClear
16 28
17 //Logicproblem writing setup 29 // Logicproblem writing setup
18 val reg = Resource.Factory.Registry.INSTANCE 30 val reg = Resource.Factory.Registry.INSTANCE
19 val map = reg.extensionToFactoryMap 31 val map = reg.extensionToFactoryMap
20 map.put("logicproblem", new XMIResourceFactoryImpl) 32 map.put("logicproblem", new XMIResourceFactoryImpl)
21 33
22 println("Input and output workspaces are created") 34 println("Input and output workspaces are created")
23 35
24 val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE) 36 val metamodel = GeneralTest.loadMetamodel(yakinduPackage.eINSTANCE)
25 val partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi") 37 val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/yakinduinstance.xmi")
26// val queries = GeneralTest.loadQueries(metamodel, FamPa 38// val queries = GeneralTest.loadQueries(metamodel, FamPa
39 val queries = null
27 40
28 println("DSL loaded") 41 println("DSL loaded")
29 42
30// GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) 43 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
44 var problem = modelGenerationProblem.output
45// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
46// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
47 workspace.writeModel(problem, "Yakindu.logicproblem")
48
49 println("Problem created")
50
51 // Start Time
52 var startTime = System.currentTimeMillis
53
54 var LogicReasoner reasoner
55 // *
56 reasoner = new VampireSolver
57
58 // /////////////////////////////////////////////////////
59 // Minimum Scope
60 val classMapMin = new HashMap<Class, Integer>
61// classMapMin.put(Function, 1)
62// classMapMin.put(FunctionalInterface, 2)
63// classMapMin.put(FunctionalOutput, 3)
64 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace)
65
66 // Maximum Scope
67 val classMapMax = new HashMap<Class, Integer>
68// classMapMax.put(Function, 5)
69// classMapMax.put(FunctionalInterface, 2)
70// classMapMax.put(FunctionalOutput, 4)
71 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace)
72
73 // Define Config File
74 val vampireConfig = new VampireSolverConfiguration => [
75 // add configuration things, in config file first
76 it.documentationLevel = DocumentationLevel::FULL
77
78 it.typeScopes.minNewElements = 20
79 it.typeScopes.maxNewElements = 30
80 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin
81 if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax
82 it.contCycleLevel = 5
83 it.uniquenessDuplicates = false
84 ]
85
86 var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace)
87
88 /*/
89 *
90 * reasoner = new AlloySolver
91 * val alloyConfig = new AlloySolverConfiguration => [
92 * it.typeScopes.maxNewElements = 7
93 * it.typeScopes.minNewElements = 3
94 * it.solutionScope.numberOfRequiredSolution = 1
95 * it.typeScopes.maxNewIntegers = 0
96 * it.documentationLevel = DocumentationLevel::NORMAL
97 * ]
98 * solution = reasoner.solve(problem, alloyConfig, workspace)
99 //*/
100 // /////////////////////////////////////////////////////
101 var totalTimeMin = (System.currentTimeMillis - startTime) / 60000
102 var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60
103
104 println("Problem solved")
105 println("Time was: " + totalTimeMin + ":" + totalTimeSec)
31 } 106 }
32 107
33
34} 108}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-17 19:48:49 +0000