-- generation of the LTS from the LOTOS specification
% (cd LOTOS ; svl)

-- generation of the LTS from the 2022 LNT specification
"lts.bcg" = generation of "hubble.lnt";

-- generation of the LTS from the 2013 LNT specification
"lts_orig.bcg" = generation of "hubble_orig.lnt";

-- comparison of these LTSs, which should all be strongly equivalent
"diag.bcg" = strong comparison "lts.bcg" == "LOTOS/lts.bcg";
"diag.bcg" = strong comparison "lts.bcg" == "lts_orig.bcg";

% BCG_MIN_OPTIONS="-epsilon 1e-6"

-- turning the LTS into a CTMC
"hubble.bcg" =  
      branching stochastic reduction of
          total rename
             "LAMBDA" -> "FAIL; rate 0.1",
                -- the average lifetime of a gyroscope is 10 years
             "MU" -> "SLEEP; rate 100", 
                -- to turn on sleep mode takes 1/100 of a year
             "NU" -> "REPAIR; rate 6" 
                -- a shuttle mission for repair takes 1/2 of a year
             in "lts.bcg"
	  end rename;

-- checking for internal transitions: if absent, hubble.bcg is a CTMC
% bcg_info -hidden "hubble.bcg"

-- analyzing for various time points: .01 .1 1 etc. measured in years
% bcg_transient -thr hubble.thr hubble.bcg .01 .1 1 10 100 1e3 1e4 1e5 1e6 

-- calling Gnuplot to generate hubble.ps
% gnuplot hubble.plot

-- displaying the Postscript file generated by Gnuplot
% "$CADP"/src/com/cadp_postscript hubble.ps

-- cleanup
% SVL_RECORD_FOR_CLEAN "hubble.thr" 
% SVL_RECORD_FOR_CLEAN "hubble.ps" 
% SVL_COMMAND_FOR_CLEAN "(cd LOTOS ; svl -clean)"