Why do I get dead-logic on transitions which can be excited through some test scenarios?

I have this stateflow diagram shown below. When I made error detection analysis on this stateflow chart, there are two transitions which are shown as dead-logic. I know that there are test scenarios that can excite these transitions so I wonder why I get dead-logic errors on these transitions. How should I change my stateflow chart in order to eliminate dead-logic errors? Thanks in advance.

Answer 1

[Pat Canny]

Hi Ilkay,

Great question. We have seen similar cases to this.

Here is what is happening:

In each case, we have (taking for example state x):

A == 1 as the first transition. This generates 2 objectives: A == 1 true and A == 1 false

A ~= 1 is the second transition and has two objectives as well: A ~= 1 true and A ~= 1 false

The A ~= 1 false is not reachable (the objective is "dead"), because it corresponds to exactly the case where A == 1 is true (which means Design Verifier would never check that transition because the first transition is always true).

How to fix: since the second transition corresponds exactly to the case where the first condition is true, you can replace the [A ~= 1] and [B ~= 1] with default transitions (with no label). This does the exact same thing.