Eliminate algebraic variables

This CIF to CIF transformation eliminates algebraic variables and their equations.

See also: Eliminate equations.

Supported specifications

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

  • Component definitions and component instantiations are not supported.

  • Automaton self references 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

For each algebraic variable with a single equation in a component or automaton, all uses of the variable (for instance in guards, invariants, etc) are replaced by the value of the variable (the right hand side of its equation). For algebraic variables with equations specified in the locations of an automaton, an 'if' expression is created. This 'if' expression uses the locations of the automaton as guards, and the right hand sides of the equations as values for each of the alternatives. The last alternative is an 'else', and thus has no guard. If the automaton has only one location, generation of the 'if' expression is suppressed.

The algebraic variables and their equations are removed.

For instance, the following specification:

alg bool b1 = true;
alg bool b2;
equation b2 = false;

automaton aut:
  alg int a;
  location l1:
    equation a = 1;
  location l2:
    equation a = 2;
end

invariant b1 or b2 or p.a > 0;

is transformed to the following specification:

automaton aut:
  location l1;
  location l2;
end

invariant true or false or if p.l1: 1 else 2 end > 0;

Renaming

n/a

Size considerations

Since algebraic variables are shortcuts for expressions, eliminating them could result in an increase of the size of the specification. Algebraic variables may be defined in terms of other algebraic variables. Therefore, in the worst case, the increase is exponential.

Optimality

For an assignment x := 1 + y, where y is an algebraic variable that is eliminated, and where y has value 5, the resulting assignment is x := 1 + 5. The result is not simplified any further. To further simplify the result, apply additional CIF to CIF transformations, such as Simplify values.

This transformation introduces 'if' expressions for algebraic variables that have an equation per location, for automata with at least two locations. The guards of such 'if' expressions refer to the locations of the automata. To eliminate such location references, apply the Eliminate the use of locations in expressions CIF to CIF transformation.

Annotations

This transformation does not process or add any annotations. As this transformation removes all algebraic variables from the specification, their annotations are removed as well.