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
  • #404
Closed
Open
Issue created Aug 17, 2022 by Ferdie Reijnen@freijnenDeveloper

Event-based synthesis analysis tool has wrong conclusion

Consider plant G and requirement H, as shown below. The synchronous product has 10 states. The synthesized supervisor has 6 states (also shown below).

Yet, the synthesis analysis tool shows the following message:

Synthesis analysis tool
1 plant automaton.
1 requirement automaton.
Synthesis created 10 states, removed 2 states, giving 8 states in the result.

It incorrectly states that 2 states were removed and 8 states remain. In reality, 4 states were removed, and 6 remained.

plant G:
    location G0: initial;
        edge a1 goto G1;
        edge a2 goto G3;

    location G1:
        edge b1 goto G2;
        edge a2 goto G4;

    location G2:
        edge a2 goto G5;

    location G3:
        edge a1 goto G4;
        edge b2 goto G6;

    location G4:
        edge b1 goto G5;
        edge b2 goto G7;

    location G5:
        edge b2 goto G8;

    location G6:
        edge a1 goto G7;

    location G7:
        edge b1 goto G8;

    location G8: marked;

end
requirement H:
    location H0: initial;
        edge a1 goto H1;
        edge a2 goto H3;

    location H1:
        edge b1 goto H2;
        edge a2 goto H9;

    location H2:
        edge a2 goto H5;

    location H3:
        edge a1 goto H4;
        edge b2 goto H6;

    location H4:
        edge b2 goto H7;

    location H9:
        edge b1 goto H5;

    location H5:
        edge b2 goto H8;

    location H6:
        edge a1 goto H7;

    location H7:
        edge b1 goto H8;

    location H8: marked;

end
controllable a1;
uncontrollable a2;
controllable b1;
uncontrollable b2;
supervisor automaton S:
  alphabet a1, a2, b1, b2;
  location s1:
    initial;
    edge a2 goto s2;
  location s2:
    edge b2 goto s3;
    edge a1 goto s4;
  location s3:
    edge a1 goto s5;
  location s4:
    edge b2 goto s5;
  location s5:
    edge b1 goto s6;
  location s6:
    marked;
end
Edited Aug 17, 2022 by Ferdie Reijnen
Assignee
Assign to
Time tracking

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