From 53a3cc7b17f4cf97075b7e71720777fd84109696 Mon Sep 17 00:00:00 2001
From: Gilles Dubochet <gilles.dubochet@epfl.ch>
Date: Fri, 16 Dec 2005 18:44:33 +0000
Subject: Created proper 'docs' folder for new layout.

---
 docs/examples/pilib/mobilePhoneProtocol.scala | 172 ++++++++++++++++++++++++++
 1 file changed, 172 insertions(+)
 create mode 100644 docs/examples/pilib/mobilePhoneProtocol.scala

(limited to 'docs/examples/pilib/mobilePhoneProtocol.scala')

diff --git a/docs/examples/pilib/mobilePhoneProtocol.scala b/docs/examples/pilib/mobilePhoneProtocol.scala
new file mode 100644
index 0000000000..0b13f78fd3
--- /dev/null
+++ b/docs/examples/pilib/mobilePhoneProtocol.scala
@@ -0,0 +1,172 @@
+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("Consummer took " + msg);
+      Consumer(get)
+    }
+
+    val put = new Chan[String];
+    val get = new Chan[String];
+    spawn < Producer(0, put) | Consumer(get) | MobileSystem(put, get) >
+  }
+
+}
+
+
-- 
cgit v1.2.3