• Alexandre Duret-Lutz's avatar
    Store membership to acceptance sets using bitsets, not BDDs. · 2c764fb3
    Alexandre Duret-Lutz authored
    This is a huge patch, that took over a month to complete.  The bit sets
    are currently restricted to what 'unsigned can store', but it should be
    easy to extend it to 'uint64_t' should we need it.
    
    * NEWS: Update.
    * src/tgba/acc.hh: New file.
    * src/tgbatest/acc.cc, src/tgbatest/acc.test: Test it.
    * src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.hh,
    src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh: Delete.  The KV
    complementation is too slow to be used in practice, and I somehow broke
    it during the conversion to bitsets.  The tgba->sgba conversion was only
    used for the KV complementation, and should be better redone on
    tgba_digraph_ptr should it be needed again.
    * src/bin/ltlcross.cc, src/dstarparse/dra2ba.cc,
    src/dstarparse/nsa2tgba.cc, src/graphtest/tgbagraph.cc,
    src/graphtest/tgbagraph.test, src/kripke/fairkripke.cc,
    src/kripke/fairkripke.hh, src/kripke/kripke.cc, src/kripke/kripke.hh,
    src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
    src/misc/hash.hh, src/neverparse/neverclaimparse.yy, src/priv/accmap.hh,
    src/ta/ta.cc, src/ta/ta.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh,
    src/ta/taproduct.cc, src/ta/taproduct.hh, src/ta/tgta.cc,
    src/ta/tgta.hh, src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh,
    src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh, src/taalgos/dotty.cc,
    src/taalgos/emptinessta.cc, src/taalgos/minimize.cc,
    src/taalgos/tgba2ta.cc, src/tgba/Makefile.am, src/tgba/fwd.hh,
    src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc,
    src/tgba/tgba.hh, src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh,
    src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc,
    src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
    src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
    src/tgbaalgos/bfssteps.cc, src/tgbaalgos/complete.cc,
    src/tgbaalgos/compsusp.cc, src/tgbaalgos/degen.cc,
    src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc,
    src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dtgbasat.cc,
    src/tgbaalgos/dupexp.cc, src/tgbaalgos/emptiness.cc,
    src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/ce.cc,
    src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
    src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
    src/tgbaalgos/gv04.cc, src/tgbaalgos/hoaf.cc,
    src/tgbaalgos/isweakscc.cc, src/tgbaalgos/lbtt.cc,
    src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/magic.cc,
    src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc,
    src/tgbaalgos/postproc.cc, src/tgbaalgos/powerset.cc,
    src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh,
    src/tgbaalgos/reducerun.cc, src/tgbaalgos/replayrun.cc,
    src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc, src/tgbaalgos/scc.cc,
    src/tgbaalgos/scc.hh, src/tgbaalgos/sccfilter.cc,
    src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh,
    src/tgbaalgos/se05.cc, src/tgbaalgos/simulation.cc,
    src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc,
    src/tgbaalgos/stripacc.cc, src/tgbaalgos/tau03.cc,
    src/tgbaalgos/tau03opt.cc, src/tgbaalgos/weight.cc,
    src/tgbaalgos/weight.hh, src/tgbaparse/tgbaparse.yy,
    src/tgbatest/Makefile.am, src/tgbatest/complementation.cc,
    src/tgbatest/complementation.test, src/tgbatest/degenlskip.test,
    src/tgbatest/det.test, src/tgbatest/dstar.test, src/tgbatest/emptchk.cc,
    src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
    src/tgbatest/explpro4.test, src/tgbatest/explprod.test,
    src/tgbatest/ltl2tgba.cc, src/tgbatest/ltl2tgba.test,
    src/tgbatest/maskacc.cc, src/tgbatest/maskacc.test,
    src/tgbatest/neverclaimread.test, src/tgbatest/randtgba.cc,
    src/tgbatest/readsave.test, src/tgbatest/sim.test,
    src/tgbatest/sim2.test, src/tgbatest/spotlbtt.test,
    src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test,
    iface/dve2/dve2.cc: Adjust or use to the new acceptance interface.
    2c764fb3
To find the state of this project's repository at the time of any of these versions, check out the tags.
NEWS 72.5 KB