From d4f03121e36bce42ce611e97ffee6e697162228e Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 19:01:08 +0200 Subject: Initial commit, migrating from SVN --- Tests/hu.bme.mit.inf.dslreasoner.run/.classpath | 9 + .../.settings/org.eclipse.jdt.core.prefs | 7 + ...ry.patternlanguage.emf.EMFPatternLanguage.prefs | 27 ++ .../META-INF/MANIFEST.MF | 30 +++ .../build.properties | 9 + .../initialModels/FAM.xmi | 3 + .../initialModels/Yakindu.xmi | 4 + Tests/hu.bme.mit.inf.dslreasoner.run/plugin.xml | 107 ++++++++ .../mit/inf/dslreasoner/run/MetamodelLoader.xtend | 132 ++++++++++ .../mit/inf/dslreasoner/run/RunMeasurements.xtend | 289 +++++++++++++++++++++ .../run/SGraphInconsistencyDetector.xtend | 82 ++++++ .../hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend | 145 +++++++++++ .../run/VisualisePartialInterpretation.xtend | 39 +++ 13 files changed, 883 insertions(+) create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/.classpath create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/.settings/org.eclipse.jdt.core.prefs create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/META-INF/MANIFEST.MF create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/build.properties create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/initialModels/FAM.xmi create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/initialModels/Yakindu.xmi create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/plugin.xml create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphInconsistencyDetector.xtend create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualisePartialInterpretation.xtend (limited to 'Tests/hu.bme.mit.inf.dslreasoner.run') diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/.classpath b/Tests/hu.bme.mit.inf.dslreasoner.run/.classpath new file mode 100644 index 00000000..2b46fc9b --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/.classpath @@ -0,0 +1,9 @@ + + + + + + + + + diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/.settings/org.eclipse.jdt.core.prefs b/Tests/hu.bme.mit.inf.dslreasoner.run/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..295926d9 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/.settings/org.eclipse.jdt.core.prefs @@ -0,0 +1,7 @@ +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled +org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 +org.eclipse.jdt.core.compiler.compliance=1.8 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.problem.enumIdentifier=error +org.eclipse.jdt.core.compiler.source=1.8 diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs b/Tests/hu.bme.mit.inf.dslreasoner.run/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs new file mode 100644 index 00000000..59a4c3b6 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs @@ -0,0 +1,27 @@ +BuilderConfiguration.is_project_specific=true +autobuilding=true +eclipse.preferences.version=1 +generateGeneratedAnnotation=false +generateSuppressWarnings=true +generatedAnnotationComment= +includeDateInGenerated=false +outlet.DEFAULT_OUTPUT.cleanDirectory=false +outlet.DEFAULT_OUTPUT.cleanupDerived=true +outlet.DEFAULT_OUTPUT.createDirectory=false +outlet.DEFAULT_OUTPUT.derived=true +outlet.DEFAULT_OUTPUT.directory=./vql-gen +outlet.DEFAULT_OUTPUT.hideLocalSyntheticVariables=true +outlet.DEFAULT_OUTPUT.installDslAsPrimarySource=false +outlet.DEFAULT_OUTPUT.keepLocalHistory=true +outlet.DEFAULT_OUTPUT.override=true +outlet.DEFAULT_OUTPUT.sourceFolder.eiq-gen.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.eiq-gen.ignore= +outlet.DEFAULT_OUTPUT.sourceFolder.output.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.output.ignore= +outlet.DEFAULT_OUTPUT.sourceFolder.src.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.src.ignore= +outlet.DEFAULT_OUTPUT.sourceFolder.xtend-gen.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.xtend-gen.ignore= +outlet.DEFAULT_OUTPUT.userOutputPerSourceFolder= +targetJavaVersion=JAVA5 +useJavaCompilerCompliance=true 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 new file mode 100644 index 00000000..9c2210bc --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/META-INF/MANIFEST.MF @@ -0,0 +1,30 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: Run +Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.run;singleton:=true +Bundle-Version: 1.0.0.qualifier +Require-Bundle: hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage, + hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", + com.google.guava, + org.eclipse.xtext.xbase.lib, + org.eclipse.xtend.lib, + org.eclipse.xtend.lib.macro, + org.eclipse.emf.ecore.xmi;bundle-version="2.11.1", + hu.bme.mit.inf.dslreasoner.smt.reasoner;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", + org.eclipse.viatra.query.runtime;bundle-version="1.5.0", + org.eclipse.viatra.query.tooling.core;bundle-version="1.5.0", + org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.5.0", + hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0", + org.eclipse.viatra.query.patternlanguage;bundle-version="1.5.0", + org.eclipse.viatra.query.patternlanguage.emf;bundle-version="1.5.0", + hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0", + org.junit;bundle-version="4.12.0", + hu.bme.mit.inf.dslreasoner.domains.transima.fam;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0", + org.eclipse.viatra.dse;bundle-version="0.15.0", + hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic;bundle-version="1.0.0" +Import-Package: org.apache.log4j +Bundle-RequiredExecutionEnvironment: JavaSE-1.8 diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/build.properties b/Tests/hu.bme.mit.inf.dslreasoner.run/build.properties new file mode 100644 index 00000000..f15423d4 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/build.properties @@ -0,0 +1,9 @@ +src.excludes = output/,\ + vql-gen/ +bin.includes = META-INF/,\ + .,\ + plugin.xml +source.. = src/,\ + xtend-gen/,\ + src-gen/ +output.. = bin/ diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/initialModels/FAM.xmi b/Tests/hu.bme.mit.inf.dslreasoner.run/initialModels/FAM.xmi new file mode 100644 index 00000000..d2797166 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/initialModels/FAM.xmi @@ -0,0 +1,3 @@ + + diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/initialModels/Yakindu.xmi b/Tests/hu.bme.mit.inf.dslreasoner.run/initialModels/Yakindu.xmi new file mode 100644 index 00000000..49b1f89d --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/initialModels/Yakindu.xmi @@ -0,0 +1,4 @@ + + diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/plugin.xml b/Tests/hu.bme.mit.inf.dslreasoner.run/plugin.xml new file mode 100644 index 00000000..6bb6c623 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/plugin.xml @@ -0,0 +1,107 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 @@ +package hu.bme.mit.inf.dslreasoner.run + +import hu.bme.mit.inf.dslreasomer.domains.transima.fam.FunctionalArchitecture.FunctionalArchitecturePackage +import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor +import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor +import java.util.LinkedHashMap +import java.util.List +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.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 + +abstract class MetamodelLoader { + protected val ReasonerWorkspace workspace + public new(ReasonerWorkspace workspace) { + this.workspace = workspace + } + def EcoreMetamodelDescriptor loadMetamodel() + def Set getRelevantTypes(EcoreMetamodelDescriptor descriptor) + def Set getRelevantReferences(EcoreMetamodelDescriptor descriptor) + def ViatraQuerySetDescriptor loadQueries(EcoreMetamodelDescriptor metamodel) + def List loadPartialModel() + + def List> additionalConstraints() + + def filterByNames(Iterable collection, Function1 nameExtractor, Collection requiredNames) { + val res = collection.filter[requiredNames.contains(nameExtractor.apply(it))] + if(res.size != requiredNames.size) throw new IllegalArgumentException + return res.toSet + } +} + +class FAMLoader extends MetamodelLoader{ + + new(ReasonerWorkspace workspace) { + super(workspace) + } + + override loadMetamodel() { + val package = FunctionalArchitecturePackage.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 descriptor.classes.filterByNames([it.name],#["FunctionalElement"]) + } + override getRelevantReferences(EcoreMetamodelDescriptor descriptor) { + return descriptor.references.filterByNames([it.name],#["subElements"]) + } + + override loadQueries(EcoreMetamodelDescriptor metamodel) { + val i = hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern.instance + val patterns = i.specifications.toList + val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet + val derivedFeatures = new LinkedHashMap + derivedFeatures.put(i.type.internalQueryRepresentation,metamodel.attributes.filter[it.name == "type"].head) + derivedFeatures.put(i.model.internalQueryRepresentation,metamodel.references.filter[it.name == "model"].head) + val res = new ViatraQuerySetDescriptor( + patterns, + wfPatterns, + derivedFeatures + ) + return res + } + override loadPartialModel() { + this.workspace.readModel(EObject,"FAM.xmi").eResource.allContents.toList + } + + override additionalConstraints() { #[] } +} + +class YakinduLoader extends MetamodelLoader{ + + new(ReasonerWorkspace workspace) { + super(workspace) + } + + override loadMetamodel() { + val package = YakindummPackage.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 loadQueries(EcoreMetamodelDescriptor metamodel) { + val i = hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns.instance + val patterns = i.specifications.toList + val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet + val derivedFeatures = new LinkedHashMap + val res = new ViatraQuerySetDescriptor( + patterns, + wfPatterns, + derivedFeatures + ) + return res + } + override getRelevantTypes(EcoreMetamodelDescriptor descriptor) { + descriptor.classes.filterByNames([it.name],#["Vertex","Transition","Synchronization"]) + } + + override getRelevantReferences(EcoreMetamodelDescriptor descriptor) { + descriptor.references.filterByNames([it.name],#["source","target"]) + } + + override loadPartialModel() { + this.workspace.readModel(EObject,"Yakindu.xmi").eResource.allContents.toList + } + + 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/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 @@ +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.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.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +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.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.io.BufferedReader +import java.io.InputStreamReader +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.junit.Test + +enum UseSolver{Viatra, Smt, ViatraWithSmt, Alloy} +enum Domain{FAM, Yakindu} +enum Diversity{No, Diverse} + +class RunMeasurements { + 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(smtSolver) + 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) + } 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 + Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("ecore",new XMIResourceFactoryImpl) + Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("logicproblem",new XMIResourceFactoryImpl) + Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("partialinterpretation",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 transformDiversity(MetamodelLoader dsl, Ecore2Logic_Trace trace, EcoreMetamodelDescriptor descriptor) { + if(diverse) { + val relevantClasses = dsl.getRelevantTypes(descriptor) + val relevantReferences = dsl.getRelevantReferences(descriptor) + val relevantTypes = relevantClasses.map[this.ecore2Logic.TypeofEClass(trace,it) as TypeDeclaration].toSet + val relevantRelations = relevantReferences.map[this.ecore2Logic.relationOfReference(trace,it) as RelationDeclaration].toSet + return new DiversityDescriptor => [ + it.relevantTypes = relevantTypes + it.relevantRelations = relevantRelations + it.maxNumber = 2 + it.range = 2 + it.parallels = 2 + ] + } else { + return null + } + } + + def executeSolver( + LogicProblem problem, + ViatraQuerySetDescriptor vq, + MetamodelLoader loader, + DiversityDescriptor diversityRequirement, + int size) + { + if(solver == UseSolver.Smt) { + val smtConfig = new SmtSolverConfiguration() => [ + it.typeScopes.maxNewElements = size + it.typeScopes.minNewElements = size + it.solutionScope.numberOfRequiredSolution = number + 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 = number + it.typeScopes.maxIntScope = 0 + it.writeToFile = true + ] + val solution = this.alloyReasoner.solve( + problem, + alloyConfig, + this.workspace + ) + return solution + } else { + val viatraConfig = new ViatraReasonerConfiguration => [ + it.runtimeLimit = 20 + it.typeScopes.maxNewElements = size + it.typeScopes.minNewElements = size + it.solutionScope.numberOfRequiredSolution = number + it.existingQueries = vq.patterns.map[it.internalQueryRepresentation] + it.nameNewElements = false + it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis + it.additionalGlobalConstraints += loader.additionalConstraints + it.stateCoderStrategy = StateCoderStrategy::Neighbourhood + ] + 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.inconsistencDetectorConfiguration = inconsistency], + this.workspace + ) + return solution + } + } + } + + @Test + def runAsTest() { + main(#[]) + } + + static val monitoring = false + static val clean = false + static val domain = Domain::Yakindu + static val solver = UseSolver::Viatra + static val diverse = false + static val wf = true + public static var sizes = #[50] + static var int number = 10 + + 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) { + val r = new RunMeasurements(id) + r.workspace.initAndClear + init + //println("- init") + val dsl = r.dslLoader(domain) + val mm = dsl.loadMetamodel() + val vq = dsl.loadQueries(mm) + //println("- Queries loaded") + + if(!wf) { + mm.attributes.forEach[it.lowerBound = 0] + mm.references.forEach[it.lowerBound = 0] + mm.references.removeAll(vq.derivedFeatures.values) + mm.attributes.removeAll(vq.derivedFeatures.values) + } + + val metamodelProblem = r.transformMMtoLogic(mm) + r.transformPSToLogic(dsl.loadPartialModel,metamodelProblem) + if(wf) { + r.transformQueriesToLogic(vq,metamodelProblem) + } + val logicProblem = metamodelProblem.output + + //r.workspace.writeModel(logicProblem,"problem.logicproblem") + //resSet.resources += viatraProblem.output.eResource + val diversityRequirement = r.transformDiversity(dsl,metamodelProblem.trace,mm) + + //println("- DSL -> Logic problem transformation finished") + + waitForEnter + + val solution = r.executeSolver(logicProblem, vq, dsl, diversityRequirement, size) + + 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.. noEntry + var ViatraQueryMatcher entryHasNoOutgoing + var ViatraQueryMatcher synchronizationHasNoOutgoing + var ViatraQueryMatcher noSynch + var ViatraQueryMatcher synchronizedSiblingRegions + var ViatraQueryMatcher noStateInRegion + + new(ModelGenerationMethod method) { + super(method) + } + + override getName() { + return SGraphInconsistencyDetector.simpleName + } + + override init(ThreadContext context) { + partialInterpretation = context.model as PartialInterpretation + + try{ + this.noEntry = method.unfinishedWF.filter[ + it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noEntryInRegion") + ].head.getMatcher(context.queryEngine) + + this.entryHasNoOutgoing = method.unfinishedWF.filter[ + 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") + ].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) + + this.noStateInRegion = method.unfinishedWF.filter[ + it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noStateInRegion") + ].head.getMatcher(context.queryEngine) + } catch(Exception e) { } + } + + override checkGlobalConstraint(ThreadContext context) { + if(noEntry !== null) { + val requiredNewObjects = + noEntry.countMatches*2 + + entryHasNoOutgoing.countMatches + + synchronizationHasNoOutgoing.countMatches + + noSynch.countMatches*2 + + synchronizedSiblingRegions.countMatches*4 + noStateInRegion.countMatches + val availableNewObjects = partialInterpretation.maxNewElements + val res = availableNewObjects >= requiredNewObjects + //println('''[«availableNewObjects» >= «requiredNewObjects»] = «res»''') + return res + } else { + true + } + + } + override createNew() { + return new SGraphInconsistencyDetector(this.method) + } +// +// def hasSynchronization() { +// this.partialInterpretation.partialtypeinterpratation. +// } +} \ 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 @@ +package hu.bme.mit.inf.dslreasoner.run + +import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace +import hu.bme.mit.inf.dslreasomer.domains.transima.fam.FunctionalArchitecture.FunctionalArchitecturePackage +import java.util.List +import org.eclipse.emf.ecore.EClass +import org.eclipse.emf.ecore.EEnumLiteral +import org.eclipse.emf.ecore.EReference +import org.eclipse.emf.ecore.EEnum +import org.eclipse.emf.ecore.EAttribute +import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import org.eclipse.emf.ecore.EObject +import java.util.LinkedHashMap +import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor +import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic +import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic +import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration +import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult +import org.eclipse.emf.ecore.resource.Resource +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 + +class SimpleRun { + + def static void main(String[] args) { + val inputs = new FileSystemWorkspace('''initialModels/''',"") + val workspace = new FileSystemWorkspace('''outputModels/''',"") + workspace.initAndClear + + println("Input and output workspaces are created") + + val metamodel = loadMetamodel() + val partialModel = loadPartialModel(inputs) + val queries = loadQueries(metamodel) + + println("DSL loaded") + + val Ecore2Logic ecore2Logic = new Ecore2Logic + val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) + val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic + + val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration()) + val modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem,partialModel) + val validModelExtensionProblem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration) + + val logicProblem = validModelExtensionProblem.output + + println("Problem created") + var LogicResult solution + + //* + val ViatraReasoner viatraSolver = new ViatraReasoner + val viatraConfig = new ViatraReasonerConfiguration => [ + it.typeScopes.maxNewElements = 10 + it.typeScopes.minNewElements = 10 + it.solutionScope.numberOfRequiredSolution = 1 + it.existingQueries = queries.patterns.map[it.internalQueryRepresentation] + it.nameNewElements = true + it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis + it.stateCoderStrategy = StateCoderStrategy::Neighbourhood + ] + solution = viatraSolver.solve(logicProblem,viatraConfig,workspace) + /*/ + val AlloySolver alloyReasoner = new AlloySolver + val alloyConfig = new AlloySolverConfiguration => [ + it.typeScopes.maxNewElements = 5 + it.typeScopes.minNewElements = 5 + it.solutionScope.numberOfRequiredSolution = 1 + it.typeScopes.maxIntScope = 0 + it.writeToFile = true + ] + solution = alloyReasoner.solve(logicProblem,alloyConfig,workspace) + //*/ + + println("Problem solved") + + solution.writeSolution(workspace) + } + + def private static loadMetamodel() { + val pckg = FunctionalArchitecturePackage.eINSTANCE + val List classes = pckg.EClassifiers.filter(EClass).toList + val List enums = pckg.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) + } + + def private static loadQueries(EcoreMetamodelDescriptor metamodel) { + val i = hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern.instance + val patterns = i.specifications.toList + val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet + val derivedFeatures = new LinkedHashMap + derivedFeatures.put(i.type.internalQueryRepresentation,metamodel.attributes.filter[it.name == "type"].head) + derivedFeatures.put(i.model.internalQueryRepresentation,metamodel.references.filter[it.name == "model"].head) + val res = new ViatraQuerySetDescriptor( + patterns, + wfPatterns, + derivedFeatures + ) + return res + } + + def static loadPartialModel(ReasonerWorkspace inputs) { + Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); + inputs.readModel(EObject,"FAM.xmi").eResource.allContents.toList + } + + def static writeSolution(LogicResult solution, ReasonerWorkspace workspace) { + if(solution instanceof ModelResult) { + val representations = solution.representation + for(representationIndex : 0..