Eliminate state/event exclusion invariants

This CIF to CIF transformation eliminates state/event exclusion invariants. It replaces them with automata with self loops.

Supported specifications

This transformation supports a subset of CIF specifications. The following restrictions apply:

  • Component definitions and component instantiations are not supported.

Preprocessing

No preprocessing is currently performed by this CIF to CIF transformation. To increase the subset of specifications that can be transformed, apply the following CIF to CIF transformations (in the given order):

Implementation details

All state/event exclusion invariants are removed from the specification.

They are replaced with automata with self loops. Per component, the state/event exclusion invariants of the component (the top level scope of the specification, groups, automata), as well as those of its locations (only for automata), are partitioned per supervisory kind. Per such partition, an automaton is created.

State/event exclusion invariants with names lose their name, as self loops cannot be named.

The automaton is put along side the component (for groups and automata), as sibling. For invariants in the top level scope of the specification, the new automaton is put in the top level scope of the specification. The new automaton gets the same name as the component that contained the invariants as prefix, with some postfixes. For invariants at the top level scope of the specification, an empty prefix is used. The first postfix is indicates the supervisory kind of the invariants of the partition: Plant, Requirement, Supervisor, or empty for regular/kindless invariants. The second postfix is StateEvtExcls. So, for an automaton Abc with some plant invariants, an automaton AbcPlantStateEvtExcls is created. The name may conflict with existing automata or other declarations, in which case it is renamed.

The automata that are created inherit the supervisory kind of the state/event exclusion invariants in the partition for which the automaton is created. The automata have a single nameless location, that is both initial and marked.

For each state/event exclusion invariant in the partition, and self loop edge is created per event. The condition predicates of the invariants are used as guard, possible after some manipulation.

For state/event exclusion invariants of the locations of automata, the condition predicate is made conditional on the location. However, this is only done for automata with at least two locations, as conditioning on an always active location is of little use. For a location loc, and a state/event exclusion invariant invariant evt needs x = 1, predicate x = 1 is changed to loc => x = 1.

For state/event exclusion invariants that indicate when an event is to be disallowed/disabled, the condition predicate is inverted. The inversion is performed after the condition predicate is made condition on the location, if applicable. For instance, for a state/event exclusion invariant invariant x != 1 disables evt in a location loc, the condition predicate x != 1 is first made conditional on the location. This results in loc => x != 1. The condition predicate is then inverted to not(loc => x != 1), which is then used as guard.

The alphabets of the automata are left implicit.

Consider the following example CIF specification:

plant automaton aut:
  controllable e1, e2, e3;
  disc int[0..10] x;

  requirement invariant e1    needs    x < 10;
  requirement invariant x = 0 disables {e1, e2};

  location:
    initial;

    requirement invariant x = 0 disables e3;

    edge e1 do x := x + 1;
    edge e2 do x := x - 1;
    edge e3 do x := 0;
end

It is transformed to the following CIF specification:

plant automaton aut:
  controllable e1, e2, e3;
  disc int[0..10] x;

  location:
    initial;

    edge e1 do x := x + 1;
    edge e2 do x := x - 1;
    edge e3 do x := 0;
end

requirement automaton autRequirementStateEvtExcls:
  location:
    initial;
    marked;

    edge aut.e1 when aut.x < 10, not(aut.x = 0);
    edge aut.e2 when not(aut.x = 0);
    edge aut.e3 when not(aut.x = 0);
end

Renaming

New automata are created. If the desired name for an automaton is already in use for some other automaton or declaration, the new automaton is given a different name. For instance, if an automaton is to be named ControllerStateEvtExcls and that name is already in use, it will be named ControllerStateEvtExcls2. If that name is also already in use, it will be named ControllerStateEvtExcls3, etc.

Size considerations

The constant amount of additional objects are created (e.g. an automaton, a location, a true initialization predicate, etc). At most one automaton is created per state/event exclusion invariant. As such, the size increase is linear in the number of state/event exclusion invariants.

Optimality

For state/event exclusion invariants that are defined in locations of automata with more than one location, this transformation makes their predicates conditional on those locations. To eliminate such location references, apply the Eliminate the use of locations in expressions CIF to CIF transformation.

This transformation generate boolean implication and inversion predicates. These are not simplified. To simply them, apply the Simplify values CIF to CIF transformation.

Annotations

This transformation does not process, add, or remove any annotations.