Some of the common concurrency problems has been modeled using Rebeca as case studies. Here, you can find the Rebeca model for them. Each of the models below has been translated to either SMV, or Promela, or both, for model checking using the developed automated tools. They are model checked afterwards using NuSMV and SPIN model checkers. The model checking results are present in the published papers, which you can download in the Publications section.

Note that in some of the following examples the "initial()" message server is obsolete in version RMC 2.5.0 and later. The initial method is defined for each reactive class and is executed automatically when an actor (rebec) is instantiated in the main part. In the version RMC 2.5.0 and later, the “initial“ method is replaced by constructor (a message server with the same name as the reactive class name). That's why you may see “initial()“ and constructor interchangeably in some examples and documents. The new version does not support CTL model checking too. So, the CTL blocks must be eliminated from properties files to make them compatible with RMC 2.5.0.

Rebeca Examples:

Timed Rebeca Examples

Probabilistic Timed Rebeca Examples