aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/hu.bme.mit.inf.dslreasoner.run
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <oszka@152.66.252.189>2017-07-05 16:38:04 +0200
committerLibravatar OszkarSemerath <oszka@152.66.252.189>2017-07-05 16:38:04 +0200
commitc085abd5f2dd49c8be1b32451c8f2ca05fa15f52 (patch)
tree3740158d8d00c8f4ede888eead105f6650871713 /Tests/hu.bme.mit.inf.dslreasoner.run
parentSupport for generationg multiple difference models by VIATRA-Solver (diff)
downloadVIATRA-Generator-c085abd5f2dd49c8be1b32451c8f2ca05fa15f52.tar.gz
VIATRA-Generator-c085abd5f2dd49c8be1b32451c8f2ca05fa15f52.tar.zst
VIATRA-Generator-c085abd5f2dd49c8be1b32451c8f2ca05fa15f52.zip
Example configuration for running measurements.
Diffstat (limited to 'Tests/hu.bme.mit.inf.dslreasoner.run')
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/.classpath2
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/META-INF/MANIFEST.MF4
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/plugin.xml29
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/DiverseMeasurementRunner.xtend288
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend24
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphInconsistencyDetector.xtend40
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend30
7 files changed, 278 insertions, 139 deletions
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/.classpath b/Tests/hu.bme.mit.inf.dslreasoner.run/.classpath
index 2b46fc9b..29ba3981 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/.classpath
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/.classpath
@@ -4,6 +4,6 @@
4 <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> 4 <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
5 <classpathentry kind="src" path="src"/> 5 <classpathentry kind="src" path="src"/>
6 <classpathentry kind="src" path="xtend-gen"/> 6 <classpathentry kind="src" path="xtend-gen"/>
7 <classpathentry kind="src" path="src-gen/"/> 7 <classpathentry kind="src" path="src-gen"/>
8 <classpathentry kind="output" path="bin"/> 8 <classpathentry kind="output" path="bin"/>
9</classpath> 9</classpath>
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/META-INF/MANIFEST.MF b/Tests/hu.bme.mit.inf.dslreasoner.run/META-INF/MANIFEST.MF
index 9c2210bc..4193c535 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/META-INF/MANIFEST.MF
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/META-INF/MANIFEST.MF
@@ -25,6 +25,8 @@ Require-Bundle: hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlan
25 hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0", 25 hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0",
26 org.eclipse.viatra.dse;bundle-version="0.15.0", 26 org.eclipse.viatra.dse;bundle-version="0.15.0",
27 hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", 27 hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0",
28 hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic;bundle-version="1.0.0" 28 hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic;bundle-version="1.0.0",
29 org.eclipse.viatra.query.runtime.localsearch;bundle-version="1.5.0",
30 hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0"
29Import-Package: org.apache.log4j 31Import-Package: org.apache.log4j
30Bundle-RequiredExecutionEnvironment: JavaSE-1.8 32Bundle-RequiredExecutionEnvironment: JavaSE-1.8
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/plugin.xml b/Tests/hu.bme.mit.inf.dslreasoner.run/plugin.xml
index 6bb6c623..6b75179d 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/plugin.xml
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/plugin.xml
@@ -68,39 +68,18 @@
68 <extension id="GeneratedQueries" point="org.eclipse.viatra.query.runtime.queryspecification"> 68 <extension id="GeneratedQueries" point="org.eclipse.viatra.query.runtime.queryspecification">
69 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:GeneratedQueries" id="GeneratedQueries"> 69 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:GeneratedQueries" id="GeneratedQueries">
70 <query-specification fqn="mayEquivalent"/> 70 <query-specification fqn="mayEquivalent"/>
71 <query-specification fqn="invalidatedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_SynchronizedRegionsAreNotSiblings"/>
72 <query-specification fqn="invalidatedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_incomingToEntry"/>
73 <query-specification fqn="invalidatedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noEntryInRegion"/>
74 <query-specification fqn="invalidatedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasNoIncomingOrOutgoing"/>
75 <query-specification fqn="invalidatedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_notSynchronizingStates"/>
76 <query-specification fqn="invalidatedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_outgoingTrainsitionToDifferentRegion"/>
77 <query-specification fqn="invalidatedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_SynchronizedVerticesInSameRegion"/>
78 <query-specification fqn="invalidatedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_multipleEntryInRegion"/>
79 <query-specification fqn="invalidatedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_multipleTransitionFromEntry"/>
80 <query-specification fqn="invalidatedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noOutgoingTransitionFromEntry"/>
81 <query-specification fqn="unfinishedLowerMultiplicity_inreference_target_Transition"/>
82 <query-specification fqn="unfinishedLowerMultiplicity_inreference_source_Transition"/>
83 <query-specification fqn="unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_SynchronizedRegionsAreNotSiblings"/>
84 <query-specification fqn="unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_incomingToEntry"/>
85 <query-specification fqn="unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noEntryInRegion"/>
86 <query-specification fqn="unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasNoIncomingOrOutgoing"/>
87 <query-specification fqn="unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_notSynchronizingStates"/>
88 <query-specification fqn="unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_outgoingTrainsitionToDifferentRegion"/>
89 <query-specification fqn="unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_SynchronizedVerticesInSameRegion"/>
90 <query-specification fqn="unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_multipleEntryInRegion"/>
91 <query-specification fqn="unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_multipleTransitionFromEntry"/>
92 <query-specification fqn="unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noOutgoingTransitionFromEntry"/>
93 <query-specification fqn="createObject_class_Entry_by_inreference_vertices_Region"/> 71 <query-specification fqn="createObject_class_Entry_by_inreference_vertices_Region"/>
94 <query-specification fqn="createObject_class_State_by_inreference_vertices_Region"/> 72 <query-specification fqn="createObject_class_State_by_inreference_vertices_Region"/>
95 <query-specification fqn="createObject_class_Transition_by_inreference_outgoingTransitions_Vertex_with_inreference_source_Transition"/>
96 <query-specification fqn="createObject_class_Region_by_inreference_regions_CompositeElement"/> 73 <query-specification fqn="createObject_class_Region_by_inreference_regions_CompositeElement"/>
74 <query-specification fqn="createObject_class_Transition_by_inreference_outgoingTransitions_Vertex_with_inreference_source_Transition"/>
75 <query-specification fqn="createObject_UndefinedPartOf_class_Statechart"/>
97 <query-specification fqn="createObject_class_Synchronization_by_inreference_vertices_Region"/> 76 <query-specification fqn="createObject_class_Synchronization_by_inreference_vertices_Region"/>
98 <query-specification fqn="refineTypeTo_class_Entry"/> 77 <query-specification fqn="refineTypeTo_class_Entry"/>
99 <query-specification fqn="refineTypeTo_class_State"/> 78 <query-specification fqn="refineTypeTo_class_State"/>
100 <query-specification fqn="refineTypeTo_class_Transition"/>
101 <query-specification fqn="refineTypeTo_class_Region"/> 79 <query-specification fqn="refineTypeTo_class_Region"/>
80 <query-specification fqn="refineTypeTo_class_Transition"/>
81 <query-specification fqn="refineTypeTo_UndefinedPartOf_class_Statechart"/>
102 <query-specification fqn="refineTypeTo_class_Synchronization"/> 82 <query-specification fqn="refineTypeTo_class_Synchronization"/>
103 <query-specification fqn="refineTypeTo_class_Statechart"/>
104 <query-specification fqn="refineRelation_inreference_incomingTransitions_Vertex_and_inreference_target_Transition"/> 83 <query-specification fqn="refineRelation_inreference_incomingTransitions_Vertex_and_inreference_target_Transition"/>
105 </group> 84 </group>
106 </extension> 85 </extension>
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 @@
1package hu.bme.mit.inf.dslreasoner.run 1package hu.bme.mit.inf.dslreasoner.run
2 2
3import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
4import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage
7import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage
8import org.eclipse.emf.ecore.resource.Resource
9import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage
10import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
11import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
12import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
13import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy
14import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
15import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
16import org.eclipse.xtend.lib.annotations.Data
17import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
18import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
20import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
21import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic 3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
22import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration 4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
23import org.eclipse.emf.ecore.EObject 5import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
24import java.util.List 6import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage
25import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage
8import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
26import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult 9import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
27import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
28import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult 10import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
29import hu.bme.mit.inf.dslreasoner.logic.model.statistics.StatisticSections2Print 11import hu.bme.mit.inf.dslreasoner.logic.model.statistics.StatisticSections2Print
12import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
13import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
14import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
15import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
16import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage
17import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
20import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage
21import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy
24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
26import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
27import java.util.List
28import org.eclipse.emf.ecore.EObject
29import org.eclipse.emf.ecore.resource.Resource
30import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
31import org.eclipse.viatra.query.runtime.api.IPatternMatch
32import org.eclipse.viatra.query.runtime.api.IQuerySpecification
33import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
34import org.eclipse.xtend.lib.annotations.Data
35import java.util.LinkedList
36import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
37import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
30 38
31enum Metamodel { 39enum Metamodel {
32 FAM, YakinduWOSynch, Yakindu 40 FAM, YakinduWOSynch, Yakindu
33} 41}
34enum Constraints { 42enum Constraints {
35 None, PlusOne, MinusOne 43 None, Metamodel, All, PlusOne, MinusOne
36} 44}
37enum StateCoder { 45enum StateCoder {
38 ID, R1, R2, R3; 46 ID, Normal, R1, R2, R3;
47}
48enum 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
51class ScenarioRunner { 63class 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
200class DiverseMeasurementRunner { 310class 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
88class YakinduLoader extends MetamodelLoader{ 88class 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
30import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml 30import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
31import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration 31import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
32import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver 32import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
33import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
34import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
35import java.util.LinkedList
33 36
34class SimpleRun { 37class 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 }