Theory Gateway

(*<*)
(*
   Title:  Gateway.thy  (Gateway: Specification)
   Author: Maria Spichkova <maria.spichkova at rmit.edu.au>, 2013
*) 
(*>*)
section ‹Gateway: Specification›

theory Gateway 
imports Gateway_types
begin

definition
 ServiceCenter :: 
   "ECall_Info istream ⇒ aType istream ⇒ bool "
where
 "ServiceCenter i a 
  ≡ 
  ∀ (t::nat). 
  a 0 = [] ∧  a (Suc t) =  (if (i t) = [] then []  else [sc_ack])"

definition
  Loss ::
   "bool istream ⇒ aType istream ⇒ ECall_Info istream ⇒ 
    aType istream ⇒ ECall_Info istream ⇒ bool"
where
 "Loss lose a i2 a2 i 
  ≡ 
  ∀ (t::nat). 
  ( if lose t =  [False]
    then a2 t = a t ∧ i t = i2 t 
    else a2 t = []  ∧ i t = []   )"

definition
 Delay ::
  "aType istream ⇒ ECall_Info istream ⇒ nat ⇒ 
   aType istream ⇒ ECall_Info istream ⇒ bool"
where
 "Delay a2 i1 d a1 i2 
  ≡ 
  ∀ (t::nat).  
   (t < d ⟶ a1 t = [] ∧ i2 t = []) ∧ 
   (t ≥ d ⟶ (a1 t = a2 (t-d)) ∧ (i2 t = i1 (t-d)))"

definition
 tiTable_SampleT ::
 "reqType istream  ⇒ aType istream ⇒ 
  stopType istream ⇒ bool istream ⇒ 
  (nat ⇒ GatewayStatus) ⇒  (nat ⇒ ECall_Info list) ⇒
  GatewayStatus istream ⇒ ECall_Info istream ⇒ vcType istream 
  ⇒ (nat ⇒ GatewayStatus) ⇒ bool "
where
 "tiTable_SampleT req a1 stop lose st_in buffer_in 
         ack i1 vc st_out
  ≡
  ∀ (t::nat) 
     (r::reqType list) (x::aType list) 
     (y::stopType list) (z::bool list).
   ― ‹1:›
   ( st_in t = init_state ∧ req t = [init]
     ⟶ ack t = [call] ∧ i1 t = [] ∧ vc t = [] 
         ∧ st_out t = call ) 
   ∧     
   ― ‹2:›
   ( st_in t = init_state ∧ req t ≠ [init]
     ⟶  ack t = [init_state] ∧ i1 t = [] ∧ vc t = [] 
         ∧ st_out t = init_state ) 
   ∧
   ― ‹3:›
   ( (st_in t = call ∨ (st_in t = connection_ok ∧ r ≠ [send])) ∧
     req t = r ∧ lose t = [False]
     ⟶  ack t = [connection_ok] ∧ i1 t = [] ∧ vc t = [] 
         ∧ st_out t = connection_ok ) 
   ∧
   ― ‹4:›
   ( (st_in t = call ∨ st_in t = connection_ok ∨ st_in t = sending_data)
     ∧ lose t = [True]
     ⟶  ack t = [init_state] ∧ i1 t = [] ∧ vc t = [] 
         ∧ st_out t = init_state ) 
   ∧
   ― ‹5:›
   ( st_in t = connection_ok ∧ req t = [send] ∧ lose t = [False]
     ⟶ ack t = [sending_data] ∧ i1 t = buffer_in t ∧ vc t = [] 
         ∧ st_out t = sending_data ) 
   ∧
   ― ‹6:›
   ( st_in t = sending_data ∧ a1 t = [] ∧ lose t = [False]
     ⟶ ack t = [sending_data] ∧ i1 t = [] ∧ vc t = [] 
         ∧ st_out t = sending_data ) 
   ∧
   ― ‹7:›
   ( st_in t = sending_data ∧ a1 t = [sc_ack] ∧ lose t = [False]
     ⟶ ack t = [voice_com] ∧ i1 t = [] ∧ vc t = [vc_com] 
         ∧ st_out t = voice_com ) 
   ∧
   ― ‹8:›
   ( st_in t = voice_com ∧ stop t = [] ∧ lose t = [False]
     ⟶ ack t = [voice_com] ∧ i1 t = [] ∧ vc t = [vc_com] 
         ∧ st_out t = voice_com ) 
   ∧
   ― ‹9:›
   ( st_in t = voice_com ∧ stop t = [] ∧ lose t = [True]
     ⟶ ack t = [voice_com] ∧ i1 t = [] ∧ vc t = [] 
         ∧ st_out t = voice_com ) 
   ∧
   ― ‹10:›
   ( st_in t = voice_com ∧ stop t = [stop_vc] 
     ⟶ ack t = [init_state] ∧ i1 t = [] ∧ vc t = [] 
         ∧ st_out t = init_state )" 

definition
 Sample_L ::
 "reqType istream  ⇒ ECall_Info istream ⇒ aType istream ⇒ 
  stopType istream ⇒ bool istream ⇒ 
  (nat ⇒ GatewayStatus) ⇒  (nat ⇒ ECall_Info list) ⇒
  GatewayStatus istream ⇒ ECall_Info istream ⇒ vcType istream 
  ⇒ (nat ⇒ GatewayStatus)  ⇒ (nat ⇒ ECall_Info list)
  ⇒ bool "
where
 "Sample_L req dt a1 stop lose st_in buffer_in 
         ack i1 vc st_out buffer_out
  ≡
  (∀ (t::nat). 
   buffer_out t = 
    (if dt t = [] then buffer_in t  else dt t) )
  ∧ 
  (tiTable_SampleT req a1 stop lose st_in buffer_in 
                   ack i1 vc st_out)" 

definition
 Sample ::
 "reqType istream  ⇒ ECall_Info istream ⇒ aType istream ⇒ 
  stopType istream ⇒ bool istream ⇒ 
  GatewayStatus istream ⇒ ECall_Info istream ⇒ vcType istream
  ⇒ bool "
where
 "Sample req dt a1 stop lose  ack i1 vc 
  ≡
  ((msg (1::nat) req) ∧ 
   (msg (1::nat) a1)  ∧ 
   (msg (1::nat) stop)) 
  ⟶ 
  (∃ st buffer. 
  (Sample_L req dt a1 stop lose 
            (fin_inf_append [init_state] st)
            (fin_inf_append [[]] buffer)
            ack i1 vc st buffer) )"

definition
 Gateway :: 
   "reqType istream ⇒ ECall_Info istream ⇒ aType istream ⇒ 
    stopType istream ⇒ bool istream ⇒ nat ⇒
    GatewayStatus istream ⇒ ECall_Info istream ⇒ vcType istream
    ⇒ bool"
where
 "Gateway req dt a stop lose d ack i vc 
  ≡ ∃ i1 i2 x y. 
    (Sample req dt x stop lose ack i1 vc) ∧ 
    (Delay y i1 d x i2) ∧ 
    (Loss lose a i2 y i)"


definition
  GatewaySystem :: 
   "reqType istream ⇒ ECall_Info istream ⇒ 
    stopType istream ⇒ bool istream ⇒ nat ⇒
    GatewayStatus istream ⇒ vcType istream
    ⇒ bool"
where
 "GatewaySystem req dt stop lose d ack vc 
  ≡
  ∃ a i. 
 (Gateway req dt a stop lose d ack i vc) ∧ 
 (ServiceCenter i a)"

definition
 GatewayReq :: 
   "reqType istream ⇒ ECall_Info istream ⇒ aType istream ⇒ 
    stopType istream ⇒ bool istream ⇒ nat ⇒
    GatewayStatus istream ⇒ ECall_Info istream ⇒ vcType istream
    ⇒ bool"
where
 "GatewayReq req dt a stop lose d ack i vc 
  ≡  
 ((msg (1::nat) req) ∧  (msg (1::nat) a)  ∧ 
  (msg (1::nat) stop) ∧  (ts lose)) 
   ⟶
  (∀ (t::nat).
  ( ack t = [init_state] ∧ req (Suc t) = [init] ∧ 
    lose (t+1) = [False] ∧ lose (t+2) = [False]
    ⟶ ack (t+2) = [connection_ok]) 
  ∧ 
  ( ack t = [connection_ok] ∧ req (Suc t)  = [send] ∧  
    (∀ (k::nat). k ≤ (d+1) ⟶ lose (t+k) = [False]) 
    ⟶ i ((Suc t) + d) = inf_last_ti dt t 
        ∧  ack (Suc t) = [sending_data])
  ∧ 
  ( ack (t+d) = [sending_data] ∧ a (Suc t) = [sc_ack] ∧  
    (∀ (k::nat). k ≤ (d+1) ⟶ lose (t+k) = [False]) 
    ⟶ vc ((Suc t) + d) = [vc_com]) )"

definition
  GatewaySystemReq :: 
   "reqType istream ⇒ ECall_Info istream ⇒ 
    stopType istream ⇒ bool istream ⇒ nat ⇒
    GatewayStatus istream ⇒ vcType istream
    ⇒ bool"
where
 "GatewaySystemReq req dt  stop lose d ack vc 
  ≡
 ((msg (1::nat) req) ∧ (msg (1::nat) stop) ∧ (ts lose))
   ⟶
  (∀ (t::nat) (k::nat). 
  ( ack t = [init_state] ∧ req (Suc t) = [init]
  ∧ (∀ t1. t1 ≤ t ⟶ req t1 = [])
  ∧ req (t+2) = []
  ∧ (∀ m. m < k + 3 ⟶ req (t + m) ≠ [send])
  ∧  req (t+3+k)  = [send] ∧  inf_last_ti dt (t+2) ≠ []
  ∧ (∀ (j::nat). 
     j ≤ (4 + k + d + d) ⟶ lose (t+j) = [False]) 
  ⟶ vc (t + 4 + k + d + d) = [vc_com]) )"

end