Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Specify python2 instead of assuming default #357

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

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