CTLFORM

var lostcycle, req, ack, m0, sreq, sack;

ctldc

-- Question 1
   MAXDCLEN( [[req]] && ([!ack]^<ack>) ) ;
-- verify the above estimate
   AG #[]( ([[req]] && slen >=9)  => <><ack>)# ;

-- Question 1(a)
MAXDCLEN( [[req]] && ((scount ack = 3)^<ack>)) ;
--verify the above estimate
AG # [] ([[req]] && (slen >=19) => (scount ack >= 3)) #  ;


-- Question 2
MAXDCLEN([[lostcycle]]) ;
-- Verify the above property
AG #[] ([[lostcycle]]   => (slen <= 4)) #  ;

-- Question 4
-- First-come-first-serve pairs
  AG #[]( (<!sreq>^[[req && !ack]]) => !<><sack>)# ;


SYSTEM smv system
aux1 m0;

OBSERVE
 lostcycle := 
    (e1.Request ||  e2.Request ||  e3.Request ||  e4.Request || e5.Request ) 
    &&  !(e1.ackout || e2.ackout || e3.ackout || e4.ackout || e5.ackout ) ;
 req := e3.Request ;
 ack := e3.ackout  ;
 sreq := e4.Request ;
 sack := e4.ackout ;
.