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;