(* all processes are defined in file "odp.lotos" *)

% DEFAULT_PROCESS_FILE="odp.lotos"

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

(*
 * generation of the state space of the whole system
 *
 * the state space of the trader is generated using an interface that
 * takes into account the environment constraints imposed on the trader by
 * three of the four objects
 *)

"odp.bcg" = generation of leaf strong reduction of
   hide all but WORK in
      par EXPORT, IMPORT in
         (refined abstraction Object_1, Object_2, Object_3
	    using "Trader_Alphabet" of "Trader")
      ||
         par WORK #2 in 
            Object_1
         || Object_2
         || Object_3
         || Object_4
         end par
      end par;

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