Skip to content

Commit

Permalink
Modify qalpha execution modes and command-line arguments (#136)
Browse files Browse the repository at this point in the history 
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.

---------

Signed-off-by: edenfrenkel <[email protected]>
  • Loading branch information
@edenfrenkel
edenfrenkel authored Jul 26, 2023
1 parent 17a52d3 commit 6c36c63
Show file tree
Hide file tree
Showing 12 changed files with 876 additions and 916 deletions.
13 changes: 7 additions & 6 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,15 +14,16 @@ correctness properties, including safety and liveness.
Run `./tools/download-solvers.sh` to get compatible versions of the supported SMT solvers (Z3, CVC5, and CVC4).

```sh
cargo run -- verify examples/lockserver.fly`
cargo run -- verify temporal-verifier/examples/lockserver.fly

cargo run -- infer qalpha examples/lockserver.fly --quantifier "F node 2" --qf-body cnf --clauses 1 --clause-size 3
cargo run -- infer qalpha temporal-verifier/examples/lockserver.fly --max-exist 0 --until-safe

env RUST_LOG=info cargo run --release -- \
infer qalpha examples/consensus_epr.fly --time \
--quantifier "E quorum 1" --quantifier "F node 3" --quantifier "F value 1" \
--max-size 3 --qf-body cnf --clauses 1 --clause-size 3
# note: this last example takes about two minutes to run
infer qalpha temporal-verifier/examples/consensus_epr.fly --time \
--custom-quant --sort quorum --sort node --sort value \
--max-exist 1 --abort-unsafe --until-safe --minimal-smt \
--extend-depth 1 --extend-width 10
# note: this last example takes several minutes to run
```

### Prerequisites
Expand Down
77 changes: 50 additions & 27 deletions inference/src/basics.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -293,35 +293,51 @@ impl FOModule {

if !core.add_counter_model(pre.clone(), Some(&unsat_core)) {
log::debug!("Found SAT with {} formulas in prestate.", core.len());
solver.save_tee();
return TransCexResult::CTI(pre, post);
}
}
Err(SolverError::Killed) => return TransCexResult::Cancelled,
Err(SolverError::Killed) => {
solver.save_tee();
return TransCexResult::Cancelled;
}
Err(SolverError::CouldNotMinimize(_)) => (),
Err(e) => panic!("error in solver: {e}"),
},
Ok(SatResp::Unsat) => {
assert!(separate_cores[t_idx].is_none());
let mut my_core = HashSet::new();
for ind in solver.get_unsat_core() {
if let Term::Id(s) = ind.0 {
let ind = s[6..].parse::<usize>().unwrap();
my_core.insert(ind);
unsat_core.insert(ind);
Ok(SatResp::Unsat) => match solver.get_unsat_core() {
Ok(solver_core) => {
assert!(separate_cores[t_idx].is_none());
let mut my_core = HashSet::new();
for ind in solver_core {
if let Term::Id(s) = ind.0 {
let ind = s[6..].parse::<usize>().unwrap();
my_core.insert(ind);
unsat_core.insert(ind);
}
}
}

if self.minimal {
assert_eq!(my_core, core.participants);
}
if self.minimal {
assert_eq!(my_core, core.participants);
}

separate_cores[t_idx] = Some(my_core);
break 'inner;
separate_cores[t_idx] = Some(my_core);
solver.save_tee();
break 'inner;
}
Err(SolverError::Killed) => {
solver.save_tee();
return TransCexResult::Cancelled;
}
Err(e) => panic!("error in solver: {e}"),
},
Err(SolverError::Killed) => {
solver.save_tee();
return TransCexResult::Cancelled;
}
Err(SolverError::Killed) => return TransCexResult::Cancelled,
Ok(SatResp::Unknown(_)) | Err(SolverError::CouldNotMinimize(_)) => (),
Err(e) => panic!("error in solver: {e}"),
}

solver.save_tee();
}
}
Expand All @@ -340,7 +356,6 @@ impl FOModule {
unsat_core.len(),
core_sizes
);

TransCexResult::UnsatCore(unsat_core)
}

Expand Down Expand Up @@ -380,6 +395,8 @@ impl FOModule {
}
SatResp::Unknown(reason) => panic!("sat solver returned unknown: {reason}"),
}

solver.save_tee();
}
}

Expand Down Expand Up @@ -533,7 +550,10 @@ impl FOModule {
}
SatResp::Unsat => {
// println!("adding group");
for (ind, b) in solver.get_unsat_core() {
for (ind, b) in solver
.get_unsat_core()
.expect("could not get unsat assumptions")
{
assert!(b, "got false in core");
// println!("adding to core: {}", clear_next(ind_to_term[&ind].clone()));
core.insert(clear_next(ind_to_term[&ind].clone()), b);
Expand Down Expand Up @@ -566,16 +586,16 @@ impl FOModule {
}
}

pub fn trans_safe_cex(&self, conf: &SolverConf, hyp: &[Term]) -> Option<Model> {
pub fn trans_safe_cex(&self, conf: &SolverConf, hyp: &[Term]) -> TransCexResult {
let mut core = HashSet::new();
for s in self.module.proofs.iter() {
if let TransCexResult::CTI(model, _) =
self.trans_cex(conf, hyp, &s.safety.x, false, true, None)
{
return Some(model);
match self.trans_cex(conf, hyp, &s.safety.x, false, true, None) {
TransCexResult::UnsatCore(new_core) => core.extend(new_core),
res => return res,
}
}

None
TransCexResult::UnsatCore(core)
}

pub fn safe_cex(&self, conf: &SolverConf, hyp: &[Term]) -> Option<Model> {
Expand All @@ -599,7 +619,7 @@ pub struct InferenceConfig {
pub cfg: QuantifierConfig,
pub qf_body: QfBody,

pub max_size: Option<usize>,
pub max_size: usize,
pub max_existentials: Option<usize>,

pub clauses: Option<usize>,
Expand All @@ -615,11 +635,14 @@ pub struct InferenceConfig {
pub disj: bool,
pub gradual_smt: bool,
pub minimal_smt: bool,
pub gradual_advance: bool,
pub indiv: bool,

pub extend_width: Option<usize>,
pub extend_depth: Option<usize>,

pub until_safe: bool,
pub abort_unsafe: bool,
pub no_search: bool,
pub growth_factor: Option<usize>,
}

pub fn parse_quantifier(
Expand Down
Loading

0 comments on commit 6c36c63

Please sign in to comment.