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
  • #99
Closed
Open
Issue created May 25, 2021 by Ferdie Reijnen@freijnenDeveloper

No location pointers for automata with single location.

Original issue text:

Currently, when introducing location pointers, we don't have a special case for automata with a single location. For such automata however, the introduced location pointer variable can only ever have one value, and is thus superfluous.

We should not introduce a location pointer for such automata, during linearization, and for the CIF to CIF transformation to eliminate location references. Both share the same code.

Obviously, if the location pointer is not introduced, we can't create 'lp = loc' kind of predicates, and we have to ensure we don't create them. In such cases, 'true' could be a substitute. If we combine this with other predicates, we get non-optimal predicates, but for the current uses, this is already the case.

Notice that we have special case dummy updates that use location pointers.

Related to this, are dummy updates, which are added to ensure that the correct updates are taken. For instance, the following specification:

automaton p:
  event e;
  disc int x = 0;
  location:
    edge e when x >= 3;
    edge e when x < 3 do x := x + 1;
end

is transformed to the following specification:

enum E = X;

automaton M:
  alphabet p_e;
  event p_e;

  disc int p_x = 0;
  disc E p in any;

  initial p = X and false;
  marked p = X and false;

  location L:
    initial;
    marked;

    edge p_e when p = X and (p_x >= 3 or p_x < 3)
             do if   p = X and p_x >= 3: p := X
                elif p = X and p_x < 3:  p_x := p_x + 1
                end;
end

In the case there is no location pointer, the dummy update should be p_x := p_x, instead of p := X

Edited May 25, 2021 by Ferdie Reijnen
Assignee
Assign to
Time tracking

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