I/O for bounded automata (adl/given branch)
We need some way to save and load the upper-cond
property introduced on the adl/given branch, unfortunately the HOA format does not allows arrays of conditions to be listed in headers, like we do for other properties. Dávid Smolka is currently using a hack where he saves the upper bound as a separate edge that is highlighted.
Since this feature is currently Spot specific, maybe we can simply extend the HOA format to support guards like
[0&1 .. 0|1]
, or maybe we introduce some more generic syntax that would allow us to deal with more extensions in the future.