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]

Does not quite work - if I click on "Use" and replace the -kbound with e.g. 10 (the default is 4), it will still call the engine with 4 and not with 10 (which it should)

[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.

[srba]

Open intro example, open query, select Overapproximation, select "Use" and add " -k 10 -t 0" at the end of the options. Now "save and verify" and you get an error:

Exception in thread "AWT-EventQueue-0" java.lang.NullPointerException: Cannot invoke "pipe.gui.petrinet.PetriNetTab.getModel()" because the return value of "dk.aau.cs.verification.VerificationResult.getUnfoldedTab()" is null
at net.tapaal.gui.petrinet.verification.RunVerification.showResult(RunVerification.java:107)
at net.tapaal.gui.petrinet.verification.RunVerificationBase.done(RunVerificationBase.java:247)
....

Seems to be a problem even if you do not select "Use" just overapproximation.

[srba]

Works fine now and good refactoring.