Theory CAVA_Abstract

section ‹Abstract Model-Checker›
theory CAVA_Abstract
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:
    \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.

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"
  "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 
  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! *)

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"


  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"
    "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
      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 

    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

  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
         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,
      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) []

  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])