type CHECK is Boolean sorts CHECK opns bottom (*! constructor *) : -> CHECK check (*! constructor *) : -> CHECK eq : CHECK, CHECK -> Bool eqns forall x, y : CHECK ofsort Bool eq (x, x) = true; (* otherwise *) eq (x, y) = false; endtype (*---------------------------------------------------------------------------*) type DATA is CHECK sorts DATA opns d1 (*! constructor *) : -> DATA (* for verification, this type is restricted to a single value *) (* d2 {*! constructor *} : -> DATA *) crc : DATA -> CHECK eq : DATA, DATA -> Bool eqns forall x, y : DATA ofsort Bool eq (x, x) = true; (* otherwise *) eq (x, y) = false; ofsort CHECK crc (x) = check; endtype (*---------------------------------------------------------------------------*) type HEADER is CHECK sorts HEADER opns h1 (*! constructor *) : -> HEADER (* for verification, this type is restricted to a single value *) (* h2 {*! constructor *} : -> HEADER *) crc : HEADER -> CHECK eq : HEADER, HEADER -> Bool eqns forall x, y : HEADER ofsort Bool eq (x, x) = true; (* otherwise *) eq (x, y) = false; ofsort CHECK crc (x) = check; endtype (*---------------------------------------------------------------------------*) type ACK is CHECK sorts ACK opns a1 (*! constructor *) : -> ACK (* for verification, this type is restricted to a single value *) (* a2 {*! constructor *} : -> ACK *) crc : ACK -> CHECK eq : ACK, ACK -> Bool eqns forall x, y : ACK ofsort Bool eq (x, x) = true; (* otherwise *) eq (x, y) = false; ofsort CHECK crc (x) = check; endtype (*---------------------------------------------------------------------------*) type BOC is CHECK sorts BOC opns release (*! constructor *), hold (*! constructor *), no_op (*! constructor *) : -> BOC eq : BOC, BOC -> Bool eqns forall x, y : BOC ofsort Bool eq (x, x) = true; (* otherwise *) eq (x, y) = false; endtype (*---------------------------------------------------------------------------*) type PHY_AREQ is CHECK sorts PHY_AREQ opns fair (*! constructor *), immediate (*! constructor *) : -> PHY_AREQ eq : PHY_AREQ, PHY_AREQ -> Bool eqns forall x, y : PHY_AREQ ofsort Bool eq (x, x) = true; (* otherwise *) eq (x, y) = false; endtype (*---------------------------------------------------------------------------*) type PHY_ACONF is CHECK sorts PHY_ACONF opns won (*! constructor *), lost (*! constructor *) : -> PHY_ACONF eq : PHY_ACONF, PHY_ACONF -> Bool eqns forall x, y : PHY_ACONF ofsort Bool eq (x, x) = true; (* otherwise *) eq (x, y) = false; endtype (*---------------------------------------------------------------------------*) type SIGNAL is ACK, CHECK, DATA, HEADER, NaturalNumber sorts SIGNAL opns destsig (*! constructor *) : Nat -> SIGNAL headsig (*! constructor *) : HEADER, CHECK -> SIGNAL datasig (*! constructor *) : DATA, CHECK -> SIGNAL acksig (*! constructor *) : ACK, CHECK -> SIGNAL dhead (*! constructor *) : -> SIGNAL Start (*! constructor *) : -> SIGNAL End (*! constructor *) : -> SIGNAL Prefix (*! constructor *) : -> SIGNAL subactgap (*! constructor *) : -> SIGNAL Dummy (*! constructor *) : -> SIGNAL is_dest, is_header, is_data, is_ack, is_physig : SIGNAL -> Bool valid_hpart, valid_ack : SIGNAL -> Bool getdest : SIGNAL -> Nat getdcrc : SIGNAL -> CHECK getdata : SIGNAL -> DATA gethead : SIGNAL -> HEADER getack : SIGNAL -> ACK corrupt : SIGNAL -> SIGNAL eq : SIGNAL, SIGNAL -> Bool eqns forall n : Nat, c : CHECK, h : HEADER, d : DATA, a : ACK, s, s1, s2 : SIGNAL ofsort Bool is_dest (destsig (n)) = true; (* otherwise *) is_dest (s) = false; is_header (headsig (h, c)) = true; (* otherwise *) is_header (s) = false; is_data (datasig (d, c)) = true; (* otherwise *) is_data (s) = false; is_ack (acksig (a, c)) = true; (* otherwise *) is_ack (s) = false; is_physig (Start) = true; is_physig (End) = true; is_physig (Prefix) = true; is_physig (subactgap) = true; (* otherwise *) is_physig (s) = false; valid_ack (acksig (a, c)) = eq (c, check); (* otherwise *) valid_ack (s) = false; valid_hpart (headsig (h, c)) = eq (c, check); (* otherwise *) valid_hpart (s) = false; ofsort Nat getdest (destsig (n)) = n; (* otherwise getdest (s) is undefined *) ofsort HEADER gethead (headsig (h, c)) = h; (* otherwise gethead (s) is undefined *) ofsort CHECK getdcrc (datasig (d, c)) = c; (* otherwise getdcrc (s) is undefined *) ofsort DATA getdata (datasig (d, c)) = d; (* otherwise getdata (s) is undefined *) ofsort ACK getack (acksig (a, c)) = a; (* otherwise getack (s) is undefined *) ofsort SIGNAL corrupt (headsig (h, c)) = headsig (h, bottom); corrupt (datasig (d, c)) = datasig (d, bottom); corrupt (acksig (a, c)) = acksig (a, bottom); ofsort Bool eq (s1, s1) = true; (* otherwise *) eq (s1, s2) = false; endtype (*---------------------------------------------------------------------------*) type SIG_TUPLE is Boolean, SIGNAL sorts SIG_TUPLE opns quadruple (*! constructor *) : SIGNAL, SIGNAL, SIGNAL, SIGNAL -> SIG_TUPLE void (*! constructor *) : -> SIG_TUPLE first, second, third, fourth : SIG_TUPLE -> SIGNAL is_void : SIG_TUPLE -> Bool eqns forall s1, s2, s3, s4 : SIGNAL ofsort SIGNAL first (quadruple (s1, s2, s3, s4)) = s1; second (quadruple (s1, s2, s3, s4)) = s2; third (quadruple (s1, s2, s3, s4)) = s3; fourth (quadruple (s1, s2, s3, s4)) = s4; ofsort Bool is_void (void) = true; is_void (quadruple (s1, s2, s3, s4)) = false; endtype (*---------------------------------------------------------------------------*) type LIN_DCONF is ACK sorts LIN_DCONF opns ackrec (*! constructor *) : ACK -> LIN_DCONF ackmiss (*! constructor *), broadsent (*! constructor *) : -> LIN_DCONF endtype (*---------------------------------------------------------------------------*) type LIN_DIND is Boolean, DATA, HEADER sorts LIN_DIND opns good (*! constructor *), broadrec (*! constructor *) : HEADER, DATA -> LIN_DIND dcrc_err (*! constructor *) : HEADER -> LIN_DIND is_broadrec : LIN_DIND -> Bool eqns forall h: HEADER, d: DATA, xind: LIN_DIND ofsort Bool is_broadrec (broadrec (h, d)) = true; (* otherwise *) is_broadrec (xind) = false; endtype (*---------------------------------------------------------------------------*) type BoolTABLE is Boolean, NaturalNumber sorts BoolTABLE opns empty (*! constructor *) : -> BoolTABLE btable (*! constructor *) : Nat, Bool, BoolTABLE -> BoolTABLE init : Nat -> BoolTABLE invert : Nat, BoolTABLE -> BoolTABLE get : Nat, BoolTABLE -> Bool zero, one, more : BoolTABLE -> Bool eqns forall n, n1, n2 : Nat, b : Bool, t : BoolTABLE ofsort BoolTABLE init (0) = empty; init (Succ (n)) = btable (n, false, init (n)); invert (n, empty) = empty; n1 eq n2 => invert (n1, btable (n2, b, t)) = btable (n2, not (b), t); n1 ne n2 => invert (n1, btable (n2, b, t)) = btable (n2, b, invert (n1, t)); ofsort Bool (* get (n, empty) is undefined *) n1 eq n2 => get (n1, btable (n2, b, t)) = b; n1 ne n2 => get (n1, btable (n2, b, t)) = get (n1, t); ofsort Bool zero (empty) = true; zero (btable (n, true, t)) = false; zero (btable (n, false, t)) = zero (t); one (empty) = false; one (btable (n, true, t)) = zero (t); one (btable (n, false, t)) = one (t); more (t) = not (zero (t)) and not (one (t)); endtype (*---------------------------------------------------------------------------*) type Version is sorts Version opns ko (*! constructor *), ok (*! constructor *) : -> Version endtype (*---------------------------------------------------------------------------*) type Scenario is Boolean, Natural sorts Scenario opns scenario_1 (*! constructor *), scenario_2 (*! constructor *), scenario_3_2 (*! constructor *), scenario_3_3 (*! constructor *), scenario_3_4 (*! constructor *) : -> Scenario _eq_ : Scenario, Scenario -> Bool eqns forall s1, s2: Scenario ofsort Bool s1 eq s1 = true; (* otherwise *) s1 eq s2 = false; endtype