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 87
    • Issues 87
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 3
    • Merge requests 3
  • 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
  • #144
Closed
Open
Issue created Jul 13, 2021 by Martijn Goorden@mgoorden7u4Reporter

Supervisor simplification with respect to plant guards misses trivial case

Problem

Consider the following MWE in CIF:

plant A:
  controllable c_a;

  location l1:
    initial;marked;
    edge c_a when false;
end

This results in the following synthesized supervisor (using data-based synthesis with default settings).

plant automaton A:
  controllable c_a;
  location l1:
    initial;
    marked;
    edge c_a when false;
end
supervisor automaton sup:
  alphabet A.c_a;
  location:
    initial;
    marked;
    edge A.c_a when false;
end

By default, supervisor guards are simplified with respect to the plant guards. In this case, I expect that the supervisor guard for event A.c_a would be true, as in the plant the guard is already stricter, i.e., the supervisor does not impose any additional restriction than the plant does.

I know the documentation states that

The simplification algorithm is not perfect, and may not simplify the predicates as much as could potentially be possible.

But this seems to be a trivial case (as it involves only Boolean constants) that should be detected by the algorithm.

Context

Inspecting the synthesized supervisor is a means to validated the input model supplied to data-based synthesis. Especially the case when false appears in the synthesized supervisor might indicate that something is modeled incorrectly. Answering the question why some behavior is absent in the synthesized supervisor is often tedious manual work.

The situation above appears in a model of mine where I use a plant definition with a Boolean parameter than enable (or disable) a particular event, such that the same definition can be use for very similar components in the system.

plant def A_def(alg bool enabled):
  controllable c_a, c_b, c_c;

  location l1:
    initial;marked;
    edge c_a goto l2;

  location l2:
    edge c_b goto l1;
    edge c_c when enabled goto l1;
end

Observe that when enabled = true, there are two options to go from l2 to l1. In defining the complete model, sometimes this definition is instantiated with enabled = true and sometimes with enabled = false. This way of modeling results in plant models having transtitions with the Boolean constant false as their guard.

Assignee
Assign to
Time tracking

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