diff options
Diffstat (limited to 'Application/hu.bme.mit.inf.dslreasoner.application/src/hu')
4 files changed, 416 insertions, 203 deletions
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" | |||
6 | generate applicationConfiguration "http://www.bme.hu/mit/inf/dslreasoner/application/ApplicationConfiguration" | 6 | generate applicationConfiguration "http://www.bme.hu/mit/inf/dslreasoner/application/ApplicationConfiguration" |
7 | 7 | ||
8 | ConfigurationScript: | 8 | ConfigurationScript: |
9 | (imports += Import)* | 9 | (imports+=Import)* |
10 | (commands += Command)* | 10 | (commands+=Command)*; |
11 | ; | ||
12 | 11 | ||
13 | Command : | 12 | Command: |
14 | Declaration | Task | 13 | Declaration | Task; |
15 | ; | ||
16 | 14 | ||
17 | QualifiedName returns ecore::EString: | 15 | QualifiedName returns ecore::EString: |
18 | ID ('.' ID)*; | 16 | ID ('.' ID)*; |
19 | REALLiteral returns ecore::EBigDecimal: '-'? INT '.' INT; | 17 | |
20 | INTLiteral returns ecore::EInt: '-'? INT; | 18 | REALLiteral returns ecore::EBigDecimal: |
19 | '-'? INT '.' INT; | ||
20 | |||
21 | INTLiteral returns ecore::EInt: | ||
22 | '-'? INT; | ||
21 | 23 | ||
22 | /////////////////////////////////////////////////// | 24 | /////////////////////////////////////////////////// |
23 | // Imports | 25 | // Imports |
24 | /////////////////////////////////////////////////// | 26 | /////////////////////////////////////////////////// |
27 | Import: | ||
28 | EPackageImport | ViatraImport | CftImport; | ||
29 | |||
30 | EPackageImport: | ||
31 | "import" "epackage" importedPackage=[ecore::EPackage|STRING]; | ||
25 | 32 | ||
26 | Import: EPackageImport | ViatraImport | CftImport; | 33 | ViatraImport: |
34 | "import" "viatra" importedViatra=[viatra::PatternModel|STRING]; | ||
27 | 35 | ||
28 | EPackageImport: "import" "epackage" importedPackage=[ecore::EPackage|STRING]; | 36 | CftImport: |
29 | ViatraImport: "import" "viatra" importedViatra=[viatra::PatternModel|STRING]; | 37 | "import" "reliability" importedCft=[cftLanguage::CftModel|STRING]; |
30 | CftImport: "import" "reliability" importedCft=[cftLanguage::CftModel|STRING]; | 38 | |
31 | |||
32 | /////////////////////////////////////////////////// | 39 | /////////////////////////////////////////////////// |
33 | // Declaration | 40 | // Declaration |
34 | /////////////////////////////////////////////////// | 41 | /////////////////////////////////////////////////// |
35 | 42 | Declaration: | |
36 | Declaration : | ||
37 | FileDeclaration | 43 | FileDeclaration |
38 | | MetamodelDeclaration | 44 | | MetamodelDeclaration |
39 | | PartialModelDeclaration | 45 | | PartialModelDeclaration |
40 | | GraphPatternDeclaration | 46 | | GraphPatternDeclaration |
41 | | ConfigDeclaration | 47 | | ConfigDeclaration |
42 | | ScopeDeclaration | 48 | | ScopeDeclaration |
43 | | ObjectiveDeclaration | 49 | | ObjectiveDeclaration; |
44 | ; | ||
45 | 50 | ||
46 | /////////////////////////////////////////////////// | 51 | /////////////////////////////////////////////////// |
47 | // Files and Folders | 52 | // Files and Folders |
48 | /////////////////////////////////////////////////// | 53 | /////////////////////////////////////////////////// |
54 | FileSpecification: | ||
55 | path=STRING; | ||
49 | 56 | ||
50 | FileSpecification: path = STRING; | 57 | FileDeclaration: |
51 | FileDeclaration: 'file' name = ID '=' specification = FileSpecification; | 58 | 'file' name=ID '=' specification=FileSpecification; |
52 | FileReference: referred = [FileDeclaration]; | 59 | |
53 | File: FileSpecification | FileReference; | 60 | FileReference: |
61 | referred=[FileDeclaration]; | ||
62 | |||
63 | File: | ||
64 | FileSpecification | FileReference; | ||
54 | 65 | ||
55 | /////////////////////////////////////////////////// | 66 | /////////////////////////////////////////////////// |
56 | // Metamodel | 67 | // Metamodel |
57 | /////////////////////////////////////////////////// | 68 | /////////////////////////////////////////////////// |
69 | MetamodelSpecification: | ||
70 | '{' (entries+=MetamodelEntry) (',' entries+=MetamodelEntry)* '}'; | ||
71 | |||
72 | MetamodelEntry: | ||
73 | MetamodelElement | AllPackageEntry; | ||
74 | |||
75 | AllPackageEntry: | ||
76 | "package" package=[ecore::EPackage|QualifiedName] ("excluding" '{' exclusion+=MetamodelElement (',' | ||
77 | exclusion+=MetamodelElement)* '}')?; | ||
58 | 78 | ||
59 | MetamodelSpecification: '{' (entries += MetamodelEntry) (',' entries += MetamodelEntry)* '}'; | 79 | MetamodelElement: |
60 | MetamodelEntry: MetamodelElement | AllPackageEntry; | 80 | (package=[ecore::EPackage|QualifiedName] '::')? classifier=[ecore::EClassifier] ('.' |
61 | AllPackageEntry: "package" package=[ecore::EPackage|QualifiedName] ("excluding" '{'exclusion +=MetamodelElement (',' exclusion +=MetamodelElement)*'}')?; | 81 | feature=[ecore::ENamedElement])?; |
62 | MetamodelElement: (package=[ecore::EPackage|QualifiedName] '::')? classifier = [ecore::EClassifier] ('.' feature= [ecore::ENamedElement])?; | ||
63 | 82 | ||
64 | MetamodelDeclaration: 'metamodel' name = ID specification = MetamodelSpecification; | 83 | MetamodelDeclaration: |
65 | MetamodelReference: referred = [MetamodelDeclaration]; | 84 | 'metamodel' name=ID specification=MetamodelSpecification; |
66 | Metamodel: MetamodelReference | MetamodelSpecification; | 85 | |
86 | MetamodelReference: | ||
87 | referred=[MetamodelDeclaration]; | ||
88 | |||
89 | Metamodel: | ||
90 | MetamodelReference | MetamodelSpecification; | ||
67 | 91 | ||
68 | /////////////////////////////////////////////////// | 92 | /////////////////////////////////////////////////// |
69 | // Partial Model | 93 | // Partial Model |
70 | /////////////////////////////////////////////////// | 94 | /////////////////////////////////////////////////// |
95 | PartialModelSpecification: | ||
96 | '{' entry+=PartialModelEntry (',' entry+=PartialModelEntry)? '}'; | ||
97 | |||
98 | PartialModelEntry: | ||
99 | ModelEntry | FolderEntry; | ||
100 | |||
101 | ModelEntry: | ||
102 | path=File; | ||
103 | |||
104 | FolderEntry: | ||
105 | "folder" path=File ("excluding" "{" exclusion+=ModelEntry ("," exclusion+=ModelEntry)* "}")?; | ||
71 | 106 | ||
72 | PartialModelSpecification: '{' entry += PartialModelEntry (',' entry += PartialModelEntry)? '}'; | 107 | PartialModelDeclaration: |
73 | PartialModelEntry: ModelEntry | FolderEntry; | 108 | 'models' name=ID specification=PartialModelSpecification; |
74 | ModelEntry: path = File; | ||
75 | FolderEntry: "folder" path = File ("excluding" "{" exclusion += ModelEntry ("," exclusion += ModelEntry)* "}")?; | ||
76 | 109 | ||
77 | PartialModelDeclaration: 'models' name = ID specification = PartialModelSpecification; | 110 | PartialModelReference: |
78 | PartialModelReference : referred = [PartialModelDeclaration]; | 111 | referred=[PartialModelDeclaration]; |
79 | PartialModel: PartialModelSpecification | PartialModelReference; | 112 | |
113 | PartialModel: | ||
114 | PartialModelSpecification | PartialModelReference; | ||
80 | 115 | ||
81 | /////////////////////////////////////////////////// | 116 | /////////////////////////////////////////////////// |
82 | // Patterns | 117 | // Patterns |
83 | /////////////////////////////////////////////////// | 118 | /////////////////////////////////////////////////// |
119 | PatternSpecification: | ||
120 | '{' entries+=PatternEntry (',' entries+=PatternEntry)* '}'; | ||
121 | |||
122 | PatternEntry: | ||
123 | PatternElement | AllPatternEntry; | ||
124 | |||
125 | AllPatternEntry: | ||
126 | 'package' package=[viatra::PatternModel|QualifiedName] ('excluding' '{' exclusuion+=PatternElement (',' | ||
127 | exclusuion+=PatternElement)* '}')?; | ||
128 | |||
129 | PatternElement: | ||
130 | (package=[viatra::PatternModel|QualifiedName] '::')? pattern=[viatra::Pattern]; | ||
84 | 131 | ||
85 | PatternSpecification: '{' entries += PatternEntry (',' entries += PatternEntry)* '}'; | 132 | GraphPatternDeclaration: |
86 | PatternEntry: PatternElement | AllPatternEntry; | 133 | 'constraints' name=ID specification=PatternSpecification; |
87 | AllPatternEntry: 'package' package = [viatra::PatternModel|QualifiedName] ('excluding' '{' exclusuion += PatternElement (',' exclusuion += PatternElement)* '}')?; | ||
88 | PatternElement: (package =[viatra::PatternModel|QualifiedName] '::')? pattern = [viatra::Pattern]; | ||
89 | 134 | ||
90 | GraphPatternDeclaration: 'constraints' name = ID specification = PatternSpecification; | 135 | GraphPatternReference: |
91 | GraphPatternReference: referred = [GraphPatternDeclaration]; | 136 | referred=[GraphPatternDeclaration]; |
92 | GraphPattern: GraphPatternReference|PatternSpecification; | 137 | |
138 | GraphPattern: | ||
139 | GraphPatternReference | PatternSpecification; | ||
93 | 140 | ||
94 | /////////////////////////////////////////////////// | 141 | /////////////////////////////////////////////////// |
95 | // Objectives | 142 | // Objectives |
96 | /////////////////////////////////////////////////// | 143 | /////////////////////////////////////////////////// |
144 | ObjectiveSpecification: | ||
145 | '{' entries+=ObjectiveEntry (',' entries+=ObjectiveEntry)* '}'; | ||
146 | |||
147 | ObjectiveEntry: | ||
148 | OptimizationEntry | ThresholdEntry; | ||
149 | |||
150 | enum OptimizationDirection: | ||
151 | MINIMIZE='minimize' | MAXIMIZE='maximize'; | ||
152 | |||
153 | OptimizationEntry: | ||
154 | direction=OptimizationDirection function=ObjectiveFunction; | ||
155 | |||
156 | enum ComparisonOperator: | ||
157 | LESS='<' | GREATER='>' | LESS_EQUALS='<=' | GREATER_EQUALS='>='; | ||
158 | |||
159 | ThresholdEntry: | ||
160 | function=ObjectiveFunction operator=ComparisonOperator threshold=REALLiteral; | ||
161 | |||
162 | ObjectiveFunction: | ||
163 | CostObjectiveFunction | ReliabilityObjectiveFunction; | ||
164 | |||
165 | CostObjectiveFunction: | ||
166 | 'cost' '{' entries+=CostEntry (',' entries+=CostEntry)* '}'; | ||
167 | |||
168 | CostEntry: | ||
169 | patternElement=PatternElement '=' weight=INTLiteral; | ||
170 | |||
171 | ReliabilityObjectiveFunction: | ||
172 | ReliabiltiyProbability | Mtff; | ||
97 | 173 | ||
98 | ObjectiveSpecification: '{' entries += ObjectiveEntry (',' entries += ObjectiveEntry)* '}'; | ||
99 | ObjectiveEntry: OptimizationEntry | ThresholdEntry; | ||
100 | enum OptimizationDirection: MINIMIZE='minimize' | MAXIMIZE='maximize'; | ||
101 | OptimizationEntry: direction=OptimizationDirection function=ObjectiveFunction; | ||
102 | enum ComparisonOperator: LESS_EQUALS='<=' | GREATER_EQUALS='>='; | ||
103 | ThresholdEntry: function=ObjectiveFunction operator=ComparisonOperator threshold=REALLiteral; | ||
104 | ObjectiveFunction: ReliabilityObjectiveFunction; | ||
105 | ReliabilityObjectiveFunction: ReliabiltiyProbability | Mtff; | ||
106 | ReliabiltiyProbability: | 174 | ReliabiltiyProbability: |
107 | 'reliability' (package=[cftLanguage::CftModel|QualifiedName] '::')? transformation = [cftLanguage::TransformationDefinition] | 175 | 'reliability' (package=[cftLanguage::CftModel|QualifiedName] '::')? |
176 | transformation=[cftLanguage::TransformationDefinition] | ||
108 | 'at' time=REALLiteral; | 177 | 'at' time=REALLiteral; |
178 | |||
109 | Mtff: | 179 | Mtff: |
110 | 'mtff' (package=[cftLanguage::CftModel|QualifiedName] '::')? transformation = [cftLanguage::TransformationDefinition]; | 180 | 'mtff' (package=[cftLanguage::CftModel|QualifiedName] '::')? transformation=[cftLanguage::TransformationDefinition]; |
181 | |||
182 | ObjectiveDeclaration: | ||
183 | 'objectives' name=ID specification=ObjectiveSpecification; | ||
184 | |||
185 | ObjectiveReference: | ||
186 | referred=[ObjectiveDeclaration]; | ||
111 | 187 | ||
112 | ObjectiveDeclaration: 'objectives' name = ID specification = ObjectiveSpecification; | 188 | Objective: |
113 | ObjectiveReference: referred = [ObjectiveDeclaration]; | 189 | ObjectiveReference | ObjectiveSpecification; |
114 | Objective: ObjectiveReference|ObjectiveSpecification; | ||
115 | 190 | ||
116 | /////////////////////////////////////////////////// | 191 | /////////////////////////////////////////////////// |
117 | // SolverConfig | 192 | // SolverConfig |
118 | /////////////////////////////////////////////////// | 193 | /////////////////////////////////////////////////// |
194 | ConfigSpecification: | ||
195 | {ConfigSpecification} '{' | ||
196 | (entries+=ConfigEntry ("," entries+=ConfigEntry)*)? | ||
197 | '}'; | ||
198 | |||
199 | ConfigDeclaration: | ||
200 | 'config' name=ID specification=ConfigSpecification; | ||
201 | |||
202 | ConfigEntry: | ||
203 | DocumentationEntry | RuntimeEntry | MemoryEntry | CustomEntry; | ||
204 | |||
205 | DocumentationEntry: | ||
206 | "log-level" '=' level=DocumentLevelSpecification; | ||
119 | 207 | ||
120 | ConfigSpecification: {ConfigSpecification}'{' | 208 | enum DocumentLevelSpecification: |
121 | (entries += ConfigEntry ("," entries += ConfigEntry)*)? | 209 | none | normal | full; |
210 | |||
211 | RuntimeEntry: | ||
212 | "runtime" "=" millisecLimit=INT; | ||
213 | |||
214 | MemoryEntry: | ||
215 | "memory" "=" megabyteLimit=INT; | ||
216 | |||
217 | CustomEntry: | ||
218 | key=STRING "=" value=STRING; | ||
219 | |||
220 | ConfigReference: | ||
221 | config=[ConfigDeclaration]; | ||
222 | |||
223 | Config: | ||
224 | ConfigSpecification | ConfigReference; | ||
225 | |||
226 | enum Solver: | ||
227 | SMTSolver | AlloySolver | ViatraSolver; | ||
228 | |||
229 | ScopeSpecification: | ||
230 | {ScopeSpecification} '{' | ||
231 | (scopes+=TypeScope (',' scopes+=TypeScope)*)? | ||
122 | '}'; | 232 | '}'; |
123 | ConfigDeclaration : | 233 | |
124 | 'config' name = ID specification = ConfigSpecification | 234 | TypeScope: |
125 | ; | 235 | ClassTypeScope | ObjectTypeScope | IntegerTypeScope | RealTypeScope | StringTypeScope; |
126 | ConfigEntry: DocumentationEntry | RuntimeEntry | MemoryEntry | CustomEntry; | 236 | |
127 | DocumentationEntry: "log-level" '=' level = DocumentLevelSpecification; | 237 | ClassTypeScope: |
128 | enum DocumentLevelSpecification: none | normal | full; | 238 | '#' type=ClassReference |
129 | RuntimeEntry: "runtime" "=" millisecLimit = INT; | 239 | (setsNew?='+=' | setsSum?='=') |
130 | MemoryEntry: "memory" "=" megabyteLimit = INT; | 240 | (number=ExactNumber | number=IntervallNumber); |
131 | CustomEntry: key = STRING "=" value = STRING; | 241 | |
132 | 242 | ObjectTypeScope: | |
133 | ConfigReference: config = [ConfigDeclaration]; | 243 | '#' type=ObjectReference |
134 | Config: ConfigSpecification | ConfigReference; | 244 | (setsNew?='+=' | setsSum?='=') |
135 | 245 | (number=ExactNumber | number=IntervallNumber); | |
136 | enum Solver: SMTSolver | AlloySolver | ViatraSolver; | 246 | |
137 | 247 | IntegerTypeScope: | |
138 | ScopeSpecification: {ScopeSpecification} '{' | 248 | '#' type=IntegerReference |
139 | (scopes += TypeScope (',' scopes += TypeScope)*)? | 249 | (setsNew?='+=' | setsSum?='=') |
140 | '}'; | 250 | (number=ExactNumber | number=IntervallNumber | number=IntEnumberation); |
141 | TypeScope: ClassTypeScope | ObjectTypeScope | IntegerTypeScope | RealTypeScope | StringTypeScope; | 251 | |
142 | ClassTypeScope: '#' type = ClassReference | 252 | RealTypeScope: |
143 | (setsNew ?='+=' | setsSum ?= '=') | 253 | '#' type=RealReference |
144 | (number = ExactNumber | number = IntervallNumber) | 254 | (setsNew?='+=' | setsSum?='=') |
145 | ; | 255 | (number=ExactNumber | number=IntervallNumber | number=RealEnumeration); |
146 | ObjectTypeScope: '#' type = ObjectReference | 256 | |
147 | (setsNew ?='+=' | setsSum ?= '=') | 257 | StringTypeScope: |
148 | (number = ExactNumber | number = IntervallNumber) | 258 | '#' type=StringReference |
149 | ; | 259 | (setsNew?='+=' | setsSum?='=') |
150 | IntegerTypeScope: '#' type = IntegerReference | 260 | (number=ExactNumber | number=IntervallNumber | number=StringEnumeration); |
151 | (setsNew ?='+=' | setsSum ?= '=') | 261 | |
152 | (number = ExactNumber | number = IntervallNumber | number = IntEnumberation) | 262 | TypeReference: |
153 | ; | 263 | ClassReference | ObjectReference | IntegerReference | RealReference | StringReference; |
154 | RealTypeScope: '#' type = RealReference | 264 | |
155 | (setsNew ?='+=' | setsSum ?= '=') | 265 | ClassReference: |
156 | (number = ExactNumber | number = IntervallNumber | number = RealEnumeration) | 266 | '<' element=MetamodelElement '>'; |
157 | ; | 267 | |
158 | StringTypeScope: '#' type = StringReference | 268 | ObjectReference: |
159 | (setsNew ?='+=' | setsSum ?= '=') | 269 | {ObjectReference} 'node'; |
160 | (number = ExactNumber | number = IntervallNumber | number = StringEnumeration) | 270 | |
161 | ; | 271 | IntegerReference: |
162 | 272 | {IntegerScope} 'int'; | |
163 | TypeReference: ClassReference | ObjectReference | IntegerReference | RealReference | StringReference; | 273 | |
164 | ClassReference: '<' element = MetamodelElement '>'; | 274 | RealReference: |
165 | ObjectReference: {ObjectReference} 'node'; | 275 | {RealScope} 'real'; |
166 | IntegerReference: {IntegerScope} 'int'; | 276 | |
167 | RealReference: {RealScope} 'real'; | 277 | StringReference: |
168 | StringReference: {StringScope} 'string'; | 278 | {StringScope} 'string'; |
169 | 279 | ||
170 | NumberSpecification: ExactNumber | IntervallNumber | IntEnumberation | RealEnumeration | StringEnumeration; | 280 | NumberSpecification: |
171 | ExactNumber: exactNumber = INT | exactUnlimited ?= '*'; | 281 | ExactNumber | IntervallNumber | IntEnumberation | RealEnumeration | StringEnumeration; |
172 | IntervallNumber: min = INT '..' (maxNumber = INT | maxUnlimited ?= '*'); | 282 | |
173 | IntEnumberation: {IntEnumberation} '{' (entry += INTLiteral (',' entry += INTLiteral)*)?'}'; | 283 | ExactNumber: |
174 | RealEnumeration: {RealEnumeration} '{' (entry += REALLiteral (',' entry += REALLiteral)*)?'}'; | 284 | exactNumber=INT | exactUnlimited?='*'; |
175 | StringEnumeration: {StringEnumeration} '{' (entry += STRING (',' entry += STRING)*)?'}'; | 285 | |
176 | 286 | IntervallNumber: | |
177 | ScopeDeclaration: 'scope' name = ID specification = ScopeSpecification; | 287 | min=INT '..' (maxNumber=INT | maxUnlimited?='*'); |
178 | ScopeReference: referred = [ScopeDeclaration]; | 288 | |
179 | Scope: ScopeSpecification | ScopeReference; | 289 | IntEnumberation: |
180 | 290 | {IntEnumberation} '{' (entry+=INTLiteral (',' entry+=INTLiteral)*)? '}'; | |
181 | Task: GenerationTask /*| CoverageCalculation | ValidationTask*/; | 291 | |
182 | 292 | RealEnumeration: | |
183 | GenerationTask: 'generate' {GenerationTask} '{'( | 293 | {RealEnumeration} '{' (entry+=REALLiteral (',' entry+=REALLiteral)*)? '}'; |
184 | 294 | ||
185 | // domain | 295 | StringEnumeration: |
186 | ('metamodel' '=' metamodel = Metamodel)? & | 296 | {StringEnumeration} '{' (entry+=STRING (',' entry+=STRING)*)? '}'; |
187 | ('partial-model' '=' partialModel = PartialModel)? & | 297 | |
188 | ('constraints' '=' patterns = GraphPattern)? & | 298 | ScopeDeclaration: |
189 | ('objectives' '=' objectives = Objective)? & | 299 | 'scope' name=ID specification=ScopeSpecification; |
190 | 300 | ||
191 | // model set | 301 | ScopeReference: |
192 | ('scope' '=' scope = Scope)? & | 302 | referred=[ScopeDeclaration]; |
193 | (numberSpecified ?= 'number' '=' number= INT)? & | 303 | |
194 | (runSpecified ?= 'runs' '=' runs = INT)? & | 304 | Scope: |
195 | // Solver | 305 | ScopeSpecification | ScopeReference; |
196 | ('solver' '=' solver = Solver)? & | 306 | |
197 | ('config' '=' config = Config)? & | 307 | Task: |
198 | 308 | GenerationTask /*| CoverageCalculation | ValidationTask*/; | |
199 | // output texts | 309 | |
200 | ('debug' '=' debugFolder = File)? & | 310 | GenerationTask: |
201 | ('log' '=' targetLogFile = File)? & | 311 | 'generate' {GenerationTask} '{' ( |
202 | ('statistics' '=' targetStatisticsFile = File)? & | 312 | |
203 | 313 | // domain | |
204 | // output models | 314 | ('metamodel' '=' metamodel=Metamodel)? & |
205 | ('output' '=' tagetFolder = File)? | 315 | ('partial-model' '=' partialModel=PartialModel)? & |
206 | 316 | ('constraints' '=' patterns=GraphPattern)? & | |
207 | )'}' | 317 | ('objectives' '=' objectives=Objective)? & |
208 | ; \ No newline at end of file | 318 | |
319 | // model set | ||
320 | ('scope' '=' scope=Scope)? & | ||
321 | (numberSpecified?='number' '=' number=INT)? & | ||
322 | (runSpecified?='runs' '=' runs=INT)? & | ||
323 | // Solver | ||
324 | ('solver' '=' solver=Solver)? & | ||
325 | ('config' '=' config=Config)? & | ||
326 | |||
327 | // output texts | ||
328 | ('debug' '=' debugFolder=File)? & | ||
329 | ('log' '=' targetLogFile=File)? & | ||
330 | ('statistics' '=' targetStatisticsFile=File)? & | ||
331 | |||
332 | // output models | ||
333 | ('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 { | |||
133 | // 5. create a solver and a configuration | 133 | // 5. create a solver and a configuration |
134 | // 5.1 initialize | 134 | // 5.1 initialize |
135 | val solver = solverLoader.loadSolver(task.solver,configurationMap) | 135 | val solver = solverLoader.loadSolver(task.solver,configurationMap) |
136 | val solverConfig = solverLoader.loadSolverConfig(task.solver,configurationMap,console) | 136 | val objectiveSpecification = scriptExecutor.getObjectiveSpecification(task.objectives) |
137 | val objectiveEntries = objectiveSpecification?.entries ?: emptyList | ||
138 | val solverConfig = solverLoader.loadSolverConfig(task.solver,configurationMap,objectiveEntries,console) | ||
137 | 139 | ||
138 | 140 | ||
139 | // 5.2 set values that defined directly | 141 | // 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 | |||
30 | import org.eclipse.core.runtime.jobs.Job | 30 | import org.eclipse.core.runtime.jobs.Job |
31 | import org.eclipse.emf.common.util.URI | 31 | import org.eclipse.emf.common.util.URI |
32 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 32 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
33 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveSpecification | ||
34 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveReference | ||
33 | 35 | ||
34 | @FinalFieldsConstructor | 36 | @FinalFieldsConstructor |
35 | class ScriptExecutor { | 37 | class ScriptExecutor { |
@@ -40,7 +42,7 @@ class ScriptExecutor { | |||
40 | /** | 42 | /** |
41 | * Executes a script | 43 | * Executes a script |
42 | */ | 44 | */ |
43 | public def executeScript(URI uri) { | 45 | def executeScript(URI uri) { |
44 | val job = new Job('''Model Generation: «uri.lastSegment»''') { | 46 | val job = new Job('''Model Generation: «uri.lastSegment»''') { |
45 | override protected run(IProgressMonitor monitor) { | 47 | override protected run(IProgressMonitor monitor) { |
46 | try{ | 48 | try{ |
@@ -57,7 +59,7 @@ class ScriptExecutor { | |||
57 | job.schedule(); | 59 | job.schedule(); |
58 | } | 60 | } |
59 | 61 | ||
60 | public def executeScript(ConfigurationScript script, IProgressMonitor monitor) { | 62 | def executeScript(ConfigurationScript script, IProgressMonitor monitor) { |
61 | script.activateAllEPackageReferences | 63 | script.activateAllEPackageReferences |
62 | val tasks = script.commands.filter(Task) | 64 | val tasks = script.commands.filter(Task) |
63 | 65 | ||
@@ -94,12 +96,12 @@ class ScriptExecutor { | |||
94 | // } | 96 | // } |
95 | } | 97 | } |
96 | 98 | ||
97 | def public dispatch execute(GenerationTask task, IProgressMonitor monitor) { | 99 | def dispatch void execute(GenerationTask task, IProgressMonitor monitor) { |
98 | val generationTaskExecutor = new GenerationTaskExecutor | 100 | val generationTaskExecutor = new GenerationTaskExecutor |
99 | generationTaskExecutor.executeGenerationTask(task,this,scriptConsoleFactory,monitor) | 101 | generationTaskExecutor.executeGenerationTask(task,this,scriptConsoleFactory,monitor) |
100 | } | 102 | } |
101 | 103 | ||
102 | def public dispatch execute(Task task, IProgressMonitor monitor) { | 104 | def dispatch void execute(Task task, IProgressMonitor monitor) { |
103 | throw new IllegalArgumentException('''Unsupported task type: «task.class.simpleName»!''') | 105 | throw new IllegalArgumentException('''Unsupported task type: «task.class.simpleName»!''') |
104 | } | 106 | } |
105 | 107 | ||
@@ -174,6 +176,16 @@ class ScriptExecutor { | |||
174 | null | 176 | null |
175 | } | 177 | } |
176 | 178 | ||
179 | def dispatch getObjectiveSpecification(ObjectiveSpecification config) { | ||
180 | config | ||
181 | } | ||
182 | def dispatch getObjectiveSpecification(ObjectiveReference config) { | ||
183 | config.referred.specification | ||
184 | } | ||
185 | def dispatch getObjectiveSpecification(Void config) { | ||
186 | null | ||
187 | } | ||
188 | |||
177 | def dispatch getConfiguration(ConfigSpecification config) { | 189 | def dispatch getConfiguration(ConfigSpecification config) { |
178 | config | 190 | config |
179 | } | 191 | } |
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.application.execution | 1 | package hu.bme.mit.inf.dslreasoner.application.execution |
2 | 2 | ||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver | ||
4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver | 3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver |
5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | 4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration |
5 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CostObjectiveFunction | ||
6 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveEntry | ||
7 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.OptimizationEntry | ||
6 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver | 8 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver |
9 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ThresholdEntry | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
8 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver | 11 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver |
9 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration | 12 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold | ||
20 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser | ||
21 | import java.util.List | ||
12 | import java.util.Map | 22 | import java.util.Map |
13 | import java.util.Optional | 23 | import java.util.Optional |
24 | import org.eclipse.viatra.query.patternlanguage.emf.vql.PatternModel | ||
25 | import org.eclipse.xtext.EcoreUtil2 | ||
14 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | 26 | import org.eclipse.xtext.xbase.lib.Functions.Function1 |
15 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
17 | 27 | ||
18 | class SolverLoader { | 28 | class SolverLoader { |
19 | def loadSolver(Solver solver, Map<String, String> config) { | 29 | def loadSolver(Solver solver, Map<String, String> config) { |
20 | switch(solver) { | 30 | switch (solver) { |
21 | case ALLOY_SOLVER: return new AlloySolver | 31 | case ALLOY_SOLVER: return new AlloySolver |
22 | case SMT_SOLVER: return new SMTSolver | 32 | case SMT_SOLVER: return new SMTSolver |
23 | case VIATRA_SOLVER: return new ViatraReasoner | 33 | case VIATRA_SOLVER: return new ViatraReasoner |
24 | } | 34 | } |
25 | } | 35 | } |
26 | 36 | ||
27 | 37 | private def <Type> Optional<Type> getAsType(Map<String, String> config, String key, ScriptConsole console, | |
28 | 38 | Function1<String, Type> parser, Class<Type> requestedType) { | |
29 | private def <Type> Optional<Type> getAsType( | 39 | if (config.containsKey(key)) { |
30 | Map<String, String> config, | ||
31 | String key, | ||
32 | ScriptConsole console, | ||
33 | Function1<String,Type> parser, | ||
34 | Class<Type> requestedType) | ||
35 | { | ||
36 | if(config.containsKey(key)) { | ||
37 | val stringValue = config.get(key) | 40 | val stringValue = config.get(key) |
38 | try{ | 41 | try { |
39 | val parsedValue = parser.apply(stringValue) | 42 | val parsedValue = parser.apply(stringValue) |
40 | return Optional.of(parsedValue) | 43 | return Optional.of(parsedValue) |
41 | } catch(Exception e) { | 44 | } catch (Exception e) { |
42 | console.writeError('''Unable to parse configuration value for "«key»" to «requestedType.simpleName»!''') | 45 | console.writeError('''Unable to parse configuration value for "«key»" to «requestedType.simpleName»!''') |
43 | return Optional::empty | 46 | return Optional::empty |
44 | } | 47 | } |
@@ -46,60 +49,131 @@ class SolverLoader { | |||
46 | return Optional::empty | 49 | return Optional::empty |
47 | } | 50 | } |
48 | } | 51 | } |
52 | |||
49 | private def getAsInteger(Map<String, String> config, String key, ScriptConsole console) { | 53 | private def getAsInteger(Map<String, String> config, String key, ScriptConsole console) { |
50 | return getAsType(config,key,console,[x|Integer.parseInt(x)],Integer) | 54 | return getAsType(config, key, console, [x|Integer.parseInt(x)], Integer) |
51 | } | 55 | } |
56 | |||
52 | private def getAsBoolean(Map<String, String> config, String key, ScriptConsole console) { | 57 | private def getAsBoolean(Map<String, String> config, String key, ScriptConsole console) { |
53 | return getAsType(config,key,console,[x|Boolean.parseBoolean(x)],Boolean) | 58 | return getAsType(config, key, console, [x|Boolean.parseBoolean(x)], Boolean) |
54 | } | 59 | } |
60 | |||
55 | private def getAsDouble(Map<String, String> config, String key, ScriptConsole console) { | 61 | private def getAsDouble(Map<String, String> config, String key, ScriptConsole console) { |
56 | return getAsType(config,key,console,[x|Double.parseDouble(x)],Double) | 62 | return getAsType(config, key, console, [x|Double.parseDouble(x)], Double) |
57 | } | 63 | } |
58 | 64 | ||
59 | def loadSolverConfig( | 65 | def loadSolverConfig(Solver solver, Map<String, String> config, List<ObjectiveEntry> objectiveEntries, |
60 | Solver solver, | 66 | ScriptConsole console) { |
61 | Map<String, String> config, | 67 | switch (solver) { |
62 | ScriptConsole console) | 68 | case ALLOY_SOLVER: { |
63 | { | 69 | if (!objectiveEntries.empty) { |
64 | if(solver === Solver::ALLOY_SOLVER) { | 70 | throw new IllegalArgumentException("Objectives are not supported by Alloy.") |
65 | return new AlloySolverConfiguration => [c| | 71 | } |
66 | config.getAsInteger("symmetry",console) | 72 | val c = new SmtSolverConfiguration |
67 | .ifPresent[c.symmetry = it] | 73 | config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it] |
68 | config.getAsType("solver",console,[x|AlloyBackendSolver::valueOf(x)],AlloyBackendSolver) | 74 | config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it] |
69 | .ifPresent[c.solver = it] | 75 | c |
70 | ] | 76 | } |
71 | } else if(solver === Solver::SMT_SOLVER) { | 77 | case SMT_SOLVER: { |
72 | return new SmtSolverConfiguration => [c| | 78 | if (!objectiveEntries.empty) { |
73 | config.getAsBoolean("fixRandomSeed",console).ifPresent[c.fixRandomSeed = it] | 79 | throw new IllegalArgumentException("Objectives are not supported by Z3.") |
74 | config.getAsType("path",console,[it],String).ifPresent[c.solverPath = it] | 80 | } |
75 | ] | 81 | val c = new SmtSolverConfiguration |
76 | } else if(solver === Solver::VIATRA_SOLVER) { | 82 | config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it] |
77 | return new ViatraReasonerConfiguration => [c| | 83 | config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it] |
84 | c | ||
85 | } | ||
86 | case VIATRA_SOLVER: { | ||
87 | val c = new ViatraReasonerConfiguration | ||
78 | c.debugConfiguration.partialInterpretatioVisualiser = new GraphvizVisualiser | 88 | c.debugConfiguration.partialInterpretatioVisualiser = new GraphvizVisualiser |
79 | if(config.containsKey("diversity-range")) { | 89 | if (config.containsKey("diversity-range")) { |
80 | val stringValue = config.get("diversity-range") | 90 | val stringValue = config.get("diversity-range") |
81 | try{ | 91 | try { |
82 | val range = Integer.parseInt(stringValue) | 92 | val range = Integer.parseInt(stringValue) |
83 | c.diversityRequirement = new DiversityDescriptor => [ | 93 | c.diversityRequirement = new DiversityDescriptor => [ |
84 | it.ensureDiversity = true | 94 | it.ensureDiversity = true |
85 | it.range = range | 95 | it.range = range |
86 | ] | 96 | ] |
87 | } catch (NumberFormatException e) {console.writeError('''Malformed number format: «e.message»''')} | 97 | } catch (NumberFormatException e) { |
98 | console.writeError('''Malformed number format: «e.message»''') | ||
99 | } | ||
88 | } | 100 | } |
89 | ] | 101 | for (objectiveEntry : objectiveEntries) { |
90 | } else { | 102 | val costObjectiveConfig = new CostObjectiveConfiguration |
91 | throw new UnsupportedOperationException('''Unknown solver: «solver»''') | 103 | switch (objectiveEntry) { |
104 | OptimizationEntry: { | ||
105 | costObjectiveConfig.findExtremum = true | ||
106 | costObjectiveConfig.kind = switch (direction : objectiveEntry.direction) { | ||
107 | case MAXIMIZE: | ||
108 | ObjectiveKind.HIGHER_IS_BETTER | ||
109 | case MINIMIZE: | ||
110 | ObjectiveKind.LOWER_IS_BETTER | ||
111 | default: | ||
112 | throw new IllegalArgumentException("Unknown direction: " + direction) | ||
113 | } | ||
114 | costObjectiveConfig.threshold = ObjectiveThreshold.NO_THRESHOLD | ||
115 | } | ||
116 | ThresholdEntry: { | ||
117 | costObjectiveConfig.findExtremum = false | ||
118 | val threshold = objectiveEntry.threshold.doubleValue | ||
119 | switch (operator : objectiveEntry.operator) { | ||
120 | case LESS: { | ||
121 | costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER | ||
122 | costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) | ||
123 | } | ||
124 | case GREATER: { | ||
125 | costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER | ||
126 | costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) | ||
127 | } | ||
128 | case LESS_EQUALS: { | ||
129 | costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER | ||
130 | costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) | ||
131 | } | ||
132 | case GREATER_EQUALS: { | ||
133 | costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER | ||
134 | costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) | ||
135 | } | ||
136 | default: | ||
137 | throw new IllegalArgumentException("Unknown operator: " + operator) | ||
138 | } | ||
139 | } | ||
140 | } | ||
141 | val function = objectiveEntry.function | ||
142 | if (function instanceof CostObjectiveFunction) { | ||
143 | for (costEntry : function.entries) { | ||
144 | val element = new CostObjectiveElementConfiguration | ||
145 | val pattern = costEntry.patternElement.pattern | ||
146 | val packageName = costEntry.patternElement.package?.packageName ?: | ||
147 | EcoreUtil2.getContainerOfType(pattern, PatternModel)?.packageName | ||
148 | element.patternQualifiedName = if (packageName.nullOrEmpty) { | ||
149 | pattern.name | ||
150 | } else { | ||
151 | packageName + "." + pattern.name | ||
152 | } | ||
153 | costObjectiveConfig.elements += element | ||
154 | } | ||
155 | } else { | ||
156 | throw new IllegalArgumentException("Only cost objectives are supported by VIATRA.") | ||
157 | } | ||
158 | c.costObjectives += costObjectiveConfig | ||
159 | } | ||
160 | c | ||
161 | } | ||
162 | default: | ||
163 | throw new UnsupportedOperationException('''Unknown solver: «solver»''') | ||
92 | } | 164 | } |
93 | } | 165 | } |
94 | 166 | ||
95 | def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { | 167 | def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex, |
96 | parameters.getAsBoolean("randomize",console).ifPresent[ | 168 | ScriptConsole console) { |
97 | if(it) { | 169 | parameters.getAsBoolean("randomize", console).ifPresent [ |
98 | config.randomise = runIndex-1 | 170 | if (it) { |
171 | config.randomise = runIndex - 1 | ||
99 | } | 172 | } |
100 | ] | 173 | ] |
101 | } | 174 | } |
102 | def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { | 175 | |
103 | 176 | def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex, | |
177 | ScriptConsole console) { | ||
104 | } | 178 | } |
105 | } \ No newline at end of file | 179 | } |