ILP-Generation.md

+# 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)
+```