Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in
  • E escet
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Graph
    • Compare
    • Locked Files
  • Issues 92
    • Issues 92
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 5
    • Merge requests 5
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Eclipse ProjectsEclipse Projects
  • Eclipse ESCET (Supervisory Control Engineering Toolkit)
  • escet
  • Issues
  • #148
Closed
Open
Issue created Jul 17, 2021 by Ferdie Reijnen@freijnenDeveloper

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 Jul 18, 2021 by Ferdie Reijnen
Assignee
Assign to
Time tracking

Copyright © Eclipse Foundation, Inc. All Rights Reserved.     Privacy Policy | Terms of Use | Copyright Agent