Take Command of Your Constraints! (Technical Report)

Constraint automata (CA) are a coordination model based on finite automata on infinite words. Although originally introduced for compositional modeling of coordinators, an interesting new application of CA is actually implementing coordinators (i.e., compiling CA to executable code). Such an approach guarantees correctness-by-construction and can even yield code that outperforms hand-crafted code. The extent to which these two potential advantages arise depends on the smartness of CA-compilers and the existence of proofs of their correctness. We present and prove the correctness of a critical optimization for CA-compilers: a sound and complete translation from declarative constraints in transition labels to imperative commands in a sequential language. This optimization avoids expensive calls to a constraint solver at run-time, otherwise performed each time a transition fires, and thereby significantly improves the performance of generated coordination code.