Search in ProB2-UI State View very slow

[leuschel]

We still have the issue that searching in the state view can be very slow for large machines. I have one machine with 185 operations where after typing in a few characters in the search field makes ProB2-UI unresponsive for several minutes. I think it is expanding all operations and subsidiary operations and possibly evaluating the guards, even though the corresponding top-level entries (Operations and Subsidiary Operations) are closed.

[leuschel]

Note: for the same model the search in ProB Tcl/Tk is instantaneous.

[leuschel]

Das passiert zB für das Modell M9_Push_Mouse_Buttons_vis.bum (v7 der AMAN 2023 Fallstudie) in der State View zb "TIME" in das Suchfeld eintippt dauert es sehr lange bis ProB2-UI reagiert. Ich glaube zu dem Zeitpunkt werden alle Subformeln virtuell ausgeklappt und berechnet; einige THEOREMS dauern sehr lange und laufen in Timeouts.

[dgelessus]

For the AMAN model, the UI already hangs if you open the "theorems (on constants)" node (only the top-level node, not any of the individual theorem sub-nodes). And if I reproduce your test case (type "TIME" into the search box), the command that takes long is:

prob2_evaluate_bvisual2_formulas([408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433,434,435,436,437,438,439,440],1,Values)

where 408..440 are the IDs of all the formulas directly under "theorems (on constants)".

We should improve this in some way of course, but I think this isn't a problem with the search feature anymore. If the search can't even expand top-level categories automatically, it wouldn't be able to find anything at all...

[leuschel]

We should solve both issues: search should ideally not require evaluating any sub-formula (or do we want to search in the values??). In Tk you only search in the expanded nodes; this solves this issue in another way; it makes search more restrictive but always fast.

Opening the theorems I guess computes the truth value of all axioms, so it is expected that this can take some time. But we should try and make this user experience more friendly (use smaller time-outs, maybe have global-time budget, make the expansion interruptable?).

[dgelessus]

The search itself doesn't evaluate the formulas, but all formulas in the search results are evaluated by the state view. In this case, the search term "TIME" also matches a theorem like ∀zoom·(zoom ∈ ZOOM_LEVELS ⇒ ∀z_·(z_ ∈ {RANGE_LAMBDA__|∃time·time ∈ [...], because the predicate contains "time" and the search is case-insensitive. Evaluating that theorem takes a few seconds until it times out. This isn't something that ProB 2 UI can control - we just call bvisual2 to evaluate everything. If possible, we evaluate multiple formulas at once, so the Prolog side could place a timeout on the entire prob2_evaluate_bvisual2_formulas or bv_get_values call.

[leuschel]

I just typed zzz into the search field and it also seems to evaluate formulas. Maybe I did not type zzz fast enough?

[leuschel]

I still have the impression that once you start typing in the search field (all?) subformulas are expanded; once that is finished typing anything in the search field is fast.

[dgelessus]

It starts searching as soon as you enter the first character, so it will start searching for "z" before "zzz". Most single letters like "z" will appear somewhere in unrelated formulas as well - especially in predicates that are complex enough to generate timeouts :) You can see the difference if you search for a letter that really appears nowhere, e. g. "j" or "ä" (almost instant), or a letter that doesn't appear in the slow theorems, e. g. "c" (takes only a second or so).

Perhaps we should delay starting the search (or at least the evaluation) until there has been no more user input for 200 ms or so. But that still doesn't solve the underlying problem that if you enter an incorrect search term, you might accidentally find a "slow" formula that blocks the entire state view.

[leuschel]

Ok, delaying 200 ms sounds good.

[leuschel]

And possibly we should only search the already opened formulas like in Tcl/Tk. If one wants to search the theorems/ASSERTIONS then one can expand them. The problem is that many Event-B machines contain theorems for proving which are big universally quantified formulas (e.g., over all subsets of some large set ...).