diff options
Diffstat (limited to 'sources/examples/pilib/mobilePhoneProtocol.scala')
| -rw-r--r-- | sources/examples/pilib/mobilePhoneProtocol.scala | 170 |
1 files changed, 170 insertions, 0 deletions
diff --git a/sources/examples/pilib/mobilePhoneProtocol.scala b/sources/examples/pilib/mobilePhoneProtocol.scala new file mode 100644 index 0000000000..553bc68e7f --- /dev/null +++ b/sources/examples/pilib/mobilePhoneProtocol.scala @@ -0,0 +1,170 @@ +/** +* Mobile phone protocol. +* Equivalent to a three-place buffer. +* @see Bjoern Victor "A verification tool for the polyadic pi-calculus". +*/ +object mobilePhoneProtocol { + + import concurrent.pilib._; + + val random = new java.util.Random(); + + // Internal messages exchanged by the protocol. + trait Message; + + // Predefined messages used by the protocol. + case class Data() extends Message; + case class HoCmd() extends Message; // handover command + case class HoAcc() extends Message; // handover access + case class HoCom() extends Message; // handover complete + case class HoFail() extends Message; // handover fail + case class ChRel() extends Message; // release + case class Voice(s: String) extends Message; // voice + case class Channel(n: Chan[Message]) extends Message; // channel + + def MobileSystem(in: Chan[String], out: Chan[String]): unit = { + + def CC(fa: Chan[Message], fp: Chan[Message], l: Chan[Channel]): unit = + choice ( + in * (v => { fa.write(Data()); fa.write(Voice(v)); CC(fa, fp, l) }) + , + l * (m_new => { + fa.write(HoCmd()); + fa.write(m_new); + choice ( + fp * ({ case HoCom() => { + System.out.println("Mobile has moved from one cell to another"); + fa.write(ChRel()); + val Channel(m_old) = fa.read; + l.write(Channel(m_old)); + CC(fp, fa, l) + }}) + , + fa * ({ case HoFail() => { + System.out.println("Mobile has failed to move from one cell to another"); + l.write(m_new); + CC(fa, fp, l) + }}) + ) + }) + ); + + /* + * Continuously orders the MSC to switch the MS to the non-used BS. + */ + def HC(l: Chan[Channel], m: Chan[Message]): unit = { + Thread.sleep(1 + random.nextInt(1000)); + l.write(Channel(m)); + val Channel(m_new) = l.read; + HC(l, m_new) + } + + /** + * Mobile switching center. + */ + def MSC(fa: Chan[Message], fp: Chan[Message], m: Chan[Message]): unit = { + val l = new Chan[Channel]; + spawn < HC(l, m) | CC(fa, fp, l) > + } + + /** + * Active base station. + */ + def BSa(f: Chan[Message], m: Chan[Message]): unit = + (f.read) match { + case Data() => { + val v = f.read; + m.write(Data()); + m.write(v); + BSa(f, m) + } + case HoCmd() => { + val v = f.read; + m.write(HoCmd()); + m.write(v); + choice ( + f * ({ case ChRel() => { + f.write(Channel(m)); + BSp(f, m) + }}) + , + m * ({ case HoFail() => { + f.write(HoFail()); + BSa(f, m) + }}) + ) + } + }; + + /** + * Passive base station. + */ + def BSp(f: Chan[Message], m: Chan[Message]): unit = { + val HoAcc = m.read; + f.write(HoCom()); + BSa(f, m) + }; + + /** + * Mobile station. + */ + def MS(m: Chan[Message]): unit = + (m.read) match { + case Data() => { + val Voice(v) = m.read; + out.write(v); + MS(m) + } + case HoCmd() => + (m.read) match { + case Channel(m_new) => { + if (random.nextInt(1) == 0) + choice ( m_new(HoAcc()) * (MS(m_new)) ); + else + choice ( m(HoFail()) * (MS(m)) ); + } + } + }; + + def P(fa: Chan[Message], fp: Chan[Message]): unit = { + val m = new Chan[Message]; + spawn < MSC(fa, fp, m) | BSp(fp, m) > + } + + def Q(fa: Chan[Message]): unit = { + val m = new Chan[Message]; + spawn < BSa(fa, m) | MS(m) > + } + + val fa = new Chan[Message]; + val fp = new Chan[Message]; + spawn < Q(fa) | P(fa, fp) >; + } + + //***************** Entry function ******************// + + def main(args: Array[String]): unit = { + + def Producer(n: Int, put: Chan[String]): unit = { + Thread.sleep(1 + random.nextInt(1000)); + val msg = "object " + n; + put.write(msg); + System.out.println("Producer gave " + msg); + Producer(n + 1, put) + } + + def Consumer(get: Chan[String]): unit = { + Thread.sleep(1 + random.nextInt(1000)); + val msg = get.read; + System.out.println("Consummer took " + msg); + Consumer(get) + } + + val put = new Chan[String]; + val get = new Chan[String]; + spawn < Producer(0, put) | Consumer(get) | MobileSystem(put, get) > + } + +} + + |