Skip to content
GitLab
  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • Spot Spot
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 132
    • Issues 132
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 2
    • Merge requests 2
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Spot
  • SpotSpot
  • Issues
  • #495
Closed
Open
Created Jan 06, 2022 by Alexandre Duret-Lutz@adlOwner

split_2step cannot complete monitors

Screenshot_from_2022-01-06_09-56-52

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking