IMCReo

IMCReo (Interactive Markov Chains for Reo) is a semantic model for the stochastic version of Reo, based on IMC, the well-studied model for performance evaluation of distributed systems introduced by Holger Hermanns.
The IMCReo model presents the following interesting characteristics:

It is compositional
inherits compositionality from the original IMC model
It captures context-dependency
interactive transitions (meaning the firing of ports) occur depending on the requests at ports
It derives directly from a Stochastic Reo connector
no intermediate model or conversion is required to obtain a IMCReo for a connector
It has tool support
IMCReo is effortlessly transformed into standard IMC, therefore tools like IMCA, CADP or PRISM may be used for quantitative/qualitative analysis

The Model

IMCReo is a concrete instance of IMC. In particular, to capture Reo-like behavior, it adds information to the states of the base transition system, and introduces a new perspective on interactive transitions.
Formally, an IMCReo is a tuple (S,Act,it,mt,s), where

  • S is a set of states,
  • Act is a set of sets of visible actions
  • it is a subset of S x Act x S, representing the interactive transitions
  • mt is a subset of S x R+ x S, representing the markovian transitions
  • s is the initial state.

States

The states capture the possible behavior of the connector in what concerns data arrivals, data flowing through ports, as well as connector internal state. Therefore each state q is composed of three components (R,T,Q).

  • R - set of port names with pending requests
  • T - set of port names through which data is being transmitted
  • Q - list of internal state identifiers (e.g., full or empty) for state-based connectors

Visually, a state may appear as follows:

  • [R]Q : for states of kind (R,0,Q), with 0 representing the empty set and R a non empty set of port names
  • {T}Q : for states of kind (0,T,Q), with 0 representing the empty set and T a non empty set of port names
  • [R]{T}Q : for states of kind (R,T,Q), with R and T non empty sets of port names
  • 0Q : for states of kind (0,0,Q), with 0 representing the empty set.

Interactive Transitions

An interactive transition (IT) in IMC Reo is different from the traditional IT, because it supports a set of actions instead of a single action.
This way, an IT (q1,{a,b,c},q2) means that the system evolves from state q1 to state q2 via a synchronous activation of the ports a, b and c.

An empty set of action in an IT, means the internal transition, i.e., tau-transition.

Visually, ITs are represented with dashed arrows with the concatenation of the actions over them.

Markovian Transitions

A markovian transition (MT) in IMC Reo is exactly the same as in the traditional IMC. It is associated with a positive real number meaning a rate of both a delay on processing data, or the actual rate of a request arriving to some port.

Visually, MTs are represented with solid arrows with the rate number over them.

Examples

IMCReo for basic channels

This image shows the IMCReo for the main basic Reo channels.
For the sync channel, the IMCReo may be interpreted in this way:

initially, no requests are pending neither in port a nor in port b. At a rate of gamma_a (resp. gamma_b) a request arrives to port a (resp. port b). At that moment, the channel blocks until a request arrives to the other port at rate gamma_b (resp. gamma_a). When state [a,b] is reached, representing a configuration in which both ports have pending requests, then both may fire. That is, actions a and b may be activated simultaneously. At this moment, the channel starts transmitting data between a and b and evolves back to the initial state at a rate of gamma_ab.

This image shows a composition of a lossy channel with a fifo channel. The interpretation is similar to that given for the basic sync channel
To avoid complexity in the drawing, references to states are made using a dashed circle.

Tool Support

Tool support for the IMCReo model counts in a first instance with a tool -- IMCREOtool -- that transforms stochastic Reo connectors into IMCReo and then into IMC (in several file formats).
This tool shall be the head of a tool chain for qualitative and quantitative analysis of IMCs. Such tool chain would take advantage of tools like IMCA, CADP or PRISM.

In version 1.3.3 it was introduced two internal tools:

  • generator - which maintains the API compatibility with the earlier release and allows for the generation of input to IMCA and CADP.
  • prismer - which allows for the generation of a suitable and yet customizable input for PRISM.

Input

The main input for IMCREOtools is an rlf script file (CooPLa Language) with connectors, from which, the name of the connector for analysis shall be picked

For the understanding of the simple CooPLa syntax, it is advised to check the example rlf files below, while there is no documentation for it...

Output

The output of IMCREOtool is varied:

  • MA file -- Markov Automata file for later use in IMCA tool.
  • RMA file -- Reo Markov Automata file for later use in IMCREOtool. It is a slightly modified version of a MA file... (not working correctly on version 1.3.3)
  • AUT file -- textual file for later use in CADP (with best usage by converting it into a BCG file within CADP)
  • DOT file -- textual file for visualization in Graphviz.

Download

Find the latest release at https://github.com/pnpo/doctools/releases

To run this tool, it would be required Java version 6 or higher.
A basic usage would be: $ java -jar IMCREOtools-1.3.3.jar generator -f file.rlf -p PatternName --cadp file.aut

Example

Here follows the material for a simple example of how to use IMCREOtools for analysis works lost in a bounded-queue printing system. (NOTE: for compatibility of the example with the latest releases, it should be added generator before the other parameters...)

One converts a lossyfifo connector into an IMC (with the help of the theory behind IMCREO) and then convert the composed IMCREO into a MA file suitable to be analyzed with the IMCA.
With the help of IMCA, one is able to see the losses with a bounded period of time.

IMCREOtool Basic Example
Channels Script (support file)
Coordination Patterns Script (support file)