Commit | Line | Data |
---|---|---|
34e49164 C |
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 | g(1); | |
16 | } else { | |
17 | g(1); | |
18 | } | |
19 | ||
20 | // g(1); // if add this then the CTL even with the direct path will this time | |
21 | // accept, but we cheat. | |
22 | } |