In the default mode, the software asks for input from the user in a format described in the next section. Usually one will write the input to a file and let the software read it from this file using a pipe (./hsolver <file).
In interactive mode (./hsolver -i), the software asks for input from the user using detailed questions. This mode is less flexible and is only provided for compatibility with earlier versions.
In the default mode, the software does verification by removing points from the state space that are not on any trajectory from an initial to an unsafe state, and hence it also may remove points in the reach set. In order to get reach set information, call HSolver with the parameter -f. Then the software only does forward checking—removing points that are not on any trajectory from an initial state, but does not do backward checking—removing points that do not lead to an unsafe state. It is also possible to do reasoning in the opposite direction: After calling HSolver with the parameter -b it computes backward reach set information, that is, points that might lead to an unsafe state.
For examples with simple continuous dynamics (e.g., clocks), slice computation improves the performance of HSolver . This feature can be turned on with the flag -s.
Call HSolver with the parameter -h to get information on further parameters.