%maxima
%
%P=?[G([A] < 7500)]
%P=?[G([B] < 3900)]

%reset to zero of B at time points:20, 40

% simple version
% if the output is switched on, B is cleaned immediately
P=?[G( [output_on] = 1 -> [B] = 0)] 

% switching off at time 20, strong version
% probability 0.99, because due to the immediate transtions it's possible, 
% that there are other time points 20, where B is not off yet;
%
P=?[(time = 20) -> [B] = 0]

% weak version, probability 1.0
% cleaning of B at time point 20
P=?[F(time = 20  ^ [B] = 0)]

% cleaing of B at time point 20, 
% ensuring that B does not get cleaned earlier
%
P=?[F([B] > 0 ^ ([B] > 0 U (time = 20 ^ [B] = 0 )))]

% cleaning of B at time point 40, 
% ensuring that B remains marked inbetween as soon as it got a token
%
P=?[F(time = 20 ^ [B] = 0) ^ F([B] > 0 ^ ([B] > 0 U (time = 40 ^ [B] = 0 )))]