search

hhu-stups / prob-issues

ProB issues (for probcli, ProB Tcl/Tk, ProB2, ProB2UI)
6 stars 0 forks source link

ProB2-UI Parse Error when Visualising Event Guard #281

Open leuschel opened 1 year ago

leuschel commented 1 year ago

In the AMAN case study M9_Push_Mouse_Buttons_vis.bum model, when I right click on the disabled event

Move_Mouse_Zoom_Zooming and choose "Visualize Expression as Graph" I get this parse error:

Could not parse formula: Parsing predicate failed because: Unexpected sub-formula, expected: a predicate but was: an expression

Unexpected sub-formula, expected: a predicate but was: an expression Parsing expression failed because: Unexpected sub-formula, expected: a predicate but was: an expression

Unexpected sub-formula, expected: a predicate but was: an expression Parsing substitution failed because: Unknown operator: (expected to find an assignment operator)

Unknown operator: (expected to find an assignment operator) Code: target_zoom & target_zoom : ZOOM_LEVELS & dragged_zoom_level /= {} & target_zoom /: dragged_zoom_level Unicode translation: target_zoom ∧ target_zoom ∈ ZOOM_LEVELS ∧ dragged_zoom_level ≠ ∅ ∧ target_zoom ∉ dragged_zoom_level

(Also, as already mentioned in some other issues: this formula should never be parsed as a substitution.) Also, the menu should say "Visualize Expression as Formula Tree".

leuschel commented 1 year ago

The properties file contains

states.statesView.contextMenu.items.visualizeExpressionGraph = Visualize Expression as Graph

However, I am not sure if we should change this. I think for some elements (like variables with a relational value) the UI probably does all another command and shows the value as a graph??

leuschel commented 1 year ago

I just checked: even for variables which are relations, the formula is shown as a tree. Maybe we should add another right-click command to show a value as a graph. The other right-click command "Visualize Expression as Table" really does show the "Value" as a table.

leuschel commented 1 year ago

I have updated the properties; but we should think whether we do not want to add another command "Visualize Formula as Tree" which does what the current command does, and adapt the implementation of the current command. Also, I noted that we have no German translations for the properties.

leuschel commented 1 year ago

I think the parser error is because ProB2-UI does create the existential quantifier; it seems to generate: bool(target_zoom & target_zoom : ZOOM_LEVELS & dragged_zoom_level /= {} & target_zoom /: dragged_zoom_level) rather than

target_zoom: (target_zoom : ZOOM_LEVELS & dragged_zoom_level /= {} & target_zoom /: dragged_zoom_level)

leuschel commented 1 year ago

Another error occurs when you use either of the "Visualize Expression..." commands on a sub-formal of the event: you then get Prolog said no. ProB returned error messages: Error: Unknown identifier "target_zoom"

Here ProB2-UI should pass the value of target_zoom from the UI or simply extract the formula and value from bvisual2, rather than pretty-printing the formula, parsing it through the parser and the evaluating it again.