4 Jan
2022
4 Jan
'22
11:44 a.m.
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.