Theory FR_types

(*<*)
(*
   Title:  FR_types.thy  (Input/Output Definitions)
   Author: Maria Spichkova <maria.spichkova at rmit.edu.au>, 2013
*) 
(*>*)
section ‹FlexRay: Types› 


theory FR_types 
imports stream
begin

record 'a Message = 
   message_id :: nat
   ftcdata    :: 'a

record 'a Frame = 
   slot :: nat
   dataF :: "('a Message) list"

record Config = 
   schedule    :: "nat list" 
   cycleLength :: nat

type_synonym 'a nFrame = "nat ⇒ ('a Frame) istream"

type_synonym nNat = "nat ⇒ nat istream"

type_synonym nConfig = "nat ⇒ Config"

consts sN :: "nat"

definition 
  sheafNumbers :: "nat list"
where
 "sheafNumbers ≡ [sN]"

end