// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //

import ComputerArchitecture.AsynchronousCircuits.AsyncArbiter.*;

//ArbiterInContext
module AsyncArbiter (bool usr1_req, usr2_req, tok1_ack, tok2_ack, src_ack,
                          usr1_ack,usr2_ack,tok1_req,tok2_req,src_req,
                          ?del1,?del2,?del3,?del4,?del5,?del6,?del7,?del8,?del9,?del10){
       T1 : Server(false,tok1_req,tok1_ack);
    || T2 : Server(false,tok2_req,tok2_ack);
    || SR : Server(false,src_req,src_ack);
    || U1 : Client(usr1_ack,usr1_req);
    || U2 : Client(usr2_ack,usr2_req);
    || AR : CorrectedArbiter(usr1_req,usr2_req,tok1_ack,tok2_ack,src_ack,
                             usr1_ack,usr2_ack,tok1_req,tok2_req,src_req,
                             del1,del2,del3,del4,del5,del6,del7,del8,del9,del10);
} satisfies {
//    mutex :
//      A G !(usr1_ack & usr2_ack);
   // --------------------------------------------------------
   // four-phase protocol with user one
   // --------------------------------------------------------
   ack_until_no_req_usr1 :
        assert A G (usr1_ack -> [usr1_ack WU (!usr1_req)]);
   no_ack_until_req_usr1 :
        assert A G (!usr1_ack -> [(!usr1_ack) WU usr1_req]);

// counterexample:
//
//       del1 _____________________||
//       del2 _____________________||
//       del3 _____________-------_||
//       del4 _____________--______||
//       del5 _____________________||
//       del6 _____________________||
//
//   usr1_req __-------_-_-________||
//   usr1_ack ________-------_____-||
//
//   usr2_req _____________________||
//   usr2_ack _____________________||
//
//   tok1_req ____-------_-___-----||
//   tok1_ack _____-------_-___----||
//
//   tok2_req _____________________||
//   tok2_ack _____________________||
//
//    src_req ______-------_-___---||
//    src_ack _______-------_-___--||


   // --------------------------------------------------------
   // four-phase protocol with user two
   // --------------------------------------------------------
//    ack_until_no_req_usr2 :
//        A G (usr2_ack -> [usr2_ack WU (!usr2_req)]);
//    no_ack_until_req_usr2 :
//        A G (!usr2_ack -> [(!usr2_ack) WU usr2_req]);
//    req_until_ack_tok1 :
//        A G (tok1_req -> [tok1_req WU (tok1_ack)]);
//    req_until_ack_tok2 :
//        A G (tok2_req -> [tok2_req WU (tok2_ack)]);
//    req_until_ack_src :
//        A G (src_req -> [src_req WU (src_ack)]);
}