[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 list-last
Used from specification nat
- nat/l-num-05
is used by
step-absstep-PROP_FO-tau,
- nat/le-num-05
is used by
step-absstep-PROP_FO-tau,
- nat/lels
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- nat/lez
is used by
step-absstep-PROP_FO-tau,
- nat/lez-01
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- nat/one-01
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- nat/succ-01
is used by
step-absstep-PROP_FO-tau,
- abs-FLIT-FLITPSCweak/isPropFO-in-bq
is used by
step-absstep-PROP_FO-tau,
- abs-FLIT-FLITPSCweak/reorder-def
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
- abs-FLIT-FLITPSCweak/reorder-isPersistFO-exists-lifted
is used by
step-absstep-PERSIST_FO-globalPERSIST_FO,
- abs-FLIT-FLITPSCweak/reorder-step-propFO-lifted
is used by
step-absstep-PROP_FO-doWriteFO,
- abs-FLIT-FLITPSCweak/reorder-step-propW-lifted
is used by
step-absstep-PROP_W-doWrite,
- abs-FLIT-FLITPSCweak/reorder-step-read-propFO-lifted
is used by
step-absstep-PROP_FO-tau,
- abs-FLIT-FLITPSCweak/propFOs-base
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
- abs-FLIT-FLITPSCweak/reorder-base
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
- abs-FLIT-FLITPSCweak/reorder-firstPersistW-eq-lifted
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- abs-FLIT-FLITPSCweak/reorder-firstPersistW-valid-lifted
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- abs-FLIT-FLITPSCweak/reorder-fo-in-p-lifted
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-ready-ready-callFLITCOMPLETE-same,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- abs-FLIT-FLITPSCweak/reorder-overwrite-p-eq-lifted
is used by
step-absstep-PROP_FO-tau,
step-absstep-R1-R2-doRead-other,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-R1-R2-doRead-same,
step-absstep-PROP_SF-propSF,
- abs-FLIT-FLITPSCweak/reorder-step-persistFO-lifted
is used by
step-absstep-PERSIST_FO-globalPERSIST_FO,
- abs-FLIT-FLITPSCweak/reorder-step-persistW-lifted
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- abs-FLIT-FLITPSCweak/reorder-step-readPWB-lifted
is used by
step-absstep-R3-R4-pwb-same,
- FLITPSC-preds/oneWriter
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- FLITPSC-preds/ctrok-size-writers-eq-ctr
is used by
step-absstep-PROP_FO-tau,
- FLITPSC-preds/notMember-onewriter-contra
is used by
step-absstep-PROP_FO-tau,
- FLITPSC-preds/onemember-eq
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLITPSC-preds/onemember-nowriter-contra
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- FLITPSC-preds/oplus-same-writes-eq
is used by
step-absstep-R1-R2-doRead-same,
- FLITPSC-preds/overwrite-def
is used by
step-absstep-PROP_FO-tau,
step-absstep-R1-R2-doRead-other,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-R1-R2-doRead-same,
step-absstep-PROP_SF-propSF,
Used from specification FLIT-preds
- FLIT-preds/isPropFO-def
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- FLIT-preds/isPropFO-drop-last-SF
is used by
step-absstep-PROP_FO-tau,
- FLIT-preds/writersOk
is used by
step-absstep-PROP_FO-tau,
- FLIT-preds/SFTrailing-attach
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-W1-W2-tau-same,
step-absstep-W5-W6-tau-same,
step-absstep-R3-R4-pwb-other,
step-absstep-W3-W4-tau-same,
step-absstep-W1-W2-tau-other,
step-absstep-R3-R4-pwb-same,
step-absstep-W3-W4-tau-other,
step-absstep-W4-W5-tau-other,
- FLIT-preds/SFTrailing-leading-SF
is used by
step-absstep-PROP_SF-propSF,
- FLIT-preds/isPropFO-SF-in-delpos
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- FLIT-preds/isPropFO-W-in-delpos
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT-preds/isPropFO-delpos-last-SF
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- FLIT-preds/isPropFO-empty
is used by
step-absstep-PROP_FO-tau,
- FLIT-preds/isPropFO-leading-SF
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- FLIT-preds/isPropFO-not-leading-FO
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT-preds/isPropFO-not-leading-W
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT-preds/noPending-no-leading-bq-W
is used by
step-absstep-W6-W7-ctrDec-other,
step-absstep-PROP_W-doWrite,
step-absstep-W6-W7-ctrDec-same,
- FLIT-preds/noPendingW-no-leading-bq-W
is used by
step-absstep-PROP_W-doWrite,
- FLIT-preds/oplus-noPendingW
is used by
step-absstep-R1-R2-doRead-same,
- FLIT-preds/pendingOk-no-two-buffered-Ws
is used by
step-absstep-PROP_W-doWrite,
- FLIT-preds/readFOsOk-empty-rfo-while-writing
is used by
step-absstep-PROP_FO-tau,
- FLIT-preds/readFOsOk-not-one-SF
is used by
step-absstep-PROP_SF-propSF,
Used from specification set-basic
- set-basic/ne-01
is used by
step-absstep-PROP_FO-tau,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- set-basic/size-zero
is used by
step-absstep-CRASH-globalCRASH,
- set-basic/size-zero-01
is used by
step-absstep-PROP_FO-tau,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
Used from specification list-getput
Used from specification nat-basic
- nat-basic/a
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- nat-basic/c
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- nat-basic/f
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- nat-basic/less-zero
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- nat-basic/one-01
is used by
step-absstep-PROP_FO-tau,
- nat-basic/oz
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- nat-basic/s-04
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- nat-basic/succ
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- nat-basic/zero
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
Used from specification list
- list/some-element
is used by
step-absstep-PROP_FO-tau,
- list/Last
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-R3-R4-pwb-other,
step-absstep-W3-W4-tau-same,
step-absstep-W1-W2-tau-other,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-W3-W4-tau-other,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-W4-W5-tau-other,
step-absstep-PROP_SF-propSF,
- list/Nil
is used by
step-absstep-PROP_FO-tau,
step-absstep-W3-W4-tau-same,
step-absstep-W3-W4-tau-other,
- list/a
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-R3-R4-pwb-other,
step-absstep-W6-W7-ctrDec-other,
step-absstep-W3-W4-tau-same,
step-absstep-W1-W2-tau-other,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-W6-W7-ctrDec-same,
step-absstep-W3-W4-tau-other,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-W4-W5-tau-other,
step-absstep-PROP_SF-propSF,
- list/app
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_SF-propSF,
- list/app-02
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-W3-W4-tau-same,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-W3-W4-tau-other,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-W4-W5-tau-other,
step-absstep-PROP_SF-propSF,
- list/app-03
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-W1-W2-tau-same,
step-absstep-W5-W6-tau-same,
step-absstep-W1-W2-tau-other,
step-absstep-W4-W5-tau-other,
- list/app-04
is used by
step-absstep-W1-W2-tau-same,
step-absstep-W1-W2-tau-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- list/app-05
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-W4-W5-tau-other,
step-absstep-PROP_SF-propSF,
- list/c
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- list/c-03
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- list/c-05
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W3-W4-tau-same,
step-absstep-W3-W4-tau-other,
step-absstep-PROP_SF-propSF,
- list/c-06
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- list/c-08
is used by
step-absstep-PROP_SF-propSF,
- list/e
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-W3-W4-tau-same,
step-absstep-W1-W2-tau-other,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-W3-W4-tau-other,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-W4-W5-tau-other,
step-absstep-PROP_SF-propSF,
- list/eq-05
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- list/first
is used by
step-absstep-W3-W4-tau-same,
step-absstep-W3-W4-tau-other,
step-absstep-PROP_SF-propSF,
- list/in-06
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_W-doWrite,
- list/in-10
is used by
step-absstep-PROP_FO-doWriteFO,
- list/in-12
is used by
step-absstep-PROP_SF-propSF,
- list/in-14
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- list/in-15
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- list/in-17
is used by
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-R3-R4-pwb-other,
step-absstep-W3-W4-tau-same,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-W3-W4-tau-other,
step-absstep-W4-W5-tau-other,
- list/in-append
is used by
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-R3-R4-pwb-other,
step-absstep-W3-W4-tau-same,
step-absstep-R3-R4-pwb-same,
step-absstep-W3-W4-tau-other,
step-absstep-W4-W5-tau-other,
- list/in-empty
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-ready-ready-callFLITCOMPLETE-same,
step-absstep-W3-W4-tau-same,
step-absstep-W6-W7-ctrDec-same,
step-absstep-W3-W4-tau-other,
step-absstep-W7-ready-retFLITWRITE-same,
step-absstep-PROP_SF-propSF,
- list/in-rec
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- list/inapp-10
is used by
step-absstep-PROP_FO-tau,
- list/len-02
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- list/len-05
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- list/len-06
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-R3-R4-pwb-same,
- list/one-01
is used by
step-absstep-PROP_FO-tau,
Used from specification FOW
Used from specification FLIT
- FLIT/FLITGInv
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/FLITInv
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/FLITLInv
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/flitInit
is used by
abs-init,
- FLIT/flitStep
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLIT/disj-R1-R3
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-R1-W2
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_SF-propSF,
- FLIT/disj-R1-W4
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-R1-W5
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-R1-W6
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-R1-crashed
is used by
step-absstep-CRASH-globalCRASH,
- FLIT/disj-R1-idle
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-R2-R3
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-R2-W2
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_SF-propSF,
- FLIT/disj-R2-W4
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-R2-W5
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-R2-W6
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-R2-crashed
is used by
step-absstep-CRASH-globalCRASH,
- FLIT/disj-R2-idle
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-R3-R4
is used by
step-absstep-R2-R4-ctrRead-other,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R2-R3-ctrRead-same,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R2-R3-ctrRead-other,
- FLIT/disj-R3-W1
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-R3-W2
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_SF-propSF,
- FLIT/disj-R3-W3
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-R3-W4
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-R3-W5
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-R3-W6
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-R3-W7
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-R3-crashed
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-R3-idle
is used by
abs-init,
step-absstep-PROP_FO-doWriteFO,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-R3-ready
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-R4-W2
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_SF-propSF,
- FLIT/disj-R4-W4
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-R4-W5
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-R4-W6
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-R4-crashed
is used by
step-absstep-CRASH-globalCRASH,
- FLIT/disj-R4-idle
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-W1-W2
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W1-W4
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-W1-W5
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-W1-W6
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W1-crashed
is used by
step-absstep-CRASH-globalCRASH,
- FLIT/disj-W1-idle
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-W2-W3
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W2-W4
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W2-W5
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W2-W6
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W2-W7
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W2-crashed
is used by
step-absstep-PROP_FO-tau,
step-absstep-CRASH-globalCRASH,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W2-idle
is used by
abs-init,
step-absstep-PROP_FO-tau,
step-absstep-CRASH-globalCRASH,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W2-ready
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W3-W4
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-W3-W5
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-W3-W6
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W3-crashed
is used by
step-absstep-CRASH-globalCRASH,
- FLIT/disj-W3-idle
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-W4-W5
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-W4-W6
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W4-W7
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-W4-crashed
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-W4-idle
is used by
abs-init,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-W4-ready
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-W5-W6
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W5-W7
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-W5-crashed
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-W5-idle
is used by
abs-init,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-W5-ready
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-W6-W7
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W6-crashed
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W6-idle
is used by
abs-init,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W6-ready
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-W7-crashed
is used by
step-absstep-CRASH-globalCRASH,
- FLIT/disj-W7-idle
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-callFLITCOMPLETE-doWrite
is used by
step-absstep-PROP_W-doWrite,
- FLIT/disj-callFLITCOMPLETE-doWriteFO
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-callFLITCOMPLETE-invFLITREAD
is used by
step-absstep-ready-ready-callFLITCOMPLETE-same,
step-absstep-ready-R1-invFLITREAD-other,
step-absstep-ready-R1-invFLITREAD-same,
step-absstep-ready-ready-callFLITCOMPLETE-other,
- FLIT/disj-callFLITCOMPLETE-invFLITWRITE
is used by
step-absstep-ready-ready-callFLITCOMPLETE-same,
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-ready-callFLITCOMPLETE-other,
step-absstep-ready-W1-invFLITWRITE-other,
- FLIT/disj-callFLITCOMPLETE-propFO
is used by
step-absstep-PROP_FO-tau,
- FLIT/disj-callFLITCOMPLETE-propSF
is used by
step-absstep-PROP_SF-propSF,
- FLIT/disj-callRUN-doWrite
is used by
step-absstep-PROP_W-doWrite,
- FLIT/disj-callRUN-doWriteFO
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-callRUN-propFO
is used by
step-absstep-PROP_FO-tau,
- FLIT/disj-callRUN-propSF
is used by
step-absstep-PROP_SF-propSF,
- FLIT/disj-crashed-idle
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-crashed-ready
is used by
step-absstep-CRASH-globalCRASH,
- FLIT/disj-ctrDec-doWrite
is used by
step-absstep-PROP_W-doWrite,
- FLIT/disj-ctrDec-doWriteFO
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-ctrDec-propFO
is used by
step-absstep-PROP_FO-tau,
- FLIT/disj-ctrDec-propSF
is used by
step-absstep-PROP_SF-propSF,
- FLIT/disj-ctrInc-doWrite
is used by
step-absstep-PROP_W-doWrite,
- FLIT/disj-ctrInc-doWriteFO
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-ctrInc-propFO
is used by
step-absstep-PROP_FO-tau,
- FLIT/disj-ctrInc-propSF
is used by
step-absstep-PROP_SF-propSF,
- FLIT/disj-ctrRead-doWrite
is used by
step-absstep-PROP_W-doWrite,
- FLIT/disj-ctrRead-doWriteFO
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-ctrRead-propFO
is used by
step-absstep-PROP_FO-tau,
- FLIT/disj-ctrRead-propSF
is used by
step-absstep-PROP_SF-propSF,
- FLIT/disj-doRead-doWrite
is used by
step-absstep-PROP_W-doWrite,
- FLIT/disj-doRead-doWriteFO
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-doRead-propFO
is used by
step-absstep-PROP_FO-tau,
- FLIT/disj-doRead-propSF
is used by
step-absstep-PROP_SF-propSF,
- FLIT/disj-doWrite-doWriteFO
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLIT/disj-doWrite-globalCRASH
is used by
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-doWrite-globalPERSISTuscFO
is used by
step-absstep-PROP_W-doWrite,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLIT/disj-doWrite-globalPERSISTuscW
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
- FLIT/disj-doWrite-invFLITREAD
is used by
step-absstep-PROP_W-doWrite,
- FLIT/disj-doWrite-invFLITWRITE
is used by
step-absstep-PROP_W-doWrite,
- FLIT/disj-doWrite-propFO
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_W-doWrite,
- FLIT/disj-doWrite-propSF
is used by
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/disj-doWrite-pwb
is used by
step-absstep-PROP_W-doWrite,
- FLIT/disj-doWrite-retFLITREAD
is used by
step-absstep-PROP_W-doWrite,
- FLIT/disj-doWrite-retFLITWRITE
is used by
step-absstep-PROP_W-doWrite,
- FLIT/disj-doWrite-sfence
is used by
step-absstep-PROP_W-doWrite,
- FLIT/disj-doWrite-tau
is used by
step-absstep-PROP_W-doWrite,
- FLIT/disj-doWriteFO-globalCRASH
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-doWriteFO-globalPERSISTuscFO
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLIT/disj-doWriteFO-globalPERSISTuscW
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
- FLIT/disj-doWriteFO-invFLITREAD
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-doWriteFO-invFLITWRITE
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-doWriteFO-propFO
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-doWriteFO-propSF
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_SF-propSF,
- FLIT/disj-doWriteFO-pwb
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-doWriteFO-retFLITREAD
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-doWriteFO-retFLITWRITE
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-doWriteFO-sfence
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-doWriteFO-tau
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/disj-globalCRASH-globalPERSISTuscFO
is used by
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLIT/disj-globalCRASH-globalPERSISTuscW
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-globalCRASH-propFO
is used by
step-absstep-PROP_FO-tau,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-globalCRASH-propSF
is used by
step-absstep-CRASH-globalCRASH,
step-absstep-PROP_SF-propSF,
- FLIT/disj-globalPERSISTuscFO-globalPERSISTuscW
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLIT/disj-globalPERSISTuscFO-propFO
is used by
step-absstep-PROP_FO-tau,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLIT/disj-globalPERSISTuscFO-propSF
is used by
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLIT/disj-globalPERSISTuscW-propFO
is used by
step-absstep-PROP_FO-tau,
step-absstep-PERSIST_W-globalPERSIST_W,
- FLIT/disj-globalPERSISTuscW-propSF
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_SF-propSF,
- FLIT/disj-idle-ready
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
- FLIT/disj-invFLITREAD-invFLITWRITE
is used by
step-absstep-ready-R1-invFLITREAD-other,
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-R1-invFLITREAD-same,
step-absstep-ready-W1-invFLITWRITE-other,
- FLIT/disj-invFLITREAD-propFO
is used by
step-absstep-PROP_FO-tau,
- FLIT/disj-invFLITREAD-propSF
is used by
step-absstep-PROP_SF-propSF,
- FLIT/disj-invFLITWRITE-propFO
is used by
step-absstep-PROP_FO-tau,
- FLIT/disj-invFLITWRITE-propSF
is used by
step-absstep-PROP_SF-propSF,
- FLIT/disj-propFO-propSF
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_SF-propSF,
- FLIT/disj-propFO-pwb
is used by
step-absstep-PROP_FO-tau,
- FLIT/disj-propFO-retFLITREAD
is used by
step-absstep-PROP_FO-tau,
- FLIT/disj-propFO-retFLITWRITE
is used by
step-absstep-PROP_FO-tau,
- FLIT/disj-propFO-sfence
is used by
step-absstep-PROP_FO-tau,
- FLIT/disj-propFO-tau
is used by
step-absstep-PROP_FO-tau,
- FLIT/disj-propSF-pwb
is used by
step-absstep-PROP_SF-propSF,
- FLIT/disj-propSF-retFLITREAD
is used by
step-absstep-PROP_SF-propSF,
- FLIT/disj-propSF-retFLITWRITE
is used by
step-absstep-PROP_SF-propSF,
- FLIT/disj-propSF-sfence
is used by
step-absstep-PROP_SF-propSF,
- FLIT/disj-propSF-tau
is used by
step-absstep-PROP_SF-propSF,
- FLIT/gstepf-R1
is used by
step-absstep-PROP_FO-tau,
step-absstep-R1-R2-doRead-other,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-R1-R2-doRead-same,
step-absstep-PROP_SF-propSF,
- FLIT/gstepf-R2
is used by
step-absstep-R2-R4-ctrRead-other,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R2-R3-ctrRead-same,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R2-R3-ctrRead-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/gstepf-R3
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/gstepf-R4
is used by
step-absstep-R4-ready-retFLITREAD-other,
step-absstep-R4-ready-retFLITREAD-same,
- FLIT/gstepf-W1
is used by
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W1-W2-tau-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/gstepf-W2
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W2-W3-ctrInc-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/gstepf-W3
is used by
step-absstep-W3-W4-tau-same,
step-absstep-W3-W4-tau-other,
- FLIT/gstepf-W4
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W4-W5-tau-other,
- FLIT/gstepf-W5
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W5-W6-tau-same,
- FLIT/gstepf-W6
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W6-W7-ctrDec-other,
step-absstep-PROP_W-doWrite,
step-absstep-W6-W7-ctrDec-same,
step-absstep-PROP_SF-propSF,
- FLIT/gstepf-W7
is used by
step-absstep-W7-ready-retFLITWRITE-other,
step-absstep-W7-ready-retFLITWRITE-same,
- FLIT/gstepf-idle-RUN
is used by
step-absstep-idle-ready-callRUN-other,
step-absstep-idle-ready-callRUN-same,
- FLIT/gstepf-ready
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-ready-ready-callFLITCOMPLETE-same,
step-absstep-ready-R1-invFLITREAD-other,
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-R1-invFLITREAD-same,
step-absstep-ready-ready-callFLITCOMPLETE-other,
step-absstep-PROP_W-doWrite,
step-absstep-ready-W1-invFLITWRITE-other,
step-absstep-PROP_SF-propSF,
- FLIT/inj-ctrDec
is used by
step-absstep-W6-W7-ctrDec-other,
step-absstep-W6-W7-ctrDec-same,
- FLIT/inj-ctrInc
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W2-W3-ctrInc-other,
- FLIT/inj-ctrRead
is used by
step-absstep-R2-R4-ctrRead-other,
step-absstep-R2-R3-ctrRead-same,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R2-R3-ctrRead-other,
- FLIT/inj-doRead
is used by
step-absstep-R1-R2-doRead-other,
step-absstep-R1-R2-doRead-same,
- FLIT/inj-doWrite
is used by
step-absstep-PROP_W-doWrite,
- FLIT/inj-doWriteFO
is used by
step-absstep-PROP_FO-doWriteFO,
- FLIT/inj-globalPERSISTuscFO
is used by
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLIT/inj-globalPERSISTuscW
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- FLIT/inj-invFLITREAD
is used by
step-absstep-ready-R1-invFLITREAD-other,
step-absstep-ready-R1-invFLITREAD-same,
- FLIT/inj-invFLITWRITE
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-W1-invFLITWRITE-other,
- FLIT/inj-propFO
is used by
step-absstep-PROP_FO-tau,
- FLIT/inj-propSF
is used by
step-absstep-PROP_SF-propSF,
- FLIT/inj-pwb
is used by
step-absstep-R3-R4-pwb-other,
step-absstep-R3-R4-pwb-same,
- FLIT/inj-retFLITREAD
is used by
step-absstep-R4-ready-retFLITREAD-other,
step-absstep-R4-ready-retFLITREAD-same,
- FLIT/inj-sfence
is used by
step-absstep-W1-W2-tau-same,
step-absstep-W1-W2-tau-other,
- FLIT/lstep
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLIT/lstepf-R1
is used by
step-absstep-PROP_FO-tau,
step-absstep-R1-R2-doRead-other,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-R1-R2-doRead-same,
step-absstep-PROP_SF-propSF,
- FLIT/lstepf-R2
is used by
step-absstep-R2-R4-ctrRead-other,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R2-R3-ctrRead-same,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R2-R3-ctrRead-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/lstepf-R3
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/lstepf-R4
is used by
step-absstep-R4-ready-retFLITREAD-same,
- FLIT/lstepf-W1
is used by
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W1-W2-tau-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/lstepf-W2
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W2-W3-ctrInc-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/lstepf-W3
is used by
step-absstep-W3-W4-tau-same,
step-absstep-W3-W4-tau-other,
- FLIT/lstepf-W4
is used by
step-absstep-W4-W5-tau-same,
step-absstep-W4-W5-tau-other,
- FLIT/lstepf-W5
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W5-W6-tau-same,
- FLIT/lstepf-W6
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W6-W7-ctrDec-other,
step-absstep-PROP_W-doWrite,
step-absstep-W6-W7-ctrDec-same,
step-absstep-PROP_SF-propSF,
- FLIT/lstepf-W7
is used by
step-absstep-W7-ready-retFLITWRITE-other,
step-absstep-W7-ready-retFLITWRITE-same,
- FLIT/lstepf-idle-RUN
is used by
step-absstep-idle-ready-callRUN-other,
step-absstep-idle-ready-callRUN-same,
- FLIT/lstepf-ready-FLITCOMPLETE
is used by
step-absstep-ready-ready-callFLITCOMPLETE-same,
step-absstep-ready-ready-callFLITCOMPLETE-other,
- FLIT/lstepf-ready-FLITREAD
is used by
step-absstep-ready-R1-invFLITREAD-other,
step-absstep-ready-R1-invFLITREAD-same,
- FLIT/lstepf-ready-FLITWRITE
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-W1-invFLITWRITE-other,
- FLIT/not-pre-global-crash
is used by
step-absstep-CRASH-globalCRASH,
- FLIT/not-pre-global-persist
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- FLIT/not-pre-global-tsync
is used by
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLIT/pcstepf-R1
is used by
step-absstep-PROP_FO-tau,
step-absstep-R1-R2-doRead-other,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-R1-R2-doRead-same,
step-absstep-PROP_SF-propSF,
- FLIT/pcstepf-R2
is used by
step-absstep-R2-R4-ctrRead-other,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R2-R3-ctrRead-same,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R2-R3-ctrRead-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pcstepf-R3
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pcstepf-R4
is used by
step-absstep-R4-ready-retFLITREAD-other,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R4-ready-retFLITREAD-same,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pcstepf-W1
is used by
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W1-W2-tau-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pcstepf-W2
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W2-W3-ctrInc-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pcstepf-W3
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W3-W4-tau-same,
step-absstep-PROP_W-doWrite,
step-absstep-W3-W4-tau-other,
step-absstep-PROP_SF-propSF,
- FLIT/pcstepf-W4
is used by
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-W4-W5-tau-other,
step-absstep-PROP_SF-propSF,
- FLIT/pcstepf-W5
is used by
step-absstep-W5-W6-tau-other,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pcstepf-W6
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W6-W7-ctrDec-other,
step-absstep-PROP_W-doWrite,
step-absstep-W6-W7-ctrDec-same,
step-absstep-PROP_SF-propSF,
- FLIT/pcstepf-W7
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-W7-ready-retFLITWRITE-other,
step-absstep-W7-ready-retFLITWRITE-same,
step-absstep-PROP_SF-propSF,
- FLIT/pcstepf-idle-RUN
is used by
step-absstep-idle-ready-callRUN-other,
step-absstep-idle-ready-callRUN-same,
- FLIT/pcstepf-ready-FLITCOMPLETE
is used by
step-absstep-ready-ready-callFLITCOMPLETE-same,
step-absstep-ready-ready-callFLITCOMPLETE-other,
- FLIT/pcstepf-ready-FLITREAD
is used by
step-absstep-ready-R1-invFLITREAD-other,
step-absstep-ready-R1-invFLITREAD-same,
- FLIT/pcstepf-ready-FLITWRITE
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-W1-invFLITWRITE-other,
- FLIT/pre-R1
is used by
step-absstep-PROP_FO-tau,
step-absstep-R1-R2-doRead-other,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-R1-R2-doRead-same,
step-absstep-PROP_SF-propSF,
- FLIT/pre-R2
is used by
step-absstep-R2-R4-ctrRead-other,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R2-R3-ctrRead-same,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R2-R3-ctrRead-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pre-R3
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pre-R4
is used by
step-absstep-R4-ready-retFLITREAD-other,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R4-ready-retFLITREAD-same,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pre-W1
is used by
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W1-W2-tau-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pre-W2
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W2-W3-ctrInc-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pre-W3
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W3-W4-tau-same,
step-absstep-PROP_W-doWrite,
step-absstep-W3-W4-tau-other,
step-absstep-PROP_SF-propSF,
- FLIT/pre-W4
is used by
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-W4-W5-tau-other,
step-absstep-PROP_SF-propSF,
- FLIT/pre-W5
is used by
step-absstep-W5-W6-tau-other,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pre-W6
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W6-W7-ctrDec-other,
step-absstep-PROP_W-doWrite,
step-absstep-W6-W7-ctrDec-same,
step-absstep-PROP_SF-propSF,
- FLIT/pre-W7
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-W7-ready-retFLITWRITE-other,
step-absstep-W7-ready-retFLITWRITE-same,
step-absstep-PROP_SF-propSF,
- FLIT/pre-crashed
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pre-idle
is used by
step-absstep-idle-ready-callRUN-other,
step-absstep-idle-ready-callRUN-same,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLIT/pre-ready
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-ready-ready-callFLITCOMPLETE-same,
step-absstep-ready-R1-invFLITREAD-other,
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-R1-invFLITREAD-same,
step-absstep-ready-ready-callFLITCOMPLETE-other,
step-absstep-PROP_W-doWrite,
step-absstep-ready-W1-invFLITWRITE-other,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotbq-dotbq
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-R3-R4-pwb-other,
step-absstep-W3-W4-tau-same,
step-absstep-W1-W2-tau-other,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-W3-W4-tau-other,
step-absstep-W4-W5-tau-other,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotbq-dotfctr
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-R3-R4-pwb-other,
step-absstep-W3-W4-tau-same,
step-absstep-W1-W2-tau-other,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-W3-W4-tau-other,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-W4-W5-tau-other,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotbq-dotfreaders
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-W1-W2-tau-same,
step-absstep-W5-W6-tau-same,
step-absstep-W3-W4-tau-same,
step-absstep-W1-W2-tau-other,
step-absstep-W3-W4-tau-other,
step-absstep-W4-W5-tau-other,
- FLIT/updsel--dotbq-dotfwriters
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-R3-R4-pwb-other,
step-absstep-W3-W4-tau-same,
step-absstep-W1-W2-tau-other,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-W3-W4-tau-other,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-W4-W5-tau-other,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotbq-dotpmem
is used by
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-W3-W4-tau-same,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotbq-dotpq
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-W1-W2-tau-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-R3-R4-pwb-other,
step-absstep-W3-W4-tau-same,
step-absstep-W1-W2-tau-other,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-W3-W4-tau-other,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-W4-W5-tau-other,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotbq-dotrfo
is used by
step-absstep-W5-W6-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-W1-W2-tau-same,
step-absstep-W5-W6-tau-same,
step-absstep-W3-W4-tau-same,
step-absstep-W1-W2-tau-other,
step-absstep-PROP_W-doWrite,
step-absstep-W3-W4-tau-other,
step-absstep-W4-W5-tau-other,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotfctr-dotbq
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-other,
step-absstep-W2-W3-ctrInc-other,
step-absstep-W6-W7-ctrDec-same,
- FLIT/updsel--dotfctr-dotfctr
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-other,
step-absstep-W2-W3-ctrInc-other,
step-absstep-CRASH-globalCRASH,
step-absstep-W6-W7-ctrDec-same,
- FLIT/updsel--dotfctr-dotfreaders
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-other,
step-absstep-W2-W3-ctrInc-other,
step-absstep-W6-W7-ctrDec-same,
- FLIT/updsel--dotfctr-dotpmem
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-CRASH-globalCRASH,
step-absstep-W6-W7-ctrDec-same,
- FLIT/updsel--dotfctr-dotpq
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-other,
step-absstep-W2-W3-ctrInc-other,
step-absstep-CRASH-globalCRASH,
step-absstep-W6-W7-ctrDec-same,
- FLIT/updsel--dotfctr-dotrfo
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-other,
step-absstep-W2-W3-ctrInc-other,
step-absstep-W6-W7-ctrDec-same,
- FLIT/updsel--dotfreaders-dotbq
is used by
step-absstep-R2-R4-ctrRead-other,
step-absstep-R1-R2-doRead-other,
step-absstep-R3-R4-pwb-other,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R3-R4-pwb-same,
step-absstep-R1-R2-doRead-same,
step-absstep-CRASH-globalCRASH,
- FLIT/updsel--dotfreaders-dotfctr
is used by
step-absstep-R2-R4-ctrRead-other,
step-absstep-R1-R2-doRead-other,
step-absstep-R3-R4-pwb-other,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R3-R4-pwb-same,
step-absstep-R1-R2-doRead-same,
step-absstep-CRASH-globalCRASH,
- FLIT/updsel--dotfreaders-dotfreaders
is used by
step-absstep-R2-R4-ctrRead-other,
step-absstep-R1-R2-doRead-other,
step-absstep-R3-R4-pwb-other,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R3-R4-pwb-same,
step-absstep-R1-R2-doRead-same,
- FLIT/updsel--dotfreaders-dotfwriters
is used by
step-absstep-R2-R4-ctrRead-other,
step-absstep-R1-R2-doRead-other,
step-absstep-R3-R4-pwb-other,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R3-R4-pwb-same,
step-absstep-R1-R2-doRead-same,
step-absstep-CRASH-globalCRASH,
- FLIT/updsel--dotfreaders-dotpmem
is used by
step-absstep-R2-R4-ctrRead-same,
step-absstep-R3-R4-pwb-same,
step-absstep-R1-R2-doRead-same,
step-absstep-CRASH-globalCRASH,
- FLIT/updsel--dotfreaders-dotpq
is used by
step-absstep-R2-R4-ctrRead-other,
step-absstep-R1-R2-doRead-other,
step-absstep-R3-R4-pwb-other,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R3-R4-pwb-same,
step-absstep-R1-R2-doRead-same,
step-absstep-CRASH-globalCRASH,
- FLIT/updsel--dotfreaders-dotrfo
is used by
step-absstep-R2-R4-ctrRead-other,
step-absstep-R1-R2-doRead-other,
step-absstep-R3-R4-pwb-other,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R3-R4-pwb-same,
step-absstep-R1-R2-doRead-same,
- FLIT/updsel--dotfwriters-dotbq
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-other,
step-absstep-W2-W3-ctrInc-other,
step-absstep-CRASH-globalCRASH,
step-absstep-W6-W7-ctrDec-same,
- FLIT/updsel--dotfwriters-dotfctr
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-other,
step-absstep-W2-W3-ctrInc-other,
step-absstep-CRASH-globalCRASH,
step-absstep-W6-W7-ctrDec-same,
- FLIT/updsel--dotfwriters-dotfreaders
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-other,
step-absstep-W2-W3-ctrInc-other,
step-absstep-W6-W7-ctrDec-same,
- FLIT/updsel--dotfwriters-dotfwriters
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-other,
step-absstep-W2-W3-ctrInc-other,
step-absstep-CRASH-globalCRASH,
step-absstep-W6-W7-ctrDec-same,
- FLIT/updsel--dotfwriters-dotpmem
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-CRASH-globalCRASH,
step-absstep-W6-W7-ctrDec-same,
- FLIT/updsel--dotfwriters-dotpq
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-other,
step-absstep-W2-W3-ctrInc-other,
step-absstep-CRASH-globalCRASH,
step-absstep-W6-W7-ctrDec-same,
- FLIT/updsel--dotfwriters-dotrfo
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-other,
step-absstep-W2-W3-ctrInc-other,
step-absstep-W6-W7-ctrDec-same,
- FLIT/updsel--dotloc-dotloc
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-R1-invFLITREAD-same,
- FLIT/updsel--dotloc-dott
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-R1-invFLITREAD-same,
- FLIT/updsel--dotpmem-dotbq
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- FLIT/updsel--dotpmem-dotfctr
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- FLIT/updsel--dotpmem-dotfwriters
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- FLIT/updsel--dotpmem-dotpmem
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- FLIT/updsel--dotpmem-dotrfo
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- FLIT/updsel--dotpq-dotbq
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLIT/updsel--dotpq-dotfctr
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotpq-dotfwriters
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotpq-dotpmem
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotpq-dotpq
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotpq-dotrfo
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLIT/updsel--dotrfo-dotbq
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-R3-R4-pwb-same,
step-absstep-CRASH-globalCRASH,
- FLIT/updsel--dotrfo-dotfctr
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotrfo-dotfwriters
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotrfo-dotpmem
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotrfo-dotpq
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotrfo-dotrfo
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLIT/updsel--dotval-dotloc
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-R1-R2-doRead-same,
- FLIT/updsel--dotval-dott
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-R1-R2-doRead-same,
- FLIT/updsel--dotval-dotval
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-R1-R2-doRead-same,
Used from specification list-data
- list-data/elim-add
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- list-data/l
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- list-data/size-nil
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
Used from specification FLITPSCweak
- FLITPSCweak/FLITPSCGInv
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/FLITPSCInv
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/FLITPSCLInv
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/flitpscInit
is used by
abs-init,
- FLITPSCweak/disj-R1-R3
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-R1-W3
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-R1-W4
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-R1-W5
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-R1-crashed
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-R1-idle
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-R2-R3
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-R2-W3
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-R2-W4
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-R2-W5
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-R2-crashed
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-R2-idle
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-R3-R4
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-R3-W1
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-R3-W2
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-R3-W3
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-R3-W4
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-R3-W5
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-R3-W6
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-R3-W7
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-R3-crashed
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-R3-idle
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-R3-ready
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-R4-W3
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-R4-W4
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-R4-W5
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-R4-crashed
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-R4-idle
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-W1-W2
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/disj-W1-W3
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W1-W4
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W1-W5
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-W1-crashed
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-W1-idle
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-W2-W3
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W2-W4
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W2-W5
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-W2-idle
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-W3-W4
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W3-W5
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W3-W6
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W3-W7
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W3-crashed
is used by
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-W3-idle
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-W3-ready
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W4-W5
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W4-W6
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W4-W7
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W4-crashed
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W4-idle
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-W4-ready
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W5-W6
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-W5-W7
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-W5-crashed
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-W5-idle
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-W5-ready
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-W6-idle
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-W7-crashed
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-W7-idle
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-callPSCCOMPLETE-doWritePSC
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-callPSCCOMPLETE-invFLITPSCREAD
is used by
step-absstep-ready-ready-callFLITCOMPLETE-same,
- FLITPSCweak/disj-callPSCCOMPLETE-invFLITPSCWRITE
is used by
step-absstep-ready-ready-callFLITCOMPLETE-same,
step-absstep-ready-W1-invFLITWRITE-same,
- FLITPSCweak/disj-callPSCCOMPLETE-pwbPSC
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-callPSCRUN-doWritePSC
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-callPSCRUN-pwbPSC
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-crashed-idle
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-crashed-ready
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-ctrDecPSC-doWritePSC
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-ctrDecPSC-pwbPSC
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-ctrIncPSC-doWritePSC
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-ctrIncPSC-pwbPSC
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-ctrReadPSC-doWritePSC
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-ctrReadPSC-pwbPSC
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-doReadPSC-doWritePSC
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-doReadPSC-pwbPSC
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-doWritePSC-globalPSCCRASH
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-doWritePSC-globalPSCPERSISTuscFO
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-doWritePSC-globalPSCPERSISTuscW
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-doWritePSC-invFLITPSCREAD
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-doWritePSC-invFLITPSCWRITE
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-doWritePSC-pwbPSC
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-doWritePSC-retFLITPSCREAD
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-doWritePSC-retFLITPSCWRITE
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-doWritePSC-sfencePSC
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/disj-globalPSCCRASH-globalPSCPERSISTuscFO
is used by
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLITPSCweak/disj-globalPSCCRASH-globalPSCPERSISTuscW
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-globalPSCCRASH-pwbPSC
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-globalPSCCRASH-sfencePSC
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/disj-globalPSCPERSISTuscFO-globalPSCPERSISTuscW
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLITPSCweak/disj-globalPSCPERSISTuscFO-pwbPSC
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-globalPSCPERSISTuscFO-sfencePSC
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/disj-globalPSCPERSISTuscW-pwbPSC
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-globalPSCPERSISTuscW-sfencePSC
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/disj-idle-ready
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/disj-invFLITPSCREAD-invFLITPSCWRITE
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-R1-invFLITREAD-same,
- FLITPSCweak/disj-invFLITPSCREAD-pwbPSC
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-invFLITPSCWRITE-pwbPSC
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-pwbPSC-retFLITPSCREAD
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-pwbPSC-retFLITPSCWRITE
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/disj-pwbPSC-sfencePSC
is used by
step-absstep-PROP_FO-doWriteFO,
- FLITPSCweak/elim-mkFLITPSCgs
is used by
step-absstep-R4-ready-retFLITREAD-same,
step-absstep-ready-R1-invFLITREAD-same,
step-absstep-PROP_SF-propSF,
- FLITPSCweak/elim-mkFLITPSCls
is used by
step-absstep-R4-ready-retFLITREAD-same,
step-absstep-ready-R1-invFLITREAD-same,
step-absstep-PROP_SF-propSF,
- FLITPSCweak/fliqtStep-lem
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLITPSCweak/gstepf-R1
is used by
step-absstep-R1-R2-doRead-same,
- FLITPSCweak/gstepf-R2
is used by
step-absstep-R2-R3-ctrRead-same,
step-absstep-R2-R4-ctrRead-same,
- FLITPSCweak/gstepf-R3
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-R3-R4-pwb-same,
- FLITPSCweak/gstepf-R4
is used by
step-absstep-R4-ready-retFLITREAD-same,
- FLITPSCweak/gstepf-W1
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/gstepf-W2
is used by
step-absstep-W2-W3-ctrInc-same,
- FLITPSCweak/gstepf-W3
is used by
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLITPSCweak/gstepf-W4
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_SF-propSF,
- FLITPSCweak/gstepf-W5
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/gstepf-W6
is used by
step-absstep-W6-W7-ctrDec-same,
- FLITPSCweak/gstepf-W7
is used by
step-absstep-W7-ready-retFLITWRITE-same,
- FLITPSCweak/gstepf-idle-PSCRUN
is used by
step-absstep-idle-ready-callRUN-same,
- FLITPSCweak/gstepf-ready
is used by
step-absstep-ready-ready-callFLITCOMPLETE-same,
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-R1-invFLITREAD-same,
- FLITPSCweak/inj-callPSCCOMPLETE
is used by
step-absstep-ready-ready-callFLITCOMPLETE-same,
- FLITPSCweak/inj-callPSCRUN
is used by
step-absstep-idle-ready-callRUN-same,
- FLITPSCweak/inj-ctrDecPSC
is used by
step-absstep-W6-W7-ctrDec-same,
- FLITPSCweak/inj-ctrIncPSC
is used by
step-absstep-W2-W3-ctrInc-same,
- FLITPSCweak/inj-ctrReadPSC
is used by
step-absstep-R2-R3-ctrRead-same,
step-absstep-R2-R4-ctrRead-same,
- FLITPSCweak/inj-doReadPSC
is used by
step-absstep-R1-R2-doRead-same,
- FLITPSCweak/inj-doWritePSC
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/inj-globalPSCPERSISTuscFO
is used by
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLITPSCweak/inj-globalPSCPERSISTuscW
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- FLITPSCweak/inj-invFLITPSCREAD
is used by
step-absstep-ready-R1-invFLITREAD-same,
- FLITPSCweak/inj-mkFLITPSCgs
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/inj-pwbPSC
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-R3-R4-pwb-same,
- FLITPSCweak/inj-retFLITPSCREAD
is used by
step-absstep-R4-ready-retFLITREAD-same,
- FLITPSCweak/inj-retFLITPSCWRITE
is used by
step-absstep-W7-ready-retFLITWRITE-same,
- FLITPSCweak/inj-sfencePSC
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/lstep
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PROP_W-doWrite,
step-absstep-CRASH-globalCRASH,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-PROP_SF-propSF,
- FLITPSCweak/lstepf-R1
is used by
step-absstep-R1-R2-doRead-same,
- FLITPSCweak/lstepf-R2
is used by
step-absstep-R2-R3-ctrRead-same,
step-absstep-R2-R4-ctrRead-same,
- FLITPSCweak/lstepf-R3
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-R3-R4-pwb-same,
- FLITPSCweak/lstepf-R4
is used by
step-absstep-R4-ready-retFLITREAD-same,
- FLITPSCweak/lstepf-W1
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/lstepf-W2
is used by
step-absstep-W2-W3-ctrInc-same,
- FLITPSCweak/lstepf-W3
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/lstepf-W4
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/lstepf-W5
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/lstepf-W6
is used by
step-absstep-W6-W7-ctrDec-same,
- FLITPSCweak/lstepf-W7
is used by
step-absstep-W7-ready-retFLITWRITE-same,
- FLITPSCweak/lstepf-idle-PSCRUN
is used by
step-absstep-idle-ready-callRUN-same,
- FLITPSCweak/lstepf-ready-FLITPSCREAD
is used by
step-absstep-ready-R1-invFLITREAD-same,
- FLITPSCweak/lstepf-ready-FLITPSCWRITE
is used by
step-absstep-ready-W1-invFLITWRITE-same,
- FLITPSCweak/lstepf-ready-PSCCOMPLETE
is used by
step-absstep-ready-ready-callFLITCOMPLETE-same,
- FLITPSCweak/not-pre-global-crash
is used by
step-absstep-CRASH-globalCRASH,
- FLITPSCweak/not-pre-global-persist
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- FLITPSCweak/not-pre-global-tsync
is used by
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLITPSCweak/pcstepf-R1
is used by
step-absstep-R1-R2-doRead-same,
- FLITPSCweak/pcstepf-R2
is used by
step-absstep-R2-R3-ctrRead-same,
step-absstep-R2-R4-ctrRead-same,
- FLITPSCweak/pcstepf-R3
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-R3-R4-pwb-same,
- FLITPSCweak/pcstepf-R4
is used by
step-absstep-R4-ready-retFLITREAD-same,
- FLITPSCweak/pcstepf-W1
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/pcstepf-W2
is used by
step-absstep-W2-W3-ctrInc-same,
- FLITPSCweak/pcstepf-W3
is used by
step-absstep-PROP_W-doWrite,
- FLITPSCweak/pcstepf-W4
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/pcstepf-W5
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/pcstepf-W6
is used by
step-absstep-W6-W7-ctrDec-same,
- FLITPSCweak/pcstepf-W7
is used by
step-absstep-W7-ready-retFLITWRITE-same,
- FLITPSCweak/pcstepf-idle-PSCRUN
is used by
step-absstep-idle-ready-callRUN-same,
- FLITPSCweak/pcstepf-ready-FLITPSCREAD
is used by
step-absstep-ready-R1-invFLITREAD-same,
- FLITPSCweak/pcstepf-ready-FLITPSCWRITE
is used by
step-absstep-ready-W1-invFLITWRITE-same,
- FLITPSCweak/pcstepf-ready-PSCCOMPLETE
is used by
step-absstep-ready-ready-callFLITCOMPLETE-same,
- FLITPSCweak/pre-R1
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-R1-R2-doRead-same,
- FLITPSCweak/pre-R2
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-R2-R3-ctrRead-same,
step-absstep-R2-R4-ctrRead-same,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/pre-R3
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-R3-R4-pwb-other,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/pre-R4
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-R4-ready-retFLITREAD-same,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/pre-W1
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLITPSCweak/pre-W2
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/pre-W3
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/pre-W4
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/pre-W5
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_SF-propSF,
- FLITPSCweak/pre-W6
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-W6-W7-ctrDec-same,
- FLITPSCweak/pre-W7
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
step-absstep-W7-ready-retFLITWRITE-same,
- FLITPSCweak/pre-crashed
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/pre-idle
is used by
step-absstep-idle-ready-callRUN-same,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/pre-ready
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-ready-ready-callFLITCOMPLETE-same,
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-R1-invFLITREAD-same,
step-absstep-PROP_W-doWrite,
- FLITPSCweak/sel-mkFLITPSCgs-dotctr
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
step-absstep-PROP_SF-propSF,
- FLITPSCweak/sel-mkFLITPSCgs-dotmem
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
step-absstep-PROP_SF-propSF,
- FLITPSCweak/sel-mkFLITPSCgs-dotp
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
step-absstep-PROP_SF-propSF,
- FLITPSCweak/sel-mkFLITPSCgs-dotreaders
is used by
abs-init,
- FLITPSCweak/sel-mkFLITPSCgs-dotwriters
is used by
abs-init,
step-absstep-CRASH-globalCRASH,
step-absstep-PROP_SF-propSF,
- FLITPSCweak/sel-mkFLITPSCls-dotl
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/sel-mkFLITPSCls-dott
is used by
abs-init,
step-absstep-PROP_SF-propSF,
- FLITPSCweak/sel-mkFLITPSCls-dotv
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/upd-mkFLITPSCgs-dotp
is used by
step-absstep-PROP_SF-propSF,
- FLITPSCweak/updsel--dotctr-dotctr
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-same,
- FLITPSCweak/updsel--dotctr-dotmem
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-same,
- FLITPSCweak/updsel--dotctr-dotp
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-same,
- FLITPSCweak/updsel--dotl-dotl
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-R1-invFLITREAD-same,
- FLITPSCweak/updsel--dotl-dott
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-ready-R1-invFLITREAD-same,
- FLITPSCweak/updsel--dotmem-dotctr
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- FLITPSCweak/updsel--dotmem-dotmem
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- FLITPSCweak/updsel--dotmem-dotwriters
is used by
step-absstep-PERSIST_W-globalPERSIST_W,
- FLITPSCweak/updsel--dotp-dotctr
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLITPSCweak/updsel--dotp-dotmem
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLITPSCweak/updsel--dotp-dotp
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLITPSCweak/updsel--dotp-dotwriters
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-PERSIST_FO-globalPERSIST_FO,
- FLITPSCweak/updsel--dotreaders-dotctr
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R3-R4-pwb-same,
step-absstep-R1-R2-doRead-same,
- FLITPSCweak/updsel--dotreaders-dotmem
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R3-R4-pwb-same,
step-absstep-R1-R2-doRead-same,
- FLITPSCweak/updsel--dotreaders-dotp
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R3-R4-pwb-same,
step-absstep-R1-R2-doRead-same,
- FLITPSCweak/updsel--dotreaders-dotwriters
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R3-R4-pwb-same,
step-absstep-R1-R2-doRead-same,
- FLITPSCweak/updsel--dotv-dotl
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-R1-R2-doRead-same,
- FLITPSCweak/updsel--dotv-dott
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-R1-R2-doRead-same,
- FLITPSCweak/updsel--dotv-dotv
is used by
step-absstep-ready-W1-invFLITWRITE-same,
step-absstep-R1-R2-doRead-same,
- FLITPSCweak/updsel--dotwriters-dotctr
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-same,
- FLITPSCweak/updsel--dotwriters-dotmem
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-same,
- FLITPSCweak/updsel--dotwriters-dotp
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-same,
- FLITPSCweak/updsel--dotwriters-dotwriters
is used by
step-absstep-W2-W3-ctrInc-same,
step-absstep-W6-W7-ctrDec-same,
Used from specification Bevent
- Bevent/disj-FO-SF
is used by
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-R3-R4-pwb-other,
step-absstep-R3-R4-pwb-same,
step-absstep-PROP_W-doWrite,
step-absstep-W4-W5-tau-other,
step-absstep-PROP_SF-propSF,
- Bevent/disj-W-FO
is used by
step-absstep-W4-W5-tau-same,
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_W-doWrite,
- Bevent/disj-W-SF
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-W5-W6-tau-same,
step-absstep-W3-W4-tau-same,
step-absstep-PROP_W-doWrite,
step-absstep-W3-W4-tau-other,
step-absstep-PROP_SF-propSF,
- Bevent/elim-W
is used by
step-absstep-PROP_W-doWrite,
- Bevent/inj-FO
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- Bevent/inj-W
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-W3-W4-tau-same,
step-absstep-PROP_W-doWrite,
step-absstep-W3-W4-tau-other,
- Bevent/test-dotWque-FO
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- Bevent/test-dotWque-SF
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_SF-propSF,
- Bevent/test-dotWque-W
is used by
step-absstep-PROP_FO-doWriteFO,
step-absstep-W3-W4-tau-same,
step-absstep-PROP_W-doWrite,
step-absstep-W3-W4-tau-other,
Used from specification list-del
- list-del/delnr-one
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- list-del/delpos-base
is used by
step-absstep-PROP_FO-tau,
- list-del/delpos-empty
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,
- list-del/delpos-rec
is used by
step-absstep-PROP_FO-tau,
- list-del/get-numrec
is used by
step-absstep-PROP_FO-tau,
- list-del/get-succ
is used by
step-absstep-PROP_FO-tau,
- list-del/get-zero
is used by
step-absstep-PROP_FO-tau,
- list-del/one-03
is used by
step-absstep-PROP_FO-tau,
step-absstep-PROP_FO-doWriteFO,