|
|
# ILP Generation in racr-mquat
|
|
|
|
|
|
## Form of the ILP for glpk
|
|
|
|
|
|
- ILP ::= "Minimize" SIMPLE-FORMULA "Subject To" CONSTRAINT+ "Bounds" BOUND* "Generals" VAR* "End"
|
|
|
- SIMPLE-FORMULA ::= \[ NAME ":" \] (("+"|"-") \[ NUMBER \] VAR)+
|
|
|
- CONSTRAINT ::= SIMPLE-FORMULAR ("<="|">="|"=") NUMBER
|
|
|
- BOUND ::= \[ NUMBER "<=" \] VAR \[ ("<="|"=") NUMBER \]
|
|
|
- NUMBER ::= ( "0" | "1" | … | "9" )+
|
|
|
- VAR ::= ( "#" | "/" | "(" | ")" | "~" | NAME )+
|
|
|
- NAME ::= ( "a" | … | "z" | "A" | … | "Z" | "_" | "-" | NUMBER )+
|
|
|
|
|
|
Eventually VAR and NAME is equal. At least the characters listed in VAR were found to be correctly parsed.
|
|
|
|
|
|
## Generation recipe
|
|
|
|
|
|
- `varname` returns a suitable name for the applied fact
|
|
|
- `objective-value` returns the value of the property for the objective function
|
|
|
- Assumption: Names of properties are unique, i.e. if referring both in SW-Comp C1, Resource R2 and Request R to the
|
|
|
property 'energy', then they all refer to the same property
|
|
|
|
|
|
### Objective
|
|
|
|
|
|
```
|
|
|
for-all implementations i
|
|
|
for-all PEs pe
|
|
|
objective += (objective-value i-deployed-on-pe) (varname i-deployed-on-pe) "+"
|
|
|
```
|
|
|
|
|
|
### Architectural Constraints
|
|
|
|
|
|
```
|
|
|
for all components c
|
|
|
constraint_c = "1 = "
|
|
|
for-all (impls-of c) i
|
|
|
for-all PEs pe
|
|
|
constraint += (varname i-deployed-on-pe) "+"
|
|
|
for-all (req-comp i) rc
|
|
|
constraint_rc = "0 = " (varname i-deployed-on-pe)
|
|
|
for-all (impls rc) rci
|
|
|
for-all PEs rcpe
|
|
|
constraint_rc += "-" (varname rci-deployed-on-rcpe)
|
|
|
constraints += constraint_rc
|
|
|
constraints += constraint
|
|
|
constraints += constraint_c
|
|
|
```
|
|
|
|
|
|
Maybe introduce binary variables for "implementation i" chosen, additionally to the
|
|
|
"implementation i deployed on pe" variables. This would greatly reduce the size of architectural constraints.
|
|
|
|
|
|
```
|
|
|
for all components c
|
|
|
constraint_c = "1 = "
|
|
|
for-all (impls-of c) i
|
|
|
constraint_c += (varname i) "+"
|
|
|
constraint_i = "0 = " "-" (varname i)
|
|
|
for-all PEs pe
|
|
|
constraint_i += (varname i-deployed-on-pe) "+"
|
|
|
for-all (req-comp i) rc
|
|
|
constraint_rc = "0 = " (varname i)
|
|
|
for-all (impls-of rc) rci
|
|
|
constraint_rc = (varname rci) "+"
|
|
|
constraints += constraint_rc
|
|
|
constraints += constraint_i
|
|
|
constraints += constraint_c
|
|
|
```
|
|
|
|
|
|
### Resource/Software NFP Negotiation
|
|
|
|
|
|
Nicht so leicht abbildbar, wenn nicht nur nach der 'Direction' der Properties
|
|
|
entschieden wird, sondern auch andere Arten von Constraints zugelassen werden, zB
|
|
|
|
|
|
- "impl1: val1 <= response-time <= val2"
|
|
|
- "impl2: response-time >= val3"
|
|
|
|
|
|
Maximum-Constraint überhaupt abbildbar mit "prop <= value * binVar"?
|
|
|
|
|
|
- bei Nicht-Auswahl der Impl ist die binVar = 0, und das Constraint ist effektiv prop <= 0
|
|
|
und gleichzeitig prop = X von der benötigten Komponente
|
|
|
- mögliche Lösung: Wenn Maximum der Property bekannt: Anstelle der tatsächlichen Werte
|
|
|
wird (Maximum - Wert) benutzt, und statt "<=" nun ">="
|
|
|
- prop hat Maximum 100
|
|
|
- "prop <= 20 * impl1pe2"
|
|
|
- "prop' >= 80 * impl1pe2" where prop' := 100 - prop
|
|
|
|
|
|
```
|
|
|
Init constraints[returntype_min-eq] to returntype ">="
|
|
|
Init constraints[returntype_max-eq] to returntype "<="
|
|
|
Init constraints[returntype-eq] to returntype "="
|
|
|
for-all PEs pe
|
|
|
for-all implementations i
|
|
|
for-all clauses c in i
|
|
|
(if c subtype? ProvClause
|
|
|
constraints[returntype-eq] += c.value (varname i-deployed-on-pe) "+"
|
|
|
(if c.comp eq? min-eq
|
|
|
constraints[returntype_min-eq] += c.value (varname i-deployed-on-pe) "+"
|
|
|
constraints[returntype_max-eq] += c.value (varname i-deployed-on-pe) "+"))
|
|
|
```
|
|
|
|
|
|
### User request
|
|
|
|
|
|
```
|
|
|
for-all request-constraints-clause c
|
|
|
constraints += (varname c.returntype) ("<="|">="|… according to c.comp) c.value
|
|
|
```
|
|
|
|
|
|
### Bounds
|
|
|
|
|
|
```
|
|
|
for-all PEs pe
|
|
|
for-all prov-clauses c in pe
|
|
|
bounds += "0 <=" (varname c.returntype) "<=" c.value
|
|
|
```
|
|
|
|
|
|
### Boolean restriction
|
|
|
|
|
|
```
|
|
|
for-all implementations i
|
|
|
for-all clauses c in i
|
|
|
generals += (varname i-deployed-on-pe)
|
|
|
``` |