% check whether certain exact time points are in the trace
%P=?[ F(time = 49999) ]
%P=?[ F(time = 50000) ]
%P=?[ F(time = 51000) ]

% lactose peaks at 50.000
%
P=?[ (49999 <= time ^ time < 50000) -> [Lactose] <= 0.01 * max([Lactose]) ]
%P=?[G( Â(49999 <= time ^ time < 50000) V [Lactose] <= 0.01*max([Lactose]))]

%P=?[ (50000 <= time ^ time < 50001) -> [Lactose] >= 0.99 * max([Lactose]) ]
P=?[ 50000 = time -> [Lactose] >= 0.99*max([Lactose]) ]
%P=?[G( Â(50000 = time) V [Lactose] >= 0.99*max([Lactose])) ]
%P=?[F( 50000 = time ^ [Lactose] >= 0.99*max([Lactose]) )]

%P=?[ (52000 <= time ^ time < 52001) -> [Lactose] <= 0.01 * max([Lactose]) ]
%P=?[ (52000 <= time ^ time < 52001) -> [Lactose] <= 0.03 * max([Lactose]) ]
%P=?[ (52000 <= time ^ time < 52001) -> [Lactose] <= 0.05 * max([Lactose]) ]
P=?[ (52000 <= time ^ time < 52001) -> [Lactose] <= 0.1 * max([Lactose]) ]
%P=?[G( Â(52000 <= time ^ time < 52001) V [Lactose] <= 0.1*max([Lactose])) ]

% Z is highly likely to be a low concentration at time point 50,000
P=?[time = 50000 -> [Z] <= 0.1*max([Z]) ]
%P=?[G( Â(time = 50000) V [Z] <= 0.1*max([Z]) )]

% Z will rise to at least 60% of its maximal value within 2,000 time units
%P=?[F( (50000 < time ^ time < 52000) ^ [Z] >= 0.6 * max([Z]) )]
%P=?[F( (50000 < time ^ time < 52000) ^ [Z] >= 0.7 * max([Z]) )]
P=?[F( (50000 < time ^ time < 52000) ^ [Z] >= 0.8 * max([Z]) )]
%P=?[F( (50000 < time ^ time < 52000) ^ [Z] >= 0.9 * max([Z]) )]


%
% peak(lactose) -> pretty soon (within 2,000 time units) peak(Z)
%
%P=?[(time=50000 ^ [Lactose]>=0.99*max([Lactose]) ^ [Z]<=0.1*max([Z])) -> F([Z]>=0.6*max([Z]) ^ time<52000 ) ]
%P=?[G( Â(time=50000 ^ [Lactose]>=0.99*max([Lactose]) ^ [Z]<=0.1*max([Z])) V F([Z]>=0.6*max([Z]) ^ time<52000 ) )]
P=?[(time=50000 ^ [Lactose]>=0.99*max([Lactose]) ^ [Z]<=0.1*max([Z])) -> F([Z]>=0.8*max([Z]) ^ time<52000 ) ]