https://www.mdu.se/

Afra is an Eclipse-based tool for the modeling and model checking of Rebeca family models. Together with the standard enriched editor, easy to trace counter-example viewer, modular temporal property definition, exporting a model and its transition system to some other formats facilities are features of Afra. Rebeca family provides actor-based modeling languages which are designed to bridge the gap between formal methods and software engineering. Faithfulness to the system being modeled, and the usability of Rebeca family languages help in ease of modeling and analysis of the model, together with the synthesis of the system based on the model. In this paper, architectural decisions and design strategies we made in the development of Afra are presented. This makes Afra an extensible and reusable application for the modeling and analysis of Rebeca family models. Here, we show how different compilers can be developed for the family of languages which are the same in general language constructs but have some minor differences. Then we show how the model checking engine for these different languages is designed. Despite the fact that Afra has a layered object-oriented design and is developed in Java technology, we use C++ codes for developing its model checking for the performance purposes. This decision made the design of the application even harder.