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
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.
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)
-
Alexandre Duret-Lutz -
Ayrat Khalimov