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_relplain_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_reloption_reloption_relplain_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_reloption_reloption_relplain_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