-
Notifications
You must be signed in to change notification settings - Fork 0
Open
Description
Currently, the hyperqube.sh shell script uses /bin/sh as its primary interpreter. On Debian/Ubuntu Linux systems, this executable is linked to the dash shell, which does not run the script in the intended manner. See the error below for more info.
============ Unrolling with genQBF + Solving with QuAbS ============
generating QBF BMC...
exec/genqbf: wrong argument '-f'; option '-F' expects one of: AA AE EE EA EAA.
Parses a Boolean formula and generates a representation of the input formula
and generates output of the formula in some formats: Boolean (default) QCIR, QDIMACS, AIGER.
It can optionally transform the formula to cnf,dnf,nnf and perform simple simplifications.
-i input file
-a do not append "_A" and "_B" for systems A and B
-I input file for initial state for A
-R input file for transition relation for A
-J input file for initial state for B
-S input file for transition relation for B
-P property file
-F {AA|AE|EE|EA|EAA}format of the unrolling: AE, AA, EE, EA, or EAA
-ES solve a series of EXISTS with same initial state and transition relation
-AS solve a series of FORALL with same initial state and transition relation
-sem {OPT|PES|TER_OPT|TER_PES}semantics of the unrolling:(optimistic/pessimistic)
-k integer depth of the unrolling
-n transform variable ids to numeric
-M set the name of the model
-o output file
-f {qcir|qdimacs|qaiger}output format: qcir, qdimacs, qaiger
-c {dnf|cnf|nnf} convert to CNF or DNF
-s perform simplification after conversion
-p only parse the input formula and print it
--debug debug output information
--fast use tail recursive faster algorithms
-help Display this list of options
--help Display this list of options
solving QBF...
Aborted (core dumped)
This error can be easily avoided by prefixing the hyperqube.sh script with bash as in bash ./hyperqube.sh ....
A proper solution for this issue would be to change the default shell in the hyperqube.sh script to /bin/bash, which would guarantee a more unified experience across different platforms.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels