• Alexandre Duret-Lutz's avatar
    dstar: implement dra_to_dba() · 9a7590a6
    Alexandre Duret-Lutz authored
    This is an implementation of Krishnan's ISAAC'94 paper to convert
    deterministic Rabin automata into DBA when possible.
    
    * src/dstarparse/dra2dba.cc: New file.
    * src/dstarparse/dstar2tgba.cc: New file.
    * src/dstarparse/Makefile.am: Add them.
    * src/dstarparse/nra2nba.cc (nra_to_nba): Adjust so
    that dra_to_dba() can call it using a masked automaton.
    * src/dstarparse/public.hh (dra_to_dba, dstar_to_tgba): Declare.
    * src/tgbatest/ltl2tgba.cc: Add an -XDD option.
    * src/tgbatest/dstar.test: More tests.
    9a7590a6
nra2nba.cc 4.2 KB