Theory PromelaLTL

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

text ‹We have a semantic engine for Promela. But we need to have 
an integration with LTL -- more specificly, we must know when a proposition
is 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
of a system automaton, but @{typ nat} instead. This index then is used to look up the
corresponding @{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 simp add: in_set_member)

lemma ltlc_aps_list'_distinct:
  "distinct l  distinct (ltlc_aps_list' φ l)"
  by (induct φ arbitrary: l) (auto simp add: in_set_member)

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 nctr 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,g0) = Promela.setUp ast;
         (APs,φi) = PromelaLTL.ltl_convert φ
      in 
         ((prog, APs, g0), φi)"

lemma prepare_instrument[code]:
  "prepare cfg ast φ  
    let
         (_,printF) = cfg;
         _ = PromelaStatistics.start (); 
         (prog,g0) = Promela.setUp ast;
         _ = printF prog;
         (APs,φi) = PromelaLTL.ltl_convert φ;
         _ = PromelaStatistics.stop_timer ()
      in 
         ((prog, APs, g0), φ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,g0)=progg in 
           r 0 = g0 
         (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