Created proper 'docs' folder for new layout.

8 files changed, 1150 insertions, 0 deletions

diff --git a/docs/examples/pilib/elasticBuffer.scala b/docs/examples/pilib/elasticBuffer.scala
new file mode 100644
index 0000000000..5e52a0fdce
--- /dev/null
+++ b/docs/examples/pilib/elasticBuffer.scala
@@ -0,0 +1,77 @@
+package examples.pilib;
+
+object elasticBuffer {
+
+  import scala.concurrent.pilib._;
+
+  /**
+  * Recursive type for channels that carry a "String" channel and
+  * an object of the type we define.
+  */
+  class MetaChan extends Chan[Pair[Chan[String], MetaChan]];
+
+  def Buffer(put: Chan[String], get: Chan[String]): unit =  {
+
+    /**
+    * An empty buffer cell, ready to pass on (o,r) to the left.
+    */
+    def Bl(i:Chan[String], l: MetaChan,
+	   o: Chan[String], r: MetaChan): unit =
+	     choice (
+	       l(Pair(o,r)) * (System.out.println("Removed one cell.")),
+	       i * (inp => Cl(i, l, o, r, inp))
+	     );
+
+    /**
+    * A buffer cell containing a value, ready to receive (o,r) from the right.
+    */
+    def Cl(i: Chan[String], l: MetaChan,
+	  o: Chan[String], r: MetaChan, content: String): unit =
+	    choice (
+	      o(content) * (Bl(i,l,o,r)),
+	      i * (inp => Dl(i,l,o,r,content, inp)),
+	      r * ( { case Pair(newo, newr) => Cl(i,l,newo,newr,content) })
+	    );
+
+    /**
+    * Two joined buffer cells, of type Cl.
+    */
+    def Dl(i: Chan[String], l: MetaChan,
+	  o: Chan[String], r: MetaChan,
+	  content: String, inp: String): unit = {
+      val newlr = new MetaChan;
+      val newio = new Chan[String];
+      spawn < Cl(i, l, newio, newlr, inp) | Cl(newio, newlr, o, r,content) >;
+    }
+
+    // l and r channels for the leftmost and rightmost cell, respectively.
+    val unused1 = new MetaChan;
+    val unused2 = new MetaChan;
+
+    Bl(put, unused1, get, unused2);
+  }
+
+  val random = new java.util.Random();
+
+  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)
+  }
+
+  def main(args: Array[String]): unit = {
+    val put = new Chan[String];
+    val get = new Chan[String];
+    spawn < Producer(0, put) | Consumer(get) | Buffer(put, get) >
+  }
+
+}
diff --git a/docs/examples/pilib/handover.scala b/docs/examples/pilib/handover.scala
new file mode 100644
index 0000000000..85fb899555
--- /dev/null
+++ b/docs/examples/pilib/handover.scala
@@ -0,0 +1,190 @@
+package examples.pilib;
+
+/**
+* Handover example with recursive types for channels.
+*/
+object handoverRecursive {
+
+  import concurrent.pilib._;
+
+  val random = new java.util.Random();
+
+  /**
+  * Recursive type for channels that carry a channel "unit" and
+  * an object of the type we define.
+  */
+  class Switch extends Chan[Pair[Chan[unit], Switch]];
+
+  /**
+  * Car.
+  */
+  def Car(talk: Chan[unit], switch: Switch): unit =
+    choice (
+      switch * ({ case Pair(t,s) => Car(t, s) }),
+      talk(()) * ( {
+	Thread.sleep(1 + random.nextInt(1000));
+	System.out.println("Car emitted a message.");
+	Car(talk, switch)
+      })
+    );
+
+  /**
+  * Control center.
+  */
+  def Control(talk1: Chan[unit], switch1: Switch,
+	      gain1: Switch, lose1: Switch,
+	      talk2: Chan[unit], switch2: Switch,
+	      gain2: Switch, lose2: Switch): unit
+  = {
+    def Control1: unit= {
+      Thread.sleep(1 + random.nextInt(1000));
+      lose1.write(Pair(talk2, switch2));
+      gain2.write(Pair(talk2, switch2));
+      Control2;
+    }
+    def Control2: unit = {
+      Thread.sleep(1 + random.nextInt(1000));
+      lose2.write(Pair(talk1, switch1));
+      gain1.write(Pair(talk1, switch1));
+      Control1;
+    }
+    Control1;
+  }
+
+  /**
+  * Active transmitter.
+  */
+  def ActiveTransmitter(id: String, talk: Chan[unit], switch: Switch,
+	    gain: Switch, lose: Switch): unit
+  =
+    choice (
+      talk * (x => {
+	System.out.println(id + " received a message.");
+	ActiveTransmitter(id, talk, switch, gain, lose)
+      }),
+      lose * ({ case Pair(t, s) => {
+	switch.write(Pair(t, s));
+	IdleTransmitter(id, gain, lose)
+      }})
+    );
+
+  /**
+  * Idle transmitter.
+  */
+  def IdleTransmitter(id: String, gain: Switch, lose: Switch): unit = {
+    val Pair(t, s) = gain.read;
+    ActiveTransmitter(id, t, s, gain, lose)
+  }
+
+  def main(args: Array[String]): unit = {
+    val talk1 = new Chan[unit];
+    val switch1 = new Switch;
+    val gain1 = new Switch;
+    val lose1 = new Switch;
+    val talk2 = new Chan[unit];
+    val switch2 = new Switch;
+    val gain2 = new Switch;
+    val lose2 = new Switch;
+    spawn <
+    Car(talk1, switch1) |
+    ActiveTransmitter("Transmitter 1", talk1, switch1, gain1, lose1) |
+    IdleTransmitter("Transmitter 2", gain2, lose2) |
+    Control(talk1, switch1, gain1, lose1, talk2, switch2, gain2, lose2)
+    >
+  }
+}
+
+/**
+* Handover example with type casts.
+*/
+object handoverCast {
+
+  import concurrent.pilib._;
+
+  val random = new java.util.Random();
+
+  /**
+  * Car.
+  */
+  def Car(talk: Chan[Any], switch: Chan[Any]): unit =
+    choice (
+      switch * (o => {
+        val Pair(t,s) = o.asInstanceOf[Pair[Chan[Any],Chan[Any]]];
+	Car(t, s)
+      }),
+      talk(()) * ( {
+	Thread.sleep(1 + random.nextInt(1000));
+	System.out.println("Car emitted a message.");
+	Car(talk, switch)
+      })
+    );
+
+  /**
+  * Control center.
+  */
+  def Control(talk1: Chan[Any], switch1: Chan[Any],
+	      gain1: Chan[Any], lose1: Chan[Any],
+	      talk2: Chan[Any], switch2: Chan[Any],
+	      gain2: Chan[Any], lose2: Chan[Any]): unit
+  = {
+    def Control1: unit= {
+      Thread.sleep(1 + random.nextInt(1000));
+      lose1.write(Pair(talk2, switch2));
+      gain2.write(Pair(talk2, switch2));
+      Control2
+    }
+    def Control2: unit = {
+      Thread.sleep(1 + random.nextInt(1000));
+      lose2.write(Pair(talk1, switch1));
+      gain1.write(Pair(talk1, switch1));
+      Control1
+    }
+    Control1
+  }
+
+  /**
+  * Active transmitter.
+  */
+  def ActiveTransmitter(id: String, talk: Chan[Any], switch: Chan[Any],
+			gain: Chan[Any], lose: Chan[Any]): unit
+  =
+    choice (
+      talk * (x => {
+	System.out.println(id + " received a message.");
+	ActiveTransmitter(id, talk, switch, gain, lose)
+      }),
+      lose * (o => {
+	val Pair(t, s) = o.asInstanceOf[Pair[Chan[Any],Chan[Any]]];
+	switch.write(Pair(t, s));
+	IdleTransmitter(id, gain, lose)
+      })
+    );
+
+  /**
+  * Idle transmitter.
+  */
+  def IdleTransmitter(id: String, gain: Chan[Any], lose: Chan[Any]): unit = {
+    val Pair(t, s) = gain.read.asInstanceOf[Pair[Chan[Any],Chan[Any]]];
+    ActiveTransmitter(id, t, s, gain, lose)
+  }
+
+  def main(args: Array[String]): unit = {
+    val talk1 = new Chan[Any];
+    val switch1 = new Chan[Any];
+    val gain1 = new Chan[Any];
+    val lose1 = new Chan[Any];
+    val talk2 = new Chan[Any];
+    val switch2 = new Chan[Any];
+    val gain2 = new Chan[Any];
+    val lose2 = new Chan[Any];
+    spawn <
+    Car(talk1, switch1) |
+    ActiveTransmitter("Transmitter 1", talk1, switch1, gain1, lose1) |
+    IdleTransmitter("Transmitter 2", gain2, lose2) |
+    Control(talk1, switch1, gain1, lose1, talk2, switch2, gain2, lose2)
+    >
+  }
+
+}
+
+
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) >
+  }
+
+}
+
+
diff --git a/docs/examples/pilib/piNat.scala b/docs/examples/pilib/piNat.scala
new file mode 100644
index 0000000000..137c0e5e6a
--- /dev/null
+++ b/docs/examples/pilib/piNat.scala
@@ -0,0 +1,92 @@
+package examples.pilib;
+
+import scala.concurrent.pilib._;
+//import pilib._;
+
+/** Church encoding of naturals in the Pi-calculus */
+object piNat with Application {
+
+  /** Locations of Pi-calculus natural */
+  class NatChan extends Chan[Triple[Chan[unit], Chan[NatChan], Chan[NatChan]]];
+
+  /** Zero */
+  def Z(l: NatChan): unit = choice (
+    l * { case Triple(z, sd, d) => z.write(()) }
+  );
+
+  /** Successor of Double */
+  def SD(n: NatChan, l: NatChan): unit = choice (
+    l * { case Triple(z, sd, d) => sd.write(n) }
+  );
+
+  /** Double */
+  def D(n: NatChan, l: NatChan): unit = choice (
+    l * { case Triple(z, sd, d) => d.write(n) }
+  );
+
+  /** Make "l" a location representing the natural "n" */
+  def make(n: int, l: NatChan): unit =
+    if (n == 0) Z(l)
+    else if (n % 2 == 0) { val l1 = new NatChan; spawn < D(l1, l) >; make(n/2, l1) }
+    else { val l1 = new NatChan; spawn < SD(l1, l) >; make(n/2, l1) };
+
+  /** Consume the natural "m" and put it successor at location "n" */
+  def Succ(m: NatChan, n: NatChan): unit = {
+    val z = new Chan[unit];
+    val sd = new Chan[NatChan];
+    val d = new Chan[NatChan];
+    spawn < m.write(Triple(z, sd, d)) >;
+    choice (
+      z  * { x => make(1, n) },
+      sd * { m1 => { val n1 = new NatChan; spawn < D(n1, n) >; Succ(m1, n1) } },
+      d  * { m1 => SD(m1, n) }
+    )
+  }
+
+  /** Consume the natural "l" and put two copies at locations "m" and "n" */
+  def Copy(l: NatChan, m: NatChan, n: NatChan): unit = {
+    val z = new Chan[unit];
+    val sd = new Chan[NatChan];
+    val d = new Chan[NatChan];
+    spawn < l.write(Triple(z, sd, d)) >;
+    choice (
+      z  * { x => spawn < Z(m) >; Z(n)  },
+      sd * { l1 => { val m1 = new NatChan; val n1 = new NatChan;
+                    spawn < SD(m1, m) | SD(n1, n) >;
+                    Copy(l1, m1, n1) } },
+      d * { l1 => { val m1 = new NatChan; val n1 = new NatChan;
+                   spawn < D(m1, m) | D(n1, n) >;
+                   Copy(l1, m1, n1) } }
+    )
+  }
+
+  /** Consume the natural at location "n" and return its value */
+  def value(n: NatChan): int =  {
+    val z = new Chan[unit];
+    val sd = new Chan[NatChan];
+    val d = new Chan[NatChan];
+    spawn < n.write(Triple(z, sd, d)) >;
+    choice (
+      z  * { x => 0  },
+      sd * { n1 => 2 * value(n1) + 1 },
+      d * { n1 => 2 * value(n1) }
+    )
+  }
+
+  // Test
+  val i = 42;
+  val l = new NatChan;
+  val l1 = new NatChan;
+  val l2 = new NatChan;
+  val l3 = new NatChan;
+
+  spawn <
+  make(i, l) |
+  Copy(l, l1, l2) |
+  Succ(l2, l3) |
+  System.out.println("" + i + " = " + value(l1)) |
+  System.out.println("succ " + i + " = " + value(l3))
+  >;
+
+}
+
diff --git a/docs/examples/pilib/rwlock.scala b/docs/examples/pilib/rwlock.scala
new file mode 100644
index 0000000000..0ed0f71a47
--- /dev/null
+++ b/docs/examples/pilib/rwlock.scala
@@ -0,0 +1,331 @@
+package examples.pilib;
+
+/**
+* From Pi to Scala: Semaphores, monitors, read/write locks.
+* Readers/writers locks.
+*/
+object rwlock {
+
+  import scala.concurrent.pilib._;
+
+  class Signal extends Chan[unit] {
+    def send = write(());
+    def receive = read;
+  }
+
+  class CountLock {
+    private val busy = new Signal;
+    def get = busy.send;
+    def release = busy.receive;
+    spawn < release >
+  }
+
+  /** A binary semaphore
+  */
+  class Lock {
+    private val busy = new Signal;
+    private val free = new Signal;
+    def get = busy.send;
+    def release = free.send;
+    spawn < (while (true) {
+      choice (
+        busy * (x => free.receive),
+	free * (x => ())
+      )
+    })
+    >
+  }
+
+  /** A monitor a la Java
+  */
+  class JavaMonitor {
+
+    private val lock = new Lock;
+
+    private var waiting: List[Signal] = Nil;
+
+    def Wait = {
+      val s = new Signal;
+      waiting = s :: waiting;
+      lock.release;
+      s.receive;
+      lock.get;
+    }
+
+    def Notify = {
+      if (!waiting.isEmpty) {
+	waiting.head.send;
+	waiting = waiting.tail;
+      }
+    }
+
+    def NotifyAll = {
+      while (!waiting.isEmpty) {
+	waiting.head.send;
+	waiting = waiting.tail;
+      }
+    }
+
+    def await(cond: => boolean): unit = while (false == cond) (Wait)
+  }
+
+  /*
+  class Buffer[a](size: Int) extends JavaMonitor with {
+    var in = 0, out = 0, n = 0;
+    val elems = new Array[a](size);
+    def put(x: a) = synchronized {
+      await(n < size);
+      elems(out) = x;
+      out = (out + 1) % size;
+    }
+    def get: a = synchronized {
+      await(n > 0);
+      val x = elems(in);
+      in = (in + 1) % size;
+      x
+    }
+  }
+  */
+
+  /** A readers/writers lock. */
+  trait ReadWriteLock {
+    def startRead: unit;
+    def startWrite: unit;
+    def endRead: unit;
+    def endWrite: unit;
+  }
+
+  /**
+  * A readers/writers lock, using monitor abstractions.
+  */
+  class ReadWriteLock1 extends JavaMonitor with ReadWriteLock {
+
+    private var nactive: int = 0;
+    private var nwriters: int = 0;
+
+    def status =
+      System.out.println(nactive + " active, " + nwriters + " writers");
+
+    def startRead = synchronized {
+      await(nwriters == 0);
+      nactive = nactive + 1;
+      status
+    }
+
+    def startWrite = synchronized {
+      nwriters = nwriters + 1;
+      await(nactive == 0);
+      nactive = 1;
+      status
+    }
+
+    def endRead = synchronized {
+      nactive = nactive - 1;
+      if (nactive == 0) NotifyAll;
+      status
+    }
+
+    def endWrite = synchronized {
+      nwriters = nwriters - 1;
+      nactive = 0;
+      NotifyAll;
+      status
+    }
+  }
+
+  /** A readers/writers lock, using semaphores
+  */
+  class ReadWriteLock2 extends ReadWriteLock {
+
+    private var rc: int = 0;  // reading readers
+    private var wc: int = 0;  // writing writers
+    private var rwc: int = 0; // waiting readers
+    private var wwc: int = 0; // waiting writers
+    private val mutex = new Lock;
+    private val rsem = new Lock;
+    private val wsem = new Lock;
+
+    def startRead = {
+      mutex.get;
+      if (wwc > 0 || wc > 0) {
+	rwc = rwc + 1;
+	mutex.release;
+	rsem.get;
+	rwc = rwc - 1;
+      }
+      rc = rc + 1;
+      if (rwc > 0) rsem.release;
+      mutex.release
+    }
+
+    def startWrite = {
+      mutex.get;
+      if (rc > 0 || wc > 0) {
+	wwc = wwc + 1;
+	mutex.release;
+	wsem.get;
+	wwc = wwc - 1;
+      }
+      wc = wc + 1;
+      mutex.release;
+    }
+
+    def endRead = {
+      mutex.get;
+      rc = rc - 1;
+      if (rc == 0 && wwc > 0) wsem.release;
+      mutex.release
+    }
+
+    def endWrite = {
+      mutex.get;
+      wc = wc - 1;
+      if (rwc > 0)
+	rsem.release
+      else if (wwc > 0) wsem.release;
+      mutex.release
+    }
+  }
+
+  /** A readers/writers lock, using channels, without priortities
+  */
+  class ReadWriteLock3 extends ReadWriteLock {
+
+    private val sr = new Signal;
+    private val er = new Signal;
+    private val sw = new Signal;
+    private val ew = new Signal;
+
+    def startRead = sr.send;
+    def startWrite = sw.send;
+    def endRead = er.send;
+    def endWrite = ew.send;
+
+    private def rwlock: unit = choice (
+      sr * (x => reading(1)),
+      sw * (x => { ew.receive; rwlock })
+    );
+
+    private def reading(n: int): unit = choice (
+      sr * (x => reading(n+1)),
+      er * (x => if (n == 1) rwlock else reading(n-1))
+    );
+
+    spawn < rwlock >;
+  }
+
+  /** Same, with sequencing
+  */
+  class ReadWriteLock4 extends ReadWriteLock {
+
+    private val rwlock = new ReadWriteLock3;
+
+    private val sr = new Signal;
+    private val ww = new Signal;
+    private val sw = new Signal;
+
+    def startRead = sr.send;
+    def startWrite = { ww.send; sw.send; }
+    def endRead = rwlock.endRead;
+    def endWrite = rwlock.endWrite;
+
+    private def queue: unit = choice (
+      sr * (x => { rwlock.startRead ; queue }),
+      ww * (x => { rwlock.startWrite; sw.receive; queue })
+    );
+
+    spawn < queue >;
+  }
+
+  /** Readwritelock where writers always have priority over readers
+  */
+  class ReadWriteLock5 extends ReadWriteLock {
+
+    private val sr = new Signal;
+    private val er = new Signal;
+    private val ww = new Signal;
+    private val sw = new Signal;
+    private val ew = new Signal;
+
+    def startRead = sr.send;
+    def startWrite = { ww.send; sw.send; }
+    def endRead = er.send;
+    def endWrite = ew.send;
+
+    private def Reading(nr: int, nw: int): unit =
+      if (nr == 0 && nw == 0)
+        choice (
+          sr * (x => Reading(1, 0)),
+          ww * (x => Reading(0, 1))
+        )
+      else if (nr == 0 && nw != 0) {
+        sw.receive;
+	Writing(nw);
+      }
+      else if (nr != 0 && nw == 0)
+        choice (
+          sr * (x => Reading(nr + 1, 0)),
+	  er * (x => Reading(nr - 1, 0)),
+          ww * (x => Reading(nr, 1))
+        )
+      else if (nr != 0 && nw != 0)
+        choice (
+          ww * (x => Reading(nr, nw + 1)),
+          er * (x => Reading(nr - 1, nw))
+        );
+
+    private def Writing(nw: int): unit  = choice (
+      ew * (x => Reading(0, nw - 1)),
+      ww * (x => Writing(nw + 1))
+    );
+
+    spawn < Reading(0, 0) >;
+
+  }
+
+  /**
+  * Main function.
+  */
+  def main(args: Array[String]): unit = {
+    val random = new java.util.Random();
+
+    def reader(i: int, rwlock: ReadWriteLock): unit = {
+      Thread.sleep(1 + random.nextInt(100));
+      System.err.println("Reader " + i + " wants to read.");
+      rwlock.startRead;
+      System.err.println("Reader " + i + " is reading.");
+      Thread.sleep(1 + random.nextInt(100));
+      rwlock.endRead;
+      System.err.println("Reader " + i + " has read.");
+      reader(i, rwlock)
+    }
+
+    def writer(i: int, rwlock: ReadWriteLock): unit = {
+      Thread.sleep(1 + random.nextInt(100));
+      System.err.println("Writer " + i + " wants to write.");
+      rwlock.startWrite;
+      System.err.println("Writer " + i + " is writing.");
+      Thread.sleep(1 + random.nextInt(100));
+      rwlock.endWrite;
+      System.err.println("Writer " + i + " has written.");
+      writer(i, rwlock)
+    }
+
+    val n = try { Integer.parseInt(args(0)) } catch { case _ => 0 }
+    if (n < 1 || 5 < n) {
+      Console.println("Usage: scala examples.pilib.rwlock <n> (n=1..5)");
+      exit
+    }
+    val rwlock = n match {
+      case 1 => new ReadWriteLock1
+      case 2 => new ReadWriteLock2
+      case 3 => new ReadWriteLock3
+      case 4 => new ReadWriteLock4
+      case 5 => new ReadWriteLock5
+    }
+    List.range(0, 5) foreach (i => spawn < reader(i, rwlock) >);
+    List.range(0, 5) foreach (i => spawn < writer(i, rwlock) >);
+  }
+
+}
+
diff --git a/docs/examples/pilib/scheduler.scala b/docs/examples/pilib/scheduler.scala
new file mode 100644
index 0000000000..3b08a9df66
--- /dev/null
+++ b/docs/examples/pilib/scheduler.scala
@@ -0,0 +1,149 @@
+package examples.pilib;
+
+import scala.concurrent.pilib._;
+
+object scheduler {
+
+  /**
+  * Random number generator.
+  */
+  val random = new java.util.Random();
+
+  //***************** Scheduler ******************//
+
+  /**
+  * A cell of the scheduler whose attached agent is allowed to start.
+  */
+  def A(a: Chan[unit], b: Chan[unit])(d: Chan[unit], c: Chan[unit]): unit = {
+    ///- ... complete here ...
+    choice ( a * { x => C(a, b)(d, c) })
+    ///+
+  }
+
+  /**
+  * A cell of the scheduler in another intermediate state.
+  */
+  def C(a: Chan[unit], b: Chan[unit])(d: Chan[unit], c: Chan[unit]): unit = {
+    ///- ... complete here ...
+    choice (c * { x => B(a, b)(d, c) })
+    ///+
+  }
+
+  /**
+  * A cell of the scheduler whose attached agent is allowed to finish.
+  */
+  def B(a: Chan[unit], b: Chan[unit])(d: Chan[unit], c: Chan[unit]): unit = {
+    ///- ... complete here ...
+    //     choice (b * { x => D(a, b)(d, c) }) // incorrect naive solution
+    choice (
+      b * { x => choice ( d(()) * A(a, b)(d, c) ) }, // b.'d.A
+      d(()) * (choice (b * { x => A(a, b)(d, c) }))  // 'd.b.A
+    )
+    ///+
+   }
+
+  /**
+  * A cell of the scheduler whose attached agent is not yet allowed to start.
+  */
+  def D(a: Chan[unit], b: Chan[unit])(d: Chan[unit], c: Chan[unit]): unit = {
+    ///- ... complete here ...
+    choice (d(()) * A(a, b)(d, c))
+    ///+
+  }
+
+  //***************** Agents ******************//
+
+  def agent(i: Int)(a: Chan[unit], b: Chan[unit]): unit = {
+    // 50% chance that we sleep forever
+    if (i == 0 && random.nextInt(10) < 5) {
+      a.attach(x => System.out.println("Start and sleeps ----> " + i));
+      Thread.sleep(random.nextInt(1000));
+      a.write(());
+    }
+    else {
+      a.attach(x => System.out.println("Start ----> " + i));
+      b.attach(x => System.out.println("Stop -> " + i));
+      Thread.sleep(random.nextInt(1000));
+      a.write(());
+      Thread.sleep(random.nextInt(1000));
+      b.write(());
+	agent(i)(a, b)
+    }
+  }
+
+  //***************** Entry function ******************//
+
+  /**
+  * Creates a scheduler for five agents (programs).
+  */
+
+  def main(args: Array[String]): unit = {
+    val agentNb = 5;
+    val agents = List.range(0, agentNb) map agent;
+    scheduleAgents(agents);
+  }
+
+  //***************** Infrastructure *****************//
+
+  /**
+  * A cell is modelled as a function that takes as parameters
+  * input and output channels and which returns nothing.
+  */
+  type Cell = (Chan[unit], Chan[unit]) => unit;
+
+  /**
+  * Creates a cell composed of two cells linked together.
+  */
+  def join(cell1: Cell, cell2: Cell): Cell =
+    (l: Chan[unit], r: Chan[unit]) => {
+      val link = new Chan[unit];
+      spawn < cell1(l, link) | cell2(link, r) >
+    };
+
+  /**
+  * Links the output of a cell to its input.
+  */
+  def close(cell: Cell): unit = {
+    val a = new Chan[unit];
+    cell(a, a)
+  }
+
+  /**
+  * Creates a cell consisting of a chain of cells.
+  */
+  def chain(cells: List[Cell]): Cell =
+    cells reduceLeft join;
+
+  /**
+  * Creates a cell consisting of a chain of cells.
+  */
+  def makeRing(cells: List[Cell]): unit =
+    close(chain(cells));
+
+  /**
+  * An agent is modelled as a function that takes as parameters channels to
+  * signal that it has started or finished.
+  */
+  type Agent = (Chan[unit], Chan[unit]) => unit;
+
+  /**
+  * Takes a list of agents and schedules them.
+  */
+  def scheduleAgents(agents: List[Agent]): unit = {
+    var firstAgent = true;
+    val cells = agents map (ag => {
+      val a = new Chan[unit];
+      val b = new Chan[unit];
+      spawn < ag(a, b) >;
+      if (firstAgent) {
+	firstAgent = false;
+	A(a, b)
+      }
+      else
+	D(a, b)
+    });
+    makeRing(cells)
+  }
+}
+
+
diff --git a/docs/examples/pilib/semaphore.scala b/docs/examples/pilib/semaphore.scala
new file mode 100644
index 0000000000..cfb0c8e5a2
--- /dev/null
+++ b/docs/examples/pilib/semaphore.scala
@@ -0,0 +1,72 @@
+package examples.pilib;
+
+/** Solution of exercise session 6 (first question). */
+object semaphore {
+
+  import scala.concurrent.pilib._;
+
+  class Signal extends Chan[unit] {
+    def send = write(());
+    def receive = read;
+  }
+
+  /** Interface. */
+  trait Semaphore {
+    def get: unit;
+    def release: unit;
+  }
+
+  /** First implementation. */
+  class Sem1 extends Semaphore {
+
+    private val g = new Signal;
+    private val r = new Signal;
+
+    def get: unit = g.send;
+    def release: unit = r.send;
+
+    private def Sched: unit = choice (
+      g * (x => { r.receive; Sched }),
+      r * (x => Sched)
+    );
+    spawn< Sched >;
+  }
+
+  /** Second implementation. */
+  class Sem2 extends Semaphore {
+
+    private val a = new Signal;
+    private val na = new Signal;
+
+    def get: unit = { a.receive; spawn< na.send > }
+    def release: unit = choice (
+      a * (x => spawn< a.send >),
+      na * (x => spawn< a.send >)
+    );
+    spawn< a.send >;
+  }
+
+  /** Test program. */
+  def main(args: Array[String]): unit = {
+    val random = new java.util.Random();
+    val sem = new Sem2;
+    def mutex(p: => unit): unit = { sem.get; p; sem.release }
+
+    spawn< {
+      Thread.sleep(1 + random.nextInt(100));
+      mutex( {
+	System.out.println("a1");
+	Thread.sleep(1 + random.nextInt(100));
+	System.out.println("a2")
+      } )
+    } | {
+      Thread.sleep(1 + random.nextInt(100));
+      mutex( {
+	System.out.println("b1");
+	Thread.sleep(1 + random.nextInt(100));
+	System.out.println("b2")
+      } )
+    } >;
+  }
+}
+
diff --git a/docs/examples/pilib/twoPlaceBuffer.scala b/docs/examples/pilib/twoPlaceBuffer.scala
new file mode 100644
index 0000000000..686547b344
--- /dev/null
+++ b/docs/examples/pilib/twoPlaceBuffer.scala
@@ -0,0 +1,67 @@
+package examples.pilib;
+
+import scala.concurrent.pilib._;
+
+/** Two-place buffer specification and implementation. */
+object twoPlaceBuffer with Application {
+
+  /**
+  * Specification.
+  */
+  def Spec[a](in: Chan[a], out: Chan[a]): unit =  {
+
+    def B0: unit = choice (
+      in * (x => B1(x))
+    );
+
+    def B1(x: a): unit = choice (
+      out(x) * (B0),
+      in * (y => B2(x, y))
+    );
+
+    def B2(x: a, y: a): unit = choice (
+      out(x) * (B1(y))
+    );
+
+    B0
+  }
+
+  /**
+  * Implementation using two one-place buffers.
+  */
+  def Impl[a](in: Chan[a], out: Chan[a]): unit =  {
+    ///- ... complete here ...
+    // one-place buffer
+    def OnePlaceBuffer[a](in: Chan[a], out: Chan[a]): unit =  {
+      def B0: unit = choice ( in * (x => B1(x)) );
+      def B1(x: a): unit = choice ( out(x) * (B0));
+      B0
+    }
+    val hidden = new Chan[a];
+    spawn < OnePlaceBuffer(in, hidden) | OnePlaceBuffer(hidden, out) >
+    ///+
+  }
+
+  val random = new java.util.Random();
+
+  def Producer(n: Int, in: Chan[String]): unit = {
+    Thread.sleep(random.nextInt(1000));
+    val msg = "" + n;
+    choice (in(msg) * {});
+    Producer(n + 1, in)
+  }
+
+  def Consumer(out: Chan[String]): unit = {
+    Thread.sleep(random.nextInt(1000));
+    choice (out * { msg => () });
+    Consumer(out)
+  }
+
+  val in = new Chan[String];
+  in.attach(s => System.out.println("put " + s));
+  val out = new Chan[String];
+  out.attach(s => System.out.println("get " + s));
+  //spawn < Producer(0, in) | Consumer(out) | Spec(in, out) >
+  spawn < Producer(0, in) | Consumer(out) | Impl(in, out) >
+
+}