[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,
Used simplifier rules/spec theorems by specification
Used from specification nat
Used from specification memory
- FLITPSC-preds/filter-w-empty
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSC-preds/no-pending-w-no-pending
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSC-preds/notMember-not-in
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSC-preds/notMember-onewriter-contra
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSC-preds/onemember-eq
is used by
step-absstep-R2-R4-tau-same,
step-absstep-R3-R4-tau-same,
step-absstep-PSCPERSIST_FO-tau,
- FLITPSC-preds/onemember-nowriter-contra
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSC-preds/onewriter-ctrok-nonzero
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-W6-W7-tau-same,
step-absstep-W6-W7-tau-other,
- FLITPSC-preds/oplus-addFO
is used by
step-absstep-W4-W5-tau-same,
step-absstep-R3-R4-tau-same,
- FLITPSC-preds/oplus-addW
is used by
step-absstep-W3-W4-doWritePSC-same,
- FLITPSC-preds/oplus-same-writes-eq
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSC-preds/overwrite-base
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSC-preds/overwrite-def
is used by
step-absstep-R1-R2-doReadPSC-same,
abs-init,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSC-preds/writersok-rm-writer
is used by
step-absstep-W6-W7-tau-other,
Used from specification PLIB-preds
- PLIB-preds/first-vol-write-split
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- PLIB-preds/nowrites-lastPersistedtrue
is used by
step-absstep-R1-R2-doReadPSC-same,
- PLIB-preds/persistDependentReads-restrict-other-loc
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- PLIB-preds/restrict-l-b-swap
is used by
step-absstep-W4-W5-tau-same,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB-preds/restrict-l-t-swap
is used by
step-absstep-W4-W5-tau-same,
- PLIB-preds/restrict-t-b-empty-expand-loc
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-ready-ready-callPSCCOMPLETE-same,
- PLIB-preds/restrict-t-b-swap
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB-preds/restrict-w-b-swap
is used by
step-absstep-R1-R2-doReadPSC-same,
- PLIB-preds/restrict-w-l-swap
is used by
step-absstep-R1-R2-doReadPSC-same,
- PLIB-preds/events-empty
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB-preds/first-vol-write-size
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- PLIB-preds/first-vol-write-size3
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- PLIB-preds/overwrite-attach-read
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
- PLIB-preds/overwrite-attach-write
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- PLIB-preds/persistDependentReads-restrict-empty
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- PLIB-preds/persistDependentReads-restrict-single-W
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- PLIB-preds/restrict-R-empty
is used by
step-absstep-W4-W5-tau-same,
- PLIB-preds/restrict-W-empty
is used by
step-absstep-R1-R2-doReadPSC-same,
- PLIB-preds/restrict-b-append
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- PLIB-preds/restrict-b-empty
is used by
step-absstep-R1-R2-doReadPSC-same,
abs-init,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- PLIB-preds/restrict-bool-one
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- PLIB-preds/restrict-false-attach-false
is used by
step-absstep-W3-W4-doWritePSC-same,
- PLIB-preds/restrict-l-append
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- PLIB-preds/restrict-l-empty
is used by
step-absstep-W4-W5-tau-same,
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB-preds/restrict-l-one
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-W4-W5-tau-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- PLIB-preds/restrict-read-one
is used by
step-absstep-W4-W5-tau-same,
- PLIB-preds/restrict-t-append
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- PLIB-preds/restrict-t-empty
is used by
step-absstep-R1-R2-doReadPSC-same,
abs-init,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCCRASH-globalPSCCRASH,
step-absstep-R1-R2-doReadPSC-other,
- PLIB-preds/restrict-t-one
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- PLIB-preds/restrict-true-attach-false
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- PLIB-preds/restrict-true-false-empty
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
Used from specification nat-basic
- nat-basic/a
is used by
step-absstep-W6-W7-tau-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
- nat-basic/c
is used by
step-absstep-W6-W7-tau-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
- nat-basic/f
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- nat-basic/oz
is used by
step-absstep-W6-W7-tau-same,
step-absstep-W6-W7-tau-other,
- nat-basic/z-01
is used by
step-absstep-W2-W3-tau-other,
Used from specification list
- list/one-01
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- list/Last
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-W4-W5-tau-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-R3-R4-tau-other,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-R3-R4-tau-same,
step-absstep-R1-R2-doReadPSC-other,
step-absstep-W4-W5-tau-other,
- list/Nil
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- list/a
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-W4-W5-tau-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-R3-R4-tau-other,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-R3-R4-tau-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
step-absstep-W4-W5-tau-other,
- list/app
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- list/app-02
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- list/c
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- list/c-04
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- list/c-05
is used by
step-absstep-W3-W4-doWritePSC-same,
- list/e
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-W4-W5-tau-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- list/eq-04
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- list/in-14
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- list/in-15
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- list/in-17
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-R3-R4-tau-other,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-R3-R4-tau-same,
step-absstep-W4-W5-tau-other,
- list/in-append
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-R3-R4-tau-other,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-R3-R4-tau-same,
step-absstep-W4-W5-tau-other,
- list/in-empty
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- list/in-rec
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- list/len
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- list/len-01
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- list/len-06
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
Used from specification RWevent
- RWevent/inj-W
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- RWevent/sel-R-dotl
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
- RWevent/sel-R-dott
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
- RWevent/sel-W-dotl
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- RWevent/sel-W-dott
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- RWevent/sel-W-dotv
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- RWevent/test-dotWque-W
is used by
step-absstep-W4-W5-tau-same,
Used from specification FOW
Used from specification PLIB
- PLIB/PLIBInv
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/PLIBLInv
is used by
step-absstep-W4-W5-tau-same,
- PLIB/plibInit
is used by
abs-init,
- PLIB/disj-AInvRead-AInvWrite
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
- PLIB/disj-AInvRead-callTSync
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-ready-ready-callPSCCOMPLETE-same,
step-absstep-ready-R1-invFLITPSCREAD-same,
- PLIB/disj-AInvWrite-callTSync
is used by
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-ready-ready-callPSCCOMPLETE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
- PLIB/disj-crashed-idle
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/disj-globalACrash-globalAPersist
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/disj-idle-invRead
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/disj-idle-invWrite
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/disj-idle-ready
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/disj-idle-resRead
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/disj-idle-resWrite
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/elim-mkPLIBgs
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-W4-W5-tau-same,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W1-W2-tau-same,
step-absstep-R3-R4-tau-other,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-R4-ready-retFLITPSCREAD-other,
step-absstep-R2-R3-tau-same,
step-absstep-R2-R3-tau-other,
step-absstep-W5-W6-tau-same,
step-absstep-W2-W3-tau-same,
step-absstep-ready-ready-callPSCCOMPLETE-same,
step-absstep-R2-R4-tau-same,
step-absstep-R3-R4-tau-same,
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-ready-W1-invFLITPSCWRITE-other,
step-absstep-W6-W7-tau-same,
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-ready-R1-invFLITPSCREAD-same,
step-absstep-W2-W3-tau-other,
step-absstep-PSCCRASH-globalPSCCRASH,
step-absstep-idle-ready-callPSCRUN-same,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
step-absstep-W4-W5-tau-other,
- PLIB/elim-mkPLIBls
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-W4-W5-tau-same,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W1-W2-tau-same,
step-absstep-R3-R4-tau-other,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-R4-ready-retFLITPSCREAD-other,
step-absstep-R2-R3-tau-same,
step-absstep-R2-R3-tau-other,
step-absstep-W5-W6-tau-same,
step-absstep-W2-W3-tau-same,
step-absstep-ready-ready-callPSCCOMPLETE-same,
step-absstep-R2-R4-tau-same,
step-absstep-R3-R4-tau-same,
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-ready-W1-invFLITPSCWRITE-other,
step-absstep-W6-W7-tau-same,
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-ready-R1-invFLITPSCREAD-same,
step-absstep-W2-W3-tau-other,
step-absstep-PSCCRASH-globalPSCCRASH,
step-absstep-idle-ready-callPSCRUN-same,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
step-absstep-W4-W5-tau-other,
- PLIB/gstepf-idle-ARun
is used by
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-idle-ready-callPSCRUN-same,
- PLIB/gstepf-invRead-ADOREAD
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
- PLIB/gstepf-invWrite-DOWRITE
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- PLIB/gstepf-ready
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-ready-ready-callPSCCOMPLETE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
- PLIB/gstepf-resRead-ARETREAD
is used by
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-R4-ready-retFLITPSCREAD-other,
- PLIB/gstepf-resWrite-RETWRITE
is used by
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
- PLIB/inj-ADoRead
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
- PLIB/inj-ADoWrite
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- PLIB/inj-AInvRead
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
- PLIB/inj-ARetRead
is used by
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-R4-ready-retFLITPSCREAD-other,
- PLIB/inj-ARetWrite
is used by
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
- PLIB/inj-callARun
is used by
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-idle-ready-callPSCRUN-same,
- PLIB/inj-callTSync
is used by
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-ready-ready-callPSCCOMPLETE-same,
- PLIB/inj-globalAPersist
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- PLIB/inj-mkPLIBgs
is used by
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-ready-W1-invFLITPSCWRITE-other,
- PLIB/inj-mkPLIBls
is used by
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-PSCPERSIST_FO-tau,
- PLIB/lstep
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/lstepf-idle-ARun
is used by
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-idle-ready-callPSCRUN-same,
- PLIB/lstepf-invRead-ADOREAD
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
- PLIB/lstepf-invWrite-DOWRITE
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- PLIB/lstepf-ready-INVREAD
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
- PLIB/lstepf-ready-INVWRITE
is used by
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
- PLIB/lstepf-ready-TSync
is used by
step-absstep-ready-ready-callPSCCOMPLETE-same,
- PLIB/lstepf-resRead-ARETREAD
is used by
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-R4-ready-retFLITPSCREAD-other,
- PLIB/lstepf-resWrite-RETWRITE
is used by
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
- PLIB/not-pre-global-crash
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/not-pre-global-persist
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- PLIB/pcstepf-idle-ARun
is used by
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-idle-ready-callPSCRUN-same,
- PLIB/pcstepf-invRead-ADOREAD
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
- PLIB/pcstepf-invWrite-DOWRITE
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- PLIB/pcstepf-ready-INVREAD
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
- PLIB/pcstepf-ready-INVWRITE
is used by
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
- PLIB/pcstepf-ready-TSync
is used by
step-absstep-ready-ready-callPSCCOMPLETE-same,
- PLIB/pcstepf-resRead-ARETREAD
is used by
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-R4-ready-retFLITPSCREAD-other,
- PLIB/pcstepf-resWrite-RETWRITE
is used by
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
- PLIB/plib-inv-allReadsOK
is used by
step-absstep-PSCPERSIST_FO-tau,
- PLIB/plibStep-lem
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/pre-idle
is used by
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-idle-ready-callPSCRUN-same,
- PLIB/pre-invRead
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
- PLIB/pre-invWrite
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- PLIB/pre-ready
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-ready-ready-callPSCCOMPLETE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
- PLIB/pre-resRead
is used by
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-R4-ready-retFLITPSCREAD-other,
- PLIB/pre-resWrite
is used by
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
- PLIB/sel-mkPLIBgs-doth
is used by
step-absstep-W4-W5-tau-same,
abs-init,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/sel-mkPLIBgs-dotpm
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/sel-mkPLIBgs-dotvm
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/sel-mkPLIBls-dotil
is used by
step-absstep-W4-W5-tau-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/sel-mkPLIBls-dotiv
is used by
step-absstep-W4-W5-tau-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/sel-mkPLIBls-dotov
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/sel-mkPLIBls-dott
is used by
step-absstep-W4-W5-tau-same,
abs-init,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- PLIB/upd-mkPLIBgs-doth
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- PLIB/upd-mkPLIBgs-dotvm
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- PLIB/upd-mkPLIBls-dotil
is used by
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
- PLIB/upd-mkPLIBls-dotiv
is used by
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
- PLIB/updsel--doth-doth
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- PLIB/updsel--doth-dotpm
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- PLIB/updsel--doth-dotvm
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- PLIB/updsel--dotil-dotil
is used by
step-absstep-ready-R1-invFLITPSCREAD-same,
- PLIB/updsel--dotil-dott
is used by
step-absstep-ready-R1-invFLITPSCREAD-same,
- PLIB/updsel--dotov-dotov
is used by
step-absstep-R1-R2-doReadPSC-same,
- PLIB/updsel--dotov-dott
is used by
step-absstep-R1-R2-doReadPSC-same,
- PLIB/updsel--dotpm-dotpm
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- PLIB/updsel--dotpm-dotvm
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
Used from specification set-union
- abs-FLITPSCweak-PLIB/abs-addReadFO
is used by
step-absstep-R3-R4-tau-same,
- abs-FLITPSCweak-PLIB/abs-addWrite
is used by
step-absstep-W3-W4-doWritePSC-same,
- abs-FLITPSCweak-PLIB/abs-addWriteFO
is used by
step-absstep-W4-W5-tau-same,
- abs-FLITPSCweak-PLIB/abs-def
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- abs-FLITPSCweak-PLIB/abs-h-p-nowritesh-allpersisted
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-W6-W7-tau-other,
- abs-FLITPSCweak-PLIB/abs-noReadFO
is used by
step-absstep-R2-R4-tau-same,
- abs-FLITPSCweak-PLIB/abs-persistFO-weak
is used by
step-absstep-PSCPERSIST_FO-tau,
- abs-FLITPSCweak-PLIB/abs-single-FO-no-pending
is used by
step-absstep-PSCPERSIST_FO-tau,
- abs-FLITPSCweak-PLIB/abs-single-FO-one-pending
is used by
step-absstep-PSCPERSIST_FO-tau,
- abs-FLITPSCweak-PLIB/counterzero
is used by
step-absstep-W6-W7-tau-other,
- abs-FLITPSCweak-PLIB/pofl-empty-all-l-persisted
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R2-R4-tau-same,
- abs-FLITPSCweak-PLIB/abs-addReadReader
is used by
step-absstep-R1-R2-doReadPSC-same,
- abs-FLITPSCweak-PLIB/abs-apply-firstPersistW
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- abs-FLITPSCweak-PLIB/abs-apply-persist-FO
is used by
step-absstep-PSCPERSIST_FO-tau,
- abs-FLITPSCweak-PLIB/abs-firstPersistW-firstVolWrite-correct-loc
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- abs-FLITPSCweak-PLIB/abs-firstPersistW-is-firstVolWrite
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- abs-FLITPSCweak-PLIB/abs-firstPersistW-is-in-hist
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- abs-FLITPSCweak-PLIB/abs-persist-firstPersistW
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- abs-FLITPSCweak-PLIB/absloc-base
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- abs-FLITPSCweak-PLIB/counterzero
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R2-R4-tau-same,
Used from specification list-data
Used from specification FLITPSCweak
- FLITPSCweak/FLITPSCInv
is used by
abs-init,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/FLITPSCLInv
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/flitpscInit
is used by
abs-init,
- FLITPSCweak/disj-R1-R2
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R1-W4
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R1-W5
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/disj-R1-crashed
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-R1-idle
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-R2-R4
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/disj-R2-W1
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R2-W2
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R2-W3
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R2-W4
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R2-W5
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R2-W6
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R2-W7
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R2-crashed
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W2-W3-tau-other,
step-absstep-PSCCRASH-globalPSCCRASH,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R2-idle
is used by
abs-init,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W2-W3-tau-other,
step-absstep-PSCCRASH-globalPSCCRASH,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R2-ready
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R3-R4
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R2-R3-tau-same,
step-absstep-R2-R3-tau-other,
step-absstep-R2-R4-tau-same,
- FLITPSCweak/disj-R3-W4
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R3-W5
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/disj-R3-crashed
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-R3-idle
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-R4-W4
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-R4-W5
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/disj-R4-crashed
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-R4-idle
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-W1-W4
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-W1-W5
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/disj-W1-crashed
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-W1-idle
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-W2-W4
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-W2-W5
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/disj-W2-crashed
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-W2-idle
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-W3-W4
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-W3-W5
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/disj-W3-crashed
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-W3-idle
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-W4-W5
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-W4-W6
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-W4-W7
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-W4-crashed
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCCRASH-globalPSCCRASH,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-W4-idle
is used by
abs-init,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCCRASH-globalPSCCRASH,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-W4-ready
is used by
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/disj-W5-W6
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/disj-W5-W7
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/disj-W5-crashed
is used by
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-W5-idle
is used by
abs-init,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-W5-ready
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/disj-W6-crashed
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-W6-idle
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-W7-crashed
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-W7-idle
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-callPSCCOMPLETE-invFLITPSCREAD
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-ready-ready-callPSCCOMPLETE-same,
step-absstep-ready-R1-invFLITPSCREAD-same,
- FLITPSCweak/disj-callPSCCOMPLETE-invFLITPSCWRITE
is used by
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-ready-ready-callPSCCOMPLETE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
- FLITPSCweak/disj-crashed-idle
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-crashed-ready
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-globalPSCCRASH-globalPSCPERSISTuscFO
is used by
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-globalPSCCRASH-globalPSCPERSISTuscW
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-globalPSCPERSISTuscFO-globalPSCPERSISTuscW
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/disj-idle-ready
is used by
abs-init,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/disj-invFLITPSCREAD-invFLITPSCWRITE
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
- FLITPSCweak/elim-mkFLITPSCgs
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-W4-W5-tau-same,
abs-init,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W1-W2-tau-same,
step-absstep-R3-R4-tau-other,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-R4-ready-retFLITPSCREAD-other,
step-absstep-R2-R3-tau-same,
step-absstep-R2-R3-tau-other,
step-absstep-W5-W6-tau-same,
step-absstep-W2-W3-tau-same,
step-absstep-ready-ready-callPSCCOMPLETE-same,
step-absstep-R2-R4-tau-same,
step-absstep-R3-R4-tau-same,
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-ready-W1-invFLITPSCWRITE-other,
step-absstep-W6-W7-tau-same,
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-ready-R1-invFLITPSCREAD-same,
step-absstep-W2-W3-tau-other,
step-absstep-PSCCRASH-globalPSCCRASH,
step-absstep-idle-ready-callPSCRUN-same,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
step-absstep-W4-W5-tau-other,
- FLITPSCweak/elim-mkFLITPSCls
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-W4-W5-tau-same,
abs-init,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-R3-R4-tau-other,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-R4-ready-retFLITPSCREAD-other,
step-absstep-R2-R3-tau-same,
step-absstep-R2-R3-tau-other,
step-absstep-W5-W6-tau-same,
step-absstep-W2-W3-tau-same,
step-absstep-ready-ready-callPSCCOMPLETE-same,
step-absstep-R2-R4-tau-same,
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-ready-W1-invFLITPSCWRITE-other,
step-absstep-W6-W7-tau-same,
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-ready-R1-invFLITPSCREAD-same,
step-absstep-W2-W3-tau-other,
step-absstep-PSCCRASH-globalPSCCRASH,
step-absstep-idle-ready-callPSCRUN-same,
step-absstep-W6-W7-tau-other,
step-absstep-R1-R2-doReadPSC-other,
step-absstep-W4-W5-tau-other,
- FLITPSCweak/fliqtStep-lem
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/gstepf-R1
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/gstepf-R2
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R2-R3-tau-same,
step-absstep-R2-R3-tau-other,
step-absstep-R2-R4-tau-same,
- FLITPSCweak/gstepf-R3
is used by
step-absstep-R3-R4-tau-other,
step-absstep-R3-R4-tau-same,
- FLITPSCweak/gstepf-R4
is used by
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-R4-ready-retFLITPSCREAD-other,
- FLITPSCweak/gstepf-W1
is used by
step-absstep-W1-W2-tau-same,
- FLITPSCweak/gstepf-W2
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W2-W3-tau-other,
- FLITPSCweak/gstepf-W3
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- FLITPSCweak/gstepf-W4
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W4-W5-tau-other,
- FLITPSCweak/gstepf-W5
is used by
step-absstep-W5-W6-tau-same,
- FLITPSCweak/gstepf-W6
is used by
step-absstep-W6-W7-tau-same,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/gstepf-W7
is used by
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
- FLITPSCweak/gstepf-idle-PSCRUN
is used by
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-idle-ready-callPSCRUN-same,
- FLITPSCweak/gstepf-ready
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-ready-ready-callPSCCOMPLETE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
- FLITPSCweak/inj-ctrDecPSC
is used by
step-absstep-W6-W7-tau-same,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/inj-ctrIncPSC
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W2-W3-tau-other,
- FLITPSCweak/inj-ctrReadPSC
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R2-R3-tau-same,
step-absstep-R2-R3-tau-other,
step-absstep-R2-R4-tau-same,
- FLITPSCweak/inj-doReadPSC
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/inj-doWritePSC
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- FLITPSCweak/inj-globalPSCPERSISTuscFO
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/inj-globalPSCPERSISTuscW
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- FLITPSCweak/inj-invFLITPSCREAD
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
- FLITPSCweak/inj-invFLITPSCWRITE
is used by
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
- FLITPSCweak/inj-pwbPSC
is used by
step-absstep-W4-W5-tau-same,
step-absstep-R3-R4-tau-other,
step-absstep-R3-R4-tau-same,
step-absstep-W4-W5-tau-other,
- FLITPSCweak/inj-retFLITPSCREAD
is used by
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-R4-ready-retFLITPSCREAD-other,
- FLITPSCweak/inj-sfencePSC
is used by
step-absstep-W1-W2-tau-same,
step-absstep-W5-W6-tau-same,
- FLITPSCweak/lstep
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/lstepf-R1
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/lstepf-R2
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R2-R3-tau-same,
step-absstep-R2-R3-tau-other,
step-absstep-R2-R4-tau-same,
- FLITPSCweak/lstepf-R3
is used by
step-absstep-R3-R4-tau-other,
step-absstep-R3-R4-tau-same,
- FLITPSCweak/lstepf-R4
is used by
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-R4-ready-retFLITPSCREAD-other,
- FLITPSCweak/lstepf-W1
is used by
step-absstep-W1-W2-tau-same,
- FLITPSCweak/lstepf-W2
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W2-W3-tau-other,
- FLITPSCweak/lstepf-W3
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- FLITPSCweak/lstepf-W4
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W4-W5-tau-other,
- FLITPSCweak/lstepf-W5
is used by
step-absstep-W5-W6-tau-same,
- FLITPSCweak/lstepf-W6
is used by
step-absstep-W6-W7-tau-same,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/lstepf-W7
is used by
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
- FLITPSCweak/lstepf-idle-PSCRUN
is used by
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-idle-ready-callPSCRUN-same,
- FLITPSCweak/lstepf-ready-FLITPSCREAD
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
- FLITPSCweak/lstepf-ready-FLITPSCWRITE
is used by
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
- FLITPSCweak/lstepf-ready-PSCCOMPLETE
is used by
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-ready-ready-callPSCCOMPLETE-same,
- FLITPSCweak/not-pre-global-crash
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/not-pre-global-persist
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- FLITPSCweak/not-pre-global-tsync
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/pcstepf-R1
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/pcstepf-R2
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R2-R3-tau-same,
step-absstep-R2-R3-tau-other,
step-absstep-R2-R4-tau-same,
- FLITPSCweak/pcstepf-R3
is used by
step-absstep-R3-R4-tau-other,
step-absstep-R3-R4-tau-same,
- FLITPSCweak/pcstepf-R4
is used by
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-R4-ready-retFLITPSCREAD-other,
- FLITPSCweak/pcstepf-W1
is used by
step-absstep-W1-W2-tau-same,
- FLITPSCweak/pcstepf-W2
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W2-W3-tau-other,
- FLITPSCweak/pcstepf-W3
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- FLITPSCweak/pcstepf-W4
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W4-W5-tau-other,
- FLITPSCweak/pcstepf-W5
is used by
step-absstep-W5-W6-tau-same,
- FLITPSCweak/pcstepf-W6
is used by
step-absstep-W6-W7-tau-same,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/pcstepf-W7
is used by
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
- FLITPSCweak/pcstepf-idle-PSCRUN
is used by
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-idle-ready-callPSCRUN-same,
- FLITPSCweak/pcstepf-ready-FLITPSCREAD
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
- FLITPSCweak/pcstepf-ready-FLITPSCWRITE
is used by
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
- FLITPSCweak/pcstepf-ready-PSCCOMPLETE
is used by
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-ready-ready-callPSCCOMPLETE-same,
- FLITPSCweak/pre-R1
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/pre-R2
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R2-R3-tau-same,
step-absstep-R2-R3-tau-other,
step-absstep-R2-R4-tau-same,
- FLITPSCweak/pre-R3
is used by
step-absstep-R3-R4-tau-other,
step-absstep-R3-R4-tau-same,
- FLITPSCweak/pre-R4
is used by
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-R4-ready-retFLITPSCREAD-other,
- FLITPSCweak/pre-W1
is used by
step-absstep-W1-W2-tau-same,
- FLITPSCweak/pre-W2
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W2-W3-tau-other,
- FLITPSCweak/pre-W3
is used by
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
- FLITPSCweak/pre-W4
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W4-W5-tau-other,
- FLITPSCweak/pre-W5
is used by
step-absstep-W5-W6-tau-same,
- FLITPSCweak/pre-W6
is used by
step-absstep-W6-W7-tau-same,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/pre-W7
is used by
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
- FLITPSCweak/pre-idle
is used by
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-idle-ready-callPSCRUN-same,
- FLITPSCweak/pre-ready
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-ready-ready-callPSCCOMPLETE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
- FLITPSCweak/sel-mkFLITPSCgs-dotctr
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/sel-mkFLITPSCgs-dotmem
is used by
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/sel-mkFLITPSCgs-dotp
is used by
abs-init,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/sel-mkFLITPSCgs-dotreaders
is used by
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/sel-mkFLITPSCgs-dotwriters
is used by
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/sel-mkFLITPSCls-dotl
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-ready-R1-invFLITPSCREAD-same,
step-absstep-PSCCRASH-globalPSCCRASH,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/sel-mkFLITPSCls-dott
is used by
step-absstep-R1-R2-doReadPSC-same,
abs-init,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-ready-R1-invFLITPSCREAD-same,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/sel-mkFLITPSCls-dotv
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
- FLITPSCweak/upd-mkFLITPSCgs-dotctr
is used by
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/upd-mkFLITPSCgs-dotmem
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- FLITPSCweak/upd-mkFLITPSCgs-dotp
is used by
step-absstep-R3-R4-tau-other,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-W4-W5-tau-other,
- FLITPSCweak/upd-mkFLITPSCgs-dotreaders
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R3-R4-tau-other,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/upd-mkFLITPSCgs-dotwriters
is used by
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/upd-mkFLITPSCls-dotl
is used by
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
- FLITPSCweak/upd-mkFLITPSCls-dotv
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/updsel--dotctr-dotctr
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W6-W7-tau-same,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/updsel--dotctr-dotmem
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W6-W7-tau-same,
- FLITPSCweak/updsel--dotctr-dotp
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W6-W7-tau-same,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/updsel--dotctr-dotreaders
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W6-W7-tau-same,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/updsel--dotmem-dotctr
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- FLITPSCweak/updsel--dotmem-dotmem
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- FLITPSCweak/updsel--dotmem-dotreaders
is used by
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
- FLITPSCweak/updsel--dotp-dotctr
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-R3-R4-tau-other,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-R3-R4-tau-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-W4-W5-tau-other,
- FLITPSCweak/updsel--dotp-dotmem
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-R3-R4-tau-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
- FLITPSCweak/updsel--dotp-dotp
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-R3-R4-tau-other,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-R3-R4-tau-same,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-W4-W5-tau-other,
- FLITPSCweak/updsel--dotp-dotreaders
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-W4-W5-tau-other,
- FLITPSCweak/updsel--dotp-dotwriters
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-R3-R4-tau-other,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-R3-R4-tau-same,
step-absstep-W4-W5-tau-other,
- FLITPSCweak/updsel--dotreaders-dotctr
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R3-R4-tau-other,
step-absstep-R2-R4-tau-same,
step-absstep-R3-R4-tau-same,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/updsel--dotreaders-dotmem
is used by
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R2-R4-tau-same,
step-absstep-R3-R4-tau-same,
- FLITPSCweak/updsel--dotreaders-dotp
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R3-R4-tau-other,
step-absstep-R2-R4-tau-same,
step-absstep-R3-R4-tau-same,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/updsel--dotreaders-dotreaders
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R3-R4-tau-other,
step-absstep-R2-R4-tau-same,
step-absstep-R3-R4-tau-same,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/updsel--dotreaders-dotwriters
is used by
step-absstep-R2-R4-tau-other,
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R3-R4-tau-other,
step-absstep-R2-R4-tau-same,
step-absstep-R3-R4-tau-same,
step-absstep-R1-R2-doReadPSC-other,
- FLITPSCweak/updsel--dotwriters-dotctr
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W6-W7-tau-same,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/updsel--dotwriters-dotmem
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W6-W7-tau-same,
- FLITPSCweak/updsel--dotwriters-dotp
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W6-W7-tau-same,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/updsel--dotwriters-dotreaders
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W6-W7-tau-same,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
- FLITPSCweak/updsel--dotwriters-dotwriters
is used by
step-absstep-W2-W3-tau-same,
step-absstep-W6-W7-tau-same,
step-absstep-W2-W3-tau-other,
step-absstep-W6-W7-tau-other,
Used from specification list-del