This repository contains Xtext-definition for model-checking DSLs.
PML - a DSL covering a fraction of Promela (the input language for Spin). The covered fraction is mainly motivated by the example file ....pml.examples/src/japaneseBodin_Orgi.pml RCRS - a DSL for formulating river-crossing problems
Both DSLs are decribed by the paper
Thomas Baar: A DSL and a SPIN-Frontend for River-Crossing Problems Defined with Xtext
published at the Bulletin of IIS, Ershov-Institute, Novosibirsk, Russia, 2016.
You can find a pre-version of the paper in folder ....rcrs/doc