From c085abd5f2dd49c8be1b32451c8f2ca05fa15f52 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Wed, 5 Jul 2017 16:38:04 +0200 Subject: Example configuration for running measurements. --- .../dslreasoner/run/DiverseMeasurementRunner.xtend | 288 ++++++++++++++------- .../mit/inf/dslreasoner/run/MetamodelLoader.xtend | 24 +- .../run/SGraphInconsistencyDetector.xtend | 40 ++- .../hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend | 30 ++- 4 files changed, 270 insertions(+), 112 deletions(-) (limited to 'Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf') 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 @@ package hu.bme.mit.inf.dslreasoner.run -import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage -import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage -import org.eclipse.emf.ecore.resource.Resource -import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage -import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage -import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor -import org.eclipse.xtend.lib.annotations.Data -import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor -import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic -import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration -import org.eclipse.emf.ecore.EObject -import java.util.List -import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration +import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult import hu.bme.mit.inf.dslreasoner.logic.model.statistics.StatisticSections2Print +import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore +import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic +import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration +import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration +import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace +import java.util.List +import org.eclipse.emf.ecore.EObject +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl +import org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.xtend.lib.annotations.Data +import java.util.LinkedList +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration enum Metamodel { FAM, YakinduWOSynch, Yakindu } enum Constraints { - None, PlusOne, MinusOne + None, Metamodel, All, PlusOne, MinusOne } enum StateCoder { - ID, R1, R2, R3; + ID, Normal, R1, R2, R3; +} +enum Solver { + ViatraSolver, Alloy } @Data @@ -46,6 +57,7 @@ class Scenario { Constraints constraints StateCoder statecoder int runs + Solver solver } class ScenarioRunner { @@ -53,12 +65,15 @@ class ScenarioRunner { // Workspace private val FileSystemWorkspace inputs = new FileSystemWorkspace('''initialModels/''',"") private val ViatraReasoner viatraSolver = new ViatraReasoner + private val AlloySolver alloySolver = new AlloySolver private var MetamodelLoader loader val Ecore2Logic ecore2Logic = new Ecore2Logic val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) + val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic + var matchStatistics = "" public def runScenario(Scenario scenario) { init() @@ -69,31 +84,46 @@ class ScenarioRunner { // printHeader(scenario) - if(scenario.constraints == Constraints.None) { + if( scenario.constraints == Constraints.None || + scenario.constraints == Constraints.Metamodel|| + scenario.constraints == Constraints.All) + { + if(scenario.constraints == Constraints.None) { + mm.attributes.forEach[it.lowerBound = 0] + mm.references.forEach[it.lowerBound = 0] + } + + val useVQ = if(scenario.constraints == Constraints.None || scenario.constraints == Constraints.Metamodel) { + new ViatraQuerySetDescriptor(emptyList,emptySet,emptyMap) + } else { + vq + } - mm.attributes.forEach[it.lowerBound = 0] - mm.references.forEach[it.lowerBound = 0] - mm.references.removeAll(vq.derivedFeatures.values) - mm.attributes.removeAll(vq.derivedFeatures.values) for(run : 1..scenario.runs) { - runCase(run==1,"noConstraints"+run,scenario,mm,new ViatraQuerySetDescriptor(vq.patterns,emptySet,emptyMap),ps) + runCase(run==1,scenario.constraints+""+run,run,scenario,mm,useVQ,ps) + + System.gc System.gc System.gc + Thread.sleep(3000) } - } else { + println(matchStatistics) + } else if(scenario.constraints == Constraints.MinusOne) { + var first = true + //for(remove : vq.validationPatterns) { + for(run : 1..scenario.runs) { + + //val removeName = remove.fullyQualifiedName + //val desc = new ViatraQuerySetDescriptor(vq.patterns,vq.validationPatterns.filter[it != remove].toSet,emptyMap) + runCase(first,"minusOne"+run,run,scenario,mm,vq,ps) + first = false + System.gc System.gc System.gc + //Thread.sleep(3000) + } + //} } - - } -// private def printHeader(Scenario scenario) { -// print("id;Solution type (ms);Transformation time (ms);Solver time (ms);") -// (1..scenario.number).forEach[print("sol"+it+" (nano);")] -// print("TransformationExecutionTime (ms);TypeAnalysisTime (ms);StateCoderTime (ms);SolutionCopyTime (ms);") -// print("SolutionDiversityCheckTime (ms);SolutionDiversitySuccessRate (%);") -// println("save") -// } - - private def runCase(boolean first, String id, Scenario scenario, EcoreMetamodelDescriptor mm, ViatraQuerySetDescriptor vq, List partialModel) { + private def runCase(boolean first, String id, int run, Scenario scenario, EcoreMetamodelDescriptor mm, ViatraQuerySetDescriptor vq, List partialModel) { // Transform val metamodelProblem = ecore2Logic.transformMetamodel(mm,new Ecore2LogicConfiguration()) instanceModel2Logic.transform(metamodelProblem,partialModel) @@ -107,9 +137,19 @@ class ScenarioRunner { val config = getSolverConfiguration(scenario,vq) // Execute - val solution = viatraSolver.solve(problem,config,workspace) - printStatistics(solution,scenario,workspace,id,first) - + val solution = getSolver(scenario).solve(problem,config,workspace) + //printMatchCountStatistics(solution,id) + val emfModels = new LinkedList + if(solution instanceof ModelResult) { + val interpretations = getSolver(scenario).getInterpretations(solution) + for(interpretation : interpretations) { + val instanceModel = logic2Ecore.transformInterpretation(interpretation,metamodelProblem.trace) + emfModels+=instanceModel + } + + } + printStatistics(solution,emfModels,scenario,workspace,id,run,first) + } private def init() { @@ -128,43 +168,67 @@ class ScenarioRunner { loader = if(metamodel == Metamodel::FAM) { new FAMLoader(inputs) } else if(metamodel == Metamodel::Yakindu || metamodel == Metamodel::YakinduWOSynch) { - new YakinduLoader(inputs) + new YakinduLoader(inputs) => [it.useSynchronization = false] } else throw new IllegalArgumentException('''Unknown domain: «metamodel»''') } + def private getSolver(Scenario scenario) { + if(scenario.solver == Solver::ViatraSolver) { + viatraSolver + } else if(scenario.solver == Solver::Alloy) { + alloySolver + } + } + def private getSolverConfiguration(Scenario scenario, ViatraQuerySetDescriptor vq) { - val viatraConfig = new ViatraReasonerConfiguration => [ - it.runtimeLimit = 300 - it.typeScopes.maxNewElements = scenario.size - it.typeScopes.minNewElements = scenario.size - it.solutionScope.numberOfRequiredSolution = scenario.number - it.existingQueries = vq.patterns.map[it.internalQueryRepresentation] - it.nameNewElements = false - it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis - it.additionalGlobalConstraints += loader.additionalConstraints - it.stateCoderStrategy = StateCoderStrategy::Neighbourhood - if(scenario.statecoder != StateCoder::ID) { - val range = if(scenario.statecoder != StateCoder::R1) { - 1 - } else if(scenario.statecoder != StateCoder::R2) { - 2 - } else if(scenario.statecoder != StateCoder::R3) { - 3 + if(scenario.solver == Solver.ViatraSolver) { + val viatraConfig = new ViatraReasonerConfiguration => [ + it.runtimeLimit = 300 + it.typeScopes.maxNewElements = scenario.size + it.typeScopes.minNewElements = scenario.size + it.solutionScope.numberOfRequiredSolution = scenario.number + it.existingQueries = vq.patterns.map[it.internalQueryRepresentation] + it.nameNewElements = false + it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis + it.additionalGlobalConstraints += loader.additionalConstraints + it.stateCoderStrategy = if(scenario.statecoder == StateCoder::ID) { + StateCoderStrategy::IDBased + } else { + StateCoderStrategy::Neighbourhood } - - it.diversityRequirement = new DiversityDescriptor => [ - it.relevantTypes = null - it.relevantRelations = null - it.maxNumber = 1 - it.range = range - it.parallels = 1 - ] - } - ] - return viatraConfig + if(scenario.statecoder != StateCoder::ID || scenario.statecoder != StateCoder::Normal) { + val range = if(scenario.statecoder != StateCoder::R1) { + 1 + } else if(scenario.statecoder != StateCoder::R2) { + 2 + } else if(scenario.statecoder != StateCoder::R3) { + 3 + } + + it.diversityRequirement = new DiversityDescriptor => [ + it.relevantTypes = null + it.relevantRelations = null + it.maxNumber = 1 + it.range = range + it.parallels = 1 + ] + } + ] + return viatraConfig + } else if(scenario.solver == Solver::Alloy) { + return new AlloySolverConfiguration => [ + it.runtimeLimit = 300 + it.typeScopes.maxNewElements = scenario.size + it.typeScopes.minNewElements = scenario.size + it.solutionScope.numberOfRequiredSolution = scenario.number + it.typeScopes.maxIntScope = 0 + it.writeToFile=true + ] + } + } - def printStatistics(LogicResult solution, Scenario scenario, FileSystemWorkspace workspace, String id, boolean printHeader) { + def printStatistics(LogicResult solution, List emfModels, Scenario scenario, FileSystemWorkspace workspace, String id,int run, boolean printHeader) { if(printHeader) { print("id;Solution type (ms);Transformation time (ms);Solver time (ms);") solution.statistics.entries.map[name].forEach[print(it+";")] @@ -179,27 +243,73 @@ class ScenarioRunner { print((new StatisticSections2Print).transformStatisticDatas2CSV(solution.statistics.entries)) - if(solution instanceof ModelResult) { - val representations = solution.representation - for(representationIndex : 0..> pattern) { + pattern.fullyQualifiedName.startsWith("currentInRelation_pattern") + //true + }*/ } class DiverseMeasurementRunner { def static void main(String[] args) { - val scenario = new Scenario(50,50,Metamodel::Yakindu,Constraints.None,StateCoder.ID,12) + val scenario = new Scenario(100,49,Metamodel::Yakindu,Constraints.All,StateCoder.Normal,1,Solver::Alloy) val scenarioRunner = new ScenarioRunner scenarioRunner.runScenario(scenario) } 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{ class YakinduLoader extends MetamodelLoader{ + private var useSynchronization = true; + public static val patternsWithSynchronization = #[ + "synchHasNoOutgoing", "synchHasNoIncoming", "SynchronizedIncomingInSameRegion", "notSynchronizingStates", + "hasMultipleOutgoingTrainsition", "hasMultipleIncomingTrainsition", "SynchronizedRegionsAreNotSiblings", + "SynchronizedRegionDoesNotHaveMultipleRegions", "synchThree", "twoSynch"] + new(ReasonerWorkspace workspace) { super(workspace) } + public def setUseSynchronization(boolean useSynchronization) { + this.useSynchronization = useSynchronization + } + override loadMetamodel() { + val useSynchInThisLoad = this.useSynchronization + val package = YakindummPackage.eINSTANCE - val List classes = package.EClassifiers.filter(EClass).toList + val List classes = package.EClassifiers.filter(EClass).filter[(useSynchInThisLoad) || (it.name != "Synchronization")].toList val List enums = package.EClassifiers.filter(EEnum).toList val List literals = enums.map[ELiterals].flatten.toList val List references = classes.map[EReferences].flatten.toList - val List attributes = classes.map[EAttributes].flatten.toList return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes) } override loadQueries(EcoreMetamodelDescriptor metamodel) { + val useSynchInThisLoad = this.useSynchronization + val i = hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns.instance - val patterns = i.specifications.toList + val patterns = i.specifications.filter[spec | + useSynchInThisLoad || + !patternsWithSynchronization.exists[spec.fullyQualifiedName.endsWith(it)] + ].toList val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet val derivedFeatures = new LinkedHashMap val res = new ViatraQuerySetDescriptor( @@ -126,7 +142,7 @@ class YakinduLoader extends MetamodelLoader{ this.workspace.readModel(EObject,"Yakindu.xmi").eResource.allContents.toList } - override additionalConstraints() { + override additionalConstraints() { //#[] #[[method | new SGraphInconsistencyDetector(method)]] } } \ 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 var PartialInterpretation partialInterpretation var ViatraQueryMatcher noEntry var ViatraQueryMatcher entryHasNoOutgoing + var ViatraQueryMatcher choiceHasNoOutgiong + var ViatraQueryMatcher choiceHasNoIncoming + //var ViatraQueryMatcher noSynch var ViatraQueryMatcher synchronizationHasNoOutgoing - var ViatraQueryMatcher noSynch + var ViatraQueryMatcher synchronizedSiblingRegions var ViatraQueryMatcher noStateInRegion @@ -36,33 +39,48 @@ class SGraphInconsistencyDetector extends ModelGenerationMethodBasedGlobalConstr it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noOutgoingTransitionFromEntry") ].head.getMatcher(context.queryEngine) - this.synchronizationHasNoOutgoing = method.unfinishedWF.filter[ - it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasNoOutgoing") + this.noStateInRegion = method.unfinishedWF.filter[ + it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noStateInRegion") ].head.getMatcher(context.queryEngine) - this.noSynch = method.unfinishedWF.filter[ - it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noSynch") + this.choiceHasNoOutgiong = method.unfinishedWF.filter[ + it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_choiceHasNoOutgoing") ].head.getMatcher(context.queryEngine) +// this.choiceHasNoIncoming = method.unfinishedWF.filter[ +// it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_choiceHasNoIncoming") +// ].head.getMatcher(context.queryEngine) + } catch(Exception e) { } + try{ +// this.noSynch = method.unfinishedWF.filter[ +// it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noSynch") +// ].head.getMatcher(context.queryEngine) +// this.synchronizedSiblingRegions = method.unfinishedWF.filter[ it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_SynchronizedRegionDoesNotHaveMultipleRegions") ].head.getMatcher(context.queryEngine) - this.noStateInRegion = method.unfinishedWF.filter[ - it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noStateInRegion") + this.synchronizationHasNoOutgoing = method.unfinishedWF.filter[ + it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_synchHasNoOutgoing") ].head.getMatcher(context.queryEngine) } catch(Exception e) { } } override checkGlobalConstraint(ThreadContext context) { if(noEntry !== null) { - val requiredNewObjects = + var requiredNewObjects = noEntry.countMatches*2 + entryHasNoOutgoing.countMatches + - synchronizationHasNoOutgoing.countMatches + - noSynch.countMatches*2 + - synchronizedSiblingRegions.countMatches*4 + choiceHasNoOutgiong.countMatches+ + //choiceHasNoIncoming.countMatches+ noStateInRegion.countMatches + if(synchronizationHasNoOutgoing!= null) { + requiredNewObjects += + //noSynch.countMatches*2 + + synchronizationHasNoOutgoing.countMatches + + synchronizedSiblingRegions.countMatches*4 + } + val availableNewObjects = partialInterpretation.maxNewElements val res = availableNewObjects >= requiredNewObjects //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 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver +import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner +import java.util.LinkedList class SimpleRun { @@ -47,6 +50,7 @@ class SimpleRun { println("DSL loaded") val Ecore2Logic ecore2Logic = new Ecore2Logic + val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic @@ -58,9 +62,9 @@ class SimpleRun { println("Problem created") var LogicResult solution - - //* - val ViatraReasoner viatraSolver = new ViatraReasoner + var LogicReasoner reasoner + /* + reasoner = new ViatraReasoner val viatraConfig = new ViatraReasonerConfiguration => [ it.typeScopes.maxNewElements = 10 it.typeScopes.minNewElements = 10 @@ -70,9 +74,9 @@ class SimpleRun { it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis it.stateCoderStrategy = StateCoderStrategy::Neighbourhood ] - solution = viatraSolver.solve(logicProblem,viatraConfig,workspace) + solution = reasoner.solve(logicProblem,viatraConfig,workspace) /*/ - val AlloySolver alloyReasoner = new AlloySolver + reasoner = new AlloySolver val alloyConfig = new AlloySolverConfiguration => [ it.typeScopes.maxNewElements = 5 it.typeScopes.minNewElements = 5 @@ -80,12 +84,19 @@ class SimpleRun { it.typeScopes.maxIntScope = 0 it.writeToFile = true ] - solution = alloyReasoner.solve(logicProblem,alloyConfig,workspace) + solution = reasoner.solve(logicProblem,alloyConfig,workspace) //*/ println("Problem solved") - solution.writeSolution(workspace) + val interpretations = reasoner.getInterpretations(solution as ModelResult) + val models = new LinkedList + for(interpretation : interpretations) { + val instanceModel = logic2Ecore.transformInterpretation(interpretation,modelGenerationProblem.trace) + models+=instanceModel + } + + solution.writeSolution(workspace, #[]) } def private static loadMetamodel() { @@ -118,7 +129,7 @@ class SimpleRun { inputs.readModel(EObject,"FAM.xmi").eResource.allContents.toList } - def static writeSolution(LogicResult solution, ReasonerWorkspace workspace) { + def static writeSolution(LogicResult solution, ReasonerWorkspace workspace, List models) { if(solution instanceof ModelResult) { val representations = solution.representation for(representationIndex : 0..