% maxima (1.0, 0.95)
P=?[G([A] < 7550)]
P=?[G([B] < 5350)]

% using constraints to get the probability range of the max
%
%x:P=?[G([B] <= max[B] ^ max[B]=$x)]
%x:P=?[max[B]=$x)]

% peaks (0.9, 1.0)
%
%P=?[F(time = 20 ^ [A] > 7300 ^ 3000 < [B] ^ [B] < 3500)]
P=?[F(time = 20 ^ [A] > 0.9*max[A] ^ 3000 < [B] ^ [B] < 3500)]

% wrong answer
%P=?[F(time=30 ^ 5000 < [A] ^ [A] < 5400 ^ [B] > 0.9*max([B]) )]
% correct answer
P=?[F(29 < time ^ time < 30 ^ 5000 < [A] ^ [A] < 5400 ^ [B] > 0.9*max([B]) )]
%x:P=?[F([A] > 5000 ^ [A] < 5500 ^ [B] > 5000 ^ [B] < 5500 ^ time = $x)]

% steady state, relative statements (0.03, 0.59, 0.8, 0.91)
%P=?[G([A] < [B])]
%x:P=?[F(time = $x ^ G([A] < [B]))]

P=?[ (time >= 50) -> G([A] < [B])]
P=?[ (time >= 55) -> G([A] < [B])]
P=?[ (time >= 60) -> G([A] < [B])]
P=?[ (time >= 70) -> G([A] < [B])]

% steady state, absolute statements (0.39, 1.0)
P=?[(time >= 50) -> G(1500 < [A] ^ [A] < 1800 ^ 1600 < [B] ^ [B] < 2000)]
P=?[(time >= 60) -> G(1500 < [A] ^ [A] < 1800 ^ 1600 < [B] ^ [B] < 2000)]