Resumen:
This article presents Makina, a new library and a domainspecific language for writing property-based testing modelsfor stateful programs. Models written in the new domainspecific language are, using Elixir macros, rewritten intonormal QuickCheck state machines. Our main goals withMakina are to facilitate the task of developing correct andmaintainable models, and to encourage model reuse. To meetthese goals, Makina provides a declarative syntax for defin-ing model states and model commands. In particular, Makinaencourages the typing of specifications, and ensures throughits rewrite rules that such type information can be used by,e.g., the Dialyzer tool, to effectively typecheck models. More-over, to promote model reuse, the domain specific languageprovides constructs to permit models to be defined in termsof collections of previously defined models.