Wrong k-bound passed when using approximation with raw verification - fix 2052379

[mtygesen]

Fixes: https://bugs.launchpad.net/tapaal/+bug/2052379

Also fixes:

• Issue where gui in some cases would be unable to display trace event though the xml received from the engine was perfectly fine.
• NPE with color switches when trying to add bindings to a net that is not unfolded

[srba]

The k-bound is not updated. In the intro example, select Overapproximation and it deletes the -kbound from the raw string as it should. Then click on exact analysis and the -k bound is not readded (but it should). Now click on "Use" and verify and you get an error (because of the missing kbound).

Also (not related to this issue but please fix it too), if you in the intro example (without overapproximation) decrease the number of extra tokens to e.g. 2 and run the verification, the trace is not returned but the following exception is raised:

org.xml.sax.SAXParseException; lineNumber: 1; columnNumber: 1; Content is not allowed in prolog. at java.xml/com.sun.org.apache.xerces.internal.util.ErrorHandlerWrapper.createSAXParseException(ErrorHandlerWrapper.java:204) at java.xml/com.sun.org.apache.xerces.internal.util.ErrorHandlerWrapper.fatalError(ErrorHandlerWrapper.java:178) at java.xml/com.sun.org.apache.xerces.internal.impl.XMLErrorReporter.reportError(XMLErrorReporter.java:400) ...

The trace parses is probably missing the trace tag.

[srba]

Needs to be fixed as it now adds k-bound twice. To reproduce: Open into example, open the query. Select "Overapproximation" (and kbound disappers as it should). Now select "Exact analysis" and the kbound is back (as it should). Now select "Use" and the kbound is added a second time - running a verification now fails because it is not allowed to have the k-bound more than once.

[srba]

A small issue: open intro example, open query, select "no trace" and overapproximation (or overapproximation) and verify. The answer is conclusive. Now open the query again and click on "Use" and the query become inconclusive.