Theory Gabow_SCC.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)  u0U0. path E u0 p v  P v  (vset p. ¬ P v)
    | None  u0U0. vE*``{u0}. ¬P v)
    }"

  lemma find_path_ex_rule:
    assumes "finite U0"
    assumes "finite (E*``U0)"
    assumes "vE*``U0. P v"
    shows "find_path E U0 P  SPEC (λr. 
      p v. r = Some (p,v)  P v  (vset p. ¬P v)  (u0U0. 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  vE+``{u0}. ¬P v)}"

  lemma (in -) find_path1_ex_rule:
    assumes "finite (E*``{u0})"
    assumes "vE+``{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