Theory CAVA_Abstract

section ‹Abstract Model-Checker›
theory CAVA_Abstract
imports 
  CAVA_Base.CAVA_Base
  CAVA_Automata.Automata
  LTL.LTL
begin
text ‹
  This theory defines the abstract version of the cava model checker, 
  as well as a generic implementation.
›

subsection ‹Specification of an LTL Model-Checker›
text ‹
  Abstractly, an LTL model-checker consists of three components:
  \begin{enumerate}
    \item A conversion of LTL-formula to Indexed Generalized Buchi Automata 
      (IGBA) over sets of atomic propositions.       
    \item An intersection construction, which takes a system and an IGBA, and 
      creates an Indexed Generalized Buchi Graph (IGBG) and a projection 
      function to project runs of the IGBG back to runs of the system.
    \item An emptiness check for IGBGs.
  \end{enumerate}
›

text ‹Given an LTL formula, the LTL to Buchi conversion
  returns a Generalized Buchi Automaton that accepts the same language.›
definition ltl_to_gba_spec 
  :: "'prop ltlc ⇒ ('q, 'prop set, _) igba_rec_scheme nres"
  ― ‹Conversion of LTL formula to generalized buchi automaton›  
  where "ltl_to_gba_spec φ ≡ SPEC (λgba. 
    igba.lang gba = language_ltlc φ ∧ igba gba ∧ finite ((g_E gba)⇧* `` g_V0 gba))"

definition inter_spec 
  :: "('s,'prop set,_) sa_rec_scheme 
  ⇒ ('q,'prop set,_) igba_rec_scheme
  ⇒ (('prod_state,_) igb_graph_rec_scheme × ('prod_state ⇒ 's)) nres"
  ― ‹Intersection of system and IGBA›
  where "⋀sys ba. inter_spec sys ba ≡ do {
    ASSERT (sa sys);
    ASSERT (finite ((g_E sys)⇧* `` g_V0 sys));
    ASSERT (igba ba);
    ASSERT (finite ((g_E ba)⇧* `` g_V0 ba));
    SPEC (λ(G,project). igb_graph G ∧ finite ((g_E G)⇧* `` g_V0 G) ∧ (∀r. 
      (∃r'. igb_graph.is_acc_run G r' ∧ r = project o r')
        ⟷ (graph_defs.is_run sys r ∧ sa_L sys o r ∈ igba.lang ba)))
  }"


definition find_ce_spec 
  :: "('q,_) igb_graph_rec_scheme ⇒ 'q word option option nres"
  ― ‹Check Generalized Buchi graph for emptiness, with optional counterexample›
  where "find_ce_spec G ≡ do {
    ASSERT (igb_graph G);
    ASSERT (finite ((g_E G)⇧* `` g_V0 G));
    SPEC (λres. case res of 
      None ⇒ (∀r. ¬igb_graph.is_acc_run G r)
    | Some None ⇒ (∃r. igb_graph.is_acc_run G r)
    | Some (Some r) ⇒ igb_graph.is_acc_run G r
    )}"

text ‹
  Using the specifications from above, we can specify the essence
  of the model-checking algorithm: Convert the LTL-formula to a GBA,
  make an intersection with the system and check the result for emptiness.
›

definition abs_model_check 
  :: "'ba_state itself ⇒ 'ba_more itself 
  ⇒ 'prod_state itself ⇒ 'prod_more itself
  ⇒ ('s,'prop set,_) sa_rec_scheme ⇒ 'prop ltlc 
  ⇒ 's word option option nres"
  where
  "abs_model_check _ _ _ _ sys φ ≡ do {
    gba :: ('ba_state,_,'ba_more) igba_rec_scheme 
      ← ltl_to_gba_spec (Not_ltlc φ);
    ASSERT (igba gba);
    ASSERT (sa sys);
    (Gprod::('prod_state,'prod_more)igb_graph_rec_scheme, map_state) 
      ← inter_spec sys gba;
    ASSERT (igb_graph Gprod);
    ce ← find_ce_spec Gprod;

    case ce of
      None ⇒ RETURN None
    | Some None ⇒ RETURN (Some None)
    | Some (Some r) ⇒ RETURN (Some (Some (map_state o r)))
  }"

text ‹
  The main correctness theorem states that our abstract model checker
  really checks whether the system satisfies the formula, and a
  correct counterexample is returned (if any). 
  Note that, if the model does not satisfy the formula, 
  returning a counterexample is optional.
›
theorem abs_model_check_correct:
  "abs_model_check T1 T2 T3 T4 sys φ ≤ do {
    ASSERT (sa sys);
    ASSERT (finite ((g_E sys)⇧* `` g_V0 sys));
    SPEC (λres. case res of
      None ⇒ sa.lang sys ⊆ language_ltlc φ
    | Some None ⇒ ¬ sa.lang sys ⊆ language_ltlc φ
    | Some (Some r) ⇒ graph_defs.is_run sys r ∧ sa_L sys ∘ r ∉ language_ltlc φ)
  }"
  unfolding abs_model_check_def ltl_to_gba_spec_def inter_spec_def 
    find_ce_spec_def
  apply (refine_rcg refine_vcg ASSERT_leI le_ASSERTI)
  apply (auto simp: sa.lang_def
    sa.accept_def[THEN meta_eq_to_obj_eq, THEN ext[of "sa.accept sys"] ]) 
    (* TODO: We really need an extended abs_def attribute, that digests 
      conditional definitions! *)
  done

subsection ‹Generic Implementation›
text ‹
  In this section, we define a generic implementation of an LTL model checker,
  that is parameterized with implementations of its components.
›

abbreviation "ltl_rel ≡ Id :: ('a ltlc × _) set"

locale impl_model_checker =
  ― ‹Assembly of a generic model-checker›
  fixes sa_rel :: "('sai × ('s,'prop set,'sa_more) sa_rec_scheme) set"
  fixes igba_rel :: "('igbai × ('q, 'prop set, 'igba_more) igba_rec_scheme) set"
  fixes igbg_rel :: "('igbgi × ('sq, 'igbg_more) igb_graph_rec_scheme) set"
  fixes ce_rel :: "('cei × 'sq word) set"
  fixes mce_rel :: "('mcei × 's word) set"
  
  fixes ltl_to_gba_impl :: "'cfg_l2b ⇒ 'prop ltlc ⇒ 'igbai"
  fixes inter_impl :: "'cfg_int ⇒ 'sai ⇒ 'igbai ⇒ 'igbgi × ('sq ⇒ 's)"
  fixes find_ce_impl :: "'cfg_ce ⇒ 'igbgi ⇒ 'cei option option"
  fixes map_run_impl :: "('sq ⇒ 's) ⇒ 'cei ⇒ 'mcei"

  assumes [relator_props, simp, intro!]: "single_valued mce_rel"

  assumes ltl_to_gba_refine: 
    "⋀cfg. (ltl_to_gba_impl cfg,ltl_to_gba_spec) 
      ∈ ltl_rel → ⟨igba_rel⟩plain_nres_rel"
  assumes inter_refine: 
    "⋀cfg. (inter_impl cfg,inter_spec) 
      ∈ sa_rel → igba_rel → ⟨igbg_rel ×⇩r (Id → Id)⟩plain_nres_rel"
  assumes find_ce_refine: 
    "⋀cfg. (find_ce_impl cfg,find_ce_spec)
      ∈ igbg_rel → ⟨⟨⟨ce_rel⟩option_rel⟩option_rel⟩plain_nres_rel"

  assumes map_run_refine: "(map_run_impl,(o)) ∈ (Id → Id) → ce_rel → mce_rel"


begin


  fun cfg_l2b where "cfg_l2b (c1,c2,c3) = c1"
  fun cfg_int where "cfg_int (c1,c2,c3) = c2"
  fun cfg_ce where "cfg_ce (c1,c2,c3) = c3"

  definition impl_model_check 
    :: "('cfg_l2b×'cfg_int×'cfg_ce) 
      ⇒ 'sai ⇒ 'prop ltlc ⇒ 'mcei option option"
    where
    "impl_model_check cfg sys φ ≡ let
      ba = ltl_to_gba_impl (cfg_l2b cfg) (Not_ltlc φ);
      (G,map_q) = inter_impl (cfg_int cfg) sys ba;
      ce = find_ce_impl (cfg_ce cfg) G
    in
      case ce of
        None ⇒ None
      | Some None ⇒ Some None
      | Some (Some ce) ⇒ Some (Some (map_run_impl map_q ce))"
  
  lemma impl_model_check_refine:
    "(impl_model_check cfg,abs_model_check 
        TYPE('q) TYPE('igba_more) TYPE('sq) TYPE('igbg_more)) 
      ∈ sa_rel → ltl_rel → ⟨⟨⟨mce_rel⟩option_rel⟩option_rel⟩plain_nres_rel"
    apply (intro fun_relI plain_nres_relI)
    unfolding abs_model_check_def impl_model_check_def

    apply (simp only: let_to_bind_conv pull_out_let_conv 
      pull_out_RETURN_case_option)

    apply (refine_rcg
      ltl_to_gba_refine[param_fo, THEN plain_nres_relD]
      rel_arg_cong[where f="Not_ltlc"]
      inter_refine[param_fo, THEN plain_nres_relD]
      find_ce_refine[param_fo, THEN plain_nres_relD]
    )

    apply (simp_all split: option.split)
    apply (auto elim: option_relE)
    apply (parametricity add: map_run_refine)
    apply simp
    done

  theorem impl_model_check_correct:
    assumes R: "(sysi,sys)∈sa_rel"
    assumes [simp]: "sa sys" "finite ((g_E sys)⇧* `` g_V0 sys)"
    shows "case impl_model_check cfg sysi φ of
      None 
        ⇒ sa.lang sys ⊆ language_ltlc φ
    | Some None 
        ⇒ ¬ sa.lang sys ⊆ language_ltlc φ
    | Some (Some ri) 
        ⇒ (∃r. (ri,r)∈mce_rel 
           ∧ graph_defs.is_run sys r ∧ sa_L sys o r ∉ language_ltlc φ)"
  proof -
    note impl_model_check_refine[
      where cfg=cfg,
      param_fo, 
      THEN plain_nres_relD, 
      OF R IdI[of φ]]
    also note abs_model_check_correct
    finally show ?thesis 
      apply (simp split: option.split)
      apply (simp add: refine_pw_simps pw_le_iff)
      apply (auto elim!: option_relE) []
      done
  qed

  theorem impl_model_check_correct_no_ce:
    assumes "(sysi,sys)∈sa_rel"
    assumes SA: "sa sys" "finite ((g_E sys)⇧* `` g_V0 sys)"
    shows "impl_model_check cfg sysi φ = None 
    ⟷ sa.lang sys ⊆ language_ltlc φ"
    using impl_model_check_correct[where cfg=cfg, OF assms, of φ]
    by (auto 
      split: option.splits 
      simp: sa.lang_def[OF SA(1)] sa.accept_def[OF SA(1), abs_def])

end


end