From c1f185fd8fc2c3dfc123d9271726c588963c7c01 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 8 Apr 2019 00:58:00 +0200 Subject: Objective POC implementation --- .../application/ApplicationConfiguration.xtext | 413 ++++++++++++++------- .../execution/GenerationTaskExecutor.xtend | 4 +- .../application/execution/ScriptExecutor.xtend | 20 +- .../application/execution/SolverLoader.xtend | 182 ++++++--- 4 files changed, 416 insertions(+), 203 deletions(-) (limited to 'Application/hu.bme.mit.inf.dslreasoner.application/src') diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/ApplicationConfiguration.xtext b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/ApplicationConfiguration.xtext index 2b4a56a6..be1ac662 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/ApplicationConfiguration.xtext +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/ApplicationConfiguration.xtext @@ -6,203 +6,328 @@ import "http://www.bme.hu/mit/inf/dslreasoner/faulttree/components/CftLanguage" generate applicationConfiguration "http://www.bme.hu/mit/inf/dslreasoner/application/ApplicationConfiguration" ConfigurationScript: - (imports += Import)* - (commands += Command)* -; + (imports+=Import)* + (commands+=Command)*; -Command : - Declaration | Task -; +Command: + Declaration | Task; QualifiedName returns ecore::EString: - ID ('.' ID)*; -REALLiteral returns ecore::EBigDecimal: '-'? INT '.' INT; -INTLiteral returns ecore::EInt: '-'? INT; + ID ('.' ID)*; + +REALLiteral returns ecore::EBigDecimal: + '-'? INT '.' INT; + +INTLiteral returns ecore::EInt: + '-'? INT; /////////////////////////////////////////////////// // Imports /////////////////////////////////////////////////// +Import: + EPackageImport | ViatraImport | CftImport; + +EPackageImport: + "import" "epackage" importedPackage=[ecore::EPackage|STRING]; -Import: EPackageImport | ViatraImport | CftImport; +ViatraImport: + "import" "viatra" importedViatra=[viatra::PatternModel|STRING]; -EPackageImport: "import" "epackage" importedPackage=[ecore::EPackage|STRING]; -ViatraImport: "import" "viatra" importedViatra=[viatra::PatternModel|STRING]; -CftImport: "import" "reliability" importedCft=[cftLanguage::CftModel|STRING]; - +CftImport: + "import" "reliability" importedCft=[cftLanguage::CftModel|STRING]; + /////////////////////////////////////////////////// // Declaration /////////////////////////////////////////////////// - -Declaration : +Declaration: FileDeclaration | MetamodelDeclaration | PartialModelDeclaration | GraphPatternDeclaration | ConfigDeclaration | ScopeDeclaration - | ObjectiveDeclaration -; + | ObjectiveDeclaration; /////////////////////////////////////////////////// // Files and Folders /////////////////////////////////////////////////// +FileSpecification: + path=STRING; -FileSpecification: path = STRING; -FileDeclaration: 'file' name = ID '=' specification = FileSpecification; -FileReference: referred = [FileDeclaration]; -File: FileSpecification | FileReference; +FileDeclaration: + 'file' name=ID '=' specification=FileSpecification; + +FileReference: + referred=[FileDeclaration]; + +File: + FileSpecification | FileReference; /////////////////////////////////////////////////// // Metamodel /////////////////////////////////////////////////// +MetamodelSpecification: + '{' (entries+=MetamodelEntry) (',' entries+=MetamodelEntry)* '}'; + +MetamodelEntry: + MetamodelElement | AllPackageEntry; + +AllPackageEntry: + "package" package=[ecore::EPackage|QualifiedName] ("excluding" '{' exclusion+=MetamodelElement (',' + exclusion+=MetamodelElement)* '}')?; -MetamodelSpecification: '{' (entries += MetamodelEntry) (',' entries += MetamodelEntry)* '}'; -MetamodelEntry: MetamodelElement | AllPackageEntry; -AllPackageEntry: "package" package=[ecore::EPackage|QualifiedName] ("excluding" '{'exclusion +=MetamodelElement (',' exclusion +=MetamodelElement)*'}')?; -MetamodelElement: (package=[ecore::EPackage|QualifiedName] '::')? classifier = [ecore::EClassifier] ('.' feature= [ecore::ENamedElement])?; +MetamodelElement: + (package=[ecore::EPackage|QualifiedName] '::')? classifier=[ecore::EClassifier] ('.' + feature=[ecore::ENamedElement])?; -MetamodelDeclaration: 'metamodel' name = ID specification = MetamodelSpecification; -MetamodelReference: referred = [MetamodelDeclaration]; -Metamodel: MetamodelReference | MetamodelSpecification; +MetamodelDeclaration: + 'metamodel' name=ID specification=MetamodelSpecification; + +MetamodelReference: + referred=[MetamodelDeclaration]; + +Metamodel: + MetamodelReference | MetamodelSpecification; /////////////////////////////////////////////////// // Partial Model /////////////////////////////////////////////////// +PartialModelSpecification: + '{' entry+=PartialModelEntry (',' entry+=PartialModelEntry)? '}'; + +PartialModelEntry: + ModelEntry | FolderEntry; + +ModelEntry: + path=File; + +FolderEntry: + "folder" path=File ("excluding" "{" exclusion+=ModelEntry ("," exclusion+=ModelEntry)* "}")?; -PartialModelSpecification: '{' entry += PartialModelEntry (',' entry += PartialModelEntry)? '}'; -PartialModelEntry: ModelEntry | FolderEntry; -ModelEntry: path = File; -FolderEntry: "folder" path = File ("excluding" "{" exclusion += ModelEntry ("," exclusion += ModelEntry)* "}")?; +PartialModelDeclaration: + 'models' name=ID specification=PartialModelSpecification; -PartialModelDeclaration: 'models' name = ID specification = PartialModelSpecification; -PartialModelReference : referred = [PartialModelDeclaration]; -PartialModel: PartialModelSpecification | PartialModelReference; +PartialModelReference: + referred=[PartialModelDeclaration]; + +PartialModel: + PartialModelSpecification | PartialModelReference; /////////////////////////////////////////////////// // Patterns /////////////////////////////////////////////////// +PatternSpecification: + '{' entries+=PatternEntry (',' entries+=PatternEntry)* '}'; + +PatternEntry: + PatternElement | AllPatternEntry; + +AllPatternEntry: + 'package' package=[viatra::PatternModel|QualifiedName] ('excluding' '{' exclusuion+=PatternElement (',' + exclusuion+=PatternElement)* '}')?; + +PatternElement: + (package=[viatra::PatternModel|QualifiedName] '::')? pattern=[viatra::Pattern]; -PatternSpecification: '{' entries += PatternEntry (',' entries += PatternEntry)* '}'; -PatternEntry: PatternElement | AllPatternEntry; -AllPatternEntry: 'package' package = [viatra::PatternModel|QualifiedName] ('excluding' '{' exclusuion += PatternElement (',' exclusuion += PatternElement)* '}')?; -PatternElement: (package =[viatra::PatternModel|QualifiedName] '::')? pattern = [viatra::Pattern]; +GraphPatternDeclaration: + 'constraints' name=ID specification=PatternSpecification; -GraphPatternDeclaration: 'constraints' name = ID specification = PatternSpecification; -GraphPatternReference: referred = [GraphPatternDeclaration]; -GraphPattern: GraphPatternReference|PatternSpecification; +GraphPatternReference: + referred=[GraphPatternDeclaration]; + +GraphPattern: + GraphPatternReference | PatternSpecification; /////////////////////////////////////////////////// // Objectives /////////////////////////////////////////////////// +ObjectiveSpecification: + '{' entries+=ObjectiveEntry (',' entries+=ObjectiveEntry)* '}'; + +ObjectiveEntry: + OptimizationEntry | ThresholdEntry; + +enum OptimizationDirection: + MINIMIZE='minimize' | MAXIMIZE='maximize'; + +OptimizationEntry: + direction=OptimizationDirection function=ObjectiveFunction; + +enum ComparisonOperator: + LESS='<' | GREATER='>' | LESS_EQUALS='<=' | GREATER_EQUALS='>='; + +ThresholdEntry: + function=ObjectiveFunction operator=ComparisonOperator threshold=REALLiteral; + +ObjectiveFunction: + CostObjectiveFunction | ReliabilityObjectiveFunction; + +CostObjectiveFunction: + 'cost' '{' entries+=CostEntry (',' entries+=CostEntry)* '}'; + +CostEntry: + patternElement=PatternElement '=' weight=INTLiteral; + +ReliabilityObjectiveFunction: + ReliabiltiyProbability | Mtff; -ObjectiveSpecification: '{' entries += ObjectiveEntry (',' entries += ObjectiveEntry)* '}'; -ObjectiveEntry: OptimizationEntry | ThresholdEntry; -enum OptimizationDirection: MINIMIZE='minimize' | MAXIMIZE='maximize'; -OptimizationEntry: direction=OptimizationDirection function=ObjectiveFunction; -enum ComparisonOperator: LESS_EQUALS='<=' | GREATER_EQUALS='>='; -ThresholdEntry: function=ObjectiveFunction operator=ComparisonOperator threshold=REALLiteral; -ObjectiveFunction: ReliabilityObjectiveFunction; -ReliabilityObjectiveFunction: ReliabiltiyProbability | Mtff; ReliabiltiyProbability: - 'reliability' (package=[cftLanguage::CftModel|QualifiedName] '::')? transformation = [cftLanguage::TransformationDefinition] + 'reliability' (package=[cftLanguage::CftModel|QualifiedName] '::')? + transformation=[cftLanguage::TransformationDefinition] 'at' time=REALLiteral; + Mtff: - 'mtff' (package=[cftLanguage::CftModel|QualifiedName] '::')? transformation = [cftLanguage::TransformationDefinition]; + 'mtff' (package=[cftLanguage::CftModel|QualifiedName] '::')? transformation=[cftLanguage::TransformationDefinition]; + +ObjectiveDeclaration: + 'objectives' name=ID specification=ObjectiveSpecification; + +ObjectiveReference: + referred=[ObjectiveDeclaration]; -ObjectiveDeclaration: 'objectives' name = ID specification = ObjectiveSpecification; -ObjectiveReference: referred = [ObjectiveDeclaration]; -Objective: ObjectiveReference|ObjectiveSpecification; +Objective: + ObjectiveReference | ObjectiveSpecification; /////////////////////////////////////////////////// // SolverConfig /////////////////////////////////////////////////// +ConfigSpecification: + {ConfigSpecification} '{' + (entries+=ConfigEntry ("," entries+=ConfigEntry)*)? + '}'; + +ConfigDeclaration: + 'config' name=ID specification=ConfigSpecification; + +ConfigEntry: + DocumentationEntry | RuntimeEntry | MemoryEntry | CustomEntry; + +DocumentationEntry: + "log-level" '=' level=DocumentLevelSpecification; -ConfigSpecification: {ConfigSpecification}'{' - (entries += ConfigEntry ("," entries += ConfigEntry)*)? +enum DocumentLevelSpecification: + none | normal | full; + +RuntimeEntry: + "runtime" "=" millisecLimit=INT; + +MemoryEntry: + "memory" "=" megabyteLimit=INT; + +CustomEntry: + key=STRING "=" value=STRING; + +ConfigReference: + config=[ConfigDeclaration]; + +Config: + ConfigSpecification | ConfigReference; + +enum Solver: + SMTSolver | AlloySolver | ViatraSolver; + +ScopeSpecification: + {ScopeSpecification} '{' + (scopes+=TypeScope (',' scopes+=TypeScope)*)? '}'; -ConfigDeclaration : - 'config' name = ID specification = ConfigSpecification -; -ConfigEntry: DocumentationEntry | RuntimeEntry | MemoryEntry | CustomEntry; -DocumentationEntry: "log-level" '=' level = DocumentLevelSpecification; -enum DocumentLevelSpecification: none | normal | full; -RuntimeEntry: "runtime" "=" millisecLimit = INT; -MemoryEntry: "memory" "=" megabyteLimit = INT; -CustomEntry: key = STRING "=" value = STRING; - -ConfigReference: config = [ConfigDeclaration]; -Config: ConfigSpecification | ConfigReference; - -enum Solver: SMTSolver | AlloySolver | ViatraSolver; - -ScopeSpecification: {ScopeSpecification} '{' - (scopes += TypeScope (',' scopes += TypeScope)*)? -'}'; -TypeScope: ClassTypeScope | ObjectTypeScope | IntegerTypeScope | RealTypeScope | StringTypeScope; -ClassTypeScope: '#' type = ClassReference - (setsNew ?='+=' | setsSum ?= '=') - (number = ExactNumber | number = IntervallNumber) -; -ObjectTypeScope: '#' type = ObjectReference - (setsNew ?='+=' | setsSum ?= '=') - (number = ExactNumber | number = IntervallNumber) -; -IntegerTypeScope: '#' type = IntegerReference - (setsNew ?='+=' | setsSum ?= '=') - (number = ExactNumber | number = IntervallNumber | number = IntEnumberation) -; -RealTypeScope: '#' type = RealReference - (setsNew ?='+=' | setsSum ?= '=') - (number = ExactNumber | number = IntervallNumber | number = RealEnumeration) -; -StringTypeScope: '#' type = StringReference - (setsNew ?='+=' | setsSum ?= '=') - (number = ExactNumber | number = IntervallNumber | number = StringEnumeration) -; - -TypeReference: ClassReference | ObjectReference | IntegerReference | RealReference | StringReference; -ClassReference: '<' element = MetamodelElement '>'; -ObjectReference: {ObjectReference} 'node'; -IntegerReference: {IntegerScope} 'int'; -RealReference: {RealScope} 'real'; -StringReference: {StringScope} 'string'; - -NumberSpecification: ExactNumber | IntervallNumber | IntEnumberation | RealEnumeration | StringEnumeration; -ExactNumber: exactNumber = INT | exactUnlimited ?= '*'; -IntervallNumber: min = INT '..' (maxNumber = INT | maxUnlimited ?= '*'); -IntEnumberation: {IntEnumberation} '{' (entry += INTLiteral (',' entry += INTLiteral)*)?'}'; -RealEnumeration: {RealEnumeration} '{' (entry += REALLiteral (',' entry += REALLiteral)*)?'}'; -StringEnumeration: {StringEnumeration} '{' (entry += STRING (',' entry += STRING)*)?'}'; - -ScopeDeclaration: 'scope' name = ID specification = ScopeSpecification; -ScopeReference: referred = [ScopeDeclaration]; -Scope: ScopeSpecification | ScopeReference; - -Task: GenerationTask /*| CoverageCalculation | ValidationTask*/; - -GenerationTask: 'generate' {GenerationTask} '{'( - - // domain - ('metamodel' '=' metamodel = Metamodel)? & - ('partial-model' '=' partialModel = PartialModel)? & - ('constraints' '=' patterns = GraphPattern)? & - ('objectives' '=' objectives = Objective)? & - - // model set - ('scope' '=' scope = Scope)? & - (numberSpecified ?= 'number' '=' number= INT)? & - (runSpecified ?= 'runs' '=' runs = INT)? & - // Solver - ('solver' '=' solver = Solver)? & - ('config' '=' config = Config)? & - - // output texts - ('debug' '=' debugFolder = File)? & - ('log' '=' targetLogFile = File)? & - ('statistics' '=' targetStatisticsFile = File)? & - - // output models - ('output' '=' tagetFolder = File)? - - )'}' -; \ No newline at end of file + +TypeScope: + ClassTypeScope | ObjectTypeScope | IntegerTypeScope | RealTypeScope | StringTypeScope; + +ClassTypeScope: + '#' type=ClassReference + (setsNew?='+=' | setsSum?='=') + (number=ExactNumber | number=IntervallNumber); + +ObjectTypeScope: + '#' type=ObjectReference + (setsNew?='+=' | setsSum?='=') + (number=ExactNumber | number=IntervallNumber); + +IntegerTypeScope: + '#' type=IntegerReference + (setsNew?='+=' | setsSum?='=') + (number=ExactNumber | number=IntervallNumber | number=IntEnumberation); + +RealTypeScope: + '#' type=RealReference + (setsNew?='+=' | setsSum?='=') + (number=ExactNumber | number=IntervallNumber | number=RealEnumeration); + +StringTypeScope: + '#' type=StringReference + (setsNew?='+=' | setsSum?='=') + (number=ExactNumber | number=IntervallNumber | number=StringEnumeration); + +TypeReference: + ClassReference | ObjectReference | IntegerReference | RealReference | StringReference; + +ClassReference: + '<' element=MetamodelElement '>'; + +ObjectReference: + {ObjectReference} 'node'; + +IntegerReference: + {IntegerScope} 'int'; + +RealReference: + {RealScope} 'real'; + +StringReference: + {StringScope} 'string'; + +NumberSpecification: + ExactNumber | IntervallNumber | IntEnumberation | RealEnumeration | StringEnumeration; + +ExactNumber: + exactNumber=INT | exactUnlimited?='*'; + +IntervallNumber: + min=INT '..' (maxNumber=INT | maxUnlimited?='*'); + +IntEnumberation: + {IntEnumberation} '{' (entry+=INTLiteral (',' entry+=INTLiteral)*)? '}'; + +RealEnumeration: + {RealEnumeration} '{' (entry+=REALLiteral (',' entry+=REALLiteral)*)? '}'; + +StringEnumeration: + {StringEnumeration} '{' (entry+=STRING (',' entry+=STRING)*)? '}'; + +ScopeDeclaration: + 'scope' name=ID specification=ScopeSpecification; + +ScopeReference: + referred=[ScopeDeclaration]; + +Scope: + ScopeSpecification | ScopeReference; + +Task: + GenerationTask /*| CoverageCalculation | ValidationTask*/; + +GenerationTask: + 'generate' {GenerationTask} '{' ( + + // domain + ('metamodel' '=' metamodel=Metamodel)? & + ('partial-model' '=' partialModel=PartialModel)? & + ('constraints' '=' patterns=GraphPattern)? & + ('objectives' '=' objectives=Objective)? & + + // model set + ('scope' '=' scope=Scope)? & + (numberSpecified?='number' '=' number=INT)? & + (runSpecified?='runs' '=' runs=INT)? & + // Solver + ('solver' '=' solver=Solver)? & + ('config' '=' config=Config)? & + + // output texts + ('debug' '=' debugFolder=File)? & + ('log' '=' targetLogFile=File)? & + ('statistics' '=' targetStatisticsFile=File)? & + + // output models + ('output' '=' tagetFolder=File)?) '}'; \ No newline at end of file diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend index 35ffaf65..8ea674d3 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend @@ -133,7 +133,9 @@ class GenerationTaskExecutor { // 5. create a solver and a configuration // 5.1 initialize val solver = solverLoader.loadSolver(task.solver,configurationMap) - val solverConfig = solverLoader.loadSolverConfig(task.solver,configurationMap,console) + val objectiveSpecification = scriptExecutor.getObjectiveSpecification(task.objectives) + val objectiveEntries = objectiveSpecification?.entries ?: emptyList + val solverConfig = solverLoader.loadSolverConfig(task.solver,configurationMap,objectiveEntries,console) // 5.2 set values that defined directly diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend index 0512a5ee..25036df6 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend @@ -30,6 +30,8 @@ import org.eclipse.core.runtime.Status import org.eclipse.core.runtime.jobs.Job import org.eclipse.emf.common.util.URI import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveSpecification +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveReference @FinalFieldsConstructor class ScriptExecutor { @@ -40,7 +42,7 @@ class ScriptExecutor { /** * Executes a script */ - public def executeScript(URI uri) { + def executeScript(URI uri) { val job = new Job('''Model Generation: «uri.lastSegment»''') { override protected run(IProgressMonitor monitor) { try{ @@ -57,7 +59,7 @@ class ScriptExecutor { job.schedule(); } - public def executeScript(ConfigurationScript script, IProgressMonitor monitor) { + def executeScript(ConfigurationScript script, IProgressMonitor monitor) { script.activateAllEPackageReferences val tasks = script.commands.filter(Task) @@ -94,12 +96,12 @@ class ScriptExecutor { // } } - def public dispatch execute(GenerationTask task, IProgressMonitor monitor) { + def dispatch void execute(GenerationTask task, IProgressMonitor monitor) { val generationTaskExecutor = new GenerationTaskExecutor generationTaskExecutor.executeGenerationTask(task,this,scriptConsoleFactory,monitor) } - def public dispatch execute(Task task, IProgressMonitor monitor) { + def dispatch void execute(Task task, IProgressMonitor monitor) { throw new IllegalArgumentException('''Unsupported task type: «task.class.simpleName»!''') } @@ -174,6 +176,16 @@ class ScriptExecutor { null } + def dispatch getObjectiveSpecification(ObjectiveSpecification config) { + config + } + def dispatch getObjectiveSpecification(ObjectiveReference config) { + config.referred.specification + } + def dispatch getObjectiveSpecification(Void config) { + null + } + def dispatch getConfiguration(ConfigSpecification config) { config } diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend index 9eceef5f..f769d46f 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend @@ -1,44 +1,47 @@ package hu.bme.mit.inf.dslreasoner.application.execution -import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CostObjectiveFunction +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveEntry +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.OptimizationEntry import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ThresholdEntry import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold +import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser +import java.util.List import java.util.Map import java.util.Optional +import org.eclipse.viatra.query.patternlanguage.emf.vql.PatternModel +import org.eclipse.xtext.EcoreUtil2 import org.eclipse.xtext.xbase.lib.Functions.Function1 -import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor class SolverLoader { def loadSolver(Solver solver, Map config) { - switch(solver) { + switch (solver) { case ALLOY_SOLVER: return new AlloySolver case SMT_SOLVER: return new SMTSolver case VIATRA_SOLVER: return new ViatraReasoner } } - - - - private def Optional getAsType( - Map config, - String key, - ScriptConsole console, - Function1 parser, - Class requestedType) - { - if(config.containsKey(key)) { + + private def Optional getAsType(Map config, String key, ScriptConsole console, + Function1 parser, Class requestedType) { + if (config.containsKey(key)) { val stringValue = config.get(key) - try{ + try { val parsedValue = parser.apply(stringValue) return Optional.of(parsedValue) - } catch(Exception e) { + } catch (Exception e) { console.writeError('''Unable to parse configuration value for "«key»" to «requestedType.simpleName»!''') return Optional::empty } @@ -46,60 +49,131 @@ class SolverLoader { return Optional::empty } } + private def getAsInteger(Map config, String key, ScriptConsole console) { - return getAsType(config,key,console,[x|Integer.parseInt(x)],Integer) + return getAsType(config, key, console, [x|Integer.parseInt(x)], Integer) } + private def getAsBoolean(Map config, String key, ScriptConsole console) { - return getAsType(config,key,console,[x|Boolean.parseBoolean(x)],Boolean) + return getAsType(config, key, console, [x|Boolean.parseBoolean(x)], Boolean) } + private def getAsDouble(Map config, String key, ScriptConsole console) { - return getAsType(config,key,console,[x|Double.parseDouble(x)],Double) + return getAsType(config, key, console, [x|Double.parseDouble(x)], Double) } - - def loadSolverConfig( - Solver solver, - Map config, - ScriptConsole console) - { - if(solver === Solver::ALLOY_SOLVER) { - return new AlloySolverConfiguration => [c| - config.getAsInteger("symmetry",console) - .ifPresent[c.symmetry = it] - config.getAsType("solver",console,[x|AlloyBackendSolver::valueOf(x)],AlloyBackendSolver) - .ifPresent[c.solver = it] - ] - } else if(solver === Solver::SMT_SOLVER) { - return new SmtSolverConfiguration => [c| - config.getAsBoolean("fixRandomSeed",console).ifPresent[c.fixRandomSeed = it] - config.getAsType("path",console,[it],String).ifPresent[c.solverPath = it] - ] - } else if(solver === Solver::VIATRA_SOLVER) { - return new ViatraReasonerConfiguration => [c| + + def loadSolverConfig(Solver solver, Map config, List objectiveEntries, + ScriptConsole console) { + switch (solver) { + case ALLOY_SOLVER: { + if (!objectiveEntries.empty) { + throw new IllegalArgumentException("Objectives are not supported by Alloy.") + } + val c = new SmtSolverConfiguration + config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it] + config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it] + c + } + case SMT_SOLVER: { + if (!objectiveEntries.empty) { + throw new IllegalArgumentException("Objectives are not supported by Z3.") + } + val c = new SmtSolverConfiguration + config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it] + config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it] + c + } + case VIATRA_SOLVER: { + val c = new ViatraReasonerConfiguration c.debugConfiguration.partialInterpretatioVisualiser = new GraphvizVisualiser - if(config.containsKey("diversity-range")) { + if (config.containsKey("diversity-range")) { val stringValue = config.get("diversity-range") - try{ + try { val range = Integer.parseInt(stringValue) c.diversityRequirement = new DiversityDescriptor => [ it.ensureDiversity = true it.range = range ] - } catch (NumberFormatException e) {console.writeError('''Malformed number format: «e.message»''')} + } catch (NumberFormatException e) { + console.writeError('''Malformed number format: «e.message»''') + } } - ] - } else { - throw new UnsupportedOperationException('''Unknown solver: «solver»''') + for (objectiveEntry : objectiveEntries) { + val costObjectiveConfig = new CostObjectiveConfiguration + switch (objectiveEntry) { + OptimizationEntry: { + costObjectiveConfig.findExtremum = true + costObjectiveConfig.kind = switch (direction : objectiveEntry.direction) { + case MAXIMIZE: + ObjectiveKind.HIGHER_IS_BETTER + case MINIMIZE: + ObjectiveKind.LOWER_IS_BETTER + default: + throw new IllegalArgumentException("Unknown direction: " + direction) + } + costObjectiveConfig.threshold = ObjectiveThreshold.NO_THRESHOLD + } + ThresholdEntry: { + costObjectiveConfig.findExtremum = false + val threshold = objectiveEntry.threshold.doubleValue + switch (operator : objectiveEntry.operator) { + case LESS: { + costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER + costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) + } + case GREATER: { + costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER + costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) + } + case LESS_EQUALS: { + costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER + costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) + } + case GREATER_EQUALS: { + costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER + costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) + } + default: + throw new IllegalArgumentException("Unknown operator: " + operator) + } + } + } + val function = objectiveEntry.function + if (function instanceof CostObjectiveFunction) { + for (costEntry : function.entries) { + val element = new CostObjectiveElementConfiguration + val pattern = costEntry.patternElement.pattern + val packageName = costEntry.patternElement.package?.packageName ?: + EcoreUtil2.getContainerOfType(pattern, PatternModel)?.packageName + element.patternQualifiedName = if (packageName.nullOrEmpty) { + pattern.name + } else { + packageName + "." + pattern.name + } + costObjectiveConfig.elements += element + } + } else { + throw new IllegalArgumentException("Only cost objectives are supported by VIATRA.") + } + c.costObjectives += costObjectiveConfig + } + c + } + default: + throw new UnsupportedOperationException('''Unknown solver: «solver»''') } } - - def dispatch void setRunIndex(AlloySolverConfiguration config, Map parameters, int runIndex, ScriptConsole console) { - parameters.getAsBoolean("randomize",console).ifPresent[ - if(it) { - config.randomise = runIndex-1 + + def dispatch void setRunIndex(AlloySolverConfiguration config, Map parameters, int runIndex, + ScriptConsole console) { + parameters.getAsBoolean("randomize", console).ifPresent [ + if (it) { + config.randomise = runIndex - 1 } ] } - def dispatch void setRunIndex(LogicSolverConfiguration config, Map parameters, int runIndex, ScriptConsole console) { - + + def dispatch void setRunIndex(LogicSolverConfiguration config, Map parameters, int runIndex, + ScriptConsole console) { } -} \ No newline at end of file +} -- cgit v1.2.3-54-g00ecf