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.

For each named state/event exclusion invariant, a separate automaton is created. For all unnamed state/event exclusion invariants within the top level scope of the specification, a group or an automaton, as well as those in locations of that automaton, the state/event exclusion invariants are partitioned per supervisory kind. Per such partition, an automaton is created.

For invariants in the top level scope of the specification, the new automata are put in the top level scope of the specification. For invariants in a group, the new automata are put inside the group. For invariants in an automaton, the new automata are put alongside the automaton, as siblings.

For each named invariant, its new automaton gets the name of the invariant. If the named invariant is part of an automaton, or part of a location in an automaton, the name of the new automaton gets prefixed with the name of the automaton.

For unnamed invariants in a partition, the new automaton gets a name consisting of a prefix and one or more postfixes. For invariants in a group or automaton, the prefix is the name of the group or automaton. For invariants in the top level scope of the specification, an empty prefix is used. The first postfix indicates the supervisory kind of the invariants of the partition: Plant, Requirement, or Supervisor. For regular/kindless invariants, an empty first postfix is used. The second postfix is StateEvtExcls. So, for an automaton Abc with some plant invariants, an automaton AbcPlantStateEvtExcls is created.

For unnamed invariants, as well as for named invariants in automata, the name of the new automaton may conflict with existing automata or other declarations in the scope where it is placed, in which case it is renamed.

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

For each state/event exclusion invariant for which a new automaton is created, and self loop edge is created per event. The condition predicates of the invariants are used as guard, possibly 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 before the condition predicate is made conditional 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 inverted to not(x != 1). Then it is made conditional on the location. This results in loc => not(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};
  requirement invariant NAME: e1 needs x < 11;

  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 autNAME:
  location:
    initial;
    marked;

    edge aut.e1 when aut.x < 11;
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

If a specification has state/event exclusion invariants for events that are not in the synchronization, send or receive alphabet of the specification, then these invariants are removed, and no automaton is created for them. This prevents the events from becoming part of the synchronization alphabet of the specification, which would mean transitions could then become possible for these events, while that was not the case before the transformation. We thus prevent the state space of the specification from changing due to such cases. If any such invariants are encountered, the transformation prints a warning.

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

A 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 any specific annotations. The annotations of unnamed state/event exclusion invariants are removed. The annotations of named state/event exclusion invariants are moved to the corresponding newly created automata. The elements of the newly created automata do not have any annotations.