Richer specification language for models
Currently, COOL models are specified simply as the coalgebra structure however other model checkers typically do not give explicit per-state models but rather some generating system description.
It is for example quite common to specify typed variables (bounded) and some guarded mechanism of how their values evolve. Some specification languages also have forms of modularization and macro mechanisms. These features are only syntactic sugar on top of the underlying coalgebra structure and can hence be compiled into bare model structures.
Specification languages
- AUT https://cadp.inria.fr/man/aut.html LTS as a list of triples
- MoDeST https://www.researchgate.net/profile/Pedro-Dargenio/publication/28552328_MODEST_A_modelling_language_for_stochastic_timed_systems/links/0deec522297224620f000000/MODEST-A-modelling-language-for-stochastic-timed-systems.pdf
- mCRL2 https://www.mcrl2.org/web/user_manual/language_reference/mcrl2.html
- SMV https://nusmv.fbk.eu/NuSMV/papers/sttt_j/html/node7.html -> NuSMV/nuXmv
- GPF -> GPUExplore https://www.win.tue.nl/~awijs/articles/GPUexplore-tacas14.pdf
- DVE/mDVE https://is.muni.cz/www/bauch/meandve.pdf -> BEEM benchmark set available in mDVE https://paradise.fi.muni.cz/beem/
- JANI https://jani-spec.org/ -> many benchmarks available in JANI
- BIR https://bogor.projects.cs.ksu.edu/manual/ch02.html -> BOGOR https://bogor.projects.cs.ksu.edu/manual/
- UPPAAL https://docs.uppaal.org/language-reference/
Vision
My goal would be to have a modular architecture where various input language features can be implemented as individual compiler passes over the input structure until it arrives at the bare coalgebra structure