Raw verification options issues - fix 2046945

[mtygesen]

Fixes:
https://bugs.launchpad.net/tapaal/+bug/2046945
https://bugs.launchpad.net/tapaal/+bug/2046960

Also fixes:

• Width of raw verification options textfield when typing in a long string and then saving and reopening
• Raw verification options showing when trace option was updated
• Bug where verification options would enable when changing queryType

[srba]

Fixes the problem but there is another one that would be nice to be fixed in this PR as well. If you open e.g. the ERK example and the query and then click on "deadlock" in the query, the buttons for editing the query are not enabled (only the "not" button is enabled). Probably a refresh of the buttons should be added somewhere.

[srba]

When you open the query and click on deadlock, the query editing buttons are still not enabled (only and/or/not). Compare to the correct behaviour in the released version 3.9.5 (can be downloaded from www.tapaal.net).

[srba]

There is a small issue: open the colored referendum example, open the first query and select "Some trace" and "Save and verify". All goes fine. Now open the query again, select "Use" and "Save and verify" again and we get an error: "the PNML file cannot be parsed due to syntax errors." This should not happen - maybe the file has a different name than what the GUI expects?

[srba]

For hyperLTL queries in the query dialog, the options "Use trace abstraction refinement" and "Use siphon-trap analysis" should be both disabled (greyed out).

[srba]

There is a slight problem with a focus for making LTL and hyperLTL queries. To reproduce, open e.g. ERK model,
make a new query select LTL (or hyperLTL), then click on the <> in the query text field, then click on "Use" and press "A" or "E" (path quantifiers). Now the logical operators are enabled but not the predicates - they get enabled first after you click again on <> in the query.
This is not a problem if you do not press "Use" and also not a problem for CTL queries.

[srba]

Also the boundendess check is broken. Open e.g. the intro example, open the query and run "check boundedness". The engine fails because it got the argument "null" from the GUI.

[srba]

There is an issue in game-harddisk. Open the model, open the query, click on "Use", then select the whole query, click on "AF" and now "Add predicate to the query" becomes enabled (but it should not, because if you press it, it will remove the quntifier AF and verification of the query fails.
This issue can be only reproduced if "Use" is pressed. Without it, it works just fine.

[srba]

One more issue to be fixed: In the intro example, when you click on the query (select all), it allows to change the quantification (to EF, AF, EG and AG) which is correct behaviour but it should not allow to change the logic (all three buttons and/or/not should be disabled). They should be enabled only if you click on the IntroExample.Target = 1 only (without the quantification).

[srba]

For CTL/Reachability untimed nets, it should still be allowed to have and/or/not before the temporal operators. This was only a problem for the timed nets like intro-example.

[srba]

For LTL and hyperLTL queries, it should be possible that after pressing "A" and then "U" and then selecting the whole "U" with both place holders, then and/or/not should be enabled, right now this is not possible - compare to 3.9.5 where it allows to add Boolean operators when the until "U" expression is selected.

[srba]

The query creating for CTL/Reachability is broken now. If you make new query (e.g. on ERK) then the Boolean operators are not enabled - but they should (compare with 3.9.5). Also if you make query like EF false and select all and want to add negation before it, then the EF false query disappears - again compare with 3.9.5.

[srba]

The behaviour for LTL and hyperLTL is not correct - it allows to add and/or/not at the highest level, which the engine does not like - compare on e.g. ERK with 3.9.5 which does not allow that.

[srba]

testing all and seems to work fine now, merging to main