HOA path formulas

[kleinj]

With this PR, PRISM learns a new mechanism for specifying path formulas: Directly via a deterministic automaton in HOA format.

PRISM already supports HOA automata, when they are constructed by an external tool from an LTL path formula. Now, one can write properties like
P=?[ HOA: {"filename.hoa"} ]
which computes the probability of the paths that are accepted by the given HOA automaton. In this short form, the atomic propositions (APs) from the automaton are matched with the corresponding labels in the model. Alternatively, one can specify state expressions for labels, e.g.,
P=?[ HOA: {"filename.hoa", "a" <- s=3, "b" <- (s=1|s=2) }
Here, the automaton has two APs, a and b, which are mapped to the set of states satisfying s=3 and (s=1|s=2), respectively.

This has a few advantages:

• It might be easier to generate a HOA automaton with an external tool directly, then store it as a file and use it in the property than to have to write wrapper scripts for the external tool.
• With the above, the generation time for the automaton can be amortized over multiple runs.
• It facilitates easier debugging and testing of the HOA functionality, as we don't have to rely on tools to produce the automata.
• It allows to use path specifications outside of LTL, i.e., the full omega-regular languages by either writing/generating the automaton directly or using tool support, e.g., Spot's support for PSL formulas.

This is the first time that properties can refer to external filenames, which raises the issue how to deal with relative filenames (similar to things like #include in C++, etc). Here, we propose to do resolution as follows:

1. First, if the property is part of a property file, we resolve relative to it's directory
2. Otherwise, if the model is from a file, we resolve relative to the model's directory
3. As a last resort, we resolve relative to the working directory

We also propose a mechanism to explicitly specify the directory for resolution by 3 macros, i.e., for following would be valid filenames for a HOA path expression:

1. $PROPERTY_DIR/filename.hoa
2. $MODEL_DIR/filename.hoa
3. $WORKING_DIR/filename.hoa

Note that these macros are only considered if they are at the beginning of the location string.

This extension was published in "Advances in Symbolic Probabilistic Model Checking with PRISM" (TACAS'16) and has been in use at TU Dresden for quite some time.

TODOs:

• Documentation for the manual
• Does this interfere with prism-games? (quoted string refactoring, new expression type)