% DEFAULT_PROCESS_FILE="sieve.lnt"

"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" = par TEMP in "medium.bcg" || "unit.bcg" end par;

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

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

% 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
         par "$L" in
            "sieve_10_incremental.bcg"
         ||
             (rename L -> "$L", T -> "$T" in "medium_unit.exp")
         end par
      end hide;
% 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";

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

% echo ""
% echo "***"
% echo "*** Checking correctness"
% echo "***"

property SIEVE_CORRECT
    "Each prime number fed as input to the sieve must eventually be delivered"
    "and each non prime number must be filtered by the sieve"
is
    "sieve_10_branching.bcg" |= with evaluator

        macro is_prime (p) =
        (
            <
                loop (n:Nat := 2) : (r:Bool) in
                    if (n * n) > (p) then
                        exit (true)
                    else
                        if ((p) % n) = 0 then
                            exit (false)
                        else
                            continue (n + 1)
                        end if
                    end if
                end loop
            > (r)
        )
        end_macro

        [ true* . { GEN ?p:Nat } ] (
            if is_prime (p) then
                mu X . (< true > true and [ not { OUTPUT !p } ] X)
            else
                [ true* . { OUTPUT !p } ] false
            end if
        );
    expected TRUE
end property

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

-- executing the former demo in LOTOS

% (cd LOTOS ; echo "" ; svl)

-- cleanup

% SVL_COMMAND_FOR_CLEAN "(cd LOTOS ; svl -clean)"

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