- 22 Apr, 2015 3 commits
-
-
Alexandre Duret-Lutz authored
Automatic mass renaming. * src/tgbaalgos/: Rename as... * src/twaalgos/: ... this. * README, configure.ac, iface/ltsmin/modelcheck.cc, src/Makefile.am, src/bin/autfilt.cc, src/bin/common_aoutput.cc, src/bin/common_aoutput.hh, src/bin/common_output.hh, src/bin/common_post.hh, src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/ltlfilt.cc, src/bin/randaut.cc, src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc, src/graphtest/twagraph.cc, src/kripke/kripkeprint.cc, src/ltlvisit/contain.cc, src/ltlvisit/contain.hh, src/ltlvisit/exclusive.cc, src/taalgos/emptinessta.hh, src/tgbatest/checkpsl.cc, src/tgbatest/checkta.cc, src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc, src/tgbatest/randtgba.cc, src/tgbatest/taatgba.cc, src/twa/twa.cc, src/twa/twagraph.hh, src/twa/twasafracomplement.cc, wrap/python/spot_impl.i: Adjust.
-
Alexandre Duret-Lutz authored
Automatic mass renaming. * src/bin/autfilt.cc, src/bin/common_aoutput.cc, src/bin/common_aoutput.hh, src/bin/common_conv.cc, src/bin/common_conv.hh, src/bin/common_output.hh, src/bin/dstar2tgba.cc, src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/randaut.cc, src/dstarparse/dra2ba.cc, src/dstarparse/dstar2tgba.cc, src/dstarparse/dstarparse.yy, src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc, src/dstarparse/public.hh, src/graphtest/tgbagraph.cc, src/hoaparse/hoaparse.yy, src/hoaparse/public.hh, src/ltlvisit/contain.hh, src/ltlvisit/exclusive.cc, src/ltlvisit/exclusive.hh, src/priv/accmap.hh, src/taalgos/minimize.cc, src/tgba/fwd.hh, src/tgba/tgba.cc, src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh, src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh, src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh, src/tgbaalgos/canonicalize.cc, src/tgbaalgos/canonicalize.hh, src/tgbaalgos/cleanacc.cc, src/tgbaalgos/cleanacc.hh, src/tgbaalgos/complete.cc, src/tgbaalgos/complete.hh, src/tgbaalgos/compsusp.cc, src/tgbaalgos/compsusp.hh, src/tgbaalgos/cycles.hh, src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh, src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dtgbacomp.hh, src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh, src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh, src/tgbaalgos/hoa.cc, src/tgbaalgos/isdet.cc, src/tgbaalgos/isdet.hh, src/tgbaalgos/lbtt.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/mask.cc, src/tgbaalgos/mask.hh, src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh, src/tgbaalgos/product.cc, src/tgbaalgos/product.hh, src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh, src/tgbaalgos/randomize.cc, src/tgbaalgos/randomize.hh, src/tgbaalgos/relabel.cc, src/tgbaalgos/relabel.hh, src/tgbaalgos/remfin.cc, src/tgbaalgos/remfin.hh, src/tgbaalgos/remprop.cc, src/tgbaalgos/remprop.hh, src/tgbaalgos/safety.cc, src/tgbaalgos/safety.hh, src/tgbaalgos/sbacc.cc, src/tgbaalgos/sbacc.hh, src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh, src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh, src/tgbaalgos/stripacc.cc, src/tgbaalgos/stripacc.hh, src/tgbaalgos/stutter.cc, src/tgbaalgos/stutter.hh, src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh, src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh, src/tgbatest/checkpsl.cc, src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc, wrap/python/spot_impl.i, wrap/python/tests/automata-io.ipynb, wrap/python/tests/automata.ipynb, wrap/python/tests/piperead.ipynb, wrap/python/tests/testingaut.ipynb: Rename tgba_digraph as twa_graph.
-
Alexandre Duret-Lutz authored
Now that we support any type of omega-accetpance, not just "Generalized Büchi", it is time to move away from GB and replace it by "ω", written just w in ASCII. This just change the name of the tgba class. This part has to be done by hand because the word "tgba" occurs in many contexts and a mass replacement would be wrong. This will be followed by some automatic renaming of all the derived types and more. * src/bin/autfilt.cc, src/bin/randaut.cc, src/kripke/fairkripke.hh, src/ta/tgta.cc, src/ta/tgta.hh, src/tgba/fwd.hh, src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc, src/tgba/tgba.hh, src/tgba/tgbagraph.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/are_isomorphic.cc, src/tgbaalgos/cleanacc.cc, src/tgbaalgos/dotty.cc, src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh, src/tgbaalgos/hoa.cc, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/simulation.cc, src/tgbaalgos/stutter.cc, src/tgbatest/checkpsl.cc, src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc, wrap/python/spot.py, wrap/python/spot_impl.i: Rename the tgba class into twa.
-
- 31 Mar, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
And add a cleanup_acceptance() version that copies. * src/tgbaalgos/cleanacc.cc, src/tgbaalgos/cleanacc.hh: Rename and add the second version. * src/bin/autfilt.cc, src/bin/ltlcross.cc, src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/remfin.cc: Use cleanup_acceptance_here.
-
- 25 Mar, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
Sometimes, simplifying the acceptance condition (because it refers to sets that do not appear in the automaton) cause more sets to be removed from the acceptance condition, and therefore warrant another pass to remove those sets from the automaton. * src/tgbaalgos/cleanacc.cc: Here. * src/tgbatest/hoaparse.test: Add a test case.
-
- 26 Feb, 2015 2 commits
-
-
Alexandre Duret-Lutz authored
* src/tgba/acc.cc, src/tgba/acc.hh: Move the strip() routine from acc_cond into acc_cond::mark_t, and the strip() routine from cleanacc.cc into acc_cond::acc_code. Introduce helper functions to create inf()/fin()/t()/f() at the acc_code level. * src/tgbaalgos/cleanacc.cc: Simplify, using the strip() function from acc_code. * src/tgbaalgos/mask.cc (mask_acc_sets): Use the strip() function from acc_code so that it work on non-Buchi acceptance. * src/tgbatest/maskacc.test: Add a test for the latter change. * src/tgbaalgos/sccfilter.cc, src/tgbatest/acc.cc: Adjust the use mark_t::strip().
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/cleanacc.cc, src/tgbaalgos/cleanacc.hh: New file. * src/tgbaalgos/Makefile.am: Add them. * src/tgba/acc.hh, src/tgba/tgba.hh (get_acceptance): Return a reference. * src/bin/autfilt.cc: Add a --cleanup-acceptance option. * src/tgbatest/hoaparse.test: Test it.
-