game/synthesis cleaning bits
Here are some small cleanups which I think are needed in the game/synthesis code. I'm currently working on the first two points, and adding more to this list as I progress.
-
update doc/org/ltlsynt.org
with more details about how ltlsynt works and its options -
document ltlsynt -x
options intospot-x(7)
-
rename spot::create_game()
to something that is related to synthesis. Maybeltl_to_game()
? -
rename spot::try_create_direct_strategy()
to something more specific, and also its documentation does not seems to be up-to-date -
the -x specification-decomposition
and-x minimization-level
could potentially be renamed to use a common prefix that makes clear these are synthesis related. In particular,minimization-level
is quite unspecific, maybeaiger-simplify=N
would be more specific.
specification-decomposition
is long to type and its size breaks the--help
-to-manpage conversion... update instead, I renamed those to--simplify
and--decompose
. -
current default for minimization-level
is 1 in some part of the code, and 0 in other parts, but I thought the conclusion of our draft paper about minimization was that the default should be 2? -
fix doc/spot.bib
's finkbeiner2021specification entry (should not be an@article
, and should follow naming conventions) -
The game_info
class unexpectedly contains things that are very specific to synthesis. Probably there should be agame_info
class, and asynthesis_game_info
subclass that adds more fields that the game code does not need. -
solve_game()
is documented as dispatching to the right solver, but seems only to callsolve_parity_game()
, and neversolve_safety_game()
. Ideally we should usesolve_game()
intut40.org
as well, as that would be a more high-level interface. -
games.ipynb
needs to be split intogames.ipynb
andsynthesis.ipynb
. People interested in games should not be overwhelmed with synthesis stuff, this particular application is best illustrated separately. -
One of the synthesis example in games.ipynb
has a comment saying "Todo arena changes when executed multiple times". This does not belong to the user's documentation. It could be a ticket in the issue tracker. -
option --aiger
defaults to--aiger=inf
which is not a recognized value -
the documentation for strategy_to_aig
does not match that of--aiger
. In particular one mentions+ud
and the other+dual
. One hassub0,sub1,sub2
and the otherso0,so1,so2,so3
. -
it's unclear what +dc
means, in a more precise way than "take advantage of don't care values". -
the Doxygen documentation should have groups synthesis
andgames
to list all those functions -
maybe add the concept of "mealy machine" as an automaton that contains a "mealy-outputs" named property. Then create_strategy()
becomessolved_game_to_mealy()
,strategy_to_aig()
ismealy_to_aiger
, etc.