Data-based synthesis should support switch expressions
Consider the following CIF specification:
plant p:
controllable c_on;
location l1:
initial;
edge c_on goto l2;
location l2:
marked;
end
input int[0..2] Z;
requirement p.c_on needs switch Z: case 0: true case 2: true else false end;
Data-based synthesis returns the following error:
ERROR: Data-based supervisory controller synthesis failed due to unsatisfied preconditions:
- Unsupported specification: unsupported part "switch Z: case 0: true case 2: true else false end" of invariant "p.c_on needs switch Z: case 0: true case 2: true else false end": predicate is not supported.
We can support them by simply converting them to if-expressions and then converting that to BDD.
Expression value = switchPred.getValue();
BDD rslt = convertPred(last(cases).getValue(), initial, synthAut);
// For each case:
SwitchCase cse = cases.get(i);
BinaryExpression equalExpr = newBinaryExpression(deepclone(value), BinaryOperator.EQUAL, null, deepclone(cse.getKey()), newBoolType());
BDD caseGuard = convertPred(equalExpr, initial, synthAut);
BDD caseThen = convertPred(cse.getValue(), initial, synthAut);
BDD caseRslt = caseGuard.ite(caseThen, rslt);
rslt = caseRslt;
Edited by Ferdie Reijnen