//
// flight rule: tliBurn can only be invoked after lsamRendezvous has been invoked
//
// this is an example of an environment assumption encoded as a forward
// matching automaton, i.e. it is synchronously executed with the state machine
// (by a configured listener) as soon as we encounter the start event
// (lsamRendezvous). In case the next event is not accepted by the automaton,
// the current event is discarded and JPF backtracks


FlightRule11 = (lsamRendezvous -> Q1),
Q1 = (tliBurn -> Q1
     | lsamRendezvous -> Q1).