# Theory Find_Path

section ‹Safety-Property Model-Checker\label{sec:find_path}›
theory Find_Path
imports
CAVA_Automata.Digraph
CAVA_Base.CAVA_Code_Target
begin
section ‹Finding Path to Error›
text ‹
This function searches a graph and a set of start nodes for a reachable
node that satisfies some property, and returns a path to such a node iff it
exists.
›
definition "find_path E U0 P ≡ do {
ASSERT (finite U0);
ASSERT (finite (E⇧*U0));
SPEC (λp. case p of
Some (p,v) ⇒ ∃u0∈U0. path E u0 p v ∧ P v ∧ (∀v∈set p. ¬ P v)
| None ⇒ ∀u0∈U0. ∀v∈E⇧*{u0}. ¬P v)
}"

lemma find_path_ex_rule:
assumes "finite U0"
assumes "finite (E⇧*U0)"
assumes "∃v∈E⇧*U0. P v"
shows "find_path E U0 P ≤ SPEC (λr.
∃p v. r = Some (p,v) ∧ P v ∧ (∀v∈set p. ¬P v) ∧ (∃u0∈U0. path E u0 p v))"
unfolding find_path_def
using assms
by (fastforce split: option.splits)

subsection ‹Nontrivial Paths›

definition "find_path1 E u0 P ≡ do {
ASSERT (finite (E⇧*{u0}));
SPEC (λp. case p of
Some (p,v) ⇒ path E u0 p v ∧ P v ∧ p≠[]
| None ⇒ ∀v∈E⇧+{u0}. ¬P v)}"

lemma (in -) find_path1_ex_rule:
assumes "finite (E⇧*{u0})"
assumes "∃v∈E⇧+{u0}. P v"
shows "find_path1 E u0 P ≤ SPEC (λr.
∃p v. r = Some (p,v) ∧ p≠[] ∧ P v ∧ path E u0 p v)"
unfolding find_path1_def
using assms
by (fastforce split: option.splits)

end