From 0d4516ef455e916ffac2702d2bfe727c71789bc0 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Wed, 27 Sep 2017 22:47:51 +0200 Subject: Research paper measurement configuration updates --- .../mit/inf/dslreasoner/run/MetamodelLoader.xtend | 150 +++++++- .../mit/inf/dslreasoner/run/RunMeasurements.xtend | 48 ++- .../inf/dslreasoner/run/RunModelExtension.xtend | 378 +++++++++++++++++++++ .../run/SGraphInconsistencyDetector.xtend | 25 +- .../hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend | 2 +- .../run/VisualiseAllModelInDirectory.xtend | 64 ++++ 6 files changed, 619 insertions(+), 48 deletions(-) create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualiseAllModelInDirectory.xtend (limited to 'Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit') 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 60908365..10072f5a 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 @@ -1,25 +1,30 @@ package hu.bme.mit.inf.dslreasoner.run import hu.bme.mit.inf.dslreasomer.domains.transima.fam.FunctionalArchitecture.FunctionalArchitecturePackage +import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.FileSystem +import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FilesystemPackage +import hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern +import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor +import hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethodBasedGlobalConstraint +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import java.util.Collection import java.util.LinkedHashMap import java.util.List +import java.util.Set import org.eclipse.emf.ecore.EAttribute import org.eclipse.emf.ecore.EClass import org.eclipse.emf.ecore.EEnum import org.eclipse.emf.ecore.EEnumLiteral +import org.eclipse.emf.ecore.EObject import org.eclipse.emf.ecore.EReference -import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethodBasedGlobalConstraint import org.eclipse.xtext.xbase.lib.Functions.Function1 -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod -import org.eclipse.emf.ecore.EObject -import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor -import java.util.Collection -import java.util.Set -import java.util.Collections +import java.util.HashMap +import org.eclipse.emf.ecore.EcorePackage +import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Ecore abstract class MetamodelLoader { protected val ReasonerWorkspace workspace @@ -65,7 +70,7 @@ class FAMLoader extends MetamodelLoader{ } override loadQueries(EcoreMetamodelDescriptor metamodel) { - val i = hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern.instance + val i = Pattern.instance val patterns = i.specifications.toList val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet val derivedFeatures = new LinkedHashMap @@ -88,11 +93,12 @@ class FAMLoader extends MetamodelLoader{ class YakinduLoader extends MetamodelLoader{ private var useSynchronization = true; + private var useComplexStates = false; public static val patternsWithSynchronization = #[ "synchHasNoOutgoing", "synchHasNoIncoming", "SynchronizedIncomingInSameRegion", "notSynchronizingStates", "hasMultipleOutgoingTrainsition", "hasMultipleIncomingTrainsition", "SynchronizedRegionsAreNotSiblings", - "SynchronizedRegionDoesNotHaveMultipleRegions", "synchThree", "twoSynch"] - + "SynchronizedRegionDoesNotHaveMultipleRegions", "synchThree", "twoSynch","noSynch2","synch","noSynch4","noSynch3","noSynch"] + public static val patternsWithComplexStates =#["outgoingFromExit","outgoingFromFinal","choiceHasNoOutgoing","choiceHasNoIncoming"] new(ReasonerWorkspace workspace) { super(workspace) } @@ -100,12 +106,19 @@ class YakinduLoader extends MetamodelLoader{ public def setUseSynchronization(boolean useSynchronization) { this.useSynchronization = useSynchronization } + public def setUseComplexStates(boolean useComplexStates) { + this.useComplexStates = useComplexStates + } override loadMetamodel() { val useSynchInThisLoad = this.useSynchronization + val useComplexStates = this.useComplexStates val package = YakindummPackage.eINSTANCE - val List classes = package.EClassifiers.filter(EClass).filter[(useSynchInThisLoad) || (it.name != "Synchronization")].toList + val List classes = package.EClassifiers.filter(EClass) + .filter[useSynchInThisLoad || (it.name != "Synchronization")] + .filter[useComplexStates || (it.name != "Choice" && it.name != "Exit" && it.name != "FinalState")] + .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 @@ -116,11 +129,17 @@ class YakinduLoader extends MetamodelLoader{ override loadQueries(EcoreMetamodelDescriptor metamodel) { val useSynchInThisLoad = this.useSynchronization - val i = hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns.instance - val patterns = i.specifications.filter[spec | - useSynchInThisLoad || - !patternsWithSynchronization.exists[spec.fullyQualifiedName.endsWith(it)] - ].toList + val i = Patterns.instance + val patterns = i.specifications + .filter[spec | + useSynchInThisLoad || + !patternsWithSynchronization.exists[spec.fullyQualifiedName.endsWith(it)] + ] + .filter[spec | + useComplexStates || + !patternsWithComplexStates.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( @@ -145,4 +164,99 @@ class YakinduLoader extends MetamodelLoader{ override additionalConstraints() { //#[] #[[method | new SGraphInconsistencyDetector(method)]] } +} + +class FileSystemLoader extends MetamodelLoader{ + + new(ReasonerWorkspace workspace) { + super(workspace) + } + + override loadMetamodel() { + val package = FilesystemPackage.eINSTANCE + val List classes = package.EClassifiers.filter(EClass).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 getRelevantTypes(EcoreMetamodelDescriptor descriptor) { + return null + } + + override getRelevantReferences(EcoreMetamodelDescriptor descriptor) { + null + } + + override loadQueries(EcoreMetamodelDescriptor metamodel) { + val patternGroup = FileSystem.instance + val patterns = patternGroup.specifications.toList + val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet + val derivedFeatures = new HashMap + derivedFeatures.put(patternGroup.live.internalQueryRepresentation,metamodel.references.filter[it.name == "live"].head) + return new ViatraQuerySetDescriptor( + patterns, + wfPatterns, + derivedFeatures + ) + + } + + override loadPartialModel() { + this.workspace.readModel(EObject,"fs.xmi").eResource.allContents.toList + } + + override additionalConstraints() { + #[[method | new FileSystemInconsistencyDetector(method)]] + } + +} + +class EcoreLoader extends MetamodelLoader { + + new(ReasonerWorkspace workspace) { + super(workspace) + } + + override loadMetamodel() { + val package = EcorePackage.eINSTANCE + val List classes = package.EClassifiers.filter(EClass).filter[it.name!="EFactory"].toList + val List enums = package.EClassifiers.filter(EEnum).toList + val List literals = enums.map[ELiterals].flatten.toList + val List references = classes.map[EReferences].flatten.filter[it.name!="eFactoryInstance"].filter[!it.derived].toList + val List attributes = #[] //classes.map[EAttributes].flatten.toList + return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes) + } + + override getRelevantTypes(EcoreMetamodelDescriptor descriptor) { + return null + } + + override getRelevantReferences(EcoreMetamodelDescriptor descriptor) { + null + } + + override loadQueries(EcoreMetamodelDescriptor metamodel) { + val patternGroup = Ecore.instance + val patterns = patternGroup.specifications.toList + val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet + val derivedFeatures = new HashMap + return new ViatraQuerySetDescriptor( + patterns, + wfPatterns, + derivedFeatures + ) + + } + + override loadPartialModel() { + this.workspace.readModel(EObject,"ecore.xmi").eResource.allContents.toList + } + + override additionalConstraints() { + #[] + } + } \ 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 index e96a6bf6..8d96958d 100644 --- 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 @@ -37,9 +37,12 @@ import org.eclipse.emf.ecore.EObject import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl import org.junit.Test +import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationSizePrinter +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml enum UseSolver{Viatra, Smt, ViatraWithSmt, Alloy} -enum Domain{FAM, Yakindu} +enum Domain{FAM, Yakindu, FileSystem,Ecore} enum Diversity{No, Diverse} class RunMeasurements { @@ -70,8 +73,12 @@ class RunMeasurements { if(dsl == Domain::FAM) { return new FAMLoader(inputs) } else if(dsl == Domain::Yakindu) { - return new YakinduLoader(inputs) - } else throw new IllegalArgumentException('''Unknown domain: «dsl»''') + return new YakinduLoader(inputs) =>[it.useSynchronization = true useComplexStates = false] + } else if(dsl == Domain::FileSystem){ + return new FileSystemLoader(inputs) + } else if(dsl == Domain::Ecore) { + return new EcoreLoader(inputs) + }else throw new IllegalArgumentException('''Unknown domain: «dsl»''') } def static init() { LogiclanguagePackage.eINSTANCE.class @@ -147,7 +154,7 @@ class RunMeasurements { return solution } else { val viatraConfig = new ViatraReasonerConfiguration => [ - it.runtimeLimit = 20 + it.runtimeLimit = 400 it.typeScopes.maxNewElements = size it.typeScopes.minNewElements = size it.solutionScope.numberOfRequiredSolution = number @@ -156,6 +163,10 @@ class RunMeasurements { it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis it.searchSpaceConstraints.additionalGlobalConstraints += loader.additionalConstraints it.stateCoderStrategy = StateCoderStrategy::Neighbourhood + it.debugCongiguration.partalInterpretationVisualisationFrequency = 100 + //it.debugCongiguration.partialInterpretatioVisualiser = + //new GraphvizVisualisation + //new PartialInterpretationSizePrinter ] viatraConfig.diversityRequirement = diversityRequirement if (solver == UseSolver.Viatra) { @@ -189,13 +200,13 @@ class RunMeasurements { } static val monitoring = false - static val clean = false - static val domain = Domain::Yakindu + static val clean = true + static val domain = Domain::FAM static val solver = UseSolver::Viatra - static val diverse = true - static val wf = false - public static var sizes = #[50] - static var int number = 3 + static val diverse = false + static val wf = true + public static var sizes = #[11,5,10,15,20,25,30,35,40,45,50,100,150,200,250,300,350,400,450,500] + static var int number = 1 def static void waitForEnter() { if(monitoring) { @@ -215,8 +226,8 @@ class RunMeasurements { //println("- Queries loaded") if(!wf) { - mm.attributes.forEach[it.lowerBound = 0] - mm.references.forEach[it.lowerBound = 0] +// mm.attributes.forEach[it.lowerBound = 0] +// mm.references.forEach[it.lowerBound = 0] mm.references.removeAll(vq.derivedFeatures.values) mm.attributes.removeAll(vq.derivedFeatures.values) } @@ -252,6 +263,15 @@ class RunMeasurements { val representationNumber = representationIndex + 1 if(representation instanceof PartialInterpretation) { r.workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''') + val partialInterpretation2GML = new PartialInterpretation2Gml + val gml = partialInterpretation2GML.transform(representation) + r.workspace.writeText('''solution«representationNumber».gml''',gml) + if(representation.newElements.size <160) { + val visualiser = new GraphvizVisualisation + val visualisation = visualiser.visualiseConcretization(representation) + visualisation.writeToFile(r.workspace,'''solution«representationNumber»''') + } + } else { r.workspace.writeText('''solution«representationNumber».txt''',representation.toString) } @@ -274,14 +294,14 @@ class RunMeasurements { println("save") //val id = 50//args.get(0) for(size : sizes) { - val run = (1..50).map['''r«it»'''] + val run = (1..10).map['''r«it»'''] for(runIndex : run) { val runID = runIndex+"_"+size print(runID + ";") try { runMeasure(runID,size) - } catch(Exception e) {} + } catch(Exception e) {e.printStackTrace} System.gc System.gc System.gc Thread.sleep(2000) diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend new file mode 100644 index 00000000..d8f75b89 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend @@ -0,0 +1,378 @@ +package hu.bme.mit.inf.dslreasoner.run + +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration +import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Statechart +import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage +import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic +import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration +import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace +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.builder.TracedOutput +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage +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.smt.reasoner.SMTSolver +import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration +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.visualisation.pi2graphviz.GraphvizVisualisation +import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace +import java.io.BufferedReader +import java.io.InputStreamReader +import java.util.ArrayList +import java.util.Collections +import java.util.LinkedList +import java.util.List +import java.util.Random +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.ViatraQueryEngine +import org.eclipse.viatra.query.runtime.emf.EMFScope +import java.lang.invoke.VolatileCallSite + +enum PartialModelSource { Homeworks, Random } +enum ValidationTechique {Alloy, Viatra} + +class RunModelExtensionMeasurements { + val String id + + new(String id) { + this.id = id + inputs = new FileSystemWorkspace('''initialModels/''',"") + workspace = new FileSystemWorkspace('''output_«id»/''',"") + } + + // Workspace + val FileSystemWorkspace inputs + val FileSystemWorkspace workspace + + // Mappers + val Ecore2Logic ecore2Logic = new Ecore2Logic + val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) + val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic + + // Solvers + val SMTSolver smtSolver = new SMTSolver + val ViatraReasoner viatraSolver = new ViatraReasoner + val ViatraReasoner viatraWithSmtSolver = new ViatraReasoner + val AlloySolver alloyReasoner = new AlloySolver + + def dslLoader(Domain dsl) { + if(dsl == Domain::FAM) { + return new FAMLoader(inputs) + } else if(dsl == Domain::Yakindu) { + return new YakinduLoader(inputs) =>[it.useSynchronization = false useComplexStates = true] + } else if(dsl == Domain::FileSystem){ + return new FileSystemLoader(inputs) + } else if(dsl == Domain::Ecore) { + return new EcoreLoader(inputs) + }else throw new IllegalArgumentException('''Unknown domain: «dsl»''') + } + def static init() { + LogiclanguagePackage.eINSTANCE.class + LogicproblemPackage.eINSTANCE.class + PartialinterpretationPackage.eINSTANCE.class + Ecore2logicannotationsPackage.eINSTANCE.class + Viatra2LogicAnnotationsPackage.eINSTANCE.class + YakindummPackage.eINSTANCE.class + Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("*",new XMIResourceFactoryImpl) + } + + def transformMMtoLogic(EcoreMetamodelDescriptor mm) { + ecore2Logic.transformMetamodel(mm,new Ecore2LogicConfiguration()) + } + def transformPSToLogic(List objects, TracedOutput metamodelProblem) { + instanceModel2Logic.transform(metamodelProblem,objects) + } + def transformQueriesToLogic(ViatraQuerySetDescriptor descriptor, TracedOutput metamodelProblem) { + viatra2Logic.transformQueries(descriptor,metamodelProblem,new Viatra2LogicConfiguration) + } + + def executeSolver( + LogicProblem problem, + ViatraQuerySetDescriptor vq, + MetamodelLoader loader, + DiversityDescriptor diversityRequirement, + int size, + UseSolver solver) + { + if(solver == UseSolver.Smt) { + val smtConfig = new SmtSolverConfiguration() => [ + it.typeScopes.maxNewElements = size + it.typeScopes.minNewElements = size + it.solutionScope.numberOfRequiredSolution = 1 + it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"''' + ] + val solution = this.smtSolver.solve( + problem, + smtConfig, + this.workspace + ) + return solution + } if(solver==UseSolver::Alloy) { + val alloyConfig = new AlloySolverConfiguration => [ + it.typeScopes.maxNewElements = size + it.typeScopes.minNewElements = size + it.solutionScope.numberOfRequiredSolution = 1 + it.typeScopes.maxNewIntegers = 0 + it.writeToFile = true + ] + val solution = this.alloyReasoner.solve( + problem, + alloyConfig, + this.workspace + ) + return solution + } else { + val viatraConfig = new ViatraReasonerConfiguration => [ + it.runtimeLimit = 400 + it.typeScopes.maxNewElements = size + it.typeScopes.minNewElements = size + it.solutionScope.numberOfRequiredSolution = 1 + it.existingQueries = vq.patterns.map[it.internalQueryRepresentation] + it.nameNewElements = false + it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis + it.searchSpaceConstraints.additionalGlobalConstraints += loader.additionalConstraints + it.stateCoderStrategy = StateCoderStrategy::Neighbourhood + it.debugCongiguration.partalInterpretationVisualisationFrequency = 100 + //it.debugCongiguration.partialInterpretatioVisualiser = + //new GraphvizVisualisation + //new PartialInterpretationSizePrinter + ] + viatraConfig.diversityRequirement = diversityRequirement + if (solver == UseSolver.Viatra) { + val solution = this.viatraSolver.solve( + problem, + viatraConfig, + this.workspace + ) + return solution + } else if(solver == UseSolver.ViatraWithSmt) { + val inconsistency = new SmtSolverConfiguration() => [ + it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"''' + it.runtimeLimit = 10 + ] + val solution = this.viatraWithSmtSolver.solve( + problem, + viatraConfig =>[ + it.internalConsistencyCheckerConfiguration.internalIncosnsitencyDetector = smtSolver + it.internalConsistencyCheckerConfiguration.internalInconsistencDetectorConfiguration = inconsistency + ], + this.workspace + ) + return solution + } + } + } + + def public static loadPartialModels(int size, int max) { + if(partialModelSource === PartialModelSource::Homeworks) { + val hfs = new FileSystemWorkspace("D:/Eclipse/GIT/RemoHF/Extracted/output","") + val allFileNames = hfs.allFiles.toList + + + val models = allFileNames.map[hfs.readModel(Statechart,it)] + //println("loaded") + val filtered = if(size===-1) { + models + } else { + models.filter[it.eAllContents.size + 1 >= size].toList + } + //println("filtered") + + val selected = if(max!==-1) { + Collections.shuffle(filtered); + filtered.subList(0,max) + } else { + filtered + } + //println("selected "+ selected.size) + val collected = selected.map[ + val r = new LinkedList + r.add(it) + r.addAll(it.eAllContents.toIterable) + return r + ].toList + //println("collected to lists") + + val list = new ArrayList(collected.size) + for(s : collected) { + list.add(s.prune(size)) + } + //println("pruned to " + size) + + return list + } else if(partialModelSource === PartialModelSource::Random) { + + } + } + + static val Random pruningRandom = new Random(0) +// def private void prune(EObject root, int targetSize) { +// var size = root.eAllContents.size + 1 +// while(size>targetSize) { +// val leafs = root.eAllContents.filter[it.eContents.empty].toList +// val leafToRemove = leafs.get(pruningRandom.nextInt(leafs.size)) +// EcoreUtil.delete(leafToRemove) +// size-- +// } +// } + def static private prune(List objects, int targetSize) { + if(targetSize !== -1) { + var size = objects.size + while(size>targetSize) { + val leafs = objects.filter[!it.eAllContents.toList.exists[child | objects.contains(child)]].toList + if(leafs.exists[it instanceof Statechart]) { + println("Gebasz!") + } + objects.remove(leafs.get(pruningRandom.nextInt(leafs.size))) + size-- + } + if(!objects.exists[it instanceof Statechart]) { + println("Gebasz2!") + } + + } + return objects; + } + + static val partialModelSource = PartialModelSource::Homeworks + static val monitoring = false + static val clean = true + public static var sizes = #[-1/*,5,10,15,20,25,30,35,40,45,50*/] + + def static void waitForEnter() { + if(monitoring) { + println(''' Press ENTER to continue''') + (new BufferedReader(new InputStreamReader(System.in))).readLine + } + } + + def static runMeasure(String id, int size){ + init + + val partialModels = loadPartialModels(size,-1) + var pmIndex = 1 + + for(partialModel : partialModels) { + + val pmID = id+"_"+(pmIndex++) + val r = new RunModelExtensionMeasurements(pmID) + r.workspace.initAndClear + print(pmID + ";") + print(partialModel.size + ";") + //println("- init") + val dsl = r.dslLoader(Domain::Yakindu) + val mm = dsl.loadMetamodel() + val vq = dsl.loadQueries(mm) + //println("- Queries loaded") + + val metamodelProblem = r.transformMMtoLogic(mm) + r.transformPSToLogic(partialModel,metamodelProblem) + r.transformQueriesToLogic(vq,metamodelProblem) + val logicProblem = metamodelProblem.output + + //println("- DSL -> Logic problem transformation finished") + + waitForEnter + + val ValidationTechique validationTechnique = ValidationTechique::Viatra + if(validationTechnique === ValidationTechique::Alloy) { + val solution = r.executeSolver(logicProblem, vq, dsl, null, 0, UseSolver::Alloy) + + print(solution.class.simpleName+";"); + print(solution.statistics.transformationTime+";") + print(solution.statistics.solverTime+";") + print((new StatisticSections2Print).transformStatisticDatas2CSV(solution.statistics.entries)) + + waitForEnter + + if(solution instanceof ModelResult) { + val representations = solution.representation + for(representationIndex : 0.. entryHasNoOutgoing var ViatraQueryMatcher choiceHasNoOutgiong var ViatraQueryMatcher choiceHasNoIncoming - //var ViatraQueryMatcher noSynch + var ViatraQueryMatcher noSynch var ViatraQueryMatcher synchronizationHasNoOutgoing var ViatraQueryMatcher synchronizedSiblingRegions @@ -47,15 +47,12 @@ class SGraphInconsistencyDetector extends ModelGenerationMethodBasedGlobalConstr 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.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) @@ -68,15 +65,13 @@ class SGraphInconsistencyDetector extends ModelGenerationMethodBasedGlobalConstr override checkGlobalConstraint(ThreadContext context) { if(noEntry !== null) { - var requiredNewObjects = - noEntry.countMatches*2 + - entryHasNoOutgoing.countMatches + - choiceHasNoOutgiong.countMatches+ - //choiceHasNoIncoming.countMatches+ - noStateInRegion.countMatches + var requiredNewObjects = noEntry.countMatches*2 +entryHasNoOutgoing.countMatches + noStateInRegion.countMatches + if(choiceHasNoOutgiong!=null) { + requiredNewObjects+=choiceHasNoOutgiong.countMatches + } if(synchronizationHasNoOutgoing!= null) { requiredNewObjects += - //noSynch.countMatches*2 + + noSynch.countMatches*2 + synchronizationHasNoOutgoing.countMatches + synchronizedSiblingRegions.countMatches*4 } 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 d73303fa..d0f88b65 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 @@ -73,7 +73,7 @@ class SimpleRun { it.existingQueries = queries.patterns.map[it.internalQueryRepresentation] it.debugCongiguration.logging = false it.debugCongiguration.partalInterpretationVisualisationFrequency = 1 - it.debugCongiguration.partialInterpretatioVisualiser = null//new GraphvizVisualisation + it.debugCongiguration.partialInterpretatioVisualiser = new GraphvizVisualisation ] solution = reasoner.solve(logicProblem,viatraConfig,workspace) /*/ diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualiseAllModelInDirectory.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualiseAllModelInDirectory.xtend new file mode 100644 index 00000000..f0059a85 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualiseAllModelInDirectory.xtend @@ -0,0 +1,64 @@ +package hu.bme.mit.inf.dslreasoner.run + +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage +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.workspace.FileSystemWorkspace +import java.io.File +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage +import org.eclipse.emf.ecore.resource.Resource +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml +import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation +import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl + +class VisualiseAllModelInDirectory { + def static void main(String[] args) { + LogiclanguagePackage.eINSTANCE.class + LogicproblemPackage.eINSTANCE.class + PartialinterpretationPackage.eINSTANCE.class + Ecore2logicannotationsPackage.eINSTANCE.class + Viatra2LogicAnnotationsPackage.eINSTANCE.class + Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("*",new XMIResourceFactoryImpl) + + //"D:/Data/ICSE18/Yakindu-WF/Largest-by-Graph-Solver".visualiseModel +// val folderName = new File("D:/Data/ICSE18/FAM+WF/Largest-by-Graph-Solver") +// for(subFolderName : folderName.listFiles) { +// subFolderName.absolutePath.visualiseModel +// } + } + + def static visualiseModel(String folderName) { + val file = new File(folderName+"/"+"solution1.partialinterpretation") + val hasSource = file.exists + + + if(hasSource) { + val hasPng = new File(folderName+"/"+"solution1.png").exists + val hasGml = new File(folderName+"/"+"solution1.gml").exists + + val workspace = new FileSystemWorkspace(folderName,"") + val model = workspace.readModel(PartialInterpretation,"solution1.partialinterpretation") + + if(!hasGml) { + val partialInterpretation2GML = new PartialInterpretation2Gml + val gmlText = partialInterpretation2GML.transform(model) + workspace.writeText('''solution1.gml''',gmlText) + println('''solution1.gml''') + } + + if(!hasPng && model.newElements.size <160) { + val visualiser = new GraphvizVisualisation + val visualisation = visualiser.visualiseConcretization(model) + visualisation.writeToFile(workspace,"solution1") + println("solution1.png") + println("Need png!") + } + + println('''«folderName» visualised''') + } else { + println('''«folderName» missing''') + } + } +} -- cgit v1.2.3-54-g00ecf