CMU 15-671  Models of Software Systems  Fall 1995

Telephone Net

Garlan & Wing  Handout 7A  27 September 1995

Preliminaries

We begin by adding a new operator to the Mathematical Tool-kit. disj is a predicate which is true of a sets of sets, S, if and only if no two distinct sets in S intersect.

[X ]

disj : � (� (� X ))

∀ S : � (� X ) • disj S ⇔ (∀ i, j : S • i ≠ j ⇒ i ∩ j = �)

Basic Telephone Net

We take the type PHONE to be a given, or primitive type. A phone connection is simply a set of phones, and we define CON to represent the type of all possible phone connections.

[PHONE]

CON == � PHONE

We now define the schema TN to model a telephone net. It consists of a set of connections, cons, and a set of requests, reqs. We require that all connections are also requests and that no phone is simultaneously in two distinct connections.

TN

reqs, cons : � CON

cons ⊆ reqs disj cons

Efficient Telephone Net

An efficient telephone net is a telephone net for which it is not possible to connect an unsatisfied request without violating the telephone net invariant.

EfficientTN

TN

¬ (∃ r : reqs \ cons • disj (cons ∪ {r}))

This schema expresses a property of maximality about the connections: it is not possible to enlarge the set of connections.

Operations

All operations that we plan to define for a telephone net will share certain properties. We capture these once and for all in the schema Event, which states that an operation will not disconnect any connections provided they are still requested after the operation.

Event ΔEfficientTN

∀ c : CON • c ∈ (cons ∩ reqs′) ⇒ c ∈ cons′

The operation Call adds a request to the set of requests of a telephone net.

Call Event ph?, dialed? : PHONE

reqs′ = reqs ∪ {{ph?, dialed?}}

Given the maximality constraint on TN it is possible to infer from this operation that if neither phone is already connected, the request will be connected. (Exercise for the reader.)

The next operation, Hangup, terminates a connnection (if any) involving the phone ph?.

Hangup Event ph? : PHONE

reqs′ = reqs \ {c : cons | ph? ∈ c}

Finally, we define an operation Busy, which tells whether a phone is involved in a connection.

YesOrNo ::= YES | NO

Busy Event ph? : PHONE busy! : YesOrNo

reqs′ = reqs busy! = YES ⇔ ph? ∈ ⋃ cons

It is possible to show that cons does not change as a result of this operation. (Exercise for the reader.)