This module implements functions for verification of safety properties using induction; in particular functions for incremental induction as used in property directed reachability (PDR). In contrast to reals PDR implementation that are based on SAT solvers (and clause sets), this version is based on BDDs.
Type  Description 
Function or value  Description 
Full Usage:
InitialChecks ostr now2nxtMap kripke
Parameters:
TextWriter
now2nxtMap : Map<AtomIndex, AtomIndex>
kripke : KripkeStructureBDD
Returns: (bool * BoolExpr list list) option

Perform the following initial checks for a safety property Φ(x), initial state predicate 𝒥(x) and transition relation 𝓡(x,x'):



Full Usage:
PropertyDirectedReachability ostr kripke
Parameters:
TextWriter
kripke : KripkeStructureBDD
Returns: bool * BoolExpr list list option

Given a safety property Φ(x), initial state predicate 𝒥(x) and a transition relation 𝓡(x,x'), this function first performs the initial setup checks by calling InitialChecks. If that is conclusive, nothing else is done, otherwise, the PDR loop is started. Having assertions ψ[0..k], it tries to construct a counterexample of length k+1 by finding a reachable state in ψ[k] with a successor outside of Φ. To that end, the validity of ψ[k](x) ⋀ 𝓡(x,x') ➞ Φ(x') is checked, and if a counterexample is found, the reachability of the a state in cube x is checked. If no subcube of cube x is reachable, cube c is removed from ψ[k] and the search for another counterexample is continued. If ψ[i]=ψ[i+1] should hold for some index i, we conclude that ψ[i] is inductive and we therefore can stop the proof search having a proof for the safety property Φ. If no counterexamples are found since ψ[k](x) ⋀ 𝓡(x,x') ➞ Φ(x') is finally valid, then the assertion list is extended by defining ψ[k+1] as the result of narrowing Φ by adding all clauses of ψ[k] that cover all successor states of ψ[k]. After this, the main loop repeats.




To refine the approximations of sets reachable in k steps when an unreachable cube has been found, we determine a minimal model, i.e., a model of a BDD that assigns Boolean values to a minimal number of variables. The negation of this model is then conjunctively added to the state sets to remove those unreachable states.


For a BDD that is not 0, the following function derives a model in terms of a cube (s,s') that consists of literals for the current variables s and the next variables s'.
