% 1-P-invariant (1.0)
%
P=?[G( ([stochastic_on] = 1 ^ [det_on] = 0) V ([stochastic_on] = 0 ^ [det_on] = 1) )]

% weak version of 1-P-invariant: both cannot be on
%
%P=?[Â F([stochastic_on] = 1 ^ [det_on] = 1)]

% both cannot be off:
%
%P=?[Â F([stochastic_on] = 0 ^ [det_on] = 0)]

% deterministic token flow from A to B for a token amount on A between 500 and 700
%
P=?[(500 <= [A] ^ [A] < 700) -> ([det_on] = 1)]

% stochastic token flow from A to B for a token amount on A less than 500 or greater or equal 700
% 
P=?[( [A] < 500 V 700 <= [A]) -> ([stochastic_on] = 1)]