| 1 | /* |
| 2 | * If still have an edge from the startif to endif (AfterNode), |
| 3 | * with a if-then-and-else, then rene will see this edge, |
| 4 | * and that means that the ctl engine will see this direct path from |
| 5 | * startif to endif as a valid execution path. So on this program, |
| 6 | * CTL will reject the formula f(X) ... g(X) because |
| 7 | * when we take the direct path (which should not exist I repeat), |
| 8 | * we can't find a later g(1). |
| 9 | */ |
| 10 | void main() { |
| 11 | |
| 12 | f(1); |
| 13 | |
| 14 | if(1) { |
| 15 | h(1); |
| 16 | } else { |
| 17 | h(1); |
| 18 | } |
| 19 | |
| 20 | |
| 21 | g(1); // if add this then the CTL even with the direct path will this time |
| 22 | // accept, but we cheat. |
| 23 | } |