>> 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?

Thanks!

On Tue, Jan 4, 2022 at 1:50 PM Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:

Ayrat Khalimov <ayrat.khalimov@gmail.com> writes:

> Wonderful! Confirm it works.
>
> A small correction: in your jupyter notebook you set outputs "x,y"
> whereas originally they were inputs. So instead I used a new variable
> "z":

Ah, sorry. In the spec file that you used, I saw:

AP: 5 "a" "b" "x" "c" "y"
controllable-AP: 4 2

which means that x and y are intended to be output, so I tried to follow
that. I did not realize that you had specified the opposite on the
command line.

Incidentally, I was working yesterday on getting Spot's HOA parser and
printer to support this controllable-AP header (and map it to Spot's
synthesis-outputs property). That will be for Spot 2.11.