Quelle  Qmsg.thy

(*  Title:       Qmsg.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
*)

section "Model the standard queuing model"

theory Qmsg
imports AWN_SOS_Labels AWN_Invariants
begin

text ‹Define the queue process›

fun Γ_QMSG :: "('m list, 'm, unit, unit label) seqp_env"
where
  "Γ_QMSG () = labelled () (receive(λmsg msgs. msgs @ [msg]). call(())
           ⊕ ⟨msgs. msgs ≠ []⟩
               (send(λmsgs. hd msgs).
                 ([msgs. tl msgs] call(())
                  ⊕ receive(λmsg msgs. tl msgs @ [msg]). call(()))
              ⊕ receive(λmsg msgs. msgs @ [msg]). call(())))"

definition σ_QMSG :: "(('m::msg) list × ('m list, 'm, unit, unit label) seqp) set"
where "σ_QMSG ≡ {([], Γ_QMSG ())}"

abbreviation qmsg
  :: "(('m::msg) list × ('m list, 'm, unit, unit label) seqp, 'm seq_action) automaton"
where
  "qmsg ≡ ( init = σ_QMSG, trans = seqp_sos Γ_QMSG )"

declare Γ_QMSG.simps [simp del, code del]
lemmas Γ_{QMSG_simps} [simp, code] = Γ_QMSG.simps [simplified]

lemma σ_{QMSG_not_empty} [simp, intro]: "σ_QMSG ≠ {}"
  unfolding σ_{QMSG_def} by simp

lemma σ_{QMSG_exists} [simp]: "∃qmsg q. (qmsg, q) ∈ σ_QMSG"
  unfolding σ_{QMSG_def} by simp

lemma qmsg_wf [simp]: "wellformed Γ_QMSG"
  by (rule wf_no_direct_calls) auto

lemmas qmsg_labels_not_empty [simp] = labels_not_empty [OF qmsg_wf]

lemma qmsg_control_within [simp]: "control_within Γ_QMSG (init qmsg)"
  unfolding σ_{QMSG_def} by (rule control_withinI) (auto simp del: Γ_{QMSG_simps})

lemma qmsg_simple_labels [simp]: "simple_labels Γ_QMSG"
  unfolding simple_labels_def by auto

lemma qmsg_trans: "trans qmsg = seqp_sos Γ_QMSG"
  by simp

lemma σ_{QMSG_labels} [simp]: "(ξ, q) ∈ σ_QMSG ==> labels Γ_QMSG q = {()-:0}"
  unfolding σ_{QMSG_def} by simp

lemma qmsg_proc_cases [dest]:
  fixes p pn
  shows "p ∈ ctermsl (Γ_QMSG pn) ==> p ∈ ctermsl (Γ_QMSG ())"
  by simp

declare
  Γ_{QMSG_simps} [cterms_env]
  qmsg_proc_cases [ctermsl_cases]
  seq_invariant_ctermsI [OF qmsg_wf qmsg_control_within qmsg_simple_labels qmsg_trans, cterms_intros]
  seq_step_invariant_ctermsI [OF qmsg_wf qmsg_control_within qmsg_simple_labels qmsg_trans, cterms_intros]

end