## ModelCheckingInduction Module

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.

### Types

 Type Description

### Functions and values

 Function or value Description  InitialChecks ostr now2nxtMap kripke  Full Usage: InitialChecks ostr now2nxtMap kripke Parameters: ostr : TextWriter now2nxtMap : Map 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'): 𝒥(x) ➞ Φ(x): if not valid, we have a counterexample of length 0 𝒥(x) ⋀ 𝓡(x,x') ➞ Φ(x'): if not valid, we have a counterexample of length 1 since x' is then a successor of initial state x violating Φ 𝒥(x) ⋀ 𝓡(x,x') ➞ 𝒥(x'): if valid, we have a proof, since the initial states 𝒥(x) are all reachable states and satisfy Φ due to the first check Φ(x) ⋀ 𝓡(x,x') ➞ Φ(x'): if valid, we have a proof, since the safety property Φ is inductive and holds on all initial states After these checks, we may have a proof, a counterexample of length 0 or 1, or do not have a decision about whether Φ holds on all reachable states. The function may therefore return one of the following results: Some(true,[]): means that the safety property Φ(x) has been proved Some(false,[s0]): means that the safety property Φ(x) is disproved since s0 is an initial state that violates it Some(false,[s0;s1]): means that the safety property Φ(x) is disproved since s0 is an initial state and s1 a successor of it that violates the safety property Φ(x) None: means that the initial checks could not decide about the validity of Φ(x), so that [𝒥(x);Φ(x)] can be used to start PDR. ostr : TextWriter now2nxtMap : Map kripke : KripkeStructureBDD Returns: (bool * BoolExpr list list) option  ModelCheckingWithInductionTool qscoll  Full Usage: ModelCheckingWithInductionTool qscoll Parameters: qscoll : NameValueCollection This function is meant to be called from cgi; qscoll : NameValueCollection  PropertyDirectedReachability ostr kripke  Full Usage: PropertyDirectedReachability ostr kripke Parameters: ostr : 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. ostr : TextWriter kripke : KripkeStructureBDD Returns: bool * BoolExpr list list option  evalBDD m bddAdr  Full Usage: evalBDD m bddAdr Parameters: m : Map bddAdr : BddAdr Returns: bool evaluate a BDD by a given variable assignment (i.e., assignment of atom indices) m : Map bddAdr : BddAdr Returns: bool  getMinimalModel phi  Full Usage: getMinimalModel phi Parameters: phi : BddAdr Returns: BoolExpr list * BoolExpr list 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. phi : BddAdr Returns: BoolExpr list * BoolExpr list  getModel phi  Full Usage: getModel phi Parameters: phi : BddAdr Returns: BoolExpr list * BoolExpr list 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'. phi : BddAdr Returns: BoolExpr list * BoolExpr list