[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Theorem base summary for Specification PLIB

ACrash(0,0)disj-ADoWrite-AInvWrite(0,0)disj-AInvWrite-globalAPersist(0,0)disj-crashed-invRead(0,0)disj-ready-resWrite(0,0)inj-ARetWrite(0,0)pcstepf-ready-INVREAD(0,0)sel-AInvWrite-dott(0,0)upd-mkPLIBls-dotil(0,0)updsel--dotlsf-dotgstate(0,0)
PLIBGInv(0,0)disj-ADoWrite-ARetRead(0,0)disj-AInvWrite-tau(0,0)disj-crashed-invWrite(0,0)disj-resRead-resWrite(0,0)inj-callARun(0,0)pcstepf-ready-INVWRITE(0,0)sel-AInvWrite-dotval(0,0)upd-mkPLIBls-dotiv(0,0)updsel--dotlsf-dotlsf(0,0)
PLIBInv(0,0)disj-ADoWrite-ARetWrite(0,0)disj-ARetRead-ARetWrite(0,0)disj-crashed-ready(0,0)elim-mkPLIBgs(0,0)inj-callTSync(0,0)pcstepf-ready-TSync(0,0)sel-ARetRead-dott(0,0)upd-mkPLIBls-dotov(0,0)updsel--dotlsf-dotpcf(0,0)
PLIBLInv(0,0)disj-ADoWrite-callARun(0,0)disj-ARetRead-callARun(0,0)disj-crashed-resRead(0,0)elim-mkPLIBls(0,0)inj-globalAPersist(0,0)pcstepf-resRead-ARETREAD(0,0)sel-ARetRead-dotv(0,0)upd-mkPLIBls-dott(0,0)updsel--dotov-dotil(0,0)
PLIBRely(0,0)disj-ADoWrite-callTSync(0,0)disj-ARetRead-callTSync(0,0)disj-crashed-resWrite(0,0)elim-mkstate(0,0)inj-mkPLIBgs(0,0)pcstepf-resWrite-RETWRITE(0,0)sel-ARetWrite-dott(0,0)upd-mkstate-dotgstate(0,0)updsel--dotov-dotiv(0,0)
case-PLIBAction(0,0)disj-ADoWrite-globalACrash(0,0)disj-ARetRead-globalACrash(0,0)disj-globalACrash-globalAPersist(0,0)gen-PLIBAction(0,0)inj-mkPLIBls(0,0)plib-inv-allReadsOK(3,2)sel-callARun-dott(0,0)upd-mkstate-dotlsf(0,0)updsel--dotov-dotov(0,0)
case-PLIBGState(0,0)disj-ADoWrite-globalAPersist(0,0)disj-ARetRead-globalAPersist(0,0)disj-globalACrash-tau(0,0)gen-PLIBGState(0,0)inj-mkstate(0,0)plibInit(0,0)sel-callTSync-dott(0,0)upd-mkstate-dotpcf(0,0)updsel--dotov-dott(0,0)
case-PLIBLState(0,0)disj-ADoWrite-tau(0,0)disj-ARetRead-tau(0,0)disj-globalAPersist-tau(0,0)gen-PLIBLState(0,0)lstep(0,0)plibStep(0,0)sel-globalAPersist-dotinvAPersistl(0,0)updsel--dotgstate-dotgstate(0,0)updsel--dotpcf-dotgstate(0,0)
case-PLIBPC(0,0)disj-AInvRead-AInvWrite(0,0)disj-ARetWrite-callARun(0,0)disj-idle-invRead(0,0)gen-PLIBPC(0,0)lstepf-idle-ARun(0,0)plibStep-lem(18,3)sel-mkPLIBgs-doth(0,0)updsel--dotgstate-dotlsf(0,0)updsel--dotpcf-dotlsf(0,0)
case-PLIBState(0,0)disj-AInvRead-ARetRead(0,0)disj-ARetWrite-callTSync(0,0)disj-idle-invWrite(0,0)gen-PLIBState(0,0)lstepf-invRead-ADOREAD(0,0)pre-crashed(0,0)sel-mkPLIBgs-dotpm(0,0)updsel--dotgstate-dotpcf(0,0)updsel--dotpcf-dotpcf(0,0)
disj-ADoRead-ADoWrite(0,0)disj-AInvRead-ARetWrite(0,0)disj-ARetWrite-globalACrash(0,0)disj-idle-ready(0,0)gstepf-idle-ARun(0,0)lstepf-invWrite-DOWRITE(0,0)pre-idle(0,0)sel-mkPLIBgs-dotvm(0,0)updsel--doth-doth(0,0)updsel--dotpm-doth(0,0)
disj-ADoRead-AInvRead(0,0)disj-AInvRead-callARun(0,0)disj-ARetWrite-globalAPersist(0,0)disj-idle-resRead(0,0)gstepf-invRead-ADOREAD(0,0)lstepf-ready-INVREAD(0,0)pre-invRead(0,0)sel-mkPLIBls-dotil(0,0)updsel--doth-dotpm(0,0)updsel--dotpm-dotpm(0,0)
disj-ADoRead-AInvWrite(0,0)disj-AInvRead-callTSync(0,0)disj-ARetWrite-tau(0,0)disj-idle-resWrite(0,0)gstepf-invWrite-DOWRITE(0,0)lstepf-ready-INVWRITE(0,0)pre-invWrite(0,0)sel-mkPLIBls-dotiv(0,0)updsel--doth-dotvm(0,0)updsel--dotpm-dotvm(0,0)
disj-ADoRead-ARetRead(0,0)disj-AInvRead-globalACrash(0,0)disj-callARun-callTSync(0,0)disj-invRead-invWrite(0,0)gstepf-ready(0,0)lstepf-ready-TSync(0,0)pre-ready(0,0)sel-mkPLIBls-dotov(0,0)updsel--dotil-dotil(0,0)updsel--dott-dotil(0,0)
disj-ADoRead-ARetWrite(0,0)disj-AInvRead-globalAPersist(0,0)disj-callARun-globalACrash(0,0)disj-invRead-ready(0,0)gstepf-resRead-ARETREAD(0,0)lstepf-resRead-ARETREAD(0,0)pre-resRead(0,0)sel-mkPLIBls-dott(0,0)updsel--dotil-dotiv(0,0)updsel--dott-dotiv(0,0)
disj-ADoRead-callARun(0,0)disj-AInvRead-tau(0,0)disj-callARun-globalAPersist(0,0)disj-invRead-resRead(0,0)gstepf-resWrite-RETWRITE(0,0)lstepf-resWrite-RETWRITE(0,0)pre-resWrite(0,0)sel-mkstate-dotgstate(0,0)updsel--dotil-dotov(0,0)updsel--dott-dotov(0,0)
disj-ADoRead-callTSync(0,0)disj-AInvWrite-ARetRead(0,0)disj-callARun-tau(0,0)disj-invRead-resWrite(0,0)inj-ADoRead(0,0)not-pre-global-crash(4,2)sel-ADoRead-dott(0,0)sel-mkstate-dotlsf(0,0)updsel--dotil-dott(0,0)updsel--dott-dott(0,0)
disj-ADoRead-globalACrash(0,0)disj-AInvWrite-ARetWrite(0,0)disj-callTSync-globalACrash(0,0)disj-invWrite-ready(0,0)inj-ADoWrite(0,0)not-pre-global-persist(4,2)sel-ADoWrite-dott(0,0)sel-mkstate-dotpcf(0,0)updsel--dotiv-dotil(0,0)updsel--dotvm-doth(0,0)
disj-ADoRead-globalAPersist(0,0)disj-AInvWrite-callARun(0,0)disj-callTSync-globalAPersist(0,0)disj-invWrite-resRead(0,0)inj-AInvRead(0,0)pcstepf-idle-ARun(0,0)sel-AInvRead-dotl(0,0)upd-mkPLIBgs-doth(0,0)updsel--dotiv-dotiv(0,0)updsel--dotvm-dotpm(0,0)
disj-ADoRead-tau(0,0)disj-AInvWrite-callTSync(0,0)disj-callTSync-tau(0,0)disj-invWrite-resWrite(0,0)inj-AInvWrite(0,0)pcstepf-invRead-ADOREAD(0,0)sel-AInvRead-dott(0,0)upd-mkPLIBgs-dotpm(0,0)updsel--dotiv-dotov(0,0)updsel--dotvm-dotvm(0,0)
disj-ADoWrite-AInvRead(0,0)disj-AInvWrite-globalACrash(0,0)disj-crashed-idle(0,0)disj-ready-resRead(0,0)inj-ARetRead(0,0)pcstepf-invWrite-DOWRITE(0,0)sel-AInvWrite-dotloc(0,0)upd-mkPLIBgs-dotvm(0,0)updsel--dotiv-dott(0,0)