Pause condition presentation

[jkrivine]

If one cannot use any expression for the pause condition, I suggest not to let the user write an arbitrary expression in a box. Maybe just an integer (as for the points).

J

[pirbo]

One CAN use any boolean expression for the pause condition!

…

Le 30 janv. 2017 à 05:27, Krivine ***@***.***> a écrit : If one cannot use any expression for the pause condition, I suggest not to let the user write an arbitrary expression in a box. Maybe just an integer (as for the points). J — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

[jkrivine]

I meant one is constrained to use inequalities. So I thought there should be a GUI way of preventing illegal pausing conditions.

[pirbo]

Well, you can use equality on values of any non time dependent variables (including observables)! I know, '[T] = ...' is tempting. That's why I've put a default value with a '>' (so the minimal edition is to keep this inequality) That's why also when you erase the condition, the hint is '[T] > 100' (once again with an inequality).

[jkrivine]

Also now when blanking the pause condition, WebSim suggests [T] = 100 in grey which is the forbidden expression.
BTW it is weird from a user standpoint that [T] = 100 is allowed in the KF but not in the pause condition. Can't you deal with the pause condition as a stopping time thing or is it treated differently?

[pirbo]

when blanking the pause condition, WebSim suggests [T] = 100.

It's indeed a mistake! (Fixed)

Can't you deal with the pause condition as a stopping time thing.

It requires (according to me unnecessary) extra machinery but it is not impossible. You would have to write:

• add_extra_stopping_times and remove_useless_stopping_times in simulation/state_interpreter.ml
• drop_already_over_stopping_time somewhere (state_interpreter store a sorted list of to happen stopping time, if you add a stopping time that should have occurred in the past, it will never pop it and therefore never do the next stopping times)
• the correct replacement to if stooping_times <> [] then failwith "..." in simulation/evaluator.ml

Help yourself :-)