--------------------- MODULE CommitmentPublicationMC ---------------------
EXTENDS ItemTimingMC
                                                                         
                                                                               
PublicationInitT11 == guideCaseT11=0 /\ \E NeutralValue00013 \in {"FacilityObserve0","FacilityObserve1"} : qT11=ItemInspectionTemporalInitialT11("SideAHand","NoValue",NeutralValue00013)
PublicationSpecT11 == PublicationInitT11 /\ [][ItemInspectionTemporalNextT11]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(ItemInspectionTemporalNextT11)
PublicationSafetyT11 == IF qT11.cost.purpose="Mid" THEN qT11.cost.paid => qT11.itemInspection.midUsed /\ qT11.midUses=1 ELSE TRUE
=============================================================================