Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
module main() // BAKERY2 (2 processes) enumerated p1,p2 {think, try, cs}; integer a,b; initial: a=0 and b=0 and p1=think and p2=think; restrict: a>=0 and b>=0; module process(y1,y2,pc) integer y1,y2; enumerated pc {think, try, cs}; a1: pc=think and y2'=y1+1 and pc'=try; a2: pc=try && pc'=cs && (y1=0 || y2=0 and b>=0 and c>=0; module process(y1,y2,y3,pc) integer y1,y2,y3; enumerated pc {think, try, cs}; a1: pc=think and (y3'=y1+1 or y3'=y2+1) and y3'>y1 and y3'>y2 and pc'=try; a2: pc=try and (y1=0 or y3 (p2!=cs and p3!=cs) ) endmodule module main() // TICKET2 (2 processes) enumerated p1,p2 {think, try, cs}; integer t,s; initial: t=s and p1=think and p2=think; restrict: t>=0 and s>=0; module process(pc) enumerated pc {think, try, cs}; integer a; a1: pc=think and a'=t and t'=t+1 and pc'=try; a2: pc=try and s>=a and pc'=cs; a3: pc=cs and s'=s+1 and pc'=think; process : a1 | a2 | a3; endmodule main: process(p1) | process(p2); spec: invariant( !(p1=cs and p2=cs) ) // spec: invariant(!(p1=try) || eventually( p1=cs )) endmodule module main() // TICKET3 (3 processes) enumerated p1,p2,p3 {think, try, cs}; integer t,s; initial: t=s and p1=think and p2=think and p3=think; restrict: t>=0 and s>=0; module process(pc) enumerated pc {think, try, cs}; integer a; a1: pc=think and a'=t and t'=t+1 and pc'=try; a2: pc=try and s>=a and pc'=cs; a3: pc=cs and s'=s+1 and pc'=think; process : a1 | a2 | a3; endmodule main: process(p1) | process(p2) | process(p3); spec: invariant( !(p1=cs and p2=cs or p1=cs and p3=cs or p2=cs and p3=cs) ) // spec: invariant(!(p1=try) || eventually( p1=cs )) endmodule module main() // BARBER // Sleeping barber monitor with 3 customer processes and 1 barber process integer barber, chair, open; initial: barber=0 and chair=0 and open=0; restrict: barber>=0 and chair>=0 and open>=0; module customerP() enumerated pc {s1,s2}; initial: pc=s1; a1: pc=s1 and barber>0 and barber'=barber-1 and chair'=chair+1 and pc'=s2; a2: pc=s2 and open>0 and open'=open-1 and pc'=s1; customerP: a1 | a2; endmodule module barberP() enumerated pc {s1,s2,s3,s4}; initial: pc=s1; a1: pc=s1 and barber'=barber+1 and pc'=s2; a2: pc=s2 and chair>0 and chair'=chair-1 and pc'=s3; a3: pc=s3 and open'=open+1 and pc'=s4; a4: pc=s4 and open=0 and pc'=s1; barberP: a1 | a2 | a3 | a4; endmodule main: customerP() | customerP() | customerP() | barberP() ; spec: invariant((chair<=1)) // spec: invariant((open<=1)) // spec: invariant((barber<=1)) endmodule module main() // BARBER // parameterized sleeping barber monitor // arbitary number of customer processes and one barber porcess integer barber, chair, open; initial: barber=0 and chair=0 and open=0; restrict: barber>=0 and chair>=0 and open>=0; module customerP() integer pc1, pc2; parameterized integer numC; initial: pc1=numC and pc2=0; restrict: numC>0 and pc1>=0 and pc2>=0; a1: pc1>0 and barber>0 and barber'=barber-1 and chair'=chair+1 and pc1'=pc1-1 and pc2'=pc2+1; a2: pc2>0 and open>0 and open'=open-1 and pc2'=pc2-1 and pc1'=pc1+1; customerP: a1 | a2; endmodule module barberP() enumerated pc {s1,s2,s3,s4}; initial: pc=s1; a1: pc=s1 and barber'=barber+1 and pc'=s2; a2: pc=s2 and chair>0 and chair'=chair-1 and pc'=s3; a3: pc=s3 and open'=open+1 and pc'=s4; a4: pc=s4 and open=0 and pc'=s1; barberP: a1 | a2 | a3 | a4; endmodule main: customerP() | barberP() ; // spec: invariant( chair<=1 ) // spec: invariant( open<=1 ) spec: invariant( barber<=1 ) endmodule module main() // COHERENCE // a parameterized cache coherence protocol boolean ex; enumerated state {Idle, ServeE, InvE, GrantE, ServeS, GrantS}; parameterized integer n; integer xNull, xWaitS, xWaitE, xShared, xExclusive; initial: state=Idle && !ex && xNull>=1 && xShared=0 && xExclusive=0 && xWaitE=0 && xWaitS=0; restrict: xNull>=0 && xWaitS>=0 && xWaitE>=0 && xShared>=0 && xExclusive>=0 && n>=1; module Request() reqS: state=Idle && xNull>=1 && state'=ServeS && xNull'=xNull-1 && xWaitS'=xWaitS+1; reqE1: state=Idle && xNull>=1 && state'=ServeE && xNull'=xNull-1 && xWaitE'=xWaitE+1; reqE2: state=Idle && xShared>=1 && state'=ServeE && xShared'=xShared-1 && xWaitE'=xWaitE+1; Request: reqS | reqE1 | reqE2; endmodule module Serve() inv: state=ServeS && ex && xExclusive>=1 && state'=GrantS && xExclusive'=xExclusive-1 && xNull'=xNull+1 && !ex'; nonex: state=ServeS && !ex && state'=GrantS; invS: state=ServeE && state'=InvE && xNull'=xNull+xShared && xShared'=0; invE: state=InvE && ex && xExclusive >=1 && state'=GrantE && xNull'=xNull+1 && xExclusive'=xExclusive-1 && !ex'; nonexE: state=InvE && !ex && state'=GrantE; Serve : inv | nonex | invS | invE | nonexE; endmodule module Grant() grantS: state=GrantS && xWaitS>=1 && state'= Idle && xWaitS'=xWaitS-1 && xShared'=xShared+1; grantE: state=GrantE && xWaitE>=1 && state'=Idle && xWaitE'=xWaitE-1 && xExclusive'=xExclusive+1 && ex'; Grant : grantS | grantE; endmodule main: Request() | Serve() | Grant(); spec: AG( !((xShared>=1 && xExclusive>=1) || xExclusive>=2) ) // spec: AG( xWaitS>=1 => AF( xShared>=1 )) // spec: AG( xWaitS>=n => AF( xShared>=n )) // spec: AG( xWaitE>=1 => AF( xExclusive>=1 )) endmodule module main() // SIS: Safety Injection system enumerated Pressure {TooLow, Permitted, TooHigh}; boolean Overridden, Block, Reset, Inject; parameterized integer low; parameterized integer permit; parameterized integer bound; integer wp1,wp2,wp3; initial: !Block and !Reset and !Inject and !Overridden and Pressure=Permitted and low<=wp1 and low<=wp2 and low<=wp3 and wp1=0 and permit>=0 and bound>=0 and wp1>=0 and wp2>=0 and wp3>=0; p1 : Pressure=TooLow and Pressure'=Permitted and (wp1'>=low and wp2'>=low and wp1'=low and wp3'>=low and wp1'=low and wp3'>=low and wp2'=low and wp2>=low and wp1=low and wp3>=low and wp1=low and wp3>=low and wp2=permit and wp2'>=permit or wp1'>=permit and wp3'>=permit or wp2'>=permit and wp3'>=permit) and !(wp1>=permit and wp2>=permit or wp1>=permit and wp3>=permit or wp2>=permit and wp3>=permit); p3 : Pressure=Permitted and Pressure'=TooLow and (wp1'=low and wp2'>=low and wp1'=low and wp3'>=low and wp1'=low and wp3'>=low and wp2'=low and wp2>=low and wp1=low and wp3>=low and wp1=low and wp3>=low and wp2 !Overridden) and ((Reset and Pressure=TooLow) => Inject) ) // spec: invariant( (Reset and !(Pressure=TooHigh)) => !Overridden ) // spec: invariant( (Reset and Pressure=TooLow) => Inject ) endmodule module main() // Office light-control enumerated Office {Empty, Occupied}; enumerated Occupants {One, Multiple}; enumerated Light {On, Off}; boolean enter, exit, turn_on, turn_off; integer count; initial : count=0 and Office=Empty; restrict: count >= 0 && (enter => !(exit || turn_on || turn_off)) && (exit => !(enter || turn_on || turn_off)) && (turn_on => !(enter || exit || turn_off)) && (turn_off => !(enter || exit || turn_on)); t1 : Office=Empty && enter && Office'=Occupied && Occupants'=One && Light'=On && count'=count+1; t2 : Office=Occupied && Occupants=One && exit && Office'=Empty && count'=count-1; t3 : Office=Occupied && Occupants=One && enter && count'=count+1 && Occupants'=Multiple; t4 : Office=Occupied && Occupants=Multiple && count=2 && exit && Occupants'=One && count'=count-1; t5 : Office=Occupied && Occupants=Multiple && count>2 && exit && count'=count-1; t6 : Office=Occupied && Occupants=Multiple && enter && count'=count+1; t7 : Office=Occupied && Light=On && turn_off && Occupants=One && Light'=Off; t8 : Office=Occupied && Light=Off && turn_on && Light'=On; t9 : Office=Occupied && Light=Off && enter && Light'=On; environment: (enter => !enter') && (exit => !exit') && (turn_on => !turn_on') && (turn_off => !turn_off'); main : (t1 | t2 | ((t3 | t4 | t5 | t6) & (t7 | t8 | t9))) & environment; // verified properties //spec: invariant( (Office=Occupied && Occupants=Multiple) => Light=On ) spec: invariant( count>1 <=> Office=Occupied && Occupants=Multiple ) // spec: invariant( count=1 <=> Office=Occupied && Occupants=One ) // spec: invariant( count=0 <=> Office=Empty ) // false properties to generate counter-example paths // spec: invariant( count>1 <=> Office=Occupied && Occupants=One ) // spec: invariant( Office=Occupied => eventually( count>1))) endmodule module main() // INSERTIONSORT // verification of array acess in an implementation of insertion sort integer i, k; parameterized integer n; enumerated pc {init, for, entryA1, while, entryA2, entryA3, end}; initial: pc = init; a1: pc=init and pc'=for and k'=1; a2: pc=for and pc'=entryA1 and k<=n-1; a3: pc=entryA1 and pc'=while and i'=k-1; a4: pc=while and pc'=entryA2 and i>=0; a5: pc=entryA2 and pc'=while and i'=i-1; a6: pc=while and pc'=entryA3; a7: pc=entryA3 and pc'=for and k'=k+1; a8: pc=for and pc'=end and k>=n; main: a1 | a2 | a3 | a4 | a5 | a6 | a7 | a8 ; // spec: invariant( !(pc=entryA1 and k>=n) ) // spec: invariant( !(pc=entryA1 and k<=-1) ) // spec: invariant( !(pc=entryA3 and i>=n-1) ) // spec: invariant( !(pc=entryA3 and i<=-2) ) // spec: invariant( !(pc=entryA2 and i<=-1) ) // spec: invariant( !(pc=entryA2 and i<=-2) ) // spec: invariant( !(pc=entryA2 and i>=n-1) ) // spec: invariant( !(pc=entryA2 and i>=n) ) spec: invariant( !((pc=entryA1 and k>=n) or (pc=entryA1 and k<=-1) or (pc=entryA3 and i>=n-1) or (pc=entryA3 and i<=-2) or (pc=entryA2 and i<=-1) or (pc=entryA2 and i<=-2) or (pc=entryA2 and i>=n-1) or (pc=entryA2 and i>=n-1)) ) endmodule module main() // RW: readers-writers monitor with 8 readers and 8 writers integer nr; boolean busy; restrict: nr >=0; initial: nr=0 and !busy; module reader() boolean reading; initial: !reading; r_enter: !reading and !busy and nr'=nr+1 and reading'; r_exit: reading and !reading' and nr'=nr-1; reader: r_enter | r_exit; endmodule module writer() boolean writing; initial: !writing; w_enter: !writing and nr=0 and !busy and writing' and busy'; w_exit: writing and !writing' and !busy'; writer: w_enter | w_exit; endmodule main: reader() | reader() | reader() | reader() | reader() | reader() | reader() | reader() | writer() | writer() | writer() | writer() | writer() | writer() | writer() | writer(); spec: invariant( busy => nr=0 ) // spec: invariant( nr>=0 and nw>=0 ) // spec: invariant( (nr=0 and nw<=1) or nw=0 ) // spec: invariant( (nr=0 or nw=0) and nw<=1 ) // spec: invariant( nr=0 or nw=0 ) // spec: AG( nr<=3 ) endmodule module main() // PC // a producer-consumer system with 10 control states integer produced, consumed, count; enumerated pready,cready {s1, s2, s3, s4, s5, s6, s7, s8, s9, ok}; parameterized integer size; initial : pready =s1 and cready = s1 and produced = 0 and consumed = 0 and count = 0 and size >= 1; restrict : size >= 1 ; P1: pready=s1 and pready'=s2; P2: pready=s2 and pready'=s3; P3: pready=s3 and pready'=s4; P4: pready=s4 and pready'=s5; P5: pready=s5 and pready'=s6; P6: pready=s6 and pready'=s7; P7: pready=s7 and pready'=s8; P8: pready=s8 and pready'=s9; P9: pready=s9 and pready'=ok; P10: pready=ok and pready'=s1; Producer : pready=ok and (count < size) and (count' = count + 1) and (produced' = produced + 1); C1: cready=s1 and cready'=s2; C2: cready=s2 and cready'=s3; C3: cready=s3 and cready'=s4; C4: cready=s4 and cready'=s5; C5: cready=s5 and cready'=s6; C6: cready=s6 and cready'=s7; C7: cready=s7 and cready'=s8; C8: cready=s8 and cready'=s9; C9: cready=s9 and cready'=ok; C10: cready=ok and cready'=s1; Consumer : cready=ok and count > 0 && count' = count - 1 && consumed' = consumed + 1 ; main : P1 | P2 | P3 | P4 | P5 | P6 | P7 | P8 | P9 | P10 | C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9 | C10 | Producer | Consumer ; spec : invariant( produced - consumed = count && count <= size ) endmodule module main() //Airport Ground Traffic Control // number of airplanes occupying runways integer numRW16R, numRW16L; // number of arriving airplanes occupying taxiWayC[3-8] integer numC3, numC4, numC5, numC6, numC7, numC8; // number of arriving airplanes occupying taxiWayB[2,7,9,10,11]A integer numB2A, numB7A, numB9A, numB10A, numB11A; // runways are initialized as available initial: numRW16R=0 and numRW16L=0; // taxiways are initialized as available initial : numC3=0 and numC4=0 and numC5=0 and numC6=0 and numC7=0 and numC8=0 and numB2A=0 and numB7A=0 and numB9A=0 and numB10A=0 and numB11A=0; restrict : numRW16R>=0 and numRW16L>=0 and numC3>=0 and numC4>=0 and numC5>=0 and numC6>=0 and numC7>=0 and numC8>=0 and numB2A>=0 and numB7A>=0 and numB9A>=0 and numB10A>=0 and numB11A>=0; module Departing() // encodes states of a departing airplane enumerated state {parked, takeOff, depFlow}; // initially parked initial : state=parked; reqTakeOff : state=parked and numRW16L=0 and numC3+numC4+numC5+numC6+numC7+numC8=0 and state'=takeOff and numRW16L'=numRW16L+1; leave : state=takeOff and state'=depFlow and numRW16L'=numRW16L-1; Departing : reqTakeOff | leave ; endmodule module Arriving() // encodes states of an arriving airplane enumerated state {arFlow, touchDown, taxiTo16LC3, taxiTo16LC4, taxiTo16LC5, taxiTo16LC6, taxiTo16LC7, taxiTo16LC8, taxiFr16LB2, taxiFr16LB7, taxiFr16LB9, taxiFr16LB10, taxiFr16LB11, parked}; // initially in arriving flow initial : state=arFlow; reqLand : state=arFlow and numRW16R=0 and state'=touchDown and numRW16R'=numRW16R+1; exitRW3 : state=touchDown and numC3=0 and state'=taxiTo16LC3 and numRW16R'=numRW16R-1 and numC3'=numC3+1; exitRW4 : state=touchDown and numC4=0 and state'=taxiTo16LC4 and numRW16R'=numRW16R-1 and numC4'=numC4+1; exitRW5 : state=touchDown and numC5=0 and state'=taxiTo16LC5 and numRW16R'=numRW16R-1 and numC5'=numC5+1; exitRW6 : state=touchDown and numC6=0 and state'=taxiTo16LC6 and numRW16R'=numRW16R-1 and numC6'=numC6+1; exitRW7 : state=touchDown and numC7=0 and state'=taxiTo16LC7 and numRW16R'=numRW16R-1 and numC7'=numC7+1; exitRW8 : state=touchDown and numC8=0 and state'=taxiTo16LC8 and numRW16R'=numRW16R-1 and numC8'=numC8+1; crossRW3 : state=taxiTo16LC3 and numRW16L=0 and numB2A=0 and state'=taxiFr16LB2 and numC3'=numC3-1 and numB2A'=numB2A+1; crossRW4 : state=taxiTo16LC4 and numRW16L=0 and numB7A=0 and state'=taxiFr16LB7 and numC4'=numC4-1 and numB7A'=numB7A+1; crossRW5 : state=taxiTo16LC5 and numRW16L=0 and numB9A=0 and state'=taxiFr16LB9 and numC5'=numC5-1 and numB9A'=numB9A+1; crossRW6 : state=taxiTo16LC6 and numRW16L=0 and numB10A=0 and state'=taxiFr16LB10 and numC6'=numC6-1 and numB10A'=numB10A+1; crossRW7 : state=taxiTo16LC7 and numRW16L=0 and numB10A=0 and state'=taxiFr16LB10 and numC7'=numC7-1 and numB10A'=numB10A+1; crossRW8 : state=taxiTo16LC8 and numRW16L=0 and numB11A=0 and state'=taxiFr16LB11 and numC8'=numC8-1 and numB11A'=numB11A+1; park2 : state=taxiFr16LB2 and state'=parked and numB2A'=numB2A-1; park7 : state=taxiFr16LB7 and state'=parked and numB7A'=numB7A-1; park9 : state=taxiFr16LB9 and state'=parked and numB9A'=numB9A-1; park10 : state=taxiFr16LB10 and state'=parked and numB10A'=numB10A-1; park11 : state=taxiFr16LB11 and state'=parked and numB11A'=numB11A-1; Arriving : reqLand | exitRW3 | exitRW4 | exitRW5 | exitRW6 | exitRW7 | exitRW8 | crossRW3 | crossRW4 | crossRW5 | crossRW6 | crossRW7 | crossRW8 | park2 | park7 | park9 | park10 | park11; endmodule // parameterized version main: Arriving()* | Departing()* ; // the version with 2 arriving 2 departing planes: // main: Arriving() | Arriving() | Departing() | Departing(); spec: AG(numRW16R <=1 and numRW16L <= 1) // spec: AG((numRW16L=0 and numC3+numC4+numC5+numC6+numC7+numC8>0) => AX(numRW16L=0)) endmodule