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.