IOA/example/Spec.thy

added IOA to isabelle/HOL

Spec = List + IOA + Action +

consts

spec_sig   :: "'m action signature"
spec_trans :: "('m action, 'm list)transition set"
spec_ioa   :: "('m action, 'm list)ioa"

rules

sig_def "spec_sig == <UN m.{S_msg(m)}, \
\                     UN m.{R_msg(m)}, \
\                     {}>"

trans_def "spec_trans =                            \
\ {tr. let s = fst(tr);                            \
\          t = snd(snd(tr))                        \
\      in                                          \
\      case fst(snd(tr))                           \
\      of                                          \
\      S_msg(m) => t = s@[m]  |                    \
\      R_msg(m) => s = (m#t)  |                    \
\      S_pkt(pkt) => False |                    \
\      R_pkt(pkt) => False |                    \
\      S_ack(b) => False |                      \
\      R_ack(b) => False |                      \
\      C_m_s => False |                            \
\      C_m_r => False |                            \
\      C_r_s => False |                            \
\      C_r_r(m) => False}"

ioa_def "spec_ioa == <spec_sig, {[]}, spec_trans>"

end