|
(* Title: HOL/HOLCF/IOA/ABP/Env.thy
Author: Olaf Müller
*)
section \<open>The environment\<close>
theory Env
imports IOA.IOA Action
begin
type_synonym
'm env_state = bool \ \give next bit to system\
definition
env_asig :: "'m action signature" where
"env_asig == ({Next},
UN m. {S_msg(m)},
{})"
definition
env_trans :: "('m action, 'm env_state)transition set" where
"env_trans =
{tr. let s = fst(tr);
t = snd(snd(tr))
in case fst(snd(tr))
of
Next => t=True |
S_msg(m) => s=True & t=False |
R_msg(m) => False |
S_pkt(pkt) => False |
R_pkt(pkt) => False |
S_ack(b) => False |
R_ack(b) => False}"
definition
env_ioa :: "('m action, 'm env_state)ioa" where
"env_ioa = (env_asig, {True}, env_trans,{},{})"
axiomatization
"next" :: "'m env_state => bool"
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
