(* Title: HOL/TLA/Buffer/Buffer.thy
Author: Stephan Merz, University of Munich
*)
section \<open>A simple FIFO buffer (synchronous communication, interleaving)\<close>
theory Buffer
imports "HOL-TLA.TLA"
begin
(* actions *)
definition BInit :: "'a stfun \ 'a list stfun \ 'a stfun \ stpred"
where "BInit ic q oc == PRED q = #[]"
definition Enq :: "'a stfun \ 'a list stfun \ 'a stfun \ action"
where "Enq ic q oc == ACT (ic$ \ $ic)
\<and> (q$ = $q @ [ ic$ ])
\<and> (oc$ = $oc)"
definition Deq :: "'a stfun \ 'a list stfun \ 'a stfun \ action"
where "Deq ic q oc == ACT ($q \ #[])
\<and> (oc$ = hd< $q >)
\<and> (q$ = tl< $q >)
\<and> (ic$ = $ic)"
definition Next :: "'a stfun \ 'a list stfun \ 'a stfun \ action"
where "Next ic q oc == ACT (Enq ic q oc \ Deq ic q oc)"
(* temporal formulas *)
definition IBuffer :: "'a stfun \ 'a list stfun \ 'a stfun \ temporal"
where "IBuffer ic q oc == TEMP Init (BInit ic q oc)
\<and> \<box>[Next ic q oc]_(ic,q,oc)
\<and> WF(Deq ic q oc)_(ic,q,oc)"
definition Buffer :: "'a stfun \ 'a stfun \ temporal"
where "Buffer ic oc == TEMP (\\q. IBuffer ic q oc)"
(* ---------------------------- Data lemmas ---------------------------- *)
(*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*)
lemma tl_not_self [simp]: "xs \ [] \ tl xs \ xs"
by (auto simp: neq_Nil_conv)
(* ---------------------------- Action lemmas ---------------------------- *)
(* Dequeue is visible *)
lemma Deq_visible: "\ _(ic,q,oc) = Deq ic q oc"
apply (unfold angle_def Deq_def)
apply (safe, simp (asm_lr))+
done
(* Enabling condition for dequeue -- NOT NEEDED *)
lemma Deq_enabled:
"\q. basevars (ic,q,oc) \ \ Enabled (_(ic,q,oc)) = (q \ #[])"
apply (unfold Deq_visible [temp_rewrite])
apply (force elim!: base_enabled [temp_use] enabledE [temp_use] simp: Deq_def)
done
(* For the left-to-right implication, we don't need the base variable stuff *)
lemma Deq_enabledE:
"\ Enabled (_(ic,q,oc)) \ (q \ #[])"
apply (unfold Deq_visible [temp_rewrite])
apply (auto elim!: enabledE simp add: Deq_def)
done
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
