Implementing a domain-specific multi-result supercompiler by means of the MRSC toolkit

The paper presents a simple domain-specific multi-result supercompiler for counter systems implemented by means of the MRSC toolkit. The input language of the supercompiler is a non-deterministic domain-specific language meant for specifying models of communication protocols. The implementation of this DSL is based on “embedding” and the heavy use of higher-order constructs. There are presented 2 versions of the multi-result supercompiler. The first one implements a naive algorithm, which turns out to be rather inefficient. The second version exploits the specifics of the domain, thereby drastically reducing the number of generated graphs of configurations and the amount of resources consumed by supercompilation.