(* the 4 graphs systol_B1.bcg, systol_F.bcg, systol_W1.bcg, and systol_W2.bcg
   are generated from the corresponding LNT specifications, compared against
   the graphs generated from the original LOTOS specifications, and finally 
   reduced for branching equivalence
*)

% for SCHEME in B1 F W1 W2
% do

    "systol_$SCHEME.bcg" = generation of "systol_$SCHEME.lnt" ;

%   (cd LOTOS ; svl demo.svl "$SCHEME" )
%   SVL_RECORD_FOR_CLEAN "LOTOS/systol_$SCHEME.bcg"

    strong comparison "systol_$SCHEME.bcg" == "LOTOS/systol_$SCHEME.bcg" ;

    "systol_branching_$SCHEME.bcg" = branching reduction of "systol_$SCHEME.bcg" ;

% done