Telecommunication example

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.

      state(m, idle): receiver is on hook and the bell is not ringing.
      state(m,dial): receiver is off hook and dial tone exists.
      state(m, dial n): receiver is off hook and m has dialed to n
      state(m, busy): receiver is off hook and there exists a signal busy.
      state(m, fastbusy): receiver is off hook and there exists a signal fastbusy.

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),
      offhook(n),
      onhook(n),
      dial(n,m),
      ring(n),
      dialtone(n),
      busy(n),
      fastbusy(n).