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
  • #324
Closed
Open
Issue created Feb 24, 2022 by Dennis Hendriks@ddennisMaintainer

Document that CIF explorer does not produce minimal state spaces

Consider the following specification:

event e;

automaton a:
  disc int[0..2] x in any;

  location:
    initial;
    marked;
    edge e;
end

The CIF explorer will produce the following statespace:

event e;

automaton statespace:
  alphabet e;

  location loc1:
    initial;
    marked;
    edge e;

  location loc2:
    initial;
    marked;
    edge e;

  location loc3:
    initial;
    marked;
    edge e;
end

This is not a minimal representation of the state space. For more information on minimal DFAs and DFA minimization, see:

  • https://en.wikipedia.org/wiki/DFA_minimization
  • https://www.eclipse.org/escet/cif/tools/eventbased/dfa-minimize.html

The CIF explorer considers the state of the CIF model, and since variable a.x is part of the CIF model's state, indeed there are 3 states for this CIF model. However, for the state space, these can no longer be distinguished as such. All three states have the exact same behavior, the same language. The minimal result would be:

event e;

automaton statespace:
  alphabet e;

  location loc1:
    initial;
    marked;
    edge e;
end

Note that you can minimize the state space resulting from the CIF explorer using the CIF event-based DFA minimization tool. This does however have several preconditions, such as not having tau events and having exactly one initial location. As such, it does not apply to the example above.

We could potentially automatically minimize the computed state space. However, this could be expensive. So, if we were to go this way, we should make it a configurable option. But, given that the CIF event-based DFA minimization tool has various restrictions, we couldn't apply that in its current form to perform the minimization.

I therefore think we should for now just document the non-minimal result in the CIF explorer documentation.

Assignee
Assign to
Time tracking

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