aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/hu.bme.mit.inf.dslreasoner.run/src
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:01:08 +0200
committerLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:01:08 +0200
commitd4f03121e36bce42ce611e97ffee6e697162228e (patch)
treebcda6a5e8d0a9d9fdc1dc8620a816e7f429f5d9a /Tests/hu.bme.mit.inf.dslreasoner.run/src
parentInitial commit (diff)
downloadVIATRA-Generator-d4f03121e36bce42ce611e97ffee6e697162228e.tar.gz
VIATRA-Generator-d4f03121e36bce42ce611e97ffee6e697162228e.tar.zst
VIATRA-Generator-d4f03121e36bce42ce611e97ffee6e697162228e.zip
Initial commit, migrating from SVN
Diffstat (limited to 'Tests/hu.bme.mit.inf.dslreasoner.run/src')
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend132
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend289
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphInconsistencyDetector.xtend82
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend145
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualisePartialInterpretation.xtend39
5 files changed, 687 insertions, 0 deletions
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
new file mode 100644
index 00000000..3da6305d
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
@@ -0,0 +1,132 @@
1package hu.bme.mit.inf.dslreasoner.run
2
3import hu.bme.mit.inf.dslreasomer.domains.transima.fam.FunctionalArchitecture.FunctionalArchitecturePackage
4import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
5import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
6import java.util.LinkedHashMap
7import java.util.List
8import org.eclipse.emf.ecore.EAttribute
9import org.eclipse.emf.ecore.EClass
10import org.eclipse.emf.ecore.EEnum
11import org.eclipse.emf.ecore.EEnumLiteral
12import org.eclipse.emf.ecore.EReference
13import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage
14import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethodBasedGlobalConstraint
15import org.eclipse.xtext.xbase.lib.Functions.Function1
16import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
17import org.eclipse.emf.ecore.EObject
18import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
19import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
20import java.util.Collection
21import java.util.Set
22import java.util.Collections
23
24abstract class MetamodelLoader {
25 protected val ReasonerWorkspace workspace
26 public new(ReasonerWorkspace workspace) {
27 this.workspace = workspace
28 }
29 def EcoreMetamodelDescriptor loadMetamodel()
30 def Set<EClass> getRelevantTypes(EcoreMetamodelDescriptor descriptor)
31 def Set<EReference> getRelevantReferences(EcoreMetamodelDescriptor descriptor)
32 def ViatraQuerySetDescriptor loadQueries(EcoreMetamodelDescriptor metamodel)
33 def List<EObject> loadPartialModel()
34
35 def List<Function1<ModelGenerationMethod,ModelGenerationMethodBasedGlobalConstraint>> additionalConstraints()
36
37 def <T> filterByNames(Iterable<T> collection, Function1<T,String> nameExtractor, Collection<String> requiredNames) {
38 val res = collection.filter[requiredNames.contains(nameExtractor.apply(it))]
39 if(res.size != requiredNames.size) throw new IllegalArgumentException
40 return res.toSet
41 }
42}
43
44class FAMLoader extends MetamodelLoader{
45
46 new(ReasonerWorkspace workspace) {
47 super(workspace)
48 }
49
50 override loadMetamodel() {
51 val package = FunctionalArchitecturePackage.eINSTANCE
52 val List<EClass> classes = package.EClassifiers.filter(EClass).toList
53 val List<EEnum> enums = package.EClassifiers.filter(EEnum).toList
54 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList
55 val List<EReference> references = classes.map[EReferences].flatten.toList
56 val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList
57 return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes)
58 }
59
60 override getRelevantTypes(EcoreMetamodelDescriptor descriptor) {
61 return descriptor.classes.filterByNames([it.name],#["FunctionalElement"])
62 }
63 override getRelevantReferences(EcoreMetamodelDescriptor descriptor) {
64 return descriptor.references.filterByNames([it.name],#["subElements"])
65 }
66
67 override loadQueries(EcoreMetamodelDescriptor metamodel) {
68 val i = hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern.instance
69 val patterns = i.specifications.toList
70 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet
71 val derivedFeatures = new LinkedHashMap
72 derivedFeatures.put(i.type.internalQueryRepresentation,metamodel.attributes.filter[it.name == "type"].head)
73 derivedFeatures.put(i.model.internalQueryRepresentation,metamodel.references.filter[it.name == "model"].head)
74 val res = new ViatraQuerySetDescriptor(
75 patterns,
76 wfPatterns,
77 derivedFeatures
78 )
79 return res
80 }
81 override loadPartialModel() {
82 this.workspace.readModel(EObject,"FAM.xmi").eResource.allContents.toList
83 }
84
85 override additionalConstraints() { #[] }
86}
87
88class YakinduLoader extends MetamodelLoader{
89
90 new(ReasonerWorkspace workspace) {
91 super(workspace)
92 }
93
94 override loadMetamodel() {
95 val package = YakindummPackage.eINSTANCE
96 val List<EClass> classes = package.EClassifiers.filter(EClass).toList
97 val List<EEnum> enums = package.EClassifiers.filter(EEnum).toList
98 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList
99 val List<EReference> references = classes.map[EReferences].flatten.toList
100
101 val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList
102
103 return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes)
104 }
105 override loadQueries(EcoreMetamodelDescriptor metamodel) {
106 val i = hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns.instance
107 val patterns = i.specifications.toList
108 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet
109 val derivedFeatures = new LinkedHashMap
110 val res = new ViatraQuerySetDescriptor(
111 patterns,
112 wfPatterns,
113 derivedFeatures
114 )
115 return res
116 }
117 override getRelevantTypes(EcoreMetamodelDescriptor descriptor) {
118 descriptor.classes.filterByNames([it.name],#["Vertex","Transition","Synchronization"])
119 }
120
121 override getRelevantReferences(EcoreMetamodelDescriptor descriptor) {
122 descriptor.references.filterByNames([it.name],#["source","target"])
123 }
124
125 override loadPartialModel() {
126 this.workspace.readModel(EObject,"Yakindu.xmi").eResource.allContents.toList
127 }
128
129 override additionalConstraints() {
130 #[[method | new SGraphInconsistencyDetector(method)]]
131 }
132} \ No newline at end of file
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend
new file mode 100644
index 00000000..7ba38ede
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend
@@ -0,0 +1,289 @@
1package hu.bme.mit.inf.dslreasoner.run
2
3import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
4import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
5import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
6import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
8import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
9import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage
10import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
14import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
15import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
16import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
17import hu.bme.mit.inf.dslreasoner.logic.model.statistics.StatisticSections2Print
18import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver
19import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration
20import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
21import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
22import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
23import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage
24import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
25import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
26import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
27import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage
28import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
29import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy
30import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
31import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
32import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
33import java.io.BufferedReader
34import java.io.InputStreamReader
35import java.util.List
36import org.eclipse.emf.ecore.EObject
37import org.eclipse.emf.ecore.resource.Resource
38import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
39import org.junit.Test
40
41enum UseSolver{Viatra, Smt, ViatraWithSmt, Alloy}
42enum Domain{FAM, Yakindu}
43enum Diversity{No, Diverse}
44
45class RunMeasurements {
46 val String id
47
48 new(String id) {
49 this.id = id
50 inputs = new FileSystemWorkspace('''initialModels/''',"")
51 workspace = new FileSystemWorkspace('''output_«id»/''',"")
52 }
53
54 // Workspace
55 val FileSystemWorkspace inputs
56 val FileSystemWorkspace workspace
57
58 // Mappers
59 val Ecore2Logic ecore2Logic = new Ecore2Logic
60 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
61 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
62
63 // Solvers
64 val SMTSolver smtSolver = new SMTSolver
65 val ViatraReasoner viatraSolver = new ViatraReasoner
66 val ViatraReasoner viatraWithSmtSolver = new ViatraReasoner(smtSolver)
67 val AlloySolver alloyReasoner = new AlloySolver
68
69 def dslLoader(Domain dsl) {
70 if(dsl == Domain::FAM) {
71 return new FAMLoader(inputs)
72 } else if(dsl == Domain::Yakindu) {
73 return new YakinduLoader(inputs)
74 } else throw new IllegalArgumentException('''Unknown domain: «dsl»''')
75 }
76 def static init() {
77 LogiclanguagePackage.eINSTANCE.class
78 LogicproblemPackage.eINSTANCE.class
79 PartialinterpretationPackage.eINSTANCE.class
80 Ecore2logicannotationsPackage.eINSTANCE.class
81 Viatra2LogicAnnotationsPackage.eINSTANCE.class
82 Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("ecore",new XMIResourceFactoryImpl)
83 Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("logicproblem",new XMIResourceFactoryImpl)
84 Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("partialinterpretation",new XMIResourceFactoryImpl)
85 }
86
87 def transformMMtoLogic(EcoreMetamodelDescriptor mm) {
88 ecore2Logic.transformMetamodel(mm,new Ecore2LogicConfiguration())
89 }
90 def transformPSToLogic(List<EObject> objects, TracedOutput<LogicProblem, Ecore2Logic_Trace> metamodelProblem) {
91 instanceModel2Logic.transform(metamodelProblem,objects)
92 }
93 def transformQueriesToLogic(ViatraQuerySetDescriptor descriptor, TracedOutput<LogicProblem, Ecore2Logic_Trace> metamodelProblem) {
94 viatra2Logic.transformQueries(descriptor,metamodelProblem,new Viatra2LogicConfiguration)
95 }
96 def transformDiversity(MetamodelLoader dsl, Ecore2Logic_Trace trace, EcoreMetamodelDescriptor descriptor) {
97 if(diverse) {
98 val relevantClasses = dsl.getRelevantTypes(descriptor)
99 val relevantReferences = dsl.getRelevantReferences(descriptor)
100 val relevantTypes = relevantClasses.map[this.ecore2Logic.TypeofEClass(trace,it) as TypeDeclaration].toSet
101 val relevantRelations = relevantReferences.map[this.ecore2Logic.relationOfReference(trace,it) as RelationDeclaration].toSet
102 return new DiversityDescriptor => [
103 it.relevantTypes = relevantTypes
104 it.relevantRelations = relevantRelations
105 it.maxNumber = 2
106 it.range = 2
107 it.parallels = 2
108 ]
109 } else {
110 return null
111 }
112 }
113
114 def executeSolver(
115 LogicProblem problem,
116 ViatraQuerySetDescriptor vq,
117 MetamodelLoader loader,
118 DiversityDescriptor diversityRequirement,
119 int size)
120 {
121 if(solver == UseSolver.Smt) {
122 val smtConfig = new SmtSolverConfiguration() => [
123 it.typeScopes.maxNewElements = size
124 it.typeScopes.minNewElements = size
125 it.solutionScope.numberOfRequiredSolution = number
126 it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"'''
127 ]
128 val solution = this.smtSolver.solve(
129 problem,
130 smtConfig,
131 this.workspace
132 )
133 return solution
134 } if(solver==UseSolver::Alloy) {
135 val alloyConfig = new AlloySolverConfiguration => [
136 it.typeScopes.maxNewElements = size
137 it.typeScopes.minNewElements = size
138 it.solutionScope.numberOfRequiredSolution = number
139 it.typeScopes.maxIntScope = 0
140 it.writeToFile = true
141 ]
142 val solution = this.alloyReasoner.solve(
143 problem,
144 alloyConfig,
145 this.workspace
146 )
147 return solution
148 } else {
149 val viatraConfig = new ViatraReasonerConfiguration => [
150 it.runtimeLimit = 20
151 it.typeScopes.maxNewElements = size
152 it.typeScopes.minNewElements = size
153 it.solutionScope.numberOfRequiredSolution = number
154 it.existingQueries = vq.patterns.map[it.internalQueryRepresentation]
155 it.nameNewElements = false
156 it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis
157 it.additionalGlobalConstraints += loader.additionalConstraints
158 it.stateCoderStrategy = StateCoderStrategy::Neighbourhood
159 ]
160 viatraConfig.diversityRequirement = diversityRequirement
161 if (solver == UseSolver.Viatra) {
162 val solution = this.viatraSolver.solve(
163 problem,
164 viatraConfig,
165 this.workspace
166 )
167 return solution
168 } else if(solver == UseSolver.ViatraWithSmt) {
169 val inconsistency = new SmtSolverConfiguration() => [
170 it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"'''
171 it.runtimeLimit = 10
172 ]
173 val solution = this.viatraWithSmtSolver.solve(
174 problem,
175 viatraConfig =>[it.inconsistencDetectorConfiguration = inconsistency],
176 this.workspace
177 )
178 return solution
179 }
180 }
181 }
182
183 @Test
184 def runAsTest() {
185 main(#[])
186 }
187
188 static val monitoring = false
189 static val clean = false
190 static val domain = Domain::Yakindu
191 static val solver = UseSolver::Viatra
192 static val diverse = false
193 static val wf = true
194 public static var sizes = #[50]
195 static var int number = 10
196
197 def static void waitForEnter() {
198 if(monitoring) {
199 println(''' Press ENTER to continue''')
200 (new BufferedReader(new InputStreamReader(System.in))).readLine
201 }
202 }
203
204 def static runMeasure(String id, int size) {
205 val r = new RunMeasurements(id)
206 r.workspace.initAndClear
207 init
208 //println("- init")
209 val dsl = r.dslLoader(domain)
210 val mm = dsl.loadMetamodel()
211 val vq = dsl.loadQueries(mm)
212 //println("- Queries loaded")
213
214 if(!wf) {
215 mm.attributes.forEach[it.lowerBound = 0]
216 mm.references.forEach[it.lowerBound = 0]
217 mm.references.removeAll(vq.derivedFeatures.values)
218 mm.attributes.removeAll(vq.derivedFeatures.values)
219 }
220
221 val metamodelProblem = r.transformMMtoLogic(mm)
222 r.transformPSToLogic(dsl.loadPartialModel,metamodelProblem)
223 if(wf) {
224 r.transformQueriesToLogic(vq,metamodelProblem)
225 }
226 val logicProblem = metamodelProblem.output
227
228 //r.workspace.writeModel(logicProblem,"problem.logicproblem")
229 //resSet.resources += viatraProblem.output.eResource
230 val diversityRequirement = r.transformDiversity(dsl,metamodelProblem.trace,mm)
231
232 //println("- DSL -> Logic problem transformation finished")
233
234 waitForEnter
235
236 val solution = r.executeSolver(logicProblem, vq, dsl, diversityRequirement, size)
237
238 print(solution.class.simpleName+";");
239 print(solution.statistics.transformationTime+";")
240 print(solution.statistics.solverTime+";")
241 print((new StatisticSections2Print).transformStatisticDatas2CSV(solution.statistics.entries))
242
243 waitForEnter
244
245 if(solution instanceof ModelResult) {
246 val representations = solution.representation
247 for(representationIndex : 0..<representations.size) {
248 val representation = representations.get(representationIndex)
249 val representationNumber = representationIndex + 1
250 if(representation instanceof PartialInterpretation) {
251 r.workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''')
252 } else {
253 r.workspace.writeText('''solution«representationNumber».txt''',representation.toString)
254 }
255 }
256 println('''saved''')
257 } else {
258 val partial = logicProblem//.eContainer
259 r.workspace.writeModel(partial, "solution.partialinterpretation")
260 println('''saved''')
261 }
262 }
263
264 def static void main(String[] args) {
265 print("id;")
266 (1..number).forEach[print("sol"+it+" (nano);")]
267 print("Solution type (ms);Transformation time (ms);Solver time (ms);TransformationExecutionTime (ms);TypeAnalysisTime (ms);StateCoderTime (ms);SolutionCopyTime (ms);")
268 if(diverse) {
269 print("SolutionDiversityCheckTime (ms);SolutionDiversitySuccessRate (%);")
270 }
271 println("save")
272 //val id = 50//args.get(0)
273 for(size : sizes) {
274 val run = (1..50).map['''r«it»''']
275 for(runIndex : run) {
276 val runID = runIndex+"_"+size
277 print(runID + ";")
278
279 try {
280 runMeasure(runID,size)
281 } catch(Exception e) {}
282
283 System.gc System.gc System.gc
284 Thread.sleep(2000)
285 }
286 }
287
288 }
289} \ 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
new file mode 100644
index 00000000..3a7c5041
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphInconsistencyDetector.xtend
@@ -0,0 +1,82 @@
1package hu.bme.mit.inf.dslreasoner.run
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethodBasedGlobalConstraint
6import org.eclipse.viatra.dse.base.ThreadContext
7import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
8
9class SGraphInconsistencyDetector extends ModelGenerationMethodBasedGlobalConstraint {
10
11 var PartialInterpretation partialInterpretation
12 var ViatraQueryMatcher<?> noEntry
13 var ViatraQueryMatcher<?> entryHasNoOutgoing
14 var ViatraQueryMatcher<?> synchronizationHasNoOutgoing
15 var ViatraQueryMatcher<?> noSynch
16 var ViatraQueryMatcher<?> synchronizedSiblingRegions
17 var ViatraQueryMatcher<?> noStateInRegion
18
19 new(ModelGenerationMethod method) {
20 super(method)
21 }
22
23 override getName() {
24 return SGraphInconsistencyDetector.simpleName
25 }
26
27 override init(ThreadContext context) {
28 partialInterpretation = context.model as PartialInterpretation
29
30 try{
31 this.noEntry = method.unfinishedWF.filter[
32 it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noEntryInRegion")
33 ].head.getMatcher(context.queryEngine)
34
35 this.entryHasNoOutgoing = method.unfinishedWF.filter[
36 it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noOutgoingTransitionFromEntry")
37 ].head.getMatcher(context.queryEngine)
38
39 this.synchronizationHasNoOutgoing = method.unfinishedWF.filter[
40 it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasNoOutgoing")
41 ].head.getMatcher(context.queryEngine)
42
43 this.noSynch = method.unfinishedWF.filter[
44 it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noSynch")
45 ].head.getMatcher(context.queryEngine)
46
47 this.synchronizedSiblingRegions = method.unfinishedWF.filter[
48 it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_SynchronizedRegionDoesNotHaveMultipleRegions")
49 ].head.getMatcher(context.queryEngine)
50
51 this.noStateInRegion = method.unfinishedWF.filter[
52 it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noStateInRegion")
53 ].head.getMatcher(context.queryEngine)
54 } catch(Exception e) { }
55 }
56
57 override checkGlobalConstraint(ThreadContext context) {
58 if(noEntry !== null) {
59 val requiredNewObjects =
60 noEntry.countMatches*2 +
61 entryHasNoOutgoing.countMatches +
62 synchronizationHasNoOutgoing.countMatches +
63 noSynch.countMatches*2 +
64 synchronizedSiblingRegions.countMatches*4
65 noStateInRegion.countMatches
66 val availableNewObjects = partialInterpretation.maxNewElements
67 val res = availableNewObjects >= requiredNewObjects
68 //println('''[«availableNewObjects» >= «requiredNewObjects»] = «res»''')
69 return res
70 } else {
71 true
72 }
73
74 }
75 override createNew() {
76 return new SGraphInconsistencyDetector(this.method)
77 }
78//
79// def hasSynchronization() {
80// this.partialInterpretation.partialtypeinterpratation.
81// }
82} \ No newline at end of file
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
new file mode 100644
index 00000000..d9536989
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend
@@ -0,0 +1,145 @@
1package hu.bme.mit.inf.dslreasoner.run
2
3import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
4import hu.bme.mit.inf.dslreasomer.domains.transima.fam.FunctionalArchitecture.FunctionalArchitecturePackage
5import java.util.List
6import org.eclipse.emf.ecore.EClass
7import org.eclipse.emf.ecore.EEnumLiteral
8import org.eclipse.emf.ecore.EReference
9import org.eclipse.emf.ecore.EEnum
10import org.eclipse.emf.ecore.EAttribute
11import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
12import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
13import org.eclipse.emf.ecore.EObject
14import java.util.LinkedHashMap
15import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
16import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
17import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
19import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
20import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
21import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
22import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy
24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
25import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
26import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
27import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
28import org.eclipse.emf.ecore.resource.Resource
29import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
30import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
31import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
32import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
33
34class SimpleRun {
35
36 def static void main(String[] args) {
37 val inputs = new FileSystemWorkspace('''initialModels/''',"")
38 val workspace = new FileSystemWorkspace('''outputModels/''',"")
39 workspace.initAndClear
40
41 println("Input and output workspaces are created")
42
43 val metamodel = loadMetamodel()
44 val partialModel = loadPartialModel(inputs)
45 val queries = loadQueries(metamodel)
46
47 println("DSL loaded")
48
49 val Ecore2Logic ecore2Logic = new Ecore2Logic
50 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
51 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
52
53 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration())
54 val modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem,partialModel)
55 val validModelExtensionProblem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration)
56
57 val logicProblem = validModelExtensionProblem.output
58
59 println("Problem created")
60 var LogicResult solution
61
62 //*
63 val ViatraReasoner viatraSolver = new ViatraReasoner
64 val viatraConfig = new ViatraReasonerConfiguration => [
65 it.typeScopes.maxNewElements = 10
66 it.typeScopes.minNewElements = 10
67 it.solutionScope.numberOfRequiredSolution = 1
68 it.existingQueries = queries.patterns.map[it.internalQueryRepresentation]
69 it.nameNewElements = true
70 it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis
71 it.stateCoderStrategy = StateCoderStrategy::Neighbourhood
72 ]
73 solution = viatraSolver.solve(logicProblem,viatraConfig,workspace)
74 /*/
75 val AlloySolver alloyReasoner = new AlloySolver
76 val alloyConfig = new AlloySolverConfiguration => [
77 it.typeScopes.maxNewElements = 5
78 it.typeScopes.minNewElements = 5
79 it.solutionScope.numberOfRequiredSolution = 1
80 it.typeScopes.maxIntScope = 0
81 it.writeToFile = true
82 ]
83 solution = alloyReasoner.solve(logicProblem,alloyConfig,workspace)
84 //*/
85
86 println("Problem solved")
87
88 solution.writeSolution(workspace)
89 }
90
91 def private static loadMetamodel() {
92 val pckg = FunctionalArchitecturePackage.eINSTANCE
93 val List<EClass> classes = pckg.EClassifiers.filter(EClass).toList
94 val List<EEnum> enums = pckg.EClassifiers.filter(EEnum).toList
95 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList
96 val List<EReference> references = classes.map[EReferences].flatten.toList
97 val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList
98 return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes)
99 }
100
101 def private static loadQueries(EcoreMetamodelDescriptor metamodel) {
102 val i = hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern.instance
103 val patterns = i.specifications.toList
104 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet
105 val derivedFeatures = new LinkedHashMap
106 derivedFeatures.put(i.type.internalQueryRepresentation,metamodel.attributes.filter[it.name == "type"].head)
107 derivedFeatures.put(i.model.internalQueryRepresentation,metamodel.references.filter[it.name == "model"].head)
108 val res = new ViatraQuerySetDescriptor(
109 patterns,
110 wfPatterns,
111 derivedFeatures
112 )
113 return res
114 }
115
116 def static loadPartialModel(ReasonerWorkspace inputs) {
117 Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl());
118 inputs.readModel(EObject,"FAM.xmi").eResource.allContents.toList
119 }
120
121 def static writeSolution(LogicResult solution, ReasonerWorkspace workspace) {
122 if(solution instanceof ModelResult) {
123 val representations = solution.representation
124 for(representationIndex : 0..<representations.size) {
125 val representation = representations.get(representationIndex)
126 val representationNumber = representationIndex + 1
127 if(representation instanceof PartialInterpretation) {
128 workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''')
129 val partialInterpretation2GML = new PartialInterpretation2Gml
130 val gml = partialInterpretation2GML.transform(representation)
131 //ecore2GML.transform(root)
132 workspace.writeText('''solutionVisualisation.gml''',gml)
133
134 } else {
135 workspace.writeText('''solution«representationNumber».txt''',representation.toString)
136 }
137 }
138 println("Solution saved and visualised")
139 }
140 }
141
142 def static visualizeSolution() {
143
144 }
145} \ No newline at end of file
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualisePartialInterpretation.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualisePartialInterpretation.xtend
new file mode 100644
index 00000000..472f79b6
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualisePartialInterpretation.xtend
@@ -0,0 +1,39 @@
1package hu.bme.mit.inf.dslreasoner.run
2
3import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
6import java.io.FileNotFoundException
7
8class VisualisePartialInterpretation {
9 def static void main(String[] args) {
10
11 val runs = 1..10
12
13
14 for(actualRun : runs) {
15 for(actualSize : RunMeasurements::sizes) {
16 val workspace = new FileSystemWorkspace('''output_r«actualRun»_«actualSize»/''',"")
17 //val ecore2GML = new Ecore2GML
18 val partialInterpretation2GML = new PartialInterpretation2Gml
19 RunMeasurements.init
20 var int i = 1
21 var boolean fileExist = true
22 while(fileExist) {
23 try{
24 val root = workspace.readModel(PartialInterpretation,'''solution«i».partialinterpretation''')
25 val gml = partialInterpretation2GML.transform(root)
26 //ecore2GML.transform(root)
27 workspace.writeText('''solutionVisualisation«i».gml''',gml)
28 println('''Solution «i» visualised''')
29 i++
30 } catch(FileNotFoundException e) {
31 fileExist = false
32 }
33 }
34
35 println('''Visualisation of «i-1» models are finished''')
36 }
37 }
38 }
39} \ No newline at end of file