Ayrat Khalimov ayrat.khalimov@gmail.com writes:
controllable-AP: 4 2
Indeed, I see: In my tool, the input HOA automaton is treated dually as a universal co-Buchi automaton, hence the inversion of inputs/ outputs.
A follow up question: trying to synthesize from the attached HOA file results in
RuntimeError: solve_parity_game(): arena must be colorized
Any ideas why this happens?
Hmm, sorry, I went too fast, and assumed that solve_parity_game() was able to solve any kind of parity game, but currently it's still restricted to max-odd colored parity.
So please change the code to look like this:
det = aut.postprocess('deterministic', 'parity max odd', 'colored', # <- two changes 'low') spot.set_synthesis_outputs(det, ...) # unchanged game = spot.split_2step(det, spot.get_synthesis_outputs(det), True) # changed game = spot.colorize_parity_here(game, True) # added spot.solve_game(game)