I wanted to show that Egel can be used to create small tools, and decided upon a temporal logic synthesizer. After reading a bit I trimmed that down to: do something useful with LTL and Z3. The first because LTL is relatively small, the latter since I want Z3 bindings for Advent of Code anyway.
Synthesis is a bit of a hopeless subject since the best you can hope for is to derive small automata with maybe five states. Moreover, it already exploded on translating LTL to negation normal form, the first ostensibly minor step in the whole process.
But I remain committed for now.
