tests/test5.res

   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   // g(1);  // if  add this then the CTL even with the direct path will this time
  21   //  accept, but we cheat.
  22 }