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