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":

z = buddy.bdd_ithvar(det.register_ap("z"))
spot.set_synthesis_outputs(det, z)

And the outcome is the same ("realisable").


best wishes,
a.

On Mon, Jan 3, 2022 at 12:30 PM Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:
Ayrat Khalimov <ayrat.khalimov@gmail.com> writes:
> Is there a way to feed HOA file (as a nondet Buchi) instead of a
> formula to ltlsynt?

Not yet.  But you can do that process in Python.