module SCENARIO_B
   (
      AUTOMATON,
      LOCAL_CONSTANTS,
      REPOSITORY,
      FILES,
      MESSAGES,
      QUEUE,
      MEDIUM,
      TFTP,
      USER
   ) is

-------------------------------------------------------------------------------

process TFTP_A [PUT, GET, RECEIVE, SEND, EVENT : any,
                END_OF_FILE, BAD_MESSAGE, BAD_INDEX, END_OF_LIST : exit]
is
   par PUT, GET in
      USER [PUT, GET, EVENT, END_OF_LIST] (NIL of FILENAME_LIST, CONS (1, NIL))
   ||
      TFTP_PROCESS [GET, PUT, RECEIVE, SEND, EVENT,
                    END_OF_FILE, BAD_MESSAGE, BAD_INDEX] (MAX_RETRIES_A)
   end par
end process

-------------------------------------------------------------------------------

process TFTP_B [PUT, GET, RECEIVE, SEND, EVENT : any,
                END_OF_FILE, BAD_MESSAGE, BAD_INDEX, END_OF_LIST : exit]
is
   par PUT, GET in
      USER [PUT, GET, EVENT, END_OF_LIST] (NIL of FILENAME_LIST, NIL of FILENAME_LIST)
   ||
      TFTP_PROCESS [GET, PUT, RECEIVE, SEND, EVENT,
                    END_OF_FILE, BAD_MESSAGE, BAD_INDEX] (MAX_RETRIES_B)
   end par
end process

-------------------------------------------------------------------------------

process RECEIVER_A [RECEIVE_A : any] is
   loop
      alt
         RECEIVE_A (DATA (1, 'A', false))
      []
         RECEIVE_A (DATA (2, 'B', true))
      []
         RECEIVE_A (ERROR of MESSAGE)
      end alt
   end loop
end process

-------------------------------------------------------------------------------

process RECEIVER_B [RECEIVE_B : any] is
   loop
      alt
         RECEIVE_B (ACK (1))
      []
         RECEIVE_B (ACK (2))
      []
         RECEIVE_B (RRQ (1))
      []
         RECEIVE_B (ERROR of MESSAGE)
      end alt
   end loop
end process

-------------------------------------------------------------------------------

process SENDER_A [SEND_A : any] is
   loop
      alt
         SEND_A (ACK (1))
      []
         SEND_A (ACK (2))
      []
         SEND_A (RRQ (1))
      []
         SEND_A (ERROR of MESSAGE)
      end alt
   end loop
end process

-------------------------------------------------------------------------------

process SENDER_B [SEND_B : any] is
   loop
      alt
         SEND_B (DATA (1, 'A', false))
      []
         SEND_B (DATA (2, 'B', true))
      []
         SEND_B (ERROR of MESSAGE)
      end alt
   end loop
end process

-------------------------------------------------------------------------------

end module