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

(* Function definitions *)

% BASE_NAME () {
%    case $1 in
%       co*_*_*_branching.bcg)
%          basename $1 _branching.bcg;;
%       co*_*_*.lnt)
%          basename $1 .lnt;;
%    esac
% }

% EXHIBITOR () {
%    echo
%    echo "Searching in $1 execution sequences matching pattern $3 of $2"
%    case $1 in
%       *.bcg)
%          OPEN_TOOL="bcg_open";;
%       *.lnt)
%          OPEN_TOOL="lnt.open";;
%    esac
%    RESULT_FILE=`BASE_NAME $1`.result
%    $OPEN_TOOL $1 exhibitor $4 -seqno $3 < $2 >> $RESULT_FILE
%    echo "Result is stored in $RESULT_FILE"
% }

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

(* generation and minimization of LNT files *)

% for PARAMS in 1_1 1_2 1a_1 1a_2 1a_3 2_1 2a_1 3_1 5_1 6_1
% do
    "co4_$PARAMS.bcg" = generation of "co4_$PARAMS.lnt";
    "co4_${PARAMS}_branching.bcg" = branching reduction of "co4_$PARAMS.bcg";
% done

(* note: co4_4_1 is skipped due to complexity issues */

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

(* Comparison with LOTOS specifications: The BCG graphs generated from LNT
 * specifications are compared  (modulo strong equivalence) against the BCG
 * graphs generated from the original LOTOS specifications, in order to show
 * that the LNT and LOTOS specifications are behaviourally equivalent
 *)

% (cd LOTOS ; echo "" ; svl)

% for PARAMS in 1_1 1_2 1a_1 1a_2 1a_3 2_1 2a_1 3_1 5_1 6_1
% do
     strong comparison "co4_$PARAMS.bcg" == "LOTOS/co4_$PARAMS.bcg";
% done

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

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

(* Verifications *)

% for PARAMS in 1_1 2_1 3_1 5_1
% do
%    for SEQNO in 1 2 3 4 5
%    do
%       EXHIBITOR co4_${PARAMS}_branching.bcg signotin.seq $SEQNO "-bfs"
%    done
% done

% for PARAMS in 1_1 1a_1
% do
     "co4_${PARAMS}_draw.bcg" = total rename using "short.rename" in 
                                "co4_${PARAMS}_branching.bcg";
%    echo
%    echo "Drawing co4_${PARAMS}_draw.bcg in co4_${PARAMS}_draw.ps with bcg_draw"
%    bcg_draw -ps co4_${PARAMS}_draw.bcg &
% done

% EXHIBITOR co4_1_2_branching.bcg inconsistent.seq 1 "-bfs"
% EXHIBITOR co4_1a_1_branching.bcg dead.seq 1 "-dfs -all"
% EXHIBITOR co4_4_1.lnt scenario_4_1.seq 1 "-dfs -first"

% for SEQNO in 1 2 3
% do
%    EXHIBITOR co4_5_1_branching.bcg unsafe.seq $SEQNO "-bfs"
% done

% EXHIBITOR co4_6_1_branching.bcg dead.seq 1 "-bfs"
% EXHIBITOR co4_6_1_branching.bcg twogroups.seq 1 "-bfs"

% rm -f co4_4_1.c co4_4_1.h co4_4_1.o
% $CADP/src/com/cadp_rm exhibitor

(* 
 * SVL_RECORD_FOR_CLEAN is defined in $CADP/src/svl/standard. 
 * It is used to mark the files not managed by SVL that must
 * be removed when SVL is called with option -clean
 *)
% for FILE in *co4*.err co4*_draw.ps co4*.result
% do
%    SVL_RECORD_FOR_CLEAN "$FILE"
% done

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