SSL Find_Path.thy

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<sup>*</sup>``{u0}. ¬P v)
    }"

  lemma find_path_ex_rule:
    assumes "finite U0"
    assumes "finite (E^*``U0)"
    assumes "∃v∈E<sup>*</sup>``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<sup>+</sup>``{u0}. ¬P v)}"

  lemma (in -) find_path1_ex_rule:
    assumes "finite (E^*``{u0})"
    assumes "∃v∈E<sup>+</sup>``{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