% DEFAULT_PROCESS_FILE="sieve.lotos"

"unit.bcg" = strong reduction of generation of UNIT [TEMP, T, OUTPUT];

"medium.bcg" = fifo 1 with 30 labels "L !%d", "TEMP !%d";

"medium_unit.exp" = "medium.bcg" |[TEMP]| "unit.bcg";

"sieve_10.exp" =
   hide all but OUTPUT in
   (
      GENERATOR [T0] (2)
   |[T0]|
      (rename L -> T0, T -> T1 in "medium_unit.exp")
   |[T1]|
      (rename L -> T1, T -> T2 in "medium_unit.exp")
   |[T2]|
      (rename L -> T2, T -> T3 in "medium_unit.exp")
   |[T3]|
      (rename L -> T3, T -> T4 in "medium_unit.exp")
   |[T4]|
      (rename L -> T4, T -> T5 in "medium_unit.exp")
   |[T5]|
      (rename L -> T5, T -> T6 in "medium_unit.exp")
   |[T6]|
      (rename L -> T6, T -> T7 in "medium_unit.exp")
   |[T7]|
      (rename L -> T7, T -> T8 in "medium_unit.exp")
   |[T8]|
      (rename L -> T8, T -> T9 in "medium_unit.exp")
   |[T9]|
      (rename L -> T9, T -> T10 in "medium_unit.exp")
   );

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

% echo ""
% echo "***"
% echo "*** Generating graph with partial order reduction turned off"
% echo "***"

% EXP_OPEN_OPTIONS=
% # GENERATOR_OPTIONS="-monitor"

"sieve_10.bcg" = generation of "sieve_10.exp";

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

% echo ""
% echo "***"
% echo "*** Computing the minimal graph modulo branching bisimulation"
% echo "***"

"sieve_10_branching.bcg" = branching reduction of "sieve_10.bcg";

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

% echo ""
% echo "***"
% echo "*** Generating graph with partial order reduction turned on"
% echo "***"

% EXP_OPEN_OPTIONS="-branching"
% # GENERATOR_OPTIONS="-monitor"

"sieve_10_partial.bcg" = generation of "sieve_10.exp";

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

% echo ""
% echo "***"
% echo "*** Generating graph using incremental reduction"
% echo "***"

% EXP_OPEN_OPTIONS=
% GENERATOR_OPTIONS=

"sieve_10_incremental.bcg" = branching reduction of GENERATOR [T0] (2);

% for N in 0 1 2 3 4 5 6 7 8 9
% do
   % L="T$N"
   % T="T`expr $N + 1`"

   "sieve_10_incremental.bcg" = branching reduction of generation of
      hide "$L", TEMP in
      (
         "sieve_10_incremental.bcg"
      |["$L"]|
         (rename L -> "$L", T -> "$T" in "medium_unit.exp")
      );
% done

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

% echo ""
% echo "***"
% echo "*** Checking equivalence modulo branching bisimulation"
% echo "***"

"diag_sieve1.seq" = branching comparison
   "sieve_10_partial.bcg" == "sieve_10_branching.bcg";

"diag_sieve2.seq" = branching comparison
   "sieve_10_incremental.bcg" == "sieve_10_branching.bcg";

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