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(a)lrde.epita.fr>
wrote:
Ayrat Khalimov <ayrat.khalimov(a)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.