% maxima
%
%P=?[G([A] <= 100)]
%P=?[G([A] >= 30)]

% the tokens on A never fall below the threshold 30 (1.0)
%
P=?[ Â F([A] < 30)]

% the transtion input tries to keep the token on A between 30 and 80.
% but there are always some tokens on B, which may return to A.
P=?[F([A] = 30 ^ G(30 <= [A] ^ [A] <= 80))]
%Probability:  0.93

P=?[F([A] = 30 ^ G(30 <= [A] ^ [A] <= 81))] 
P=?[F([A] = 30 ^ G(30 <= [A] ^ [A] <= 82))]
P=?[F([A] = 30 ^ G(30 <= [A] ^ [A] <= 83))]
P=?[F([A] = 30 ^ G(30 <= [A] ^ [A] <= 84))]
P=?[F([A] = 30 ^ G(30 <= [A] ^ [A] <= 85))]

% there is a constant inflow due to the input transition,
% and the rate of t1 is (significantly) higher than of t2. 
% therefore, B increases permanently and without limits.
% true in the averaged case, e.g. 100 runs
P=?[G(d[B] >= 0)]

%x,y:P=?[G([B] = $x -> F([B] = $y ^ $y > $x))]
% -> unrecognised syntax

%x:P=?[G([B] = $x -> F([B] = $x+1))]
% -> unrecognised syntax