% INITIALIZE() {
-- argument 1: name of the experiment

% echo ""
% echo "$1"

-- set rates to their default values

% ALPHA="RATE (48.0)"
% BETA="RATE (0.01)"
% DELTA1="RATE (0.00035)"
% DELTA2="RATE (0.0007)"
% LAMBDA1="RATE (0.01667)"
% LAMBDA2="RATE (0.16)"
% MU1="RATE (0.033)"
% MU2="RATE (2.0)"
% NU="RATE (12.0)"
% PHI="RATE (0.00334)"
% XI="RATE (0.3)"

-- set parameters to their default values

% INIT_PHASE=1
% PROG_SIZE=4
% USER_SIZE=4

% }

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

% GENERATE() {
-- argument 1: file base name (1 or 2)

"$1a.bcg" = generation of
           MAIN [C, FAIL, GET_PROG_JOB, GET_USER_JOB, PROG_JOB, PROG_JOB_READY,
                 REPAIR, USER_JOB, USER_JOB_READY, Z_AVAIL,
                 Z_PROG_QUEUE, Z_USER_QUEUE]
                ("$ALPHA", "$BETA", "$DELTA1", "$DELTA2", "$LAMBDA1",
                 "$LAMBDA2", "$MU1", "$MU2", "$NU", "$PHI", "$XI",
                 "$INIT_PHASE", "$PROG_SIZE", "$USER_SIZE");

-- in "$1a.bcg", all symbolic rates (e.g., ALPHA) have been replaced by their
-- numerical values (e.g., 48.0)

% bcg_info -deadlock "$1a.bcg"
% bcg_info -hidden "$1a.bcg"
-- % bcg_info -labels "$1a.bcg"

% SVL_RECORD_FOR_SWEEP "$1a.bcg"

% }

-------------------------------------------------------------------------------
-- PART 1: check strong (non-stochastic) equivalence with and without probes
-------------------------------------------------------------------------------

% INITIALIZE "Probe checking"

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

-- generate state space of mainframe without probes

% cat mainframe.lnt |
% sed -e 's/module mainframe/module mainframe_without_probes/' |
% sed -e 's/^[ ]*Z_AVAIL[ ]*$/access Z_AVAIL/' |
% sed -e 's/^[ ]*Z_PROG_QUEUE (I)[ ]*$/access Z_PROG_QUEUE/' |
% sed -e 's/^[ ]*Z_USER_QUEUE (I)[ ]*$/access Z_USER_QUEUE/' |
% cat > mainframe_without_probes.lnt

% SVL_RECORD_FOR_SWEEP "mainframe_without_probes.lnt"

% DEFAULT_PROCESS_FILE="mainframe_without_probes.lnt"

% GENERATE 1

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

-- generate state space of mainframe with probes

% DEFAULT_PROCESS_FILE="mainframe.lnt"

% GENERATE 2

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

property EQUIVALENCE
   "check that the LNT model without probes (1a.bcg) is strongly bisimilar"
   "to the LNT model with probes (2a.bcg) in which the probes have been cut"
is
   strong comparison "1a.bcg" == cut "Z_.*" in "2a.bcg";
end property

-------------------------------------------------------------------------------
-- PART 2: check that all probes are self-loop transitions
-------------------------------------------------------------------------------

-- change all transitions "ACTION !RATE (ALPHA)" to "ACTION; rate ALPHA"

"2b.bcg" = single rename
              "^\([A-Z_]*\) !RATE (\([0-9.]*\))" -> "\1; rate \2"
           in "2a.bcg";

-- % bcg_info -labels "2b.bcg"

% SVL_RECORD_FOR_SWEEP "2b.bcg"

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

"2c.bcg" = strong stochastic reduction of "2b.bcg";

-- using "branching stochastic reduction" instead of "strong stochastic
-- reduction" would not change "2c.bcg", because there are no tau-transitions

% bcg_info -deadlock "2c.bcg"
% bcg_info -hidden "2c.bcg"
% bcg_info -unreachable "2c.bcg"
-- % bcg_info -labels "2c.bcg"

% SVL_RECORD_FOR_SWEEP "2c.bcg"

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

property SELF_LOOP (ACTION)
   "check that all probe transitions named \"$ACTION\" are self-loops"
is
   -- these properties hold on "2c.bcg", but some do not hold on "2a.bcg",
   --  which is not minimal, so that self-loops may be unfolded in "2a.bcg"

   "2c.bcg" |= with xtl
      (* E = set of transitions named $ACTION that are not probes *)
      let E : edgeset = { T : edge where (label (T) -> [ $ACTION ... ]) and
                                         (source (T) <> target (T)) }
      in
         print (card (E) = 0) fby
         printf ("\n")
      end_let;
end property

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

check SELF_LOOP ("Z_AVAIL");

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

% I=0
% while [ $I -le $PROG_SIZE ]
% do
	check SELF_LOOP ("Z_PROG_QUEUE !$I");
%	I=`expr $I + 1`
% done

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

% I=0
% while [ $I -le $USER_SIZE ]
% do
	check SELF_LOOP ("Z_USER_QUEUE !$I");
%	I=`expr $I + 1`
% done

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