Theory FR

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

theory  FR 
imports FR_types
begin

subsection ‹Auxiliary predicates›

― ‹The predicate DisjointSchedules is true  for sheaf of channels of type Config,›
― ‹if all bus configurations have disjoint scheduling tables.›
definition
  DisjointSchedules :: "nat ⇒ nConfig ⇒ bool" 
where
 "DisjointSchedules n nC
  ≡
  ∀ i j. i < n ∧ j < n ∧ i ≠ j ⟶ 
  disjoint (schedule (nC i))  (schedule (nC j))" 

― ‹The predicate IdenticCycleLength is true  for sheaf of channels of type Config,› 
― ‹if all bus configurations have the equal length of the communication round.›
definition
   IdenticCycleLength :: "nat ⇒ nConfig ⇒ bool"
where
  "IdenticCycleLength n nC
   ≡
   ∀ i j. i < n ∧ j < n ⟶ 
   cycleLength (nC i) = cycleLength (nC j)"
   
― ‹The predicate FrameTransmission defines the correct message transmission:›
― ‹if the time t is equal modulo the length of the cycle (Flexray communication round)›
― ‹to the element of the scheduler table of the node k, then this and only this node›
― ‹can send a data atn the $t$th time interval.›
definition
   FrameTransmission :: 
     "nat ⇒ 'a nFrame ⇒ 'a nFrame ⇒ nNat ⇒ nConfig ⇒ bool"
where
  "FrameTransmission n nStore nReturn nGet nC
   ≡
   ∀ (t::nat) (k::nat). k < n ⟶
   ( let s = t mod (cycleLength (nC k))
     in 
     ( s mem (schedule (nC k))
       ⟶
       (nGet k t) = [s] ∧  
       (∀ j. j < n ∧ j ≠ k ⟶ 
            ((nStore j) t) =  ((nReturn k) t)) ))" 

― ‹The   predicate Broadcast describes properties of FlexRay broadcast.›
definition
   Broadcast :: 
     "nat ⇒ 'a nFrame ⇒ 'a Frame istream ⇒ bool"
where
  "Broadcast n nSend recv
   ≡ 
   ∀ (t::nat). 
    ( if ∃ k. k < n ∧ ((nSend k) t) ≠ []
      then (recv t) = ((nSend (SOME k. k < n ∧ ((nSend k) t) ≠ [])) t)
      else (recv t) = [] )"  
      
― ‹The predicate Receive defines the  relations on the streams  to represent› 
― ‹data receive by FlexRay controller.›
definition
  Receive :: 
  "'a Frame istream ⇒ 'a Frame istream ⇒ nat istream ⇒ bool"     
where
  "Receive recv store activation
   ≡
   ∀ (t::nat).
    ( if  (activation t) = []
      then (store t) = (recv t)
      else (store t) = [])"

― ‹The predicate Send defines the  relations on the streams  to represent›
― ‹sending data  by FlexRay controller.›
definition
  Send :: 
  "'a Frame istream ⇒ 'a Frame istream ⇒ nat istream ⇒ nat istream ⇒ bool"
where
  "Send return send get activation
   ≡
   ∀ (t::nat). 
   ( if  (activation t) = []
     then (get t) = [] ∧ (send t) = []
     else (get t) = (activation t) ∧ (send t) = (return t)  )"   
    
 
subsection ‹Specifications of the FlexRay components›

definition
   FlexRay :: 
  "nat ⇒ 'a nFrame ⇒ nConfig ⇒ 'a nFrame ⇒ nNat ⇒ bool"
where
  "FlexRay n nReturn nC nStore nGet
   ≡ 
   (CorrectSheaf n)  ∧  
   ((∀ (i::nat). i < n ⟶ (msg 1 (nReturn i))) ∧ 
    (DisjointSchedules n nC) ∧ (IdenticCycleLength n nC) 
   ⟶
    (FrameTransmission n nStore nReturn nGet nC) ∧ 
    (∀ (i::nat). i < n ⟶ (msg 1 (nGet i)) ∧ (msg 1 (nStore i))) )"

definition 
   Cable :: "nat ⇒ 'a nFrame ⇒ 'a Frame istream ⇒ bool" 
where
  "Cable n nSend recv 
   ≡
   (CorrectSheaf n) 
    ∧  
   ((inf_disj n nSend) ⟶ (Broadcast n nSend recv))"

definition
   Scheduler :: "Config ⇒ nat istream ⇒ bool"
where
  "Scheduler c activation
   ≡ 
   ∀ (t::nat).
   ( let s = (t mod (cycleLength c))
      in
       ( if  (s mem (schedule c))
         then (activation t) = [s]
         else (activation t) = []) )"
         
definition
  BusInterface :: 
    "nat istream ⇒ 'a Frame istream ⇒ 'a Frame istream ⇒ 
     'a Frame istream ⇒ 'a Frame istream ⇒ nat istream ⇒ bool"
where
  "BusInterface activation return recv  store send get
   ≡
   (Receive recv store activation) ∧
   (Send return send get activation)"


definition
   FlexRayController :: 
     "'a Frame istream ⇒ 'a Frame istream ⇒  Config ⇒
      'a Frame istream ⇒ 'a Frame istream ⇒ nat istream ⇒ bool"
where
  "FlexRayController return recv c store send get
   ≡
  (∃ activation. 
     (Scheduler c activation) ∧
     (BusInterface activation return recv store send get))"
 

definition
  FlexRayArchitecture :: 
   "nat ⇒ 'a nFrame ⇒ nConfig ⇒ 'a nFrame ⇒ nNat ⇒ bool"   
where
  "FlexRayArchitecture n nReturn nC nStore nGet
   ≡
   (CorrectSheaf n) ∧
   (∃ nSend recv.
     (Cable n nSend recv) ∧ 
     (∀ (i::nat). i < n ⟶  
         FlexRayController (nReturn i) recv (nC i) 
                           (nStore i) (nSend i) (nGet i)))"  
   
definition
  FlexRayArch :: 
   "nat ⇒ 'a nFrame ⇒ nConfig ⇒ 'a nFrame ⇒ nNat ⇒ bool"   
where
  "FlexRayArch n nReturn nC nStore nGet
   ≡
   (CorrectSheaf n)  ∧ 
   ((∀ (i::nat). i < n ⟶ msg 1 (nReturn i)) ∧ 
    (DisjointSchedules n nC) ∧ (IdenticCycleLength n nC)    
    ⟶
    (FlexRayArchitecture n nReturn nC nStore nGet))"    

end