hello, Is there a way to feed HOA file (as a nondet Buchi) instead of a formula to ltlsynt? I tried smth (see below), but I am getting 'unrealisable' for nondet Buchi automaton spec that is supposed to be realisable (see attached). Maybe I missing something? (like ltlsynt dualising the automaton, etc.) Here is what I tried. Into file synthesis.cc, add: #include "spot/parseaut/public.hh" Then in line 822, comment out: // auto aut = trans.run(f); and instead add: spot::bdd_dict_ptr dict = spot::make_bdd_dict(); auto parsed_aut = parse_aut("/tmp/spec.hoa", dict); if (parsed_aut->aborted) abort(); auto aut = parsed_aut->aut; This forces ltlsynt to read file "/tmp/spec.hoa" and ignore the formula. Further, when calling ltlsynt, pass the argument --decompose=no ('just in case'): ./ltlsynt --formula="GF a" --ins=x,y --dot --outs=a,b,c --decompose=no and provide the correct --ins and --outs arguments, and any formula with one of those propositions. The tool outputs expected implementations on toy examples, but on a larger example attached it outputs "unrealizable" instead of "realizable". That is why the question. best wishes, Ayrat
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.
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.
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.
Ayrat Khalimov <ayrat.khalimov@gmail.com> writes:
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?
Hmm, sorry, I went too fast, and assumed that solve_parity_game() was able to solve any kind of parity game, but currently it's still restricted to max-odd colored parity. So please change the code to look like this: det = aut.postprocess('deterministic', 'parity max odd', 'colored', # <- two changes 'low') spot.set_synthesis_outputs(det, ...) # unchanged game = spot.split_2step(det, spot.get_synthesis_outputs(det), True) # changed game = spot.colorize_parity_here(game, True) # added spot.solve_game(game)
participants (2)
-
Alexandre Duret-Lutz -
Ayrat Khalimov