Drawing a symbolically encoded Kripke structure with a highlighted set of states as svg graphics. The function returns the state encoding as an array of variable assignments.

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.

This function is meant to be called from cgi;

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.

evaluate a BDD by a given variable assignment (i.e., assignment of atom indices)

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'.