osek-verification.cabal

Previously, we had

  while (triggered something) {
     if (decision) trigger_int1;
     if (decision) trigger_int2;
     if (decision) trigger_int3;
  }

which was not thought out perfectly: In the event that the state-hash
changes when we come back from trigger_int1, we effectively begin a
new cycle for a new state at trigger_int2. In this case, not
triggering int2, int3 and finally also not triggering int1 should
complete the cycle and leave the loop but it doesn't because this code
expects int1,int2,int3 to be triggered (or not triggered) in this
exact order.

We now allow the search procedure to trigger interrupts in any order
it likes by repeatedly presenting it with a decision tree that has the
interrupts and "exit the loop" as leaves:

  while (1) {
    if (decision) {
      if (decision) {
        break;
      } else {
        trigger_int1;
      }
    } else {
      if (decision) {
        trigger_int2;
      } else {
      	trigger_int3;
      }
    }
  }