diff options
Diffstat (limited to 'Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit')
4 files changed, 270 insertions, 112 deletions
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/DiverseMeasurementRunner.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/DiverseMeasurementRunner.xtend index f2a70552..e6ee0ad9 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/DiverseMeasurementRunner.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/DiverseMeasurementRunner.xtend | |||
@@ -1,41 +1,52 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run | 1 | package hu.bme.mit.inf.dslreasoner.run |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | ||
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage | ||
8 | import org.eclipse.emf.ecore.resource.Resource | ||
9 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
11 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
16 | import org.eclipse.xtend.lib.annotations.Data | ||
17 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor | ||
18 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | ||
20 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | ||
21 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | 3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic |
22 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration |
23 | import org.eclipse.emf.ecore.EObject | 5 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor |
24 | import java.util.List | 6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage |
25 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult |
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
29 | import hu.bme.mit.inf.dslreasoner.logic.model.statistics.StatisticSections2Print | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.statistics.StatisticSections2Print |
12 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | ||
13 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | ||
14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | ||
15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor | ||
16 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy | ||
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | ||
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
26 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
27 | import java.util.List | ||
28 | import org.eclipse.emf.ecore.EObject | ||
29 | import org.eclipse.emf.ecore.resource.Resource | ||
30 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
31 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
32 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
33 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
34 | import org.eclipse.xtend.lib.annotations.Data | ||
35 | import java.util.LinkedList | ||
36 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver | ||
37 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
30 | 38 | ||
31 | enum Metamodel { | 39 | enum Metamodel { |
32 | FAM, YakinduWOSynch, Yakindu | 40 | FAM, YakinduWOSynch, Yakindu |
33 | } | 41 | } |
34 | enum Constraints { | 42 | enum Constraints { |
35 | None, PlusOne, MinusOne | 43 | None, Metamodel, All, PlusOne, MinusOne |
36 | } | 44 | } |
37 | enum StateCoder { | 45 | enum StateCoder { |
38 | ID, R1, R2, R3; | 46 | ID, Normal, R1, R2, R3; |
47 | } | ||
48 | enum Solver { | ||
49 | ViatraSolver, Alloy | ||
39 | } | 50 | } |
40 | 51 | ||
41 | @Data | 52 | @Data |
@@ -46,6 +57,7 @@ class Scenario { | |||
46 | Constraints constraints | 57 | Constraints constraints |
47 | StateCoder statecoder | 58 | StateCoder statecoder |
48 | int runs | 59 | int runs |
60 | Solver solver | ||
49 | } | 61 | } |
50 | 62 | ||
51 | class ScenarioRunner { | 63 | class ScenarioRunner { |
@@ -53,12 +65,15 @@ class ScenarioRunner { | |||
53 | // Workspace | 65 | // Workspace |
54 | private val FileSystemWorkspace inputs = new FileSystemWorkspace('''initialModels/''',"") | 66 | private val FileSystemWorkspace inputs = new FileSystemWorkspace('''initialModels/''',"") |
55 | private val ViatraReasoner viatraSolver = new ViatraReasoner | 67 | private val ViatraReasoner viatraSolver = new ViatraReasoner |
68 | private val AlloySolver alloySolver = new AlloySolver | ||
56 | private var MetamodelLoader loader | 69 | private var MetamodelLoader loader |
57 | 70 | ||
58 | val Ecore2Logic ecore2Logic = new Ecore2Logic | 71 | val Ecore2Logic ecore2Logic = new Ecore2Logic |
59 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | 72 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) |
73 | val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) | ||
60 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | 74 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic |
61 | 75 | ||
76 | var matchStatistics = "" | ||
62 | 77 | ||
63 | public def runScenario(Scenario scenario) { | 78 | public def runScenario(Scenario scenario) { |
64 | init() | 79 | init() |
@@ -69,31 +84,46 @@ class ScenarioRunner { | |||
69 | 84 | ||
70 | // printHeader(scenario) | 85 | // printHeader(scenario) |
71 | 86 | ||
72 | if(scenario.constraints == Constraints.None) { | 87 | if( scenario.constraints == Constraints.None || |
88 | scenario.constraints == Constraints.Metamodel|| | ||
89 | scenario.constraints == Constraints.All) | ||
90 | { | ||
91 | if(scenario.constraints == Constraints.None) { | ||
92 | mm.attributes.forEach[it.lowerBound = 0] | ||
93 | mm.references.forEach[it.lowerBound = 0] | ||
94 | } | ||
95 | |||
96 | val useVQ = if(scenario.constraints == Constraints.None || scenario.constraints == Constraints.Metamodel) { | ||
97 | new ViatraQuerySetDescriptor(emptyList,emptySet,emptyMap) | ||
98 | } else { | ||
99 | vq | ||
100 | } | ||
73 | 101 | ||
74 | mm.attributes.forEach[it.lowerBound = 0] | ||
75 | mm.references.forEach[it.lowerBound = 0] | ||
76 | mm.references.removeAll(vq.derivedFeatures.values) | ||
77 | mm.attributes.removeAll(vq.derivedFeatures.values) | ||
78 | for(run : 1..scenario.runs) { | 102 | for(run : 1..scenario.runs) { |
79 | runCase(run==1,"noConstraints"+run,scenario,mm,new ViatraQuerySetDescriptor(vq.patterns,emptySet,emptyMap),ps) | 103 | runCase(run==1,scenario.constraints+""+run,run,scenario,mm,useVQ,ps) |
104 | |||
105 | System.gc System.gc System.gc | ||
106 | Thread.sleep(3000) | ||
80 | } | 107 | } |
81 | } else { | 108 | println(matchStatistics) |
82 | 109 | ||
110 | } else if(scenario.constraints == Constraints.MinusOne) { | ||
111 | var first = true | ||
112 | //for(remove : vq.validationPatterns) { | ||
113 | for(run : 1..scenario.runs) { | ||
114 | |||
115 | //val removeName = remove.fullyQualifiedName | ||
116 | //val desc = new ViatraQuerySetDescriptor(vq.patterns,vq.validationPatterns.filter[it != remove].toSet,emptyMap) | ||
117 | runCase(first,"minusOne"+run,run,scenario,mm,vq,ps) | ||
118 | first = false | ||
119 | System.gc System.gc System.gc | ||
120 | //Thread.sleep(3000) | ||
121 | } | ||
122 | //} | ||
83 | } | 123 | } |
84 | |||
85 | |||
86 | } | 124 | } |
87 | 125 | ||
88 | // private def printHeader(Scenario scenario) { | 126 | private def runCase(boolean first, String id, int run, Scenario scenario, EcoreMetamodelDescriptor mm, ViatraQuerySetDescriptor vq, List<EObject> partialModel) { |
89 | // print("id;Solution type (ms);Transformation time (ms);Solver time (ms);") | ||
90 | // (1..scenario.number).forEach[print("sol"+it+" (nano);")] | ||
91 | // print("TransformationExecutionTime (ms);TypeAnalysisTime (ms);StateCoderTime (ms);SolutionCopyTime (ms);") | ||
92 | // print("SolutionDiversityCheckTime (ms);SolutionDiversitySuccessRate (%);") | ||
93 | // println("save") | ||
94 | // } | ||
95 | |||
96 | private def runCase(boolean first, String id, Scenario scenario, EcoreMetamodelDescriptor mm, ViatraQuerySetDescriptor vq, List<EObject> partialModel) { | ||
97 | // Transform | 127 | // Transform |
98 | val metamodelProblem = ecore2Logic.transformMetamodel(mm,new Ecore2LogicConfiguration()) | 128 | val metamodelProblem = ecore2Logic.transformMetamodel(mm,new Ecore2LogicConfiguration()) |
99 | instanceModel2Logic.transform(metamodelProblem,partialModel) | 129 | instanceModel2Logic.transform(metamodelProblem,partialModel) |
@@ -107,9 +137,19 @@ class ScenarioRunner { | |||
107 | val config = getSolverConfiguration(scenario,vq) | 137 | val config = getSolverConfiguration(scenario,vq) |
108 | 138 | ||
109 | // Execute | 139 | // Execute |
110 | val solution = viatraSolver.solve(problem,config,workspace) | 140 | val solution = getSolver(scenario).solve(problem,config,workspace) |
111 | printStatistics(solution,scenario,workspace,id,first) | 141 | //printMatchCountStatistics(solution,id) |
112 | 142 | val emfModels = new LinkedList | |
143 | if(solution instanceof ModelResult) { | ||
144 | val interpretations = getSolver(scenario).getInterpretations(solution) | ||
145 | for(interpretation : interpretations) { | ||
146 | val instanceModel = logic2Ecore.transformInterpretation(interpretation,metamodelProblem.trace) | ||
147 | emfModels+=instanceModel | ||
148 | } | ||
149 | |||
150 | } | ||
151 | printStatistics(solution,emfModels,scenario,workspace,id,run,first) | ||
152 | |||
113 | } | 153 | } |
114 | 154 | ||
115 | private def init() { | 155 | private def init() { |
@@ -128,43 +168,67 @@ class ScenarioRunner { | |||
128 | loader = if(metamodel == Metamodel::FAM) { | 168 | loader = if(metamodel == Metamodel::FAM) { |
129 | new FAMLoader(inputs) | 169 | new FAMLoader(inputs) |
130 | } else if(metamodel == Metamodel::Yakindu || metamodel == Metamodel::YakinduWOSynch) { | 170 | } else if(metamodel == Metamodel::Yakindu || metamodel == Metamodel::YakinduWOSynch) { |
131 | new YakinduLoader(inputs) | 171 | new YakinduLoader(inputs) => [it.useSynchronization = false] |
132 | } else throw new IllegalArgumentException('''Unknown domain: «metamodel»''') | 172 | } else throw new IllegalArgumentException('''Unknown domain: «metamodel»''') |
133 | } | 173 | } |
134 | 174 | ||
175 | def private getSolver(Scenario scenario) { | ||
176 | if(scenario.solver == Solver::ViatraSolver) { | ||
177 | viatraSolver | ||
178 | } else if(scenario.solver == Solver::Alloy) { | ||
179 | alloySolver | ||
180 | } | ||
181 | } | ||
182 | |||
135 | def private getSolverConfiguration(Scenario scenario, ViatraQuerySetDescriptor vq) { | 183 | def private getSolverConfiguration(Scenario scenario, ViatraQuerySetDescriptor vq) { |
136 | val viatraConfig = new ViatraReasonerConfiguration => [ | 184 | if(scenario.solver == Solver.ViatraSolver) { |
137 | it.runtimeLimit = 300 | 185 | val viatraConfig = new ViatraReasonerConfiguration => [ |
138 | it.typeScopes.maxNewElements = scenario.size | 186 | it.runtimeLimit = 300 |
139 | it.typeScopes.minNewElements = scenario.size | 187 | it.typeScopes.maxNewElements = scenario.size |
140 | it.solutionScope.numberOfRequiredSolution = scenario.number | 188 | it.typeScopes.minNewElements = scenario.size |
141 | it.existingQueries = vq.patterns.map[it.internalQueryRepresentation] | 189 | it.solutionScope.numberOfRequiredSolution = scenario.number |
142 | it.nameNewElements = false | 190 | it.existingQueries = vq.patterns.map[it.internalQueryRepresentation] |
143 | it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis | 191 | it.nameNewElements = false |
144 | it.additionalGlobalConstraints += loader.additionalConstraints | 192 | it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis |
145 | it.stateCoderStrategy = StateCoderStrategy::Neighbourhood | 193 | it.additionalGlobalConstraints += loader.additionalConstraints |
146 | if(scenario.statecoder != StateCoder::ID) { | 194 | it.stateCoderStrategy = if(scenario.statecoder == StateCoder::ID) { |
147 | val range = if(scenario.statecoder != StateCoder::R1) { | 195 | StateCoderStrategy::IDBased |
148 | 1 | 196 | } else { |
149 | } else if(scenario.statecoder != StateCoder::R2) { | 197 | StateCoderStrategy::Neighbourhood |
150 | 2 | ||
151 | } else if(scenario.statecoder != StateCoder::R3) { | ||
152 | 3 | ||
153 | } | 198 | } |
154 | 199 | if(scenario.statecoder != StateCoder::ID || scenario.statecoder != StateCoder::Normal) { | |
155 | it.diversityRequirement = new DiversityDescriptor => [ | 200 | val range = if(scenario.statecoder != StateCoder::R1) { |
156 | it.relevantTypes = null | 201 | 1 |
157 | it.relevantRelations = null | 202 | } else if(scenario.statecoder != StateCoder::R2) { |
158 | it.maxNumber = 1 | 203 | 2 |
159 | it.range = range | 204 | } else if(scenario.statecoder != StateCoder::R3) { |
160 | it.parallels = 1 | 205 | 3 |
161 | ] | 206 | } |
162 | } | 207 | |
163 | ] | 208 | it.diversityRequirement = new DiversityDescriptor => [ |
164 | return viatraConfig | 209 | it.relevantTypes = null |
210 | it.relevantRelations = null | ||
211 | it.maxNumber = 1 | ||
212 | it.range = range | ||
213 | it.parallels = 1 | ||
214 | ] | ||
215 | } | ||
216 | ] | ||
217 | return viatraConfig | ||
218 | } else if(scenario.solver == Solver::Alloy) { | ||
219 | return new AlloySolverConfiguration => [ | ||
220 | it.runtimeLimit = 300 | ||
221 | it.typeScopes.maxNewElements = scenario.size | ||
222 | it.typeScopes.minNewElements = scenario.size | ||
223 | it.solutionScope.numberOfRequiredSolution = scenario.number | ||
224 | it.typeScopes.maxIntScope = 0 | ||
225 | it.writeToFile=true | ||
226 | ] | ||
227 | } | ||
228 | |||
165 | } | 229 | } |
166 | 230 | ||
167 | def printStatistics(LogicResult solution, Scenario scenario, FileSystemWorkspace workspace, String id, boolean printHeader) { | 231 | def printStatistics(LogicResult solution, List<EObject> emfModels, Scenario scenario, FileSystemWorkspace workspace, String id,int run, boolean printHeader) { |
168 | if(printHeader) { | 232 | if(printHeader) { |
169 | print("id;Solution type (ms);Transformation time (ms);Solver time (ms);") | 233 | print("id;Solution type (ms);Transformation time (ms);Solver time (ms);") |
170 | solution.statistics.entries.map[name].forEach[print(it+";")] | 234 | solution.statistics.entries.map[name].forEach[print(it+";")] |
@@ -179,27 +243,73 @@ class ScenarioRunner { | |||
179 | 243 | ||
180 | print((new StatisticSections2Print).transformStatisticDatas2CSV(solution.statistics.entries)) | 244 | print((new StatisticSections2Print).transformStatisticDatas2CSV(solution.statistics.entries)) |
181 | 245 | ||
182 | if(solution instanceof ModelResult) { | 246 | val representations = solution.representation |
183 | val representations = solution.representation | 247 | for(representationIndex : 0..<representations.size) { |
184 | for(representationIndex : 0..<representations.size) { | 248 | val representation = representations.get(representationIndex) |
185 | val representation = representations.get(representationIndex) | 249 | val emfModel = emfModels.get(representationIndex) |
186 | val representationNumber = representationIndex + 1 | 250 | val representationNumber = representationIndex + 1 |
187 | if(representation instanceof PartialInterpretation) { | 251 | if(representation instanceof PartialInterpretation) { |
188 | workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''') | 252 | workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''') |
189 | } else { | 253 | val partialInterpretation2GML = new PartialInterpretation2Gml |
190 | workspace.writeText('''solution«representationNumber».txt''',representation.toString) | 254 | val gml = partialInterpretation2GML.transform(representation) |
191 | } | 255 | //ecore2GML.transform(root) |
256 | workspace.writeText('''solutionVisualisation«representationNumber».gml''',gml) | ||
257 | } else { | ||
258 | workspace.writeText('''solution«representationNumber».txt''',representation.toString) | ||
192 | } | 259 | } |
193 | println('''saved''') | 260 | workspace.writeModel(emfModel,'''AM_«run»_«representationIndex+1».xmi''') |
194 | } else { | ||
195 | println('''notsaved''') | ||
196 | } | 261 | } |
262 | println('''saved''') | ||
197 | } | 263 | } |
264 | |||
265 | /* | ||
266 | def printMatchCountStatistics(LogicResult solution, String run) { | ||
267 | //val additionalMatches = ViatraReasoner::additionalMatches | ||
268 | val allPatterns = ViatraReasoner::allPatterns | ||
269 | val allModels = solution.representation | ||
270 | //val header = additionalMatches.head.keySet | ||
271 | //var res = '''run;model;«FOR pattern: header SEPARATOR ";"»«pattern»«ENDFOR» | ||
272 | //''' | ||
273 | var res = '''run;model;«FOR pattern: allPatterns.filter[calculateCount] SEPARATOR ";"»«pattern.fullyQualifiedName»«ENDFOR» | ||
274 | ''' | ||
275 | var modelIndex = 1 | ||
276 | for(model : allModels) { | ||
277 | //println(modelIndex) | ||
278 | val actualModel = model as PartialInterpretation | ||
279 | |||
280 | // Access the default local search hint | ||
281 | val localSearchHint = LocalSearchHints.getDefault().build(); | ||
282 | |||
283 | // Build an engine options with the local search hint | ||
284 | //val options = ViatraQueryEngineOptions. | ||
285 | // defineOptions(). | ||
286 | // withDefaultHint(localSearchHint). | ||
287 | // withDefaultBackend(localSearchHint.getQueryBackendFactory()). // this line is needed in 1.4 due to bug 507777 | ||
288 | // build(); | ||
289 | |||
290 | val engine = ViatraQueryEngine.on(new EMFScope(actualModel),options) | ||
291 | var line = '''«run»;«modelIndex»''' | ||
292 | for(pattern : allPatterns.filter[calculateCount]) { | ||
293 | val matcher = pattern.getMatcher(engine) | ||
294 | line+=";"+matcher.countMatches | ||
295 | } | ||
296 | //;«FOR pattern : model.entrySet SEPARATOR ";"»«pattern.value»«ENDFOR»''' | ||
297 | //val p = model as PartialInterpretation; | ||
298 | modelIndex++ | ||
299 | res+=line+"\n" | ||
300 | } | ||
301 | matchStatistics+= res | ||
302 | } | ||
303 | |||
304 | def boolean calculateCount(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> pattern) { | ||
305 | pattern.fullyQualifiedName.startsWith("currentInRelation_pattern") | ||
306 | //true | ||
307 | }*/ | ||
198 | } | 308 | } |
199 | 309 | ||
200 | class DiverseMeasurementRunner { | 310 | class DiverseMeasurementRunner { |
201 | def static void main(String[] args) { | 311 | def static void main(String[] args) { |
202 | val scenario = new Scenario(50,50,Metamodel::Yakindu,Constraints.None,StateCoder.ID,12) | 312 | val scenario = new Scenario(100,49,Metamodel::Yakindu,Constraints.All,StateCoder.Normal,1,Solver::Alloy) |
203 | val scenarioRunner = new ScenarioRunner | 313 | val scenarioRunner = new ScenarioRunner |
204 | scenarioRunner.runScenario(scenario) | 314 | scenarioRunner.runScenario(scenario) |
205 | } | 315 | } |
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend index 3da6305d..60908365 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend | |||
@@ -87,24 +87,40 @@ class FAMLoader extends MetamodelLoader{ | |||
87 | 87 | ||
88 | class YakinduLoader extends MetamodelLoader{ | 88 | class YakinduLoader extends MetamodelLoader{ |
89 | 89 | ||
90 | private var useSynchronization = true; | ||
91 | public static val patternsWithSynchronization = #[ | ||
92 | "synchHasNoOutgoing", "synchHasNoIncoming", "SynchronizedIncomingInSameRegion", "notSynchronizingStates", | ||
93 | "hasMultipleOutgoingTrainsition", "hasMultipleIncomingTrainsition", "SynchronizedRegionsAreNotSiblings", | ||
94 | "SynchronizedRegionDoesNotHaveMultipleRegions", "synchThree", "twoSynch"] | ||
95 | |||
90 | new(ReasonerWorkspace workspace) { | 96 | new(ReasonerWorkspace workspace) { |
91 | super(workspace) | 97 | super(workspace) |
92 | } | 98 | } |
93 | 99 | ||
100 | public def setUseSynchronization(boolean useSynchronization) { | ||
101 | this.useSynchronization = useSynchronization | ||
102 | } | ||
103 | |||
94 | override loadMetamodel() { | 104 | override loadMetamodel() { |
105 | val useSynchInThisLoad = this.useSynchronization | ||
106 | |||
95 | val package = YakindummPackage.eINSTANCE | 107 | val package = YakindummPackage.eINSTANCE |
96 | val List<EClass> classes = package.EClassifiers.filter(EClass).toList | 108 | val List<EClass> classes = package.EClassifiers.filter(EClass).filter[(useSynchInThisLoad) || (it.name != "Synchronization")].toList |
97 | val List<EEnum> enums = package.EClassifiers.filter(EEnum).toList | 109 | val List<EEnum> enums = package.EClassifiers.filter(EEnum).toList |
98 | val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList | 110 | val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList |
99 | val List<EReference> references = classes.map[EReferences].flatten.toList | 111 | val List<EReference> references = classes.map[EReferences].flatten.toList |
100 | |||
101 | val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList | 112 | val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList |
102 | 113 | ||
103 | return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes) | 114 | return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes) |
104 | } | 115 | } |
105 | override loadQueries(EcoreMetamodelDescriptor metamodel) { | 116 | override loadQueries(EcoreMetamodelDescriptor metamodel) { |
117 | val useSynchInThisLoad = this.useSynchronization | ||
118 | |||
106 | val i = hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns.instance | 119 | val i = hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns.instance |
107 | val patterns = i.specifications.toList | 120 | val patterns = i.specifications.filter[spec | |
121 | useSynchInThisLoad || | ||
122 | !patternsWithSynchronization.exists[spec.fullyQualifiedName.endsWith(it)] | ||
123 | ].toList | ||
108 | val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet | 124 | val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet |
109 | val derivedFeatures = new LinkedHashMap | 125 | val derivedFeatures = new LinkedHashMap |
110 | val res = new ViatraQuerySetDescriptor( | 126 | val res = new ViatraQuerySetDescriptor( |
@@ -126,7 +142,7 @@ class YakinduLoader extends MetamodelLoader{ | |||
126 | this.workspace.readModel(EObject,"Yakindu.xmi").eResource.allContents.toList | 142 | this.workspace.readModel(EObject,"Yakindu.xmi").eResource.allContents.toList |
127 | } | 143 | } |
128 | 144 | ||
129 | override additionalConstraints() { | 145 | override additionalConstraints() { //#[] |
130 | #[[method | new SGraphInconsistencyDetector(method)]] | 146 | #[[method | new SGraphInconsistencyDetector(method)]] |
131 | } | 147 | } |
132 | } \ No newline at end of file | 148 | } \ No newline at end of file |
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphInconsistencyDetector.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphInconsistencyDetector.xtend index 3a7c5041..230bb692 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphInconsistencyDetector.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphInconsistencyDetector.xtend | |||
@@ -11,8 +11,11 @@ class SGraphInconsistencyDetector extends ModelGenerationMethodBasedGlobalConstr | |||
11 | var PartialInterpretation partialInterpretation | 11 | var PartialInterpretation partialInterpretation |
12 | var ViatraQueryMatcher<?> noEntry | 12 | var ViatraQueryMatcher<?> noEntry |
13 | var ViatraQueryMatcher<?> entryHasNoOutgoing | 13 | var ViatraQueryMatcher<?> entryHasNoOutgoing |
14 | var ViatraQueryMatcher<?> choiceHasNoOutgiong | ||
15 | var ViatraQueryMatcher<?> choiceHasNoIncoming | ||
16 | //var ViatraQueryMatcher<?> noSynch | ||
14 | var ViatraQueryMatcher<?> synchronizationHasNoOutgoing | 17 | var ViatraQueryMatcher<?> synchronizationHasNoOutgoing |
15 | var ViatraQueryMatcher<?> noSynch | 18 | |
16 | var ViatraQueryMatcher<?> synchronizedSiblingRegions | 19 | var ViatraQueryMatcher<?> synchronizedSiblingRegions |
17 | var ViatraQueryMatcher<?> noStateInRegion | 20 | var ViatraQueryMatcher<?> noStateInRegion |
18 | 21 | ||
@@ -36,33 +39,48 @@ class SGraphInconsistencyDetector extends ModelGenerationMethodBasedGlobalConstr | |||
36 | it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noOutgoingTransitionFromEntry") | 39 | it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noOutgoingTransitionFromEntry") |
37 | ].head.getMatcher(context.queryEngine) | 40 | ].head.getMatcher(context.queryEngine) |
38 | 41 | ||
39 | this.synchronizationHasNoOutgoing = method.unfinishedWF.filter[ | 42 | this.noStateInRegion = method.unfinishedWF.filter[ |
40 | it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasNoOutgoing") | 43 | it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noStateInRegion") |
41 | ].head.getMatcher(context.queryEngine) | 44 | ].head.getMatcher(context.queryEngine) |
42 | 45 | ||
43 | this.noSynch = method.unfinishedWF.filter[ | 46 | this.choiceHasNoOutgiong = method.unfinishedWF.filter[ |
44 | it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noSynch") | 47 | it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_choiceHasNoOutgoing") |
45 | ].head.getMatcher(context.queryEngine) | 48 | ].head.getMatcher(context.queryEngine) |
46 | 49 | ||
50 | // this.choiceHasNoIncoming = method.unfinishedWF.filter[ | ||
51 | // it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_choiceHasNoIncoming") | ||
52 | // ].head.getMatcher(context.queryEngine) | ||
53 | } catch(Exception e) { } | ||
54 | try{ | ||
55 | // this.noSynch = method.unfinishedWF.filter[ | ||
56 | // it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noSynch") | ||
57 | // ].head.getMatcher(context.queryEngine) | ||
58 | // | ||
47 | this.synchronizedSiblingRegions = method.unfinishedWF.filter[ | 59 | this.synchronizedSiblingRegions = method.unfinishedWF.filter[ |
48 | it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_SynchronizedRegionDoesNotHaveMultipleRegions") | 60 | it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_SynchronizedRegionDoesNotHaveMultipleRegions") |
49 | ].head.getMatcher(context.queryEngine) | 61 | ].head.getMatcher(context.queryEngine) |
50 | 62 | ||
51 | this.noStateInRegion = method.unfinishedWF.filter[ | 63 | this.synchronizationHasNoOutgoing = method.unfinishedWF.filter[ |
52 | it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noStateInRegion") | 64 | it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_synchHasNoOutgoing") |
53 | ].head.getMatcher(context.queryEngine) | 65 | ].head.getMatcher(context.queryEngine) |
54 | } catch(Exception e) { } | 66 | } catch(Exception e) { } |
55 | } | 67 | } |
56 | 68 | ||
57 | override checkGlobalConstraint(ThreadContext context) { | 69 | override checkGlobalConstraint(ThreadContext context) { |
58 | if(noEntry !== null) { | 70 | if(noEntry !== null) { |
59 | val requiredNewObjects = | 71 | var requiredNewObjects = |
60 | noEntry.countMatches*2 + | 72 | noEntry.countMatches*2 + |
61 | entryHasNoOutgoing.countMatches + | 73 | entryHasNoOutgoing.countMatches + |
62 | synchronizationHasNoOutgoing.countMatches + | 74 | choiceHasNoOutgiong.countMatches+ |
63 | noSynch.countMatches*2 + | 75 | //choiceHasNoIncoming.countMatches+ |
64 | synchronizedSiblingRegions.countMatches*4 | ||
65 | noStateInRegion.countMatches | 76 | noStateInRegion.countMatches |
77 | if(synchronizationHasNoOutgoing!= null) { | ||
78 | requiredNewObjects += | ||
79 | //noSynch.countMatches*2 + | ||
80 | synchronizationHasNoOutgoing.countMatches + | ||
81 | synchronizedSiblingRegions.countMatches*4 | ||
82 | } | ||
83 | |||
66 | val availableNewObjects = partialInterpretation.maxNewElements | 84 | val availableNewObjects = partialInterpretation.maxNewElements |
67 | val res = availableNewObjects >= requiredNewObjects | 85 | val res = availableNewObjects >= requiredNewObjects |
68 | //println('''[«availableNewObjects» >= «requiredNewObjects»] = «res»''') | 86 | //println('''[«availableNewObjects» >= «requiredNewObjects»] = «res»''') |
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend index d9536989..20683fff 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend | |||
@@ -30,6 +30,9 @@ import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | |||
30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml | 30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml |
31 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | 31 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration |
32 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver | 32 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver |
33 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
35 | import java.util.LinkedList | ||
33 | 36 | ||
34 | class SimpleRun { | 37 | class SimpleRun { |
35 | 38 | ||
@@ -47,6 +50,7 @@ class SimpleRun { | |||
47 | println("DSL loaded") | 50 | println("DSL loaded") |
48 | 51 | ||
49 | val Ecore2Logic ecore2Logic = new Ecore2Logic | 52 | val Ecore2Logic ecore2Logic = new Ecore2Logic |
53 | val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) | ||
50 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | 54 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) |
51 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | 55 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic |
52 | 56 | ||
@@ -58,9 +62,9 @@ class SimpleRun { | |||
58 | 62 | ||
59 | println("Problem created") | 63 | println("Problem created") |
60 | var LogicResult solution | 64 | var LogicResult solution |
61 | 65 | var LogicReasoner reasoner | |
62 | //* | 66 | /* |
63 | val ViatraReasoner viatraSolver = new ViatraReasoner | 67 | reasoner = new ViatraReasoner |
64 | val viatraConfig = new ViatraReasonerConfiguration => [ | 68 | val viatraConfig = new ViatraReasonerConfiguration => [ |
65 | it.typeScopes.maxNewElements = 10 | 69 | it.typeScopes.maxNewElements = 10 |
66 | it.typeScopes.minNewElements = 10 | 70 | it.typeScopes.minNewElements = 10 |
@@ -70,9 +74,9 @@ class SimpleRun { | |||
70 | it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis | 74 | it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis |
71 | it.stateCoderStrategy = StateCoderStrategy::Neighbourhood | 75 | it.stateCoderStrategy = StateCoderStrategy::Neighbourhood |
72 | ] | 76 | ] |
73 | solution = viatraSolver.solve(logicProblem,viatraConfig,workspace) | 77 | solution = reasoner.solve(logicProblem,viatraConfig,workspace) |
74 | /*/ | 78 | /*/ |
75 | val AlloySolver alloyReasoner = new AlloySolver | 79 | reasoner = new AlloySolver |
76 | val alloyConfig = new AlloySolverConfiguration => [ | 80 | val alloyConfig = new AlloySolverConfiguration => [ |
77 | it.typeScopes.maxNewElements = 5 | 81 | it.typeScopes.maxNewElements = 5 |
78 | it.typeScopes.minNewElements = 5 | 82 | it.typeScopes.minNewElements = 5 |
@@ -80,12 +84,19 @@ class SimpleRun { | |||
80 | it.typeScopes.maxIntScope = 0 | 84 | it.typeScopes.maxIntScope = 0 |
81 | it.writeToFile = true | 85 | it.writeToFile = true |
82 | ] | 86 | ] |
83 | solution = alloyReasoner.solve(logicProblem,alloyConfig,workspace) | 87 | solution = reasoner.solve(logicProblem,alloyConfig,workspace) |
84 | //*/ | 88 | //*/ |
85 | 89 | ||
86 | println("Problem solved") | 90 | println("Problem solved") |
87 | 91 | ||
88 | solution.writeSolution(workspace) | 92 | val interpretations = reasoner.getInterpretations(solution as ModelResult) |
93 | val models = new LinkedList | ||
94 | for(interpretation : interpretations) { | ||
95 | val instanceModel = logic2Ecore.transformInterpretation(interpretation,modelGenerationProblem.trace) | ||
96 | models+=instanceModel | ||
97 | } | ||
98 | |||
99 | solution.writeSolution(workspace, #[]) | ||
89 | } | 100 | } |
90 | 101 | ||
91 | def private static loadMetamodel() { | 102 | def private static loadMetamodel() { |
@@ -118,7 +129,7 @@ class SimpleRun { | |||
118 | inputs.readModel(EObject,"FAM.xmi").eResource.allContents.toList | 129 | inputs.readModel(EObject,"FAM.xmi").eResource.allContents.toList |
119 | } | 130 | } |
120 | 131 | ||
121 | def static writeSolution(LogicResult solution, ReasonerWorkspace workspace) { | 132 | def static writeSolution(LogicResult solution, ReasonerWorkspace workspace, List<EObject> models) { |
122 | if(solution instanceof ModelResult) { | 133 | if(solution instanceof ModelResult) { |
123 | val representations = solution.representation | 134 | val representations = solution.representation |
124 | for(representationIndex : 0..<representations.size) { | 135 | for(representationIndex : 0..<representations.size) { |
@@ -135,6 +146,9 @@ class SimpleRun { | |||
135 | workspace.writeText('''solution«representationNumber».txt''',representation.toString) | 146 | workspace.writeText('''solution«representationNumber».txt''',representation.toString) |
136 | } | 147 | } |
137 | } | 148 | } |
149 | for(model : models) { | ||
150 | workspace.writeModel(model,"model.xmi") | ||
151 | } | ||
138 | println("Solution saved and visualised") | 152 | println("Solution saved and visualised") |
139 | } | 153 | } |
140 | } | 154 | } |