module APPLI (DATA, CHANNELS) is

process Application [TDreq: Dreq] (n: Nat, id: Nat, s: Scenario) is
   var dest: Nat, h: HEADER, d: DATA, r: Nat in
      case s in
         scenario_1 ->
            only if id == 0 then
               -- send a request for transaction with a *different* node
               dest := any Nat where (dest <= n) and (dest <> id);
               h := any HEADER;
               d := any DATA;
               TDreq (id, dest, h, d);
               stop
            end if
      |  scenario_2 ->
            -- send a request for transaction with a *different* node
            dest := any Nat where (dest <= n) and (dest <> id);
            h := any HEADER;
            d := any DATA;
            TDreq (id, dest, h, d);
            stop
      |  scenario_3_2 | scenario_3_3 | scenario_3_4 ->
            only if id == 0 then
               h := any HEADER;
               d := any DATA;
               for r := requests (s) while r > 0  by r := r - 1 loop
                  TDreq (id, n, h, d)
               end loop;
               stop
            end if
      end case
   end var
end process

end module