book( bId : BOOKID ) = 
    Acquire(bId,_) . 
    (
      ( | mId : [11 .. 20] : loan(mId,bId) )^*
    ||
      ( ||| mId : [11 .. 20] : reservation(mId,bId)^* )
    ).
    ( Sell(bId) | Discard(bId) ) ;
    
loan( mId : MEMBERID , bId : BOOKID ) =
    ( Lend(mId,bId,_) | Take(mId,bId,_) ).
    ( Renew(mId,bId,_)^* ).
    Return(mId,bId,_) ;
    
member(mId : MEMBERID ) =
    Join(mId,_,_).
    (
      ( ||| bId : [1 .. 10] : loan(mId,bId)^* )
    ||
      ( ||| bId : [1 .. 10] : reservation(mId,bId)^* )
    ||
      ( Modify_Member(mId,_) )^*
    ).
    Leave(mId) ;
    
reservation( mId : MEMBERID , bId : BOOKID ) =
    Reserve(mId,bId,_).
    ( Take(mId,bId,_) | Cancel(mId,bId) )