src/HOL/HOLCF/IOA/ABP/Spec.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 42151 4da4fc77664b
child 59503 9937bc07202b
permissions -rw-r--r--
modernized header;
     1 (*  Title:      HOL/HOLCF/IOA/ABP/Spec.thy
     2     Author:     Olaf Müller
     3 *)
     4 
     5 section {* The specification of reliable transmission *}
     6 
     7 theory Spec
     8 imports IOA Action
     9 begin
    10 
    11 definition
    12   spec_sig :: "'m action signature" where
    13   sig_def: "spec_sig = (UN m.{S_msg(m)},
    14                        UN m.{R_msg(m)} Un {Next},
    15                        {})"
    16 
    17 definition
    18   spec_trans :: "('m action, 'm list)transition set" where
    19   trans_def: "spec_trans =
    20    {tr. let s = fst(tr);
    21             t = snd(snd(tr))
    22         in
    23         case fst(snd(tr))
    24         of
    25         Next =>  t=s |            (* Note that there is condition as in Sender *)
    26         S_msg(m) => t = s@[m]  |
    27         R_msg(m) => s = (m#t)  |
    28         S_pkt(pkt) => False |
    29         R_pkt(pkt) => False |
    30         S_ack(b) => False |
    31         R_ack(b) => False}"
    32 
    33 definition
    34   spec_ioa :: "('m action, 'm list)ioa" where
    35   ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans)"
    36 
    37 end