Quelle  PromelaLTL.thy

section "LTL integration"
theory PromelaLTL
imports
  Promela
  LTL.LTL
begin

text ‹We have a semantic engine for Promela. But we need to have
  integration with LTL -- more specificly, we must know when a proposition
  true in a global state. This is achieved in this theory.›

subsection ‹LTL optimization›

text ‹For efficiency reasons, we do not store the whole @{typ expr} on the labels
  a system automaton, but @{typ nat} instead. This index then is used to look up the
  @{typ expr}.›

type_synonym APs = "expr iarray"

primrec ltlc_aps_list' :: "'a ltlc ==> 'a list ==> 'a list"
where
  "ltlc_aps_list' True_ltlc l = l"
| "ltlc_aps_list' False_ltlc l = l"
| "ltlc_aps_list' (Prop_ltlc p) l = (if List.member l p then l else p#l)"
| "ltlc_aps_list' (Not_ltlc x) l = ltlc_aps_list' x l"
| "ltlc_aps_list' (Next_ltlc x) l = ltlc_aps_list' x l"
| "ltlc_aps_list' (Final_ltlc x) l = ltlc_aps_list' x l"
| "ltlc_aps_list' (Global_ltlc x) l = ltlc_aps_list' x l"
| "ltlc_aps_list' (And_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"
| "ltlc_aps_list' (Or_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"
| "ltlc_aps_list' (Implies_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"
| "ltlc_aps_list' (Until_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"
| "ltlc_aps_list' (Release_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"
| "ltlc_aps_list' (WeakUntil_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"
| "ltlc_aps_list' (StrongRelease_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"

lemma ltlc_aps_list'_correct:
  "set (ltlc_aps_list' φ l) = atoms_ltlc φ ∪ set l"
  by (induct φ arbitrary: l) auto

lemma ltlc_aps_list'_distinct:
  "distinct l ==> distinct (ltlc_aps_list' φ l)"
  by (induct φ arbitrary: l) auto

definition ltlc_aps_list :: "'a ltlc ==> 'a list"
where
  "ltlc_aps_list φ = ltlc_aps_list' φ []"

lemma ltlc_aps_list_correct:
  "set (ltlc_aps_list φ) = atoms_ltlc φ"
  unfolding ltlc_aps_list_def
  by (force simp: ltlc_aps_list'_correct)

lemma ltlc_aps_list_distinct:
  "distinct (ltlc_aps_list φ)"
  unfolding ltlc_aps_list_def
  by (auto intro: ltlc_aps_list'_distinct)

primrec idx' :: "nat ==> 'a list ==> 'a ==> nat option" where
  "idx' _ [] _ = None"
| "idx' ctr (x#xs) y = (if x = y then Some ctr else idx' (ctr+1) xs y)"

definition "idx = idx' 0"

lemma idx'_correct:
  assumes "distinct xs"
  shows "idx' ctr xs y = Some n ⟷ n ≥ ctr ∧ n < length xs + ctr ∧ xs ! (n-ctr) = y"
using assms
proof (induction xs arbitrary: n ctr)
  case (Cons x xs)
  show ?case
  proof (cases "x=y")
    case True with Cons.prems have *: "y ∉ set xs" by auto
    {
      assume A: "(y#xs)!(n-ctr) = y"
      and less: "ctr ≤ n"
      and length: "n < length (y#xs) + ctr"
      have "n = ctr"
      proof (rule ccontr)
        assume "n ≠ ctr" with less have "n-ctr > 0" by auto
        moreover from ‹n≠ctr› length have "n-ctr < length(y#xs)" by auto
        ultimately have "(y#xs)!(n-ctr) ∈ set xs" by simp
        with A * show False by auto
      qed
    }
    with True Cons show ?thesis by auto
  next
    case False 
    from Cons have "distinct xs" by simp
    with Cons.IH False have "idx' (Suc ctr) xs y = Some n ⟷ Suc ctr ≤ n ∧ n < length xs + Suc ctr ∧ xs ! (n - Suc ctr) = y"
      by simp
    with False show ?thesis
      apply -
      apply (rule iffI)
      apply clarsimp_all
      done
  qed
qed simp

lemma idx_correct:
  assumes "distinct xs"
  shows "idx xs y = Some n ⟷ n < length xs ∧ xs ! n = y"
  using idx'_correct[OF assms]
  by (simp add: idx_def)

lemma idx_dom:
  assumes "distinct xs"
  shows "dom (idx xs) = set xs"
  by (auto simp add: idx_correct assms in_set_conv_nth)

lemma idx_image_self:
  assumes "distinct xs"
  shows "(the ∘ idx xs) ` set xs = {..<length xs}"
proof (safe)
  fix x
  assume "x ∈ set xs" with in_set_conv_nth obtain n where n: "n < length xs" "xs ! n = x" by metis
  with idx_correct[OF assms] have "idx xs x = Some n" by simp
  hence "the (idx xs x) = n" by simp
  with n show "(the ∘ idx xs) x < length xs" by simp
next
  fix n
  assume "n < length xs" 
  moreover with nth_mem have "xs ! n ∈ set xs" by simp
  then obtain x where "xs ! n = x" "x ∈ set xs" by simp_all
  ultimately have "idx xs x = Some n" by (simp add: idx_correct[OF assms])
  hence "the (idx xs x) = n" by simp
  thus "n ∈ (the ∘ idx xs) ` set xs" 
    using ‹x ∈ set xs›
    by auto
qed

lemma idx_ran:
  assumes "distinct xs"
  shows "ran (idx xs) = {..<length xs}"
  using ran_is_image[where M="idx xs"]
  using idx_image_self[OF assms] idx_dom[OF assms]
  by simp

lemma idx_inj_on_dom:
  assumes "distinct xs"
  shows "inj_on (idx xs) (dom (idx xs))"
  by (fastforce simp add: idx_dom assms in_set_conv_nth idx_correct
                intro!: inj_onI)

definition ltl_convert :: "expr ltlc ==> APs × nat ltlc" where
  "ltl_convert φ = (
      let APs = ltlc_aps_list φ;
          φ_i = map_ltlc (the ∘ idx APs) φ
      in (IArray APs, φ_i))"

lemma ltl_convert_correct:
  assumes "ltl_convert φ = (APs, φ_i)"
  shows "atoms_ltlc φ = set (IArray.list_of APs)" (is "?P1")
  and "atoms_ltlc φ_i = {..<IArray.length APs}" (is "?P2")
  and "φ_i = map_ltlc (the ∘ idx (IArray.list_of APs)) φ" (is "?P3")
  and "distinct (IArray.list_of APs)"
proof -
  let ?APs = "IArray.list_of APs"

  from assms have APs_def: "?APs = ltlc_aps_list φ"
    unfolding ltl_convert_def by auto

  with ltlc_aps_list_correct show APs_set: ?P1 by metis

  from assms show ?P3
    unfolding ltl_convert_def
    by auto

  from assms have "atoms_ltlc φ_i = (the ∘ idx ?APs) ` atoms_ltlc φ"
    unfolding ltl_convert_def
    by (auto simp add: ltlc.set_map)
  moreover from APs_def ltlc_aps_list_distinct show "distinct ?APs" by simp
  note idx_image_self[OF this]
  moreover note APs_set
  ultimately show ?P2 by simp
qed

definition prepare 
  :: "_ × (program ==> unit) ==> ast ==> expr ltlc ==> (program × APs × gState) × nat ltlc" 
  where
  "prepare cfg ast φ ≡
      let
         (prog,g₀) = Promela.setUp ast;
         (APs,φ_i) = PromelaLTL.ltl_convert φ
      in
         ((prog, APs, g₀), φ_i)"

lemma prepare_instrument[code]:
  "prepare cfg ast φ ≡
    let
         (_,printF) = cfg;
         _ = PromelaStatistics.start ();
         (prog,g₀) = Promela.setUp ast;
         _ = printF prog;
         (APs,φ_i) = PromelaLTL.ltl_convert φ;
         _ = PromelaStatistics.stop_timer ()
      in
         ((prog, APs, g₀), φ_i)"
  by (simp add: prepare_def)

export_code prepare checking SML

subsection ‹Language of a Promela program›

definition propValid :: "APs ==> gState ==> nat ==> bool" where
  "propValid APs g i ⟷ i < IArray.length APs ∧ exprArith g emptyProc (APs!!i) ≠ 0"

definition promela_E :: "program ==> (gState × gState) set"
  ― ‹Transition relation of a promela program›
where
  "promela_E prog ≡ {(g,g'). g' ∈ ls.α (nexts_code prog g)}"

definition promela_E_ltl :: "program × APs ==> (gState × gState) set" where
  "promela_E_ltl = promela_E ∘ fst"

definition promela_is_run' :: "program × gState ==> gState word ==> bool"
  ― ‹Predicate defining runs of promela programs›
where
  "promela_is_run' progg r ≡
      let (prog,g₀)=progg in
           r 0 = g₀
        ∧ (∀i. r (Suc i) ∈ ls.α (nexts_code prog (r i)))"

abbreviation "promela_is_run ≡ promela_is_run' ∘ setUp"

definition promela_is_run_ltl :: "program × APs × gState ==> gState word ==> bool"
where 
  "promela_is_run_ltl promg r ≡ let (prog,APs,g) = promg in promela_is_run' (prog,g) r"

definition promela_props :: "gState ==> expr set" 
where
  "promela_props g = {e. exprArith g emptyProc e ≠ 0}"

definition promela_props_ltl :: "APs ==> gState ==> nat set"
where
  "promela_props_ltl APs g ≡ Collect (propValid APs g)"

definition promela_language :: "ast ==> expr set word set" where
  "promela_language ast ≡ {promela_props ∘ r | r. promela_is_run ast r}"

definition promela_language_ltl :: "program × APs × gState ==> nat set word set" where
  "promela_language_ltl promg ≡ let (prog,APs,g) = promg in
                    {promela_props_ltl APs ∘ r | r. promela_is_run_ltl promg r}"

lemma promela_props_ltl_map_aprops:
  assumes "ltl_convert φ = (APs,φ_i)"
  shows "promela_props_ltl APs =
          map_props (idx (IArray.list_of APs)) ∘ promela_props"
proof -
  let ?APs = "IArray.list_of APs"
  let ?idx = "idx ?APs"

  from ltl_convert_correct assms have D: "distinct ?APs" by simp

  show ?thesis
  proof (intro ext set_eqI iffI)
    fix g i
    assume "i ∈ promela_props_ltl APs g"
    hence "propValid APs g i" by (simp add: promela_props_ltl_def)
    hence l: "i < IArray.length APs" "exprArith g emptyProc (APs!!i) ≠ 0" 
      by (simp_all add: propValid_def)
    hence "APs!!i ∈ promela_props g" by (simp add: promela_props_def)
    moreover from idx_correct l D have "?idx (APs!!i) = Some i" by fastforce
    ultimately show "i ∈ (map_props ?idx ∘ promela_props) g"
      unfolding o_def map_props_def
      by blast
  next
    fix g i
    assume "i ∈ (map_props ?idx ∘ promela_props) g"
    then obtain p where p_def: "p ∈ promela_props g" "?idx p = Some i" 
      unfolding map_props_def o_def 
      by auto
    hence expr: "exprArith g emptyProc p ≠ 0" by (simp add: promela_props_def)
  
    from D p_def have "i < IArray.length APs" "APs !! i = p"
      using idx_correct by fastforce+
    with expr have "propValid APs g i" by (simp add: propValid_def)
    thus "i ∈ promela_props_ltl APs g"
      by (simp add: promela_props_ltl_def)
  qed
qed

lemma promela_run_in_language_iff:
  assumes conv: "ltl_convert φ = (APs,φ_i)"
  shows "promela_props ∘ ξ ∈ language_ltlc φ
          ⟷ promela_props_ltl APs ∘ ξ ∈ language_ltlc φ_i" (is "?L ⟷ ?R")
proof -
  let ?APs = "IArray.list_of APs"

  from conv have D: "distinct ?APs"
    by (simp add: ltl_convert_correct)
  with conv have APs: "atoms_ltlc φ ⊆ dom (idx ?APs)"
    by (simp add: idx_dom ltl_convert_correct)

  note map_semantics = map_semantics_ltlc[OF idx_inj_on_dom[OF D] APs]
                       promela_props_ltl_map_aprops[OF conv]
                       ltl_convert_correct[OF conv]

  have "?L ⟷ (promela_props ∘ ξ) ⊨_c φ" by (simp add: language_ltlc_def)
  also have "... ⟷ (promela_props_ltl APs ∘ ξ) ⊨_c φ_i"
    using map_semantics
    by (simp add: o_assoc)
  also have "... ⟷ ?R"
    by (simp add: language_ltlc_def)
  finally show ?thesis .
qed

lemma promela_language_sub_iff:
  assumes conv: "ltl_convert φ = (APs,φ_i)"
  and setUp: "setUp ast = (prog,g)"
  shows "promela_language_ltl (prog,APs,g) ⊆ language_ltlc φ_i ⟷ promela_language ast ⊆ language_ltlc φ"
  using promela_run_in_language_iff[OF conv] setUp
  by (auto simp add: promela_language_ltl_def promela_language_def promela_is_run_ltl_def)


(* from PromelaDatastructures *)
hide_const (open) abort abortv 
                  err errv
                  usc
                  warn the_warn with_warn

hide_const (open) idx idx'
end