# 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 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 (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