Subsituations

Like interfaces, states and classes, situations may be specialized into subsituations. Subsituation relations are analogs of the subtype relations underlying interface inheritance. Mechanics follow those for ordinary sets defined via predicates. For example, situation Q: {in(readrequest) && isOpen(f)} is a subsituation of P: {in(readrequest)} in which case we say that Q P.

If Q P, then fewer possible realizations match Q than P. Every situation is a subsituation of the empty situation {} (or equivalently { true }), which is matched by all realizations. The situation { false } (matched by no realizations) is a subsituation of all others. We say that expression expr holds in situation S if S { expr }. Conversely, we define set-like union and intersection operators in terms of the corresponding boolean relations on their component expressions [17,62]. In PSL/IDL A B is expressed as { expr } && { expr }, and A B as { expr } || { expr }.

The simplest and most common means of constructing a subsituation is to ``strengthen'' an expression by and'ing an independent predicate p, since A { p } A. Strengthening may also occur by replacing a predicate with one that implies it. For example, a situation including out( m) might be strengthened by replacing it with the more committal out( m)by( p ).

Partitions. PSL does not use any special notation to declare that one situation is a subsituation of another except in the special case of disjoint union where S . This represents a set of subsituations that are constrained to completely partition a situation-space S. Partitioned subsituations must be exhaustive and mutually exclusive. Partitioning is thus one way to express the notion that one situation ``disables'' another[67].

In PSL/IDL, partitions are enclosed in case. Successive cases are interpreted in the same way as case, cond, and if ... elsif statements in most languages, implicitly negating the expressions in all previous cases. The special trailing situation default matches only if all previous cases fail, thus acting as a generalized else.

Conditional protocol rules can be expressed using partitions. Ordering operators ``distribute'' through situation partitionings to describe conditional paths. Since ordering operators have lower precedence than the && operator combining situations, expressions common to all partitions can be described in a situation linked by && to the cases. For example, to indicate that a TRUE reply is enabled if some function ok holds, and conversely for FALSE:

{ out(req) } pair
{ in(req) } && {
 case { ok(req) } enable { out(reply(TRUE)) }
 case { default } enable { out(reply(FALSE)) } }

In PSL/IDL-G, partitioning is indicated via nested StateCharts [24]. Each enclosed box represents a partition. The special trailing ``else'' box contains only the expression default. Expressions common to all partitioned subsituations may be listed outside of the nested boxes. The accompanying fragment of a PSL/IDL-G protocol for a simple File illustrates some of the interplay between conditionals and temporal operators.

In this example, the use of linking the ``normal'' read reply indicates that a situation in which a reply is generated occurs only when a file is open and receives a read request, but may not occur at all so far as can be determined from the perspective of the roles parameterized within the current rules declaration. For example, there may be ``downstream'' errors stemming from internal invocations that are not visible at this scope or level of specification. However, if a reply occurs, the return value c is subject to the listed constraints that amount to a guarantee that the return value is a 7-bit character value.

In contrast, the ``exceptional'' reply situation is linked via , indicating that (only) when a read request is received by a file that is not open, an exception reply to the request is always generated. This does not indicate that this is the only context in which the NotOpen exception is thrown. It says instead that this is the only context in which it is thrown as a reply to read. If for some reason we had wanted to make the weaker claim that NotOpen is possible but not guaranteed, we would have used . Had we wanted to make the differently weaker claim that NotOpen is always issued not only here, but perhaps also in some other context (i.e., even if the file is open) we would have used .