% 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 between time points 10 and 30 (1.0)
%
P=?[(10 <= time ^ time < 30) -> [det_on] = 1]

% exchanging the implication by G(!A V B) 
%
%P=?[G(Â(10 <= time ^ time < 30) V [det_on] = 1)]

%P=?[(time = 8) -> [stochastic_on] = 1]
%P=?[(time = 9) -> [stochastic_on] = 1]
%P=?[(time = 10) -> [stochastic_on] = 1]
%P=?[(time = 10) -> [det_on] = 1]

%P=?[(time = 29) -> [det_on] = 1]
%P=?[(time = 29) -> [stochastic_on] = 1]
%P=?[(time = 30) -> [stochastic_on] = 1]
%P=?[(time = 31) -> [stochastic_on] = 1]

% stochastic token flow from A to B before time points 10 and after 30 (1.0)
%
P=?[(time < 10 V 30 <= time) -> [stochastic_on] = 1]
%P=?[G(Â(time < 10 V 30 <= time) V [stochastic_on] = 1)]