dreal3 icon indicating copy to clipboard operation
dreal3 copied to clipboard

Specify `python2` instead of assuming default

Open maxvonhippel opened this issue 4 years ago • 0 comments

Currently the script fails if your default python is version 3, in this fashion:

(base) max@max-XPS-13-9310:~/tools/dreal3/dReal-3.16.06.02-linux/bin$ ./dReach -k 10      bouncing_ball.drh --verbose --precision 0.001 --visualize
  File "<string>", line 1
    import os,sys; print os.path.realpath("./dReach")
                         ^
SyntaxError: invalid syntax
usage: ./dReach options <*.drh> <options to dReal>

dReach: Bounded Model Checking for for Nonlinear Hybrid Systems

OPTIONS:

   -k <N> / -u <N>  specify the upperbound of unrolling steps (default: 3)

   -l <N>           specify the lowerbound of unrolling steps (default: 0)

   -b               use BMC heuristic with disjunctive path encoding (default: do not use)

   -r               -b and filter unreachable modes from SMT encoding (default: do not use)

   -e               -r and filter continuous variables from SMT encoding (default: do not use)

   -d               disjunctive path encoding (default: do not use)

   -z               apply exit codes (default: do not use):
                                51 if SAT,
                                52 if UNSAT,
                                1 abnormal termination

   -n               parse new .drh file format (default: do not use)

   -s               parse new .drh file format and use synchronous encoding (default: do not use)
   
EXAMPLE:

   dReach -k 10      bouncing_ball.drh --verbose --precision 0.001 --visualize
   dReach -l 3 -u 10 bouncing_ball.drh --verbose --precision 0.001 --visualize

an easy fix is just to specify that you want to use version 2. On my system, and indeed on most systems, if you say python2 it'll use 2.7, which is probably what you intend.

Thanks for making contributions to dReal! Before opening a pull-request, please check the following things:

  • [ ] Run make and check the code compiles. Please try both of gcc and clang.
  • [ ] Run make format to run clang-format over your contributions.
  • [ ] Run make style and check there is no style error.
  • [ ] Follow our Git commit message convention.
  • [x] Ensure the PR description clearly describes the problem and solution. Include the relevant issue number if applicable.
  • [ ] Rebase your commits based on master branch of dreal/dreal3 repository.

maxvonhippel avatar Feb 20 '21 19:02 maxvonhippel