Skip to content
  • Thibaud Michaud's avatar
    add ltlsynt executable · 0821c97e
    Thibaud Michaud authored
    For now, ltlsynt only handles LTL realizability. It uses a reduction to
    parity game followed by Calude et al.'s reduction from parity game to
    reachability game.
    
    * bin/ltlsynt.cc, bin/Makefile.am, bin/man/ltlsynt.x,
    bin/man/Makefile.am, bin/.gitignore: New binary.
    * doc/org/arch.tex, doc/Makefile.am, doc/org/tools.org,
    doc/org/ltlsynt.org: Document it.
    * spot/misc/game.cc, spot/misc/game.hh, spot/misc/Makefile.am: Parity
    game wrapper for parity automata + reachability game interface from
    Calude et al.'s paper.
    0821c97e
To find the state of this project's repository at the time of any of these versions, check out the tags.