(* 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" % SVL_RECORD_FOR_CLEAN "LOTOS/systol_$SCHEME@1.o" strong comparison "systol_$SCHEME.bcg" == "LOTOS/systol_$SCHEME.bcg" ; "systol_branching_$SCHEME.bcg" = branching reduction of "systol_$SCHEME.bcg" ; % done