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; ```
issue

Copyright © Eclipse Foundation AISBL. All rights reserved.     Privacy Policy | Terms of Use | Copyright Agent