## Michael Harrison, Newcastle University, 1 November 2010 ## This model ignores the alarm but accommodates the options list ## also ignores the possibility of unit changes ## incorporates query but simply -- really only dealing with locks ## it further abstracts over infusion rate and volumes. defines maxrate=3 maxinfuse=10 maxbags=9 bigstep=2 infusemin=2 drate=0 dvtbi=1 dvol=2 dtime=3 dbags=4 dquery=5 dkvorate=6 dlock=0 ddosing=1 dsetup=2 dsetvtbi=3 dadjustav=4 ddisablerate=5 dpdtls=6 mbags=9 timeout=5 maxtime=10 types imode={hold, infuse} iline={holding, infusing, volume, dispvtbi, attention, vtbidone, dispkvo, setvtbi, locked, options, dispinfo, blank} imid=array drate..dkvorate of boolean ifunctions = {fvol, fvtbi, fcancel, fclear, fnull, fback, fok, fbags, fquit} irates=0..maxrate iratesaux=1..maxrate ivols=0..maxinfuse itimes=0..maxtime ibags=0..maxbags ibagscursor=0..mbags qcurse=dlock..dpdtls abags = array 0..mbags of ibags interactor main attributes [vis] infusionstatus: imode [vis] infusionrate: irates kvorate: irates infusionrateaux: iratesaux [vis] volumeinfused: ivols [vis] vtbi: ivols oldvtbi: ivols [vis] time: itimes elapse: itimes [vis] topline: iline [vis] middisp: imid [vis] bagscursor: ibagscursor [vis] qcursor: qcurse [vis] bagsval: abags [vis] fndisp1: ifunctions [vis] fndisp2: ifunctions [vis] fndisp3: ifunctions [vis] runlight: boolean [vis] pauselight: boolean [vis] onlight: boolean vtmode: boolean rmode: boolean bagmode: boolean qmode: boolean rlock: boolean rdisabled: boolean kvoflag: boolean actions [vis] run [vis] pause [vis] on [vis] key1 [vis] key2 [vis] key3 [vis] fup [vis] sup [vis] fdown [vis] sdown [vis] query tick axioms [] topline=blank & !runlight & !pauselight & !onlight & !middisp[drate] & !middisp[dvtbi] & !middisp[dvol] & !middisp[dtime] & !middisp[dbags] & !middisp[dkvorate] & infusionstatus=hold & infusionrate=0 & volumeinfused=0 & vtbi=0 & oldvtbi=0 & elapse=0 & bagscursor=5 & qcursor=dlock & !vtmode & !rmode & !bagmode & !qmode & !rlock & !rdisabled & !kvoflag & fndisp1=fnull & fndisp2=fnull & fndisp3=fnull #invariant bagsval[0]=0 & bagsval[1]=1 & bagsval[2]=2 & bagsval[3]=3 & bagsval[4]=4 & bagsval[5]=5 & bagsval[6]=6 & bagsval[7]=7 & bagsval[8]=8 & bagsval[mbags]=9 #invariant infusionrate>0 -> infusionrateaux=infusionrate infusionrate>0 -> time=(vtbi/infusionrateaux) infusionrate=0 -> time=0 # defining on topline=blank -> [on] topline'=holding & infusionstatus'=hold & middisp[drate]' & (vtbi=0 -> (!middisp[dvtbi]' & !middisp[dtime]')) & (vtbi!=0 -> (middisp[dvtbi]' & middisp[dtime]')) & middisp[dvol]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & fndisp1'=fvol & fndisp2'=fvtbi & fndisp3'=fnull & elapse'=0 & !vtmode' & rmode' & !bagmode' & !qmode' & !rdisabled' & !kvoflag' & onlight' & pauselight' & !runlight' & keep(volumeinfused, vtbi, bagscursor, infusionrate, rlock) # on turns it off when infusion status is hold topline!=blank -> [on] topline'=blank & !middisp[drate]' & !middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & infusionstatus'=hold & bagscursor'=5 & !vtmode' & !rmode' & !bagmode' & !qmode' & !kvoflag' & !onlight' & !pauselight' & !runlight' & fndisp1'=fnull & fndisp2'=fnull & fndisp3'=fnull & elapse'=0 & keep(rdisabled, volumeinfused, vtbi, infusionrate, rlock, kvoflag) # starting the infusion process using run per(run) -> (topline=holding) & !(infusionrate=0) !(vtbi=0) -> [run] (topline'=infusing) & (infusionstatus'=infuse) & middisp[drate]' & middisp[dvtbi]' & middisp[dvol]' & middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & (fndisp1'=fvol) & (fndisp2'=fvtbi) & (fndisp3'=fnull) & !vtmode' & !rmode' & !bagmode' & !qmode' & (elapse'=0) & onlight' & runlight' & !pauselight' & keep(infusionrate, volumeinfused, vtbi, rlock, rdisabled, kvoflag) (vtbi=0) & kvoflag -> [run] (topline'=vtbidone) & (infusionstatus'=hold) & !middisp[drate]' & !middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & (fndisp1'=fclear) & (fndisp2'=fnull) & (fndisp3'=fquit) & !vtmode' & !rmode' & !bagmode' & !qmode' & (elapse'=0) & !kvoflag' & keep(infusionrate, volumeinfused, vtbi, rlock, rdisabled, onlight, runlight, pauselight) (vtbi=0) & !kvoflag -> [run] (topline'=setvtbi) & !middisp[drate]' & !middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & (fndisp1'=fnull) & (fndisp2'=fvtbi) & (fndisp3'=fcancel) & !vtmode' & !rmode' & !bagmode' & !qmode' & (elapse'=0) & keep(infusionrate, infusionstatus, volumeinfused, vtbi, rlock, rdisabled, kvoflag, onlight, runlight, pauselight) per(pause) -> (infusionstatus=infuse) & !(topline=vtbidone) [pause] (topline'=holding) & (infusionstatus'=hold) & middisp[drate]' & (vtbi=0 -> (!middisp[dvtbi]' & !middisp[dtime]')) & (vtbi!=0 -> (middisp[dvtbi]' & middisp[dtime]')) & middisp[dvol]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & (fndisp1'=fvol) & (fndisp2'=fvtbi) & (fndisp3'=fnull) & !vtmode' & rmode' & !bagmode' & !qmode' & elapse'=0 & pauselight' & !runlight' & keep(infusionrate, volumeinfused, vtbi, kvoflag, rlock, rdisabled, onlight) per(query) -> topline=holding [query] (rdisabled -> qcursor'=ddosing) & (!rdisabled -> qcursor'=dlock) & (topline'=options) & !middisp[drate]' & !middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dkvorate]' & !middisp[dbags]' & middisp[dquery]' & (fndisp1'=fok) & (fndisp2'=fnull) & (fndisp3'=fquit) & !rmode' & !vtmode' & !bagmode' & qmode' & elapse'=0 & keep(infusionstatus, infusionrate, volumeinfused, vtbi, kvoflag, rlock, rdisabled, onlight) per(tick) -> topline in {holding, volume, dispvtbi, locked, options, dispinfo} | (infusionstatus=infuse) topline=locked -> [tick] (topline'=holding) & (infusionstatus'=hold) & middisp[drate]' & (vtbi=0 -> (!middisp[dvtbi]' & !middisp[dtime]')) & (vtbi!=0 -> (middisp[dvtbi]' & middisp[dtime]')) & middisp[dvol]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & (fndisp1'=fvol) & (fndisp2'=fvtbi) & (fndisp3'=fnull) & !vtmode' & rmode' & !bagmode' & !qmode' & elapse'=0 & pauselight' & !runlight' & keep(infusionrate, volumeinfused, vtbi, kvoflag, rlock, rdisabled, onlight) (topline in {holding, volume, dispvtbi, options, dispinfo}) & (elapse=timeout) -> [tick] topline'=attention & !middisp[drate]' & !middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & fndisp1'=fnull & fndisp2'=fnull & fndisp3'=fcancel & elapse'=0 & !rmode' & !vtmode' & !bagmode' & !qmode' & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) (topline in {holding, volume, dispvtbi, options, dispinfo}) & (elapse [tick] elapse'=elapse+1 & keep(topline, infusionstatus, fndisp1, fndisp2, fndisp3, middisp, infusionrate, volumeinfused, vtbi, rmode, vtmode, bagmode, qmode, bagscursor, qcursor, oldvtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) (infusionstatus=infuse) & (infusionrate < vtbi) -> [tick] vtbi'=vtbi - infusionrate & volumeinfused'=volumeinfused + infusionrate & keep(topline, middisp, infusionstatus, fndisp1, fndisp2, fndisp3, infusionrate, rmode, vtmode, bagmode, qmode, elapse, oldvtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) # need to deal with the special case, ie assumption that there is volume and reduction of rate (infusionstatus=infuse) & (infusionrate >= vtbi) & (vtbi != 0) -> [tick] (vtbi'=0) & (volumeinfused'=volumeinfused + vtbi) & ((infusionrate (kvorate'=infusionrate)) & ((infusionrate>=infusemin) -> (kvorate'=infusemin)) & (topline'=vtbidone) & kvoflag' & !middisp[drate]' & !middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dquery]' & !middisp[dkvorate]' & (fndisp1'=fnull) & (fndisp2'=fnull) & (fndisp3'=fcancel) & !vtmode' & !rmode' & !bagmode' & keep(infusionrate, elapse, infusionstatus, onlight, runlight, pauselight, rdisabled, rlock, qmode) (infusionstatus=infuse) & (infusionrate >= vtbi) & (vtbi=0) -> [tick] (volumeinfused'=volumeinfused+kvorate) & keep(topline, infusionrate, middisp, infusionstatus, fndisp1, fndisp2, fndisp3, vtmode, rmode, bagmode, qmode, vtbi, elapse, kvorate, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) # per(key1) -> false per(key1) -> (fndisp1!=fnull) & (topline in {holding, dispvtbi, dispkvo, vtbidone, options}) # when the top line is holding topline=holding -> [key1] topline'=volume & !middisp[drate]' & !middisp[dvtbi]' & middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & fndisp1'=fnull & fndisp2'=fclear & fndisp3'=fquit & !vtmode' & !rmode' & !bagmode' & !qmode' & elapse'=0 & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) # when in kvo mode topline=dispkvo -> [key1] topline'=volume & !middisp[drate]' & !middisp[dvtbi]' & middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & fndisp1'=fnull & fndisp2'=fclear & fndisp3'=fquit & !vtmode' & !rmode' & !bagmode' & !qmode' & elapse'=0 & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) # when the top line is vtbi topline=dispvtbi -> [key1] (vtmode -> (topline'=holding & (vtbi=0 -> !middisp[dvtbi]' & !middisp[dtime]') & (vtbi!=0 -> middisp[dvtbi]' & middisp[dtime]') & middisp[drate]' & middisp[dvol]' & fndisp1'=fvol & fndisp2'=fvtbi & fndisp3'=fnull & !vtmode' & rmode' & vtbi'=vtbi)) & (bagmode -> (topline'=dispvtbi & !middisp[drate]' & !middisp[dvol]' & !middisp[dtime]' & fndisp1'=fok & fndisp2'=fbags & fndisp3'=fquit & vtmode' & !rmode' & middisp[dvtbi]' & (bagscursor=0 -> vtbi'=bagsval[0]) & (bagscursor=1 -> vtbi'=bagsval[1]) & (bagscursor=2 -> vtbi'=bagsval[2]) & (bagscursor=3 -> vtbi'=bagsval[3]) & (bagscursor=4 -> vtbi'=bagsval[4]) & (bagscursor=5 -> vtbi'=bagsval[5]) & (bagscursor=6 -> vtbi'=bagsval[6]) & (bagscursor=7 -> vtbi'=bagsval[7]) & (bagscursor=8 -> vtbi'=bagsval[8]) & (bagscursor=9 -> vtbi'=bagsval[9]) )) & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & !bagmode' & !qmode' & !kvoflag' & elapse' = 0 & keep(infusionstatus, infusionrate, volumeinfused, oldvtbi, onlight, runlight, pauselight, rdisabled, rlock) topline=vtbidone -> [key1] (topline'=holding) & (infusionstatus'=hold) & middisp[drate]' & (vtbi=0 -> (!middisp[dvtbi]' & !middisp[dtime]')) & (vtbi!=0 -> (middisp[dvtbi]' & middisp[dtime]')) & middisp[dvol]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & (fndisp1'=fvol) & (fndisp2'=fvtbi) & (fndisp3'=fnull) & !vtmode' & rmode' & !bagmode' & !qmode' & elapse'=0 & pauselight' & !runlight' & keep(infusionrate, volumeinfused, vtbi, kvoflag, rlock, rdisabled, onlight) # when top line is options topline=options -> [key1] ((qcursor=dlock -> ((rlock -> !rlock') & (!rlock -> rlock') & topline'=holding & middisp[drate]' & (vtbi=0 -> !middisp[dvtbi]' & !middisp[dtime]') & (vtbi!=0 -> middisp[dvtbi]' & middisp[dtime]') & middisp[dvol]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & fndisp1'=fvol & fndisp2'=fvtbi & fndisp3'=fnull & !vtmode' & rmode' & !bagmode' & !qmode' & elapse'=0 & !kvoflag' & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled))) & (qcursor in {ddosing, dsetup, dsetvtbi, dadjustav, dpdtls} -> (topline'=dispinfo & !middisp[drate]' & !middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & fndisp1'=fnull & fndisp2'=fnull & fndisp3'=fquit & !vtmode' & !rmode' & !bagmode' & !qmode' & elapse'=0 & !kvoflag' & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled))) & (qcursor=ddisablerate -> ( (!rdisabled -> rdisabled') & (rdisabled -> !rdisabled') & topline'=holding & middisp[drate]' & middisp[dvtbi]' & middisp[dvol]' & middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & fndisp1'=fvol & fndisp2'=fvtbi & fndisp3'=fnull & !vtmode' & rmode' & !bagmode' & !qmode' & elapse'=0 & !kvoflag' & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rlock)))) # key 2 # per(key2) -> false per(key2) -> !(fndisp2=fnull) & (topline in {holding, volume, dispvtbi}) # when top line is holding key 2 (topline=holding) & !kvoflag -> [key2] topline'=dispvtbi & oldvtbi'=vtbi & middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & fndisp1'=fok & fndisp2'=fbags & fndisp3'=fquit & vtmode' & !rmode' & !bagmode' & !qmode' & elapse'=0 & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) (topline=holding) & kvoflag -> [key2] topline'=vtbidone & oldvtbi'=vtbi & !middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & fndisp1'=fclear & fndisp2'=fnull & fndisp3'=fquit & !vtmode' & !rmode' & !bagmode' & !qmode' & elapse'=0 & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) # when the top line is volume topline=volume -> [key2] (kvoflag -> (topline'=dispkvo & fndisp2'=fnull & !rmode' & middisp[dvtbi]' & middisp[dtime]')) & (!kvoflag ->(topline'=holding & (vtbi=0 -> !middisp[dvtbi]' & !middisp[dtime]') & (vtbi!=0 -> middisp[dvtbi]' & middisp[dtime]') & fndisp2'=fvtbi & rmode')) & volumeinfused'=0 & elapse' = 0 & middisp[dvol]' & middisp[drate]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & fndisp1'=fvol & fndisp3'=fnull & !vtmode' & !bagmode' & !qmode' & keep(infusionstatus, infusionrate, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) # when the top line is VTBI topline=dispvtbi -> [key2] topline'=dispvtbi & !middisp[drate]' & !middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & middisp[dbags]' & !middisp[dkvorate]' & bagscursor'=5 & fndisp1'=fok & fndisp2'=fnull & fndisp3'=fback & !vtmode' & !rmode' & bagmode' & elapse' = 0 & !qmode' & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag, oldvtbi) topline=setvtbi -> [key2] topline'=dispvtbi & oldvtbi'=vtbi & middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & fndisp1'=fok & fndisp2'=fbags & fndisp3'=fquit & vtmode' & !rmode' & !bagmode' & !qmode' & elapse'=0 & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) # key 3 # per(key3) -> false per(key3) -> (fndisp3!=fnull) & (topline in {attention, volume, vtbidone, dispvtbi, options, dispinfo}) # top line is attention topline=attention -> [key3] (topline'=holding) & (infusionstatus'=hold) & middisp[drate]' & (vtbi=0 -> (!middisp[dvtbi]' & !middisp[dtime]')) & (vtbi!=0 -> (middisp[dvtbi]' & middisp[dtime]')) & middisp[dvol]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & (fndisp1'=fvol) & (fndisp2'=fvtbi) & (fndisp3'=fnull) & !vtmode' & rmode' & !bagmode' & !qmode' & elapse'=0 & pauselight' & !runlight' & keep(infusionrate, volumeinfused, vtbi, kvoflag, rlock, rdisabled, onlight) # top line is volume topline=volume -> [key3] (!kvoflag -> (topline'=holding & (vtbi=0 -> !middisp[dvtbi]' & !middisp[dtime]') & (vtbi!=0 -> middisp[dvtbi]' & middisp[dtime]') & fndisp2'=fvtbi & rmode')) & (kvoflag -> (topline'=dispkvo & fndisp2'=fnull & middisp[dvtbi]' & middisp[dtime]' & !rmode')) & middisp[drate]' & middisp[dvol]' & !middisp[dbags]' & !middisp[dkvorate]' & fndisp1'=fvol & fndisp3'=fnull & !vtmode' & rmode' & !bagmode' & !qmode' & elapse' = 0 & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) #topline is vtbi done (topline=vtbidone) & (infusionstatus=infuse) -> [key3] topline'=dispkvo & !middisp[drate]' & !middisp[dbags]' & middisp[dkvorate]' & middisp[dvtbi]' & middisp[dvol]' & middisp[dtime]' & !middisp[dquery]' & fndisp1'=fvol & fndisp2'=fnull & fndisp3'=fnull & keep(infusionrate, infusionstatus, volumeinfused, vtmode, rmode, bagmode, qmode, vtbi, elapse, kvorate, rlock, rdisabled, kvoflag, onlight, runlight, pauselight) (topline=vtbidone) & (infusionstatus=hold) -> [key3](topline'=holding) & (infusionstatus'=hold) & middisp[drate]' & (vtbi=0 -> (!middisp[dvtbi]' & !middisp[dtime]')) & (vtbi!=0 -> (middisp[dvtbi]' & middisp[dtime]')) & middisp[dvol]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & (fndisp1'=fvol) & (fndisp2'=fvtbi) & (fndisp3'=fnull) & !vtmode' & rmode' & !bagmode' & !qmode' & elapse'=0 & pauselight' & !runlight' & keep(infusionrate, volumeinfused, vtbi, kvoflag, rlock, rdisabled, onlight) # top line is VTBI (topline=dispvtbi) -> [key3] (vtmode -> (topline'=holding & vtbi' = oldvtbi & (vtbi=0 -> !middisp[dvtbi]' & !middisp[dtime]') & (vtbi!=0 -> middisp[dvtbi]' & middisp[dtime]') & middisp[drate]' & middisp[dvol]' & fndisp1'=fvol & fndisp2'=fvtbi & fndisp3'=fnull & !vtmode' & rmode')) & (bagmode -> (topline'=dispvtbi & vtbi'=vtbi & !middisp[dvol]' & !middisp[dtime]' & !middisp[drate]' & fndisp1'=fok & fndisp2'=fbags & middisp[dvtbi]' & fndisp3'=fquit & vtmode' & !rmode')) & !bagmode' & !qmode' & elapse' = 0 & !middisp[dbags]' & !middisp[dkvorate]' & keep(infusionstatus, infusionrate, volumeinfused, oldvtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) (topline=setvtbi) -> [key3] (topline'=holding) & (infusionstatus'=hold) & middisp[drate]' & (vtbi=0 -> (!middisp[dvtbi]' & !middisp[dtime]')) & (vtbi!=0 -> (middisp[dvtbi]' & middisp[dtime]')) & middisp[dvol]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & (fndisp1'=fvol) & (fndisp2'=fvtbi) & (fndisp3'=fnull) & !vtmode' & rmode' & !bagmode' & !qmode' & elapse'=0 & pauselight' & !runlight' & keep(infusionrate, volumeinfused, vtbi, kvoflag, rlock, rdisabled, onlight) topline in {options, dispinfo} -> [key3](topline'=holding) & (infusionstatus'=hold) & middisp[drate]' & (vtbi=0 -> (!middisp[dvtbi]' & !middisp[dtime]')) & (vtbi!=0 -> (middisp[dvtbi]' & middisp[dtime]')) & middisp[dvol]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & (fndisp1'=fvol) & (fndisp2'=fvtbi) & (fndisp3'=fnull) & !vtmode' & rmode' & !bagmode' & !qmode' & elapse'=0 & pauselight' & !runlight' & keep(infusionrate, volumeinfused, vtbi, kvoflag, rlock, rdisabled, onlight) #the up and down chevrons # per(fup) -> false per(fup) -> infusionstatus=hold & (rmode | qmode | vtmode | bagmode | topline in {vtbidone, setvtbi}) # per(sup) -> false per(sup) -> infusionstatus=hold & (rmode | qmode | vtmode | bagmode | topline in {vtbidone, setvtbi}) # per(fdown) -> false per(fdown) -> infusionstatus=hold & (rmode | qmode | vtmode | bagmode | topline in {vtbidone, setvtbi}) # per(sdown) -> false per(sdown) -> infusionstatus=hold & (rmode | qmode | vtmode | bagmode | topline in {vtbidone, setvtbi}) # definition seems to go further than below and includes decimal points # if in vtbi done or set vtbi mode topline in {vtbidone, setvtbi} -> [fup] topline'=dispvtbi & oldvtbi'=vtbi & middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & !kvoflag' & fndisp1'=fok & fndisp2'=fbags & fndisp3'=fquit & vtmode' & !rmode' & !bagmode' & !qmode' & elapse'=0 & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock) topline in {vtbidone, setvtbi} -> [sup] topline'=dispvtbi & oldvtbi'=vtbi & middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & !kvoflag' & fndisp1'=fok & fndisp2'=fbags & fndisp3'=fquit & vtmode' & !rmode' & !bagmode' & !qmode' & elapse'=0 & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock) topline in {vtbidone, setvtbi} -> [fdown] topline'=dispvtbi & oldvtbi'=vtbi & middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & fndisp1'=fok & fndisp2'=fbags & fndisp3'=fquit & vtmode' & !rmode' & !bagmode' & !qmode' & elapse'=0 & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) topline in {vtbidone, setvtbi} -> [sdown] topline'=dispvtbi & oldvtbi'=vtbi & middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & !middisp[dquery]' & fndisp1'=fok & fndisp2'=fbags & fndisp3'=fquit & vtmode' & !rmode' & !bagmode' & !qmode' & elapse'=0 & keep(infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) # infusion rate is changed rmode & !rlock -> [fup] ((infusionrate <= (maxrate - bigstep)) -> infusionrate'=infusionrate + bigstep) & ((infusionrate>(maxrate - bigstep)) -> infusionrate'=maxrate) & elapse'=0 & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, volumeinfused, vtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) rmode & rlock -> [fup] topline'=locked & !rmode' & !middisp[drate]' & !middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & fndisp1'=fnull & fndisp2'=fnull & fndisp3'=fnull & elapse'=0 & keep(vtmode, bagmode, qmode, infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) rmode & !rlock -> [sup] ((infusionrate < maxrate) -> infusionrate' = infusionrate + 1) & ((infusionrate=maxrate) -> infusionrate'=maxrate) & elapse'=0 & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, volumeinfused, vtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) rmode & rlock -> [sup] topline'=locked & !rmode' & !middisp[drate]' & !middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & fndisp1'=fnull & fndisp2'=fnull & fndisp3'=fnull & elapse'=0 & keep(vtmode, bagmode, qmode, infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) rmode & !rlock -> [fdown] ((infusionrate >= bigstep) -> infusionrate' = infusionrate - bigstep) & ((infusionrate < bigstep) -> infusionrate' = 0) & elapse'=0 & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, volumeinfused, vtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) rmode & rlock -> [fdown] topline'=locked & !rmode' & !middisp[drate]' & !middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & fndisp1'=fnull & fndisp2'=fnull & fndisp3'=fnull & elapse'=0 & keep(vtmode, bagmode, qmode, infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) rmode & !rlock -> [sdown] ((infusionrate > 0) -> infusionrate' = infusionrate - 1) & ((infusionrate = 0) -> infusionrate'=0) & elapse'=0 & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, volumeinfused, vtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) rmode & rlock -> [sdown] topline'=locked & !rmode' & !middisp[drate]' & !middisp[dvtbi]' & !middisp[dvol]' & !middisp[dtime]' & !middisp[dbags]' & !middisp[dkvorate]' & fndisp1'=fnull & fndisp2'=fnull & fndisp3'=fnull & elapse'=0 & keep(vtmode, bagmode, qmode, infusionstatus, infusionrate, volumeinfused, vtbi, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) vtmode -> [fup] ((vtbi <= (maxinfuse - bigstep)) -> vtbi'=vtbi + bigstep) & ((vtbi > (maxinfuse - bigstep)) -> vtbi'=maxinfuse) & elapse'=0 & !kvoflag' & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, volumeinfused, infusionrate, oldvtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock) vtmode -> [sup] ((vtbi < maxinfuse) -> vtbi' = vtbi + 1) & ((vtbi = maxinfuse) -> vtbi'=maxinfuse) & elapse'=0 & !kvoflag' & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, volumeinfused, infusionrate, oldvtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock) vtmode -> [fdown] ((vtbi >= bigstep) -> vtbi'=vtbi - bigstep) & ((vtbi vtbi'=0) & elapse'=0 & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, volumeinfused, infusionrate, oldvtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) vtmode -> [sdown] ((vtbi > 0) -> vtbi' = (vtbi - 1)) & ((vtbi = 0) -> vtbi'=0) & elapse'=0 & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, volumeinfused, infusionrate, oldvtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) # bag mode bagmode -> [fup] bagscursor'=mbags & elapse'=0 & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, infusionrate, volumeinfused, oldvtbi, vtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) bagmode -> [sup] (bagscursor< mbags -> bagscursor'=bagscursor+1) & (bagscursor= mbags -> keep(bagscursor)) & elapse'=0 & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, infusionrate, volumeinfused, oldvtbi, vtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) bagmode -> [fdown] bagscursor'=0 & elapse'=0 & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, infusionrate, volumeinfused, oldvtbi, vtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) bagmode -> [sdown] (bagscursor>0 -> (bagscursor'=bagscursor - 1)) & (bagscursor=0 -> keep(bagscursor)) & elapse'=0 & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, infusionrate, volumeinfused, oldvtbi, vtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) # query mode qmode -> [fup] (rdisabled -> qcursor'=ddosing) & (!rdisabled -> qcursor'=dlock) & (elapse'=0) & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, infusionrate, volumeinfused, oldvtbi, vtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) qmode -> [sup] ((!rlock & !rdisabled) -> (qcursor=dlock -> keep(qcursor)) & ((qcursor!=dlock) -> qcursor'=qcursor=1)) & (rlock -> (qcursor=dlock -> keep(qcursor)) & (qcursor=dpdtls -> qcursor'=qcursor - 2) & (!(qcursor in {dlock, dpdtls}) -> qcursor'=qcursor - 1)) & (rdisabled -> (qcursor=ddosing -> keep(qcursor)) & (qcursor!=ddosing -> qcursor'=qcursor - 1)) & (elapse'=0) & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, infusionrate, volumeinfused, oldvtbi, vtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) qmode -> [fdown] (qcursor'=dpdtls) & (elapse'=0) & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, infusionrate, volumeinfused, oldvtbi, vtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) qmode -> [sdown] ((qcursor=dpdtls) -> keep(qcursor)) & (((qcursor=dadjustav) & rlock) -> qcursor'=dpdtls) & ((!(qcursor in {dadjustav, dpdtls}) & rlock) -> qcursor'=qcursor+1) & (((qcursor != dpdtls) & !rlock) -> qcursor'=qcursor+1) & (elapse'=0) & keep(topline, infusionstatus, middisp, fndisp1, fndisp2, fndisp3, infusionrate, volumeinfused, oldvtbi, vtbi, rmode, vtmode, bagmode, qmode, onlight, runlight, pauselight, rdisabled, rlock, kvoflag) [nil] true test AG(vtbi=9 -> AG(volumeinfused != 9)) #Not Verified test AG(topline=holding -> infusionstatus=hold) #Not Verified test AG(topline in {holding, dispvtbi, setvtbi, attention, volume, options, locked, blank} <-> infusionstatus=hold) #Not Verified test AG(topline in {infusing, dispkvo, vtbidone} <-> infusionstatus=infuse) #Not Verified test AG(vtmode -> middisp[dvtbi]) #Not Verified test AG(rmode -> middisp[drate]) #Not Verified test AG(bagmode -> middisp[dvtbi]) #Not Verified test AG(bagmode -> middisp[dbags]) #Not Verified test AG(qmode -> middisp[dquery]) #Not Verified test AG(topline=holding <-> rmode) #Not Verified test AG(topline=dispvtbi <-> vtmode) #Not Verified test AG(topline in {vtbidone, dispkvo} -> vtbi=0) #Not Verified test AG(fndisp3 != fnull -> fndisp3=fquit) #Not Verified test AG((fndisp3 != fnull) & !bagmode & !(topline in {attention, vtbidone, setvtbi}) -> fndisp3=fquit) #Verified True test AG((fndisp1 != fnull) & !rmode & (infusionstatus=hold) & topline != vtbidone -> fndisp1=fok) #Verified False test AG(infusionstatus=hold -> AX(run -> !(infusionstatus=hold))) #Not Verified test AG(infusionstatus=infuse -> AX(run -> !(infusionstatus=infuse))) #Not Verified test AG(topline=holding -> AX(key1 -> !(topline=holding))) #Not Verified test AG(topline=infusing -> AX(key1 -> !(topline=infusing))) #Not Verified test AG(topline=volume -> AX(key1 -> !(topline=volume))) #Not Verified test AG(topline=dispvtbi -> AX(key1 -> !(topline=dispvtbi))) #Not Verified test AG(topline=vtbidone -> AX(key1 -> !(topline=vtbidone))) #Not Verified test AG(topline=dispkvo -> AX(key1 -> !(topline=dispkvo))) #Not Verified test AG(topline=setvtbi -> AX(key1 -> !(topline=setvtbi))) #Not Verified test AG(topline=locked -> AX(key1 -> !(topline=locked))) #Not Verified test AG(topline=options -> AX(key1 -> !(topline=options))) #Not Verified test AG(topline=dispinfo -> AX(key1 -> !(topline=dispinfo))) #Not Verified test AG(topline=blank -> AX(key1 -> !(topline=blank))) #Not Verified test AG(topline=holding -> AX(key2 -> !(topline=holding))) #Not Verified test AG(topline=infusing -> AX(key2 -> !(topline=infusing))) #Not Verified test AG(topline=volume -> AX(key2 -> !(topline=volume))) #Not Verified test AG(topline=dispvtbi -> AX(key2 -> !(topline=dispvtbi))) #Not Verified test AG(topline=vtbidone -> AX(key2 -> !(topline=vtbidone))) #Not Verified test AG(topline=dispkvo -> AX(key2 -> !(topline=dispkvo))) #Not Verified test AG(topline=setvtbi -> AX(key2 -> !(topline=setvtbi))) #Not Verified test AG(topline=locked -> AX(key2 -> !(topline=locked))) #Not Verified test AG(topline=options -> AX(key2 -> !(topline=options))) #Not Verified test AG(topline=dispinfo -> AX(key2 -> !(topline=dispinfo))) #Not Verified test AG(topline=blank -> AX(key2 -> !(topline=blank))) #Not Verified test AG(topline=holding -> AX(key3 -> !(topline=holding))) #Not Verified test AG(topline=infusing -> AX(key3 -> !(topline=infusing))) #Not Verified test AG(topline=volume -> AX(key3 -> !(topline=volume))) #Not Verified test AG(topline=dispvtbi -> AX(key3 -> !(topline=dispvtbi))) #Not Verified test AG(topline=vtbidone -> AX(key3 -> !(topline=vtbidone))) #Not Verified test AG(topline=dispkvo -> AX(key3 -> !(topline=dispkvo))) #Not Verified test AG(topline=setvtbi -> AX(key3 -> !(topline=setvtbi))) #Not Verified test AG(topline=locked -> AX(key3 -> !(topline=locked))) #Not Verified test AG(topline=options -> AX(key3 -> !(topline=options))) #Not Verified test AG(topline=dispinfo -> AX(key3 -> !(topline=dispinfo))) #Not Verified test AG(topline=blank -> AX(key3 -> !(topline=blank))) #Not Verified test AG(rmode=true & infusionrate=0 -> AX(sup -> !(infusionrate=0))) #Not Verified test AG(rmode=true & infusionrate=1 -> AX(sup -> !(infusionrate=1))) #Not Verified test AG(rmode=true & infusionrate=2 -> AX(sup -> !(infusionrate=2))) #Not Verified test AG(rmode=true & infusionrate=3 -> AX(sup -> !(infusionrate=3))) #Not Verified test AG(rmode=true & infusionrate=0 -> AX(fup -> !(infusionrate=0))) #Not Verified test AG(rmode=true & infusionrate=1 -> AX(fup -> !(infusionrate=1))) #Not Verified test AG(rmode=true & infusionrate=2 -> AX(fup -> !(infusionrate=2))) #Not Verified test AG(rmode=true & infusionrate=3 -> AX(fup -> !(infusionrate=3))) #Not Verified test AG(rmode=true & infusionrate=0 -> AX(sdown -> !(infusionrate=0))) #Not Verified test AG(rmode=true & infusionrate=1 -> AX(sdown -> !(infusionrate=1))) #Not Verified test AG(rmode=true & infusionrate=2 -> AX(sdown -> !(infusionrate=2))) #Not Verified test AG(rmode=true & infusionrate=3 -> AX(sdown -> !(infusionrate=3))) #Not Verified test AG(rmode=true & infusionrate=0 -> AX(fdown -> !(infusionrate=0))) #Not Verified test AG(rmode=true & infusionrate=1 -> AX(fdown -> !(infusionrate=1))) #Not Verified test AG(rmode=true & infusionrate=2 -> AX(fdown -> !(infusionrate=2))) #Not Verified test AG(rmode=true & infusionrate=3 -> AX(fdown -> !(infusionrate=3))) #Not Verified test AG(rmode=true & !rlock & infusionrate=0 -> AX(fdown -> !(infusionrate=0))) #Not Verified test AG(rmode=true & !rlock & infusionrate=1 -> AX(fdown -> !(infusionrate=1))) #Not Verified test AG(rmode=true & !rlock & infusionrate=2 -> AX(fdown -> !(infusionrate=2))) #Not Verified test AG(rmode=true & !rlock & infusionrate=3 -> AX(fdown -> !(infusionrate=3))) #Not Verified test AG(rmode=true & !rlock & infusionrate=0 -> AX(fup -> !(infusionrate=0))) #Not Verified test AG(rmode=true & !rlock & infusionrate=1 -> AX(fup -> !(infusionrate=1))) #Not Verified test AG(rmode=true & !rlock & infusionrate=2 -> AX(fup -> !(infusionrate=2))) #Not Verified test AG(rmode=true & !rlock & infusionrate=3 -> AX(fup -> !(infusionrate=3))) #Not Verified test AG(rmode=true & !rlock & infusionrate=0 -> AX(sup -> !(infusionrate=0))) #Not Verified test AG(rmode=true & !rlock & infusionrate=1 -> AX(sup -> !(infusionrate=1))) #Not Verified test AG(rmode=true & !rlock & infusionrate=2 -> AX(sup -> !(infusionrate=2))) #Not Verified test AG(rmode=true & !rlock & infusionrate=3 -> AX(sup -> !(infusionrate=3))) #Not Verified test AG(rmode=true & !rlock & infusionrate=0 -> AX(sdown -> !(infusionrate=0))) #Not Verified test AG(rmode=true & !rlock & infusionrate=1 -> AX(sdown -> !(infusionrate=1))) #Not Verified test AG(rmode=true & !rlock & infusionrate=2 -> AX(sdown -> !(infusionrate=2))) #Not Verified test AG(rmode=true & !rlock & infusionrate=3 -> AX(sdown -> !(infusionrate=3))) #Not Verified test AG(vtmode=true & vtbi=0 -> AX(fdown -> !(vtbi=0))) #Not Verified test AG(vtmode=true & vtbi=1 -> AX(fdown -> !(vtbi=1))) #Not Verified test AG(vtmode=true & vtbi=2 -> AX(fdown -> !(vtbi=2))) #Not Verified test AG(vtmode=true & vtbi=3 -> AX(fdown -> !(vtbi=3))) #Not Verified test AG(vtmode=true & vtbi=4 -> AX(fdown -> !(vtbi=4))) #Not Verified test AG(vtmode=true & vtbi=5 -> AX(fdown -> !(vtbi=5))) #Not Verified test AG(vtmode=true & vtbi=6 -> AX(fdown -> !(vtbi=6))) #Not Verified test AG(vtmode=true & vtbi=7 -> AX(fdown -> !(vtbi=7))) #Not Verified test AG(vtmode=true & vtbi=8 -> AX(fdown -> !(vtbi=8))) #Not Verified test AG(vtmode=true & vtbi=9 -> AX(fdown -> !(vtbi=9))) #Not Verified test AG(vtmode=true & vtbi=10 -> AX(fdown -> !(vtbi=10))) #Not Verified test AG(vtmode=true & vtbi=0 -> AX(fup -> !(vtbi=0))) #Not Verified test AG(vtmode=true & vtbi=1 -> AX(fup -> !(vtbi=1))) #Not Verified test AG(vtmode=true & vtbi=2 -> AX(fup -> !(vtbi=2))) #Not Verified test AG(vtmode=true & vtbi=3 -> AX(fup -> !(vtbi=3))) #Not Verified test AG(vtmode=true & vtbi=4 -> AX(fup -> !(vtbi=4))) #Not Verified test AG(vtmode=true & vtbi=5 -> AX(fup -> !(vtbi=5))) #Not Verified test AG(vtmode=true & vtbi=6 -> AX(fup -> !(vtbi=6))) #Not Verified test AG(vtmode=true & vtbi=7 -> AX(fup -> !(vtbi=7))) #Not Verified test AG(vtmode=true & vtbi=8 -> AX(fup -> !(vtbi=8))) #Not Verified test AG(vtmode=true & vtbi=9 -> AX(fup -> !(vtbi=9))) #Not Verified test AG(vtmode=true & vtbi=10 -> AX(fup -> !(vtbi=10))) #Not Verified test AG(vtmode=true & vtbi=0 -> AX(sdown -> !(vtbi=0))) #Not Verified test AG(vtmode=true & vtbi=1 -> AX(sdown -> !(vtbi=1))) #Not Verified test AG(vtmode=true & vtbi=2 -> AX(sdown -> !(vtbi=2))) #Not Verified test AG(vtmode=true & vtbi=3 -> AX(sdown -> !(vtbi=3))) #Not Verified test AG(vtmode=true & vtbi=4 -> AX(sdown -> !(vtbi=4))) #Not Verified test AG(vtmode=true & vtbi=5 -> AX(sdown -> !(vtbi=5))) #Not Verified test AG(vtmode=true & vtbi=6 -> AX(sdown -> !(vtbi=6))) #Not Verified test AG(vtmode=true & vtbi=7 -> AX(sdown -> !(vtbi=7))) #Not Verified test AG(vtmode=true & vtbi=8 -> AX(sdown -> !(vtbi=8))) #Not Verified test AG(vtmode=true & vtbi=9 -> AX(sdown -> !(vtbi=9))) #Not Verified test AG(vtmode=true & vtbi=10 -> AX(sdown -> !(vtbi=10))) #Not Verified test AG(vtmode=true & vtbi=0 -> AX(sup -> !(vtbi=0))) #Not Verified test AG(vtmode=true & vtbi=1 -> AX(sup -> !(vtbi=1))) #Not Verified test AG(vtmode=true & vtbi=2 -> AX(sup -> !(vtbi=2))) #Not Verified test AG(vtmode=true & vtbi=3 -> AX(sup -> !(vtbi=3))) #Not Verified test AG(vtmode=true & vtbi=4 -> AX(sup -> !(vtbi=4))) #Not Verified test AG(vtmode=true & vtbi=5 -> AX(sup -> !(vtbi=5))) #Not Verified test AG(vtmode=true & vtbi=6 -> AX(sup -> !(vtbi=6))) #Not Verified test AG(vtmode=true & vtbi=7 -> AX(sup -> !(vtbi=7))) #Not Verified test AG(vtmode=true & vtbi=8 -> AX(sup -> !(vtbi=8))) #Not Verified test AG(vtmode=true & vtbi=9 -> AX(sup -> !(vtbi=9))) #Not Verified test AG(vtmode=true & vtbi=10 -> AX(sup -> !(vtbi=10))) #Not Verified test AG((infusionstatus=infuse) -> (infusionrate=0)) #Not Verified test AG((infusionstatus=infuse) -> (infusionrate!=0)) #Not Verified test AG((infusionstatus=hold) -> topline in {holding, dispvtbi, volume, attention, options, locked, dispkvo, setvtbi, vtbidone, dispinfo, blank}) #Not Verified test AG(topline=holding -> AX(key1 -> topline=holding)) #Not Verified test AG(topline=dispkvo -> AX(pause -> topline=holding)) #Not Verified test AG(topline=volume -> (fndisp1=fnull & fndisp2=fclear & fndisp3=fquit)) #Not Verified test AG(topline=volume & infusionstatus=hold -> AX(key2 -> volumeinfused=0)) #Not Verified