search

hhu-stups / prob-issues

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

Deactivate Visualise Formula as Graph/Table sometimes #8

Open favu100 opened 3 years ago

favu100 commented 3 years ago

Deactivate MenuItem for visualising formula as graph/table for formulas that are not expression or predicate. Required changes in prob2_interface are already implemented.

Another remark: Also deactivate MenuItem if value does not exist because uninitialized machine

favu100 commented 3 years ago

For most entries in the StateView, the MenuItems are deactivated as expected. Still, there are some cases where the MenuItem is activated unexpectedly. E.g. for the top-level entry INVARIANT, the corresponding type is predicate because the corresponding value is a predicate. Again, INT is identified as type "other"

favu100 commented 3 years ago

There are some cases that are not supported for visualisation yet.

E.g. you can have parameters in operations, or nested formulas with quantification. Visualising such as a formula and its subformulas requires information about used bounded variables and how they are instantiated (to make the whole predicate true)