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

CIF event-based language equivalence check generates incorrect counterexamples

Run "event-based synthesis -> language equivalence" on the cif spec.

The answer is correct but the explanation is not. The languages are not equivalent because the automata differ only on their marked language. Specifically, automaton B has L3 marked, whereas automaton A has not.
Instead, the explanation says "From location "L2" of automaton "A", event "b" can be performed, but from the equivalent location "L2" of automaton "B", the event cannot be performed." (such a transition can be taken from both automata in L2).

event a,b,c;

automaton A:
    location L1: initial; marked;
        edge a goto L2;

    location L2:
        edge b goto L3;

    location L3:
        edge c goto L1;
end

automaton B:
    location L1: initial; marked;
        edge a goto L2;

    location L2:
        edge b goto L3;

    location L3: marked;
        edge c goto L1;
end
Edited Aug 19, 2022 by Ferdie Reijnen
Assignee
Assign to
Time tracking

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