IOA/example/Sender.thy
author clasohm
Wed, 02 Nov 1994 11:50:09 +0100
changeset 156 fd1be45b64bf
child 168 44ff2275d44f
permissions -rw-r--r--
added IOA to isabelle/HOL
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
156
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     1
Sender = IOA + Action + Multiset + List + "Lemmas" +
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     2
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     3
types
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     4
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     5
'm sender_state = "'m list * bool multiset * bool multiset * bool * bool"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     6
(*                messages   #sent           #received      header  mode *)
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     7
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     8
consts
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     9
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    10
sender_asig   :: "'m action signature"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    11
sender_trans  :: "('m action, 'm sender_state)transition set"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    12
sender_ioa    :: "('m action, 'm sender_state)ioa"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    13
sq            :: "'m sender_state => 'm list"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    14
ssent,srcvd   :: "'m sender_state => bool multiset"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    15
sbit          :: "'m sender_state => bool"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    16
ssending      :: "'m sender_state => bool"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    17
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    18
rules
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    19
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    20
sq_def       "sq == fst"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    21
ssent_def    "ssent == fst o snd"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    22
srcvd_def    "srcvd == fst o snd o snd"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    23
sbit_def     "sbit == fst o snd o snd o snd"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    24
ssending_def "ssending == snd o snd o snd o snd"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    25
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    26
sender_asig_def
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    27
  "sender_asig == <(UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    28
\                  UN pkt. {S_pkt(pkt)},                           \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    29
\                  {C_m_s,C_r_s}>"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    30
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    31
sender_trans_def "sender_trans ==                                     \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    32
\ {tr. let s = fst(tr);                                               \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    33
\          t = snd(snd(tr))                                           \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    34
\      in case fst(snd(tr))                                           \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    35
\      of                                                             \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    36
\      S_msg(m) => sq(t)=sq(s)@[m]   &                                \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    37
\                  ssent(t)=ssent(s) &                                \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    38
\                  srcvd(t)=srcvd(s) &                                \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    39
\                  sbit(t)=sbit(s)   &                                \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    40
\                  ssending(t)=ssending(s) |                          \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    41
\      R_msg(m) => False |                                            \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    42
\      S_pkt(pkt) => hdr(pkt) = sbit(s)      &                     \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    43
\                       (? Q. sq(s) = (msg(pkt)#Q))  &               \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    44
\                       sq(t) = sq(s)           &                     \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    45
\                       ssent(t) = addm(ssent(s),sbit(s)) &           \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    46
\                       srcvd(t) = srcvd(s) &                         \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    47
\                       sbit(t) = sbit(s)   &                         \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    48
\                       ssending(s)         &                         \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    49
\                       ssending(t) |                                 \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    50
\    R_pkt(pkt) => False |                                         \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    51
\    S_ack(b)   => False |                                         \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    52
\      R_ack(b) => sq(t)=sq(s)                  &                  \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    53
\                     ssent(t)=ssent(s)            &                  \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    54
\                     srcvd(t) = addm(srcvd(s),b)  &                  \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    55
\                     sbit(t)=sbit(s)              &                  \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    56
\                     ssending(t)=ssending(s) |                       \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    57
\      C_m_s => count(ssent(s),~sbit(s)) < count(srcvd(s),~sbit(s)) & \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    58
\               sq(t)=sq(s)       &                                   \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    59
\               ssent(t)=ssent(s) &                                   \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    60
\               srcvd(t)=srcvd(s) &                                   \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    61
\               sbit(t)=sbit(s)   &                                   \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    62
\               ssending(s)       &                                   \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    63
\               ~ssending(t) |                                        \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    64
\      C_m_r => False |                                               \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    65
\      C_r_s => count(ssent(s),sbit(s)) <= count(srcvd(s),~sbit(s)) & \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    66
\               sq(t)=tl(sq(s))      &                                \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    67
\               ssent(t)=ssent(s)    &                                \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    68
\               srcvd(t)=srcvd(s)    &                                \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    69
\               sbit(t) = (~sbit(s)) &                                \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    70
\               ~ssending(s)         &                                \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    71
\               ssending(t) |                                         \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    72
\      C_r_r(m) => False}"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    73
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    74
sender_ioa_def "sender_ioa == \
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    75
\ <sender_asig, {<[],{|},{|},False,True>}, sender_trans>"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    76
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    77
end