--
-- Safety-Critical Systems 3, SoSe 2003
--
-- water level controller,
-- as developed interactively in the "Uebung" on Jul. 10, 2003
--
-- (see watertank.ps from the HyTech distribution for a slide with the
-- problem description)
--
-- Jan Bredereke
--

var
    t: clock;
    y: analog;

-- the water level controller
automaton wc

initially opened & y=1 & t=0;

synclabs: close, open;

loc opened: while y<=10 wait {dy=1}
    when y=10 do {t'=0} sync close goto closing;

loc closing: while t<=2 wait {dy=1}
    when t=2 goto closed;

loc closed: while y>=5 wait {dy=-2}
    when y=5 do {t'=0} sync open goto opening;

loc opening: while t<=2 wait {dy=-2}
    when t=2 goto opened;

end


-- analysis of the water level controller

var initReg, reachableReg, safeReg: region;

initReg := loc[wc] = opened & y=1 & t=0;

-- the reachable states:
reachableReg :=
    reach forward from initReg endreach;

-- the safe states:
safeReg := y>=1 & y<=12;

if empty(reachableReg & ~safeReg)
then
    prints "Controller maintains water level correctly.";
else
    prints "Controller does not maintain water level correctly.";
    print trace to ~safeReg using reachableReg;
endif;