split_2step cannot complete monitors
Function split_2step()
has no documented precondition, so it seems wrong to have it fail on monitors (or any acceptance for which no rejecting set of colors exist). In that case, one could for instance remove all colors (if there are any), set the acceptance to Fin(0)
and color the the sink. (The complete()
function does the opposite, it sets the acceptance to Inf(0)
, color all original transitions as {0}
and leave the sink uncolored, but we probably want to favor max-odd acceptance until solve_parity_game()
is generalized.)
Also, while we are at it, I do not understand the last note in the documentation:
/// \param aut automaton to be transformed
/// \param output_bdd conjunction of all output AP, all APs not present
/// are treated as inputs
/// \param complete_env Whether the automaton should be complete for the
/// environment, i.e. the player of inputs
/// \note This function also computes the state players
/// \note If the automaton is to be completed for both env and player
/// then egdes between the sinks will be added
The "both env and player" makes no sense to me, as the environment is also a player, and we do not have an option to produce an output-complete arena.