Simulink Design Verifier Dead Logic

Question

0 votes

I have recently used simulink design verifier to check my state machine model. And some dead logics are detected. But in fact this dead logic is resulted from the execution order. Here is an example: State A is active when transition 1 [a>20] is true, State B is active when transition 2 [a<=20] is active. And the execution order is that first the transition 1 will be checked and then transition 2. My Simulink Design Verifier told me that transition 2 can not be false. The reason behind is that every time when a>20 the transition 1 will be firstly checked and fulfilled. The system goes directly in state A. So the transition 2 will not be checked.

Now the model should be optimized to avoid this error detection with Design Verifier. Has anybody ideas?