handling unconstrained I/O in ltlsynt
It's possible to call ltlsynt
with --ins
and --outs
options that refers to AP that are not in the formula, or that disappear from the formula after simplification. Currently those AP are added to the automaton after translation, but it's probably more efficient to just add them to the output once the game has been solved.