Basic reductions
Universal reductions (both for CFA declaration and instance)
RemoveLocationsWithNoIncomingTransition
Removes the locations with no incoming transition.
Pattern to match
- location loc
- no incoming transition
- not frozen, nor initial or end location
- has no frozen outgoing transition
Modification
- all outgoing transitions of loc are deleted
- location loc is deleted
OverlapVarAssignments
CFA instance and CFA declaration (latter with name OverlapAssignments
) reduction.
This reduction tries to merge consecutive transitions by moving the variable assignments of the second transition to the first one.
Pattern to match
- assignment transition tA
- may have a guard (c)
- source=loc1, target=loc2
- has variable assignments VA1:=EA1; VA2:=EA2; ...
- not frozen
- assignment transition tB
- no guard (TRUE literal)
- source=loc2, target=loc3
- has variable assignments VB1:=EB1; VB2:=EB2; ...
- not frozen
- location loc2
- 1 incoming transition (t1)
- 1 outgoing transition (t2)
- not frozen, not initial location, not end location
- no conflict between the variable assignments, i.e.,
- (the variables assigned in tA are not read in tB)
- (the variables assigned in tB are not read in tA)
- (the variables assigned in tA are not assigned in tB)
- Note: , , , .
Modification
- all assignments of tB (VB1:=EB1; VB2:=EB2; ...) are moved to tA
- target of transition tA is modified to loc3 (instead of loc2)
- location loc2 is deleted
- transition tB deleted
Result
RemoveEmptyTransitions
Merges the two ends of the transitions where the guard is a constant true literal and there is no variable assignment.
Pattern to match
- assignment transition t
- guard: 'TRUE'
- not frozen
- source: loc1, target: loc2
- has no assignments
- location loc1
- not frozen, not initial location, not end location
- 1 outgoing transition (t)
- location loc2
- not frozen, not initial location, not end location
- 1 incoming transition (t)
Modification
- transition t is deleted
- all outgoing transitions of loc2 are moved to loc1
- location loc2 is deleted
- The CFD reduction will move the annotations of loc2 to loc1. The CFI reduction assumes that there are no annotations.
Result
CFA instance reductions
ConditionPushDown
It aims to push guard conditions deeper, essentially merging nested conditional branches and to reduce the number of locations.
Pattern to match
- assignment transition t
- has no variable assignment
- has guard (c)
- source=loc1, target=loc2
- not frozen
- location loc1
- has 0..* (any) incoming transition
- has 1..* (at least one) outgoing transition (including t)
- not frozen
- location loc2
- exactly 1 incoming transition (t)
- 2.. outgoing assignment* transitions (with guards c1, c2, ...)
- not frozen
Modification
- all outgoing transitions of loc2 will be extended with "c AND" and their source changed do loc1
- location loc2 deleted
- transition t deleted
Result
RemoveEmptyConditionalBranch
Removes unnecessary parallel empty transitions.
Pattern to match
location loc1
- has exactly 2 outgoing transitions (t1, t2) and they both lead to the same location (loc2)
assignment transition t1
- has a guard c1
- does not have any variable assignments
- may be frozen
assignment transition t2
- has a guard c2 which equals to NOT c1
- does not have any variable assignments
- not frozen
Modification
- t1's guard changed to 'TRUE'
- t2 deleted Note that if t1 is frozen, t2 will still be merged into t1 by modifying its guard.
Result
RemoveFalseTransitions
CFI reduction. Removes the transitions where the guard is a constant false literal.
Pattern to match
- assignment transition t
- guard is 'FALSE'
- not frozen
Modification
- transition t is deleted
RemoveIdentityAssignments
Removes the variable assignments where the left and right values equal.
Pattern to match
- assignment amt
- not frozen
- its left and right value equal (α := α)
Modification
- variable assignment amt is deleted
Result
RemoveUnreadAssignments
Removes the variable assignments which are not read. I.e., if between the assignment v1 := <Expr1>;
and v1 := <Expr2>;
there is no reference to variable v1
, then the first assignment.
The reduction will keep track of assignments of variables while traversing the CFA. If another assignment is found for a variable in a way that:
- There was no convergence or divergence in the CFA (each location inbetween had exactly 1 incoming and 1 outgoing transition),
- There was no call transition since the last assignment,
- There was no reference to the variable since the last assignment,
- The last assignment is not frozen,
then the previous assignment will be removed.
RemoveUnreadVariables
Reduction that removes the unread variables of the given CFA. A variable will be removed if it is never read (and not frozen), independently from how many times it is assigned (zero, one or several times). If the variable is assigned and none of its assignments are frozen, the assignments are also removed. If any of the assignments of the variable is frozen, the variable will not be removed.
It is assumed that the variables in the requirement are frozen, thus they cannot be removed.
SimplifyTrivialConditionalBranches/1
It translates the trivial conditional branches assigning Boolean variables into (more complex) variable assignments by including the guard directly in the assignment.
Pattern to match
location loc1
- has two outgoing transitions (tA, tB), both assignment transitions
- not frozen, not initial location, not end location
assignment transition tA
- has a guard c1
- assigns the expression α to variable boolVar (which has a type
BoolType
)- this assignment is not frozen
- may have additional variable assignments (VA1)
assignment transition tB
- has a guard c2 which equals to NOT c1
- assigns the expression β to variable boolVar (which has a type
BoolType
)- this assignment is not frozen
- may have additional variable assignments (VA2)
- The boolVar variable cannot be used in c1 or c2. (In this case the extraction of the assignment would alter the satisfaction of the guard c1 and/or c2.)
Modification
- creates a new location loc0
- creates a new assignment transition t0 from loc0 to loc1
- creates a new assignment boolVar := (c1 AND α) OR (NOT c1 AND β) attached to t0
- removes the assignments of boolVar from tA and tB
Result
SimplifyTrivialConditionalBranches/2
It translates the trivial conditional branches assigning Boolean variables into (more complex) variable assignments by including the guard directly in the assignment.
Pattern to match
location loc1
- has two outgoing transitions (tA, tB), both assignment transitions
- not frozen, not initial location, not end location
assignment transition tA
- has a guard c1
- assigns the expression α to variable boolVar (which has a type
BoolType
)- this assignment is not frozen
- may have additional variable assignments (VA1)
assignment transition tB
- has a guard c2 which equals to NOT c1
- DOES NOT assign the variable boolVar
- may have variable assignments (VA2)
Modification
- creates a new location loc0
- creates a new assignment transition t0 from loc0 to loc1
- creates a new assignment boolVar := (c1 AND α) OR (NOT c1 AND boolVar) attached to t0
- removes the assignment of boolVar from tA
Result
ExpressionSimplification
Simplifies logic and arithmetic expressions.
- Negation expressions (
UnaryLogicExpression
with operator=NEG
):- !(FALSE) --> TRUE
- !(TRUE) --> FALSE
- AND expressions (
BinaryLogicExpression
with operator=AND
):- TRUE AND right --> right
- left AND TRUE --> left
- left AND FALSE --> FALSE
- FALSE AND right --> FALSE
- left AND left --> left
- left AND (NOT left) --> FALSE
- (NOT right) AND right --> FALSE
- (a OR b) AND (a OR c) --> a AND (b OR c) (in all 4 combinations)
- (a AND b) AND (a AND c) --> (a AND b) ANDc (in all 4 combinations)
- OR expressions (
BinaryLogicExpression
with operator=OR
):- FALSE OR right --> right
- left OR FALSE --> left
- left OR TRUE --> TRUE
- TRUE OR right --> TRUE
- left OR left --> left
- left OR (NOT left) --> TRUE
- (NOT right) OR right --> TRUE
- (a OR b) OR (a OR c) --> (a OR b) OR c (in all 4 combinations)
- IMPLIES expressions (
BinaryLogicExpression
with operator=IMPLIES
):- FALSE IMPLIES right --> TRUE
- TRUE IMPLIES right --> right
- equality expressions (
ComparisonExpression
with operator=EQUALS
):- alpha == alpha --> TRUE
- alpha == TRUE --> alpha
- non-equality expressions (
ComparisonExpression
with operator=NOT_EQUALS
):- alpha != alpha --> FALSE
- binary arithmetic expressions and comparisons: replaces computable subtrees with the computed literals (e.g.
120 / 5
-->24
;TRUE == FALSE
-->FALSE
,2 > 1
-->TRUE
).
ExpressionPropagation
Replaces the references to variables in guards and variable assignment right values to the definition of the referred variable, if possible.
E.g. the sequence v1 := TRUE; v2 := v1;
can be simplified to v1 := TRUE; v2 := TRUE;
.
If it is instantiated with constantPropagationOnly
=true, only constants (literals) can be substituted. If constantPropagationOnly
=false, expressions can also be propagated, i.e., v1 := a OR b; v2 := v1;
can be reduced to v1 := a OR b; v2 := a OR b;
.
The reduction infers for each transition the values of variables at the end of the transition based on the guards and variable assignments. For example, based on a transition with guard [a = TRUE AND b = FALSE]
and assignment c := a AND d
it can be inferred that a = TRUE; b = FALSE; c = TRUE and d
. This information (held by a propagation table) is propagated throughout the whole CFA and updated at each transition accordingly. In case of forks (i.e., a location has multiple outgoing transitions), the same propagation table is propagated to all outgoing transitions. In case of merges (i.e., a location has multiple incoming transitions), the propagation tables computed for each incoming transitions are combined (intersected), i.e., their conflicting values are removed. For instance, the combination of a=1; b=2; c=3
and a=2; c=3
is c=3
. In case it is not possible to calculate the propagation tables for each incoming transition (e.g., in case there is a loop in the CFA), the propagation is continued with an empty propagation table from that location.
Whenever an expression is recorded in the propagation table, it is simplified using the ExpressionSimplification.trySimplifySubtree()
method. When the expression propagation replaces a variable with a propagated value, the whole expression subtree where the replacement happened will be simplified using the ExpressionSimplification.trySimplifySubtree()
method.
Currently, the following information is used for the expression propagation reduction:
- Variable assignments, if they are deterministic
- Guards, if they are in one of the following forms:
[<variable> = <expr>]
,[<expr> = <variable>]
,[<boolean_variable>]
,[NOT <boolean_variable>]
, or the AND connection of any of these.
The expression propagation shall never create conflicts. For instance, if the propagation table contains [a = c]
and a transition has the variable assignments b := a
and c := d
, the a
shall not be replaced by c
, as it would cause conflicting variable assignments: b := c; c := d;
which is forbidden.
Example.
Take the following SCL code as example. (Assume that b1
, b2
, b3
are BOOL variables, i1
, i2
, i3
are INT variables.)
b1 := TRUE;
b2 := b1 AND I0.0;
b3 := b1 AND b2;
i1 := 5;
i2 := i2 * 3;
i3 := i1 + i2;
If it is translated into CFA and then expression propagation is used with constantPropagationOnly
=true, the result will be equivalent to having the following code translated into CFA:
b1 := TRUE;
b2 := TRUE; // simplified from 'TRUE AND I0.0'
b3 := TRUE; // simplified from 'TRUE AND TRUE'
i1 := 5;
i2 := 15; // simplified from '5 * 3'
i3 := 20; // simplified from '5 + 15'
Notice that even if only the propagation of constants (literals) was permitted, due to the automated expression simplification it was able to propagate values for variables whose definition originally contained non-literals (e.g., b2 := b1 AND I0.0;
was possible to be propagated even though I0.0
is not a literal).
Example: propagation of guard values. Not only variable assignments can be the source of information for expression propagation. Take the following SCL code as example:
IF I0.0 = TRUE AND I0.1 = FALSE THEN
b1 := I0.0;
b2 := I0.1;
END_IF;
b3 := b1;
If it is translated into CFA and then expression propagation is used, the result will be equivalent to having the following code translated into CFA:
IF I0.0 = TRUE AND I0.1 = FALSE THEN
b1 := TRUE;
b2 := FALSE;
END_IF;
b3 := b1;
Example: propagation over conditional locations. Expressions can be propagated over forks and merges too.
Take the following SCL code as example:
a := 1;
IF b > 2 THEN
c := b;
ELSE
d := b - 1;
END_IF;
e := a;
If it is translated into CFA and then expression propagation is used, the result will be equivalent to having e := 1;
in the last line of the example code.
CoiReduction
The cone of influence (COI) reduction explores the dependencies between variables, then removes the variables which the requirement does not depend on. For this, two kinds of dependencies are defined.
- There is an assignment dependency between the variables
a
andb
ifa
has an assignment which refers to the value ofb
(e.g.,a := 2 * b;
). In this casea
is a dependent variable which depends onb
. - There is a control dependency between the variables
a
andb
ifa
has an assignment which is conditional, depending on the value ofb
. For example, if there is an assignmenta := c + d;
on a transition which includesb
in its guard. Note that a variablev
can have control dependency on variables which are not present in the guard of the transition assigningv
. To determine the control dependencies an over-approximating heuristic is used. For this first the unconditional locations are identified. A location is unconditional if every path from the initial location will go through the given location. The control dependencies for a given assignment of a variable are determined based on the guards between the nearest unconditional location before the place of assignment and the transition of assignment.
The main steps of the algorithm are the following:
- First, the reduction will find all frozen variables. The variables present in frozen assignments will be made frozen too.
- Then, it will collect the variable dependencies using
VariableDependencies.collect()
. For diagnostic purposes, the variable dependency graph created this way can be visualized usingPrintVarDepGraph.print()
. - Next, it will collect the needed variables. A variable is needed if it is frozen, or if there is an already needed variable which depends on it (either through an assignment or a control dependency). Here, a fixed point is computed.
- The unnecessary variables are removed:
- The assignments assigning unnecessary variables are removed.
- Guards containing unnecessary variables are replaced with
[TRUE]
. - The last step may have lead to parallel transitions having
[TRUE]
guards and no assignments. They will be removed. - If there are any more uses of the unnecessary variables (which is unexpected), they are removed and logged (with Warning severity).
- Finally, the unnecessary variables are removed.
Example. Take the following SCL code as example:
FUNCTION coi_func1 : INT
VAR
b, c, d : INT;
x, y, z : INT;
END_VAR
IF x > 0 THEN
y := z;
END_IF;
IF b > 0 THEN
d := c;
END_IF;
//#ASSERT d > 0
END_FUNCTION
If it is translated into CFA and then expression propagation is used, the result will be equivalent to having the following code translated into CFA:
FUNCTION coi_func1 : INT
VAR
b, c, d : INT;
END_VAR
// 'x', 'y' and 'z' are not needed
IF b > 0 THEN
// 'b' is needed because it is a control dependency of 'd'
// 'c' is needed because it is an assignment dependency of 'd'
d := c;
END_IF;
//#ASSERT d > 0
// 'd' is needed because of the requirement
END_FUNCTION