(* test suite for the abracadabra protocol *)

(* sort bool / Booleans *)
let bool_values: bool = [true, false] ;

  true != false ;
  for p: bool in bool_values [[
    not (not (p)) = p ;
  ]]
  for p, q: bool in bool_values [[
    p and q = q and p ;
    p or q = q or p ;
  ]]

(* sort nat / Natural Numbers *)
let nat_values: nat = [0 of nat, Succ (0), Succ (Succ (0))] ;

  0 of nat != Succ (0) ;
  Succ (0) gt 0 ;
  Succ (Succ (0)) gt 0 ;
  Succ (Succ (0)) gt Succ (0) ;
  for m, n: nat in nat_values [[
    m gt n => m eq n = false ;
    m gt n => n gt m = false ;
  ]]

  (* equations from spec *)
  0 of nat eq 0 = true ;
  for m : nat in nat_values [[
    Succ (m) eq 0 = false ;
    0 eq Succ (m) = false ;
  ]]
  for m, n: nat in nat_values [[
    Succ (m) eq Succ (n) = m eq n ;
  ]]
  
  for m : nat in nat_values [[
    0 gt m = false ;
    Succ (m) gt 0 = true ;
  ]]
  for m, n: nat in nat_values [[
    Succ (m) gt Succ (n) = m gt n ;
  ]]

(* sort decdigit / Decimal Digits *)
  for m <> n : decdigit IN [0 of decdigit, 1, 2, 3, 4] [[
    m != n;
  ]]
  for m: decdigit IN [0 of decdigit, 1, 2, 3, 4, 5, 6, 7, 8, 9] [[
    m eq m;
  ]]

(* sort SP / service primitives *)
let ConSP: sp = [ConReq, ConInd, ConResp, ConConf] ;
let DatSP: sp = [DatReq (d1), DatInd (d1)] ;
let DisSP: sp = [DisReq, DisInd] ;

  for sp1 <> sp2 : sp IN ConSP | DatSP | DisSP [[
    sp1 != sp2;
  ]]

  isConReq (ConReq);
  isConInd (ConInd);
  isConResp (ConResp);
  isConConf (ConConf);

  isDatReq (DatReq (d1));
  isDatInd (DatInd (d1));

  isDisReq (DisReq);
  isDisInd (DisInd);

  for sp: SP in ConSP [[
    isCon (sp) ;
  ]]
  for sp: SP in DatSP | DisSP [[
    isCon (sp) = false ;
  ]]

  for sp: SP in DatSP [[
    isDat (sp) ;
  ]]
  for sp: SP in ConSP | DisSP [[
    isDat (sp) = false ;
  ]]

  for sp: SP in DisSP[[
    isDis (sp) ;
  ]]
  for sp: SP in ConSP | DatSP [[
    isDis (sp) = false ;
  ]]

(* sort bit / Bits for the alternating bit protocol *)
  A0 != A1 ;
  for b: bit in [A0, A1] [[
    next (next (b)) = b ;
  ]]

(* sort PDU / Protocol Data Units *)
  for pdu1 < pdu2 : pdu in [CR, CC, DT (A1, d1), AK (A1), DR, DC] [[
    pdu1 != pdu2;
  ]]

(* sort cmsp / Communications medium service primitives *)
  for pdu: PDU in [CR, CC, DT (A1, d1), AK (A1), DR, DC] [[
    UnitReq (pdu) != UnitInd (pdu);
    isUnitInd (UnitInd (pdu));
    isUnitReq (UnitReq (pdu));
    isUnitInd (UnitReq (pdu)) = false;
    isUnitReq (UnitInd (pdu)) = false;
  ]]

(* sort queue / fifo queue of sdu (service user data) *)

let qs: queue = [empty, empty+d1, empty+d1+d2, empty+d1+d2+d3] ;

  for q: queue in qs [[
    hasany (q) => first (q) = d1;
    hasany (q), hasany (advance (q)) =>
      first (advance (q)) = d2;
    hasany (q), hasany (advance (q)), hasany (advance (advance (q))) =>
      first (advance (advance (q))) = d3;
  ]]
  hasany (empty) = false;
  hasany (advance (empty+d1)) = false ;
  empty+d1 = advance (empty+d2+d1);

(* ------- *)
(* ------- *)
(* ------- *)
(* ------- *)
(* ------- *)
(* ------- *)
(* ------- *)
(* ------- *)
