User guide

20-10
Using OpenVera Assertions
Whenever "a" is false, event "e1" will match because the "if - then"
implication is satisfied. This means that "e2" will also trigger and try
to match on "c" at the next clock tick. This may not be, however, what
is intended. A modification to consider is to change event "e1" as
follows:
event e1: a #1 b;
GR3: WARNING "if" appears in the middle of a longer
sequence, or a composition of sequences where both
contain an "if" without an "else"
Example:
event ev: if a then #1 (if b then #1 c);
If "a" is true, then in the next cycle event e will match even if "b" is
false. This may not be the intended behavior.
Consider changing the event as follows:
event ev: if a then (#1 b #1 c);
Note 1: The portion of the original event "ev" in parentheses could
have been an event declared separately and instantiated in
"e", thus possibly hiding the fact that it contains an "if".
Note 2: The following use of if-then-else can be useful, however:
event ev: if a then #1 if b then d else e;
Here a, b, c, d and e are some boolean expressions.
GR6: WARNING OVA * repetition factor contains a 0.
Example:
a*[m..n] #k b;
Here m is a 0 or a parameter with default value of 0