This example is used as a benchmark for transition consistency and completeness of basic protocols. There are 24 MSC diagrams taken from expert on telecommunication used as basic protocols. They describe POTS (plain old telephone system) extended by two features: Call Waiting (CW) and 3-way connection (3WAY).
Predicates
To formalize basic protocols three predicates were introduced that characterize the states of a telephone system. They are binary predicate state(m,s), ternary predicate rel(m,n,r), and unary predicate valid(m). Here m and n are telephone numbers, s is the name of a state of a telephone, r is the name of relation which can join two telephones.
States
The following symbols are used for the names of states: idle, dial, dial n, ringing n, busy.
Relations
The names of relations are
connected, three_wayhold, three_wayconnected k, cw_hold, cw hold connect k,
and they have the following meaning.
rel(m,n,connected): m and n are connected and in talk.
rel(m,n,three_wayhold): 3WAY phone m holds n to include to 3 way connection after connecting to a third phone.
rel(m, n, three_wayconnected k): phones m and n are in 3 way connection organized by k.
rel(m,n, cw hold): m holds n for call waiting.
rel(m,n, cw hold connect k): m holds n and at the same time is connected with k.
Messages
flash(n),