TABLE OF CONTENTS Until now, we have spoken in terms of a PSL property holding or not on a given trace, and in fact, the meaning of a PSL operator is given by defining when a property using it holds or does not hold. However, PSL actually defines four additional terms that can be used to relate a property to a trace. The four levels of satisfaction are:
holds strongly
holds but does not hold strongly
pending
fails
All four terms are based upon the basic notion of a property holding, and all four refer to what would happen to a finite trace if the simulation were to be continued, thus lengthening the trace. Would the property continue to hold or not? Holds strongly means that no matter what we do, we cannot undo the holding of the property. Holds but does not hold strongly means what it says: the property holds, but not strongly. Pending means that while the property doesn't hold, continuing the simulation could go either way, depending on how we lengthen the trace. Fails means that the property doesn't hold, and in addition, we cannot get it to hold by lengthening the trace. Thus, holds strongly and holds but does not hold strongly are two degrees of holding, while pending and fails are two degrees of not holding.
NOTE: Similarly to the leniency and strictness of strong and weak operators discussed...
