aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
diff options
context:
space:
mode:
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend97
1 files changed, 88 insertions, 9 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}