Skip to content

Conversation

@maxvonhippel
Copy link

@maxvonhippel maxvonhippel commented Feb 20, 2021

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.
  • 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.

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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant