Read MPSat verification results from XML output

Currently the results of MPSat verification are parsed from a human-readable output that is not formally specified. A better option is to read the verification results from a precisely structured XML output. The toolchain starts with PUNF and only if it succeeds it proceeds with MPSAT, see details below.

== Possible outcomes for PUNF: ==

1) PUNF fails due to memory overflow, or syntax error)
   * exit code >= 2
   * message in stderr (Error: ....)
   * no trace
   * impossible to proceed with MPSAT

2) PUNF fials due to safeness or inconsistency
  * exit code >= 2
  * message in stderr
    - Error: the net is not safe, place PLACE_NAME; trace: TRACE
    - Error: the STG is inconsistent, signal SIGNAL_NAME; trace: TRACE
  * trace in stderr
  * impossible to proceed with MPSAT
  * Error: the net is not safe, place PLACE_NAME; trace: TRACE

3) PUNF succeeds
  * exit code <= 1
  * proceed with MPSAT

== Possible outcomes of MPSAT (only if PUNF succeeds) ==

1) MPSAT fails
  - exit code >= 2
  - message in stderr (Error: ...)
  - no XML

2) MPSAT succeeds
  - exit code <= 1
  - read XML for verification result

== Examples of XML output ==

1) Example with several solutions:

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<result status="success" message="some additional details"/>
<solutions>
    <solution cost=23 message="details about this solution with 3 traces">
        <trace>
            <transition name="a+" event=1/>
            <transition name="b-/1" event=3/>
        </trace>
        <trace/> <!-- empty trace -->
        <trace>
            <transition name="a+" event=1/>
        </trace>
    </solution>
    <solution cost=0 message="solution with an empty trace">
        <trace/>
    </solution>
</solutions>

2) Example with an empty solution:

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<result status="success" message="some additional detail"/>
<solutions>
    <solution/>
</solutions>

3) Example with no solutions:

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<result status="success" message="some additional detail"/>
<solutions/>

4) Example with an error:

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<result status="failure" message="reason for failure"/>

== Notes about XML output of MPSAT ==

In the usual MPSAT call syntax:
 mpsat mode [options] inputfilename [outputfilename]

if outputfilename ends with ".xml", the solution in XML form is used. The option should work well for all verification modes (-D, -C, -U, -N, -F, -Fs). It occasionally works for other modes, but there changes are very likely as the solutions are not traces anymore.

There are some changes to the syntax you wrote in your message below, most importantly "solutions" tag is now a child of "result" - I think this is more logical and I had an impression this is what we had agreed. In any case, making it as you suggested would violate XML syntax as there must be a single root (an XML document must be a tree, not a forest).

Also, some modes use extra tags and attributes:

1) "solution" has attribute "cost" which is a natural number.

2) for -C and -N modes, "solution" has attribute "signal" saying for which output or internal signal the CSC conflict or normalcy violation was detected.

3) for -N mode, "solution" has attribute "reason", which could be one of the following:
 - "mixed_triggers" normalcy violation due to different triggers' signs for a signal; one trace is then given, and the set of triggers using the new tag "triggers".
 - "contradictious_hypotheses" normalcy violation due to contradictious hypotheses about normalcy type; two traces are then given, each trace is followed by the corresponding set of triggers as above.
 - "CSC_conflict" normalcy violation due to CSC conflict; two traces are then given, no triggers.
 - "other" complex normalcy violation; three traces are then given, only the first trace is followed by the corresponding set of triggers as above. In WC, as only two traces can be displayed, the last two traces should be preferred.

4) for -N mode, "solution" has attribute "normalcy_type_hypothesis", which could be either "p", "n" or "?".

== Comments ==

It would be useful to keep the following details in the xml file (if high level of details is selected), so the results can be reproduced with a single xml file:
  - command line;
  - original Reach expression;
  - expanded Reach expression (after all regular expressions are resolved);
  - maybe even the whole net (as a zipped stream).

Just another element like this:
<setup
  command_line="mpsat ..."
  reach_original="let a=PP\"p*\"..."
  reach_expanded="let a={P\"p0\",P\"p1\"}..."
  net="pnml.gz stream"
/>