4 Jan
2022
4 Jan
'22
2:46 p.m.
> 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(a)lrde.epita.fr>
wrote:
Ayrat Khalimov <ayrat.khalimov(a)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.
