diff options
Diffstat (limited to 'docs/examples/pilib/mobilePhoneProtocol.scala')
-rw-r--r-- | docs/examples/pilib/mobilePhoneProtocol.scala | 172 |
1 files changed, 0 insertions, 172 deletions
diff --git a/docs/examples/pilib/mobilePhoneProtocol.scala b/docs/examples/pilib/mobilePhoneProtocol.scala deleted file mode 100644 index e8c0ac1dc4..0000000000 --- a/docs/examples/pilib/mobilePhoneProtocol.scala +++ /dev/null @@ -1,172 +0,0 @@ -package examples.pilib - -/** -* 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("Consumer took " + msg); - Consumer(get) - } - - val put = new Chan[String]; - val get = new Chan[String]; - spawn < Producer(0, put) | Consumer(get) | MobileSystem(put, get) > - } - -} - - |