Timed Rebeca to Erlang Translation Tool

Language: Haskell

This document describes how to get the timedreb2erl tool up and running.

Follow the rest of this document in order to produce an executable file.

All commands should be executed from the project root, i.e. the directory this README file lies in.


McErlang is required to be able to verify and simulate the generated Erlang code.


cabal install

And now we have a fresh binary timedreb2erl in our cabal bin directory.


Given a timed rebeca model, we can generate Erlang source code for the model such that we can simulate it with McErlang.

timedreb2erl [OPTIONS] FILE

Common flags:
  -m --mcerlang          Use McErlang
  -c --mcerlangoutput    McErlang: Output CSV when using McErlang
  -p --partialorder      McErlang: Use EXPERIMENTAL partial order reduction
  -e --eventviewer       Include event viewer in the generated erlang code
  -l --logtodb           Log msgsrv calls to a database
  -t --timelimit=INT     Time limit for the simulation & execution
  -r --rtfactor=INT    
  -o --outputdir=FOLDER
  -? --help              Display help message
  -V --version           Print version information

If no outputdir is specified the resulting Erlang code is printed to stdout.

Using mcerlangoutput is essential for doing simulation with DTime (Discrete time) McErlang.

The partialorder flag uses an partial order branch wich is essential for verifying the generated Erlang source code. If this is not used we will not use urgent constructs and therefore traverse the state-space incorrectly.

The rtfactor flag specifies what time units are in the generated code (in milliseconds). Default 1000.

The monitor flag has no effect unless outputdir is used.

Project Statistics

Sourcerank 3
Repository Size 583 KB
Forks 0
Watchers 2
Dependencies 0
Tags 0
Last updated

Something wrong with this page? Make a suggestion

Last synced: 2018-02-04 14:40:00 UTC

Login to resync this repository