Exercise: Instant Messenger

The goal of this exercise is to model and implement a simple instant messenger application using Reo. Make sure you have installed the Reo Core Tools version 3.2.1 or higher, and the code generation and automata tools. You should prepare your Eclipse workbench by

  1. switching to the Reo perspective (Window menu),
  2. creating a new project or using an exisiting one, and
  3. create a new Reo connector file, called messenger.reo inside of the project.

1) Modeling and Simulation

In this example, you will create an application that consists of two components, called clients, and one Reo connector that is used to coordinate the clients. The idea is that the clients exchange messages and the connector determines the protocol being used.

Before drawing the connector, create two components first and call them ClientA and ClientB. Then create in both components a source end, called in, and a sink end, called out. You have to add them at the title bar of the component. You can later move the ends along the border of the component. Now create a connector Messenger, add four nodes and connect them to the component ends using links. The actual conector should be according to the following protocol.

  1. Synchronized message receival: For each of the clients, the connector can buffer one message. The connector releases buffered messages only together, i.e. client A receives a message from B, if and only if B also gets a message from A.

    Verify your connector in the animation view. For this, you have to specify how the two components should behave. You can do this by adding a property to the components, with the name mode and the value one of EmptyFIFO, FullFIFO or ReadOrWrite. The behavior is different for each of these modes. Simulate the network stepwise using guided animations.

    Which (combinations of) component modes produce deadlocks and which not?

  2. Now we change the protocol. Duplicate the current network for this (see context menu) and change the copy. The new protocol is as follows:

    Alternating message receival: The connector again buffers exactly one message from each client, but it now alternates the receival: first A gets a message from B, then B gets a message from A, then again A gets a message from B, etc.

    Verify again, which component modes deadlocks produce.

  3. We change the protocol one more time. Duplicate the current network. The new protocol is as follows:

    Confirmations: The connector again buffers exactly one message from each client. Messages can be sent in any order, but the sender always receives a copy of his message when the other client received it.

    Verify again, which component modes deadlocks produce.

2) Implementation and Execution

  1. Code generation: Generate Java code from one of the three networks. Create the component classes ClientA and ClientB with the following initial code:
    package connector;
    import cwi.ea.runtime.ReoComponent;
    import cwi.ea.runtime.Sink;
    import cwi.ea.runtime.Source;
    public class ClientA implements ReoComponent<String> {
       private Source<String> in;
       private Sink<String> out;
       public ReoComponent<String> withSinkPorts(Sink<String>... sinks) {
          out = sinks[0];
          return this;
       public ReoComponent<String> withSourcePorts(Source<String>... sources) {
          in = sources[0];
          return this;
       public void run() {
          // TODO: Perform I/O operation in a loop here.
  2. Execution tests: Choose one combination of the component modes EmptyFIFO, FullFIFO and ReadOrWrite that produced and one that didn't produce a deadlock in the animation for this network. Modify the client implementations so that the behave according to these modes. Execute the application and verify that it indeed produces / does not produce a deadlock.

  3. ReoLive: Now we use a different approach of executing the coordinator, i.e. the coordination web service ReoLive. For this, find another group and together choose one messenger network that you want to use. Save the *.reo and upload it to the ReoLive web interface at http://reo.project.cwi.nl/live. Delete networks that you don't want to use and write down the number of the network you want to use.

    Now, click on your network and then on the components. One group should download the implementation stubs for ClientA and one for ClientB. Unpack the downloaded archives. In Eclipse, click on File -> New -> Other -> Java project from existing Ant Buildfile. Use the file build.xml in the extracted folder.

    Adjust the client implementations. Start the network in the ReoLive network list. Then execute both clients and test the application. What happens if you stop the network again, without stopping the clients?

3) Model Checking

Use the Vereofy model checker to check the following properties. Vereofy considers only the connectors, and not the components. Therefore, give the boundary nodes of the your connectors names using the Properties view.

  1. Synchronized message receival:
    1. after ClientA has sent a message, ClientB can receive a message
    2. if ClientA receives a message, ClientB also receives one

  2. Alternating message receival:
    1. if ClientA receives a message, ClientB cannot, and vice versa

  3. Confirmations:
    1. if ClientA or ClientB has sent a message, ClientA can receive a message