% 1-P-invariant (1.0)
%P=?[Â F([input_on] = 1 ^ [input_off] = 1)]
%
P=?[G(([input_on] = 1 ^ [input_off] = 0) V ([input_on] = 0 ^ [input_off] = 1))]

% input is switched on if the token amount on A crosses the threshold 10 (1.0)
% 
P=?[G( [A] < 10 -> [input_on] = 1 )]
%P=?[G( Â([A] < 10) V [input_on] = 1 )]

% input is switched off if the token amount on A crosses the threshold 30 (1.0)
%
P=?[G([A] >= 30 -> [input_off] = 1)]
%P=?[G( Â([A] >= 30) V [input_off] = 1)]

% minima
%P=?[G([A] > 9)]
%P=?[G([A] > 8)]
%P=?[G([A] > 7)]
%P=?[G([A] > 6)]
%% P=?[G([A] > 5)]
%% P=?[G([A] > 4)]

% maxima
%P=?[G([A] < 31)]
%P=?[G([A] < 32)]
%P=?[G([A] < 33)]
%P=?[G([A] < 34)]
%% P=?[G([A] < 35)]
%% P=?[G([A] < 36)]

% range
% There is a delay of 0.5 time units between the switch on/off 
% and the reaction of the actual inflow transition.
% E.g., after having switched off the input, 5 additional tokens will arrive 
% by the already triggered firing of the transition $input$. 
% Thus, even a weaker range than specified by the threshold values does not get probability 1 (0.995)
%P=?[G([A] > 9 ^ [A] <= 30)]
%P=?[G([A] >= 8 ^ [A] <= 35)]
P=?[G(5 <= [A] ^ [A] <= 40)]