ProbReach v1.3

• Removed dReach and bmc_main.native from the tool chain
• Added algorithm for probabilistic reachability in hybrid systems with nondeterministic parameters
• Added statistical model checking (Chernoff-Hoeffding bound, Bayesian estimations)
• Parameter synthesis is _not_ currently supported

ProbReach v1.2

• dReal3 static binary included (much faster!)

ProbReach v1.1

Usage:

./ProbReach <options> <model-file.pdrh> --dreach <dReach-options> --dreal <dReal-options>

options:
        -e <double> - length of probability interval or maximum length of the box (default 0.001)
        -l <string> - full path to dReach binary (default dReach)
        -t <int> - number of CPU cores (default max cores available)
        -h/--help - help message
        --version - version of the tool
        --verbose - output computation details
        --visualize <string> - produces <model-file.json> containing Borel set for parameter <string> and probability value with respect to time
        --dreach - delimits dReach options (e.g. reachability depth)
        --dreal - delimits dReal options (e.g. precision, ode step)

Archives <*-full.zip> contain complete set of binaries and models

ProbReach v1.0.1

Usage:
./ProbReach <options> <model-file.pdrh> <dReach-options>

options:
        -e <double> - length of probability interval or maximum length of the box (default 0.001)
        -d <double> - precision used to call dReach (default 0.001)
        -l <string> - full path to dReach binary (default dReach)
        -t <int> - number of CPU cores (default 1)
        -k <int> - reachability depth (default 0)
        -h/--help - help message
        --version - version of the tool
        --verbose - output computation details

This version of ProbReach computes exact -k step probabilistic reachability. When using a dReach version that supports up to -k steps reachability (with-l and -u flags) -l must be specified and equal to -k.

ProbReach v1.0

To run ProbReach use the following version of dReal/dReach

Usage:

./ProbReach <options> <model-file.pdrh>:

options:

-e <double> - length of probability interval or maximum length of the box (default 0.001)
-d <double> - prescision used to call dReach (default 0.001)
-l <string> - full path to dReach binary (default empty)
-k <int> - reachability depth (default 0)