An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
BSD 2-Clause "Simplified" License
14
stars
1
forks
source link
Modify qalpha execution modes and command-line arguments #136
This is an overhaul of the qalpha execution modes and their command-line arguments, as well as a clean-up and reorganization of the inference code. This includes:
Removal of unused functionality which requires excessive maintenance and code duplication, such as searching for individually inductive lemmas via --indiv or gradually weakening the Frontier using --gradual-advance.
Simplification of remaining functionality, such as replacing Frontier with the much simpler InductionFrame, and simplifying the run_qalpha code as a result.
Changes to command-line arguments:
Instead of inputting the precise quantifier configuration using a sequence of --quantifier, the default mode now uses the sort order in the module file to generate a default quantifier configuration which should be enough to prove safety for all EPR examples, (provided that their sorts are ordered correctly.) This also includes a default for the quantifier-free body, although these can be set manually as before using --qf-body, --cube-size, etc.
To manually set the quantifier configuration, a new flag --custom-quant is introduced. It can be used to define a sort ordering different than the one in the file, using a sequence of --sort arguments, or to define a precise configuration using a sequence of --quantifier arguments as before.
--disj and --search have been replaced with --no-disj and --no-search, respectively, which means that by default, qalpha now splits the transition relation disjunctively when making SMT queries, and executes a gradual search over sub-domains of the quantifier configuration rather than using the precise, maximal specification (which is now accessible via --no-search.)
Added --until-safe, which halts the execution once a fixpoint was found which proves safety.
Added --abort-unsafe, which aborts a fixpoint computation once it is evident that it cannot prove safety.
Additionally, due to the heavier use of the search functionality, the exploration of sub-domains has been modified. Specifically, the domain of the fixpoint computation begins from some size (currently 100), and each iteration grows by some factor which can be set using --growth-factor (current default: 5). Growing the domain involves adding the smallest uncovered sub-domains until it passes the threshold for that iteration.
Lastly, if a fixpoint has been found which proves safety, qalpha now prints both the entire fixpoint, as well as a minimized subset of it which is inductive and proves safety. This requires no extra computation, as this information exists in the UNSAT-cores generated by the safety check and by the inductiveness check of the fixpoint.
This is an overhaul of the qalpha execution modes and their command-line arguments, as well as a clean-up and reorganization of the inference code. This includes:
--indivor gradually weakening theFrontierusing--gradual-advance.Frontierwith the much simplerInductionFrame, and simplifying therun_qalphacode as a result.--quantifier, the default mode now uses the sort order in the module file to generate a default quantifier configuration which should be enough to prove safety for all EPR examples, (provided that their sorts are ordered correctly.) This also includes a default for the quantifier-free body, although these can be set manually as before using--qf-body,--cube-size, etc.--custom-quantis introduced. It can be used to define a sort ordering different than the one in the file, using a sequence of--sortarguments, or to define a precise configuration using a sequence of--quantifierarguments as before.--disjand--searchhave been replaced with--no-disjand--no-search, respectively, which means that by default, qalpha now splits the transition relation disjunctively when making SMT queries, and executes a gradual search over sub-domains of the quantifier configuration rather than using the precise, maximal specification (which is now accessible via--no-search.)--until-safe, which halts the execution once a fixpoint was found which proves safety.--abort-unsafe, which aborts a fixpoint computation once it is evident that it cannot prove safety.--growth-factor(current default: 5). Growing the domain involves adding the smallest uncovered sub-domains until it passes the threshold for that iteration.