Simplify values

> > >

This CIF to CIF transformation simplifies CIF specifications, by applying the following value-related simplifications:

Evaluation of constant (sub-)expressions. For instance, 1 + 1 is simplified to 2.
Simplification of short-circuit boolean binary operators. For instance, true and x is simplified to x.
Simplification of boolean unary operators. For instance, not not x is simplified to x.
Removal of default values. For instance, true state invariants are removed.

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):

Eliminate component definition/instantiation

Implementation details

The following is a complete list of the short-circuit boolean binary operators that are simplified (with x an arbitrary boolean expression):

Original Simplified

Original	Simplified
`true and x`	`x`
`x and true`	`x`
`false and x`	`false`
`x and false`	`false`
`true or x`	`true`
`x or true`	`true`
`false or x`	`x`
`x or false`	`x`
`true => x`	`x`
`x => true`	`true`
`false => x`	`true`
`x => false`	`not x`
`true <=> x`	`x`
`x <=> true`	`x`
`false <=> x`	`not x`
`x <=> false`	`not x`

true and x

x

x and true

x

false and x

false

x and false

false

true or x

true

x or true

true

false or x

x

x or false

x

true => x

x

x => true

true

false => x

true

x => false

not x

true <=> x

x

x <=> true

x

false <=> x

not x

x <=> false

not x

The following is a complete list of the boolean unary operators that are simplified (with x and y two arbitrary expressions):

Original Simplified

Original	Simplified
`not not x`	`x`
`not(x < y)`	`x >= y`
`not(x <= y)`	`x > y`
`not(x = y)`	`x != y`
`not(x != y)`	`x = y`
`not(x > y)`	`x ⇐ y`
`not(x >= y)`	`x < y`
`not(x => y)`	`x and not y`

not not x

x

not(x < y)

x >= y

not(x <= y)

x > y

not(x = y)

x != y

not(x != y)

x = y

not(x > y)

x ⇐ y

not(x >= y)

x < y

not(x => y)

x and not y

Default values are removed in the following places:

Initialization predicates of components (including automata) and locations.
Marker predicates of components (including automata) and locations.
Invariants of components (including automata) and locations.
Guards of edges.
Guards of 'if' and 'elif' updates on edges.
Guards of 'if' and 'elif' expressions.

Predicates that are trivially equal to the default value are removed. If a trivial value is found that is equal to the negation of the default value, the entire feature gets the non-default value. For instance, for guards on edges, true, 1 = 1, etc, are removed as they are all trivially true (the default for guards). If however, false, 1 = 2, 1 != 1, or any other trivially false guards is found, all guards on that edge are removed, and a single false guard is added.

Renaming

n/a

Size considerations

This transformation tries to simplify the specification, possibly reducing its size.

All uses of constants lead to constant (sub-)expressions, and they are evaluated. This leads to constants being inlined. For constants with large literal values, this may significantly increase the size of the specification, especially if the constant is used more than once. For information on how to prevent this, see the Simplify values (no references) CIF to CIF transformation.

Optimality

Not all simplifications that could potentially be performed are implemented in this transformation.

Annotations

This transformation does not process, add, or remove any annotations. The values of annotation arguments may be simplified.