process Application [TDreq] (n: Nat, id: Nat, s: Scenario) : noexit :=
   [s eq scenario_1] ->
      [id eq 0] ->
         (
         (* send a request for transaction with a *different* node *)
         choice dest: Nat, h: HEADER, d: DATA []
            [(dest le n) and (dest ne id)] ->
               TDreq !id !dest !h !d;
               stop
         )
   []
   [s eq scenario_2] ->
      (
      (* send a request for transaction with a *different* node *)
      choice dest: Nat, h: HEADER, d: DATA []
         [(dest le n) and (dest ne id)] ->
            TDreq !id !dest !h !d;
            stop
      )
   []
   [(s eq scenario_3_2) or (s eq scenario_3_3) or (s eq scenario_3_4)] ->
      [id eq 0] ->
         (
         (* 2, 3 or 4 requests in sequence *)
         choice h: HEADER, d: DATA []
            TDreq !id !n !h !d;
            TDreq !id !n !h !d;
            (
            [s eq scenario_3_2] ->
               stop
            []
            [s eq scenario_3_3] ->
               TDreq !id !n !h !d;
               stop
            []
            [s eq scenario_3_4] ->
               TDreq !id !n !h !d;
               TDreq !id !n !h !d;
               stop
            )
        )
endproc