1. 21 Jan, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      typos · 2364ff81
      Alexandre Duret-Lutz authored
      * bin/autfilt.cc, spot/twaalgos/degen.cc, spot/twaalgos/dtwasat.cc,
      spot/twaalgos/remfin.cc, spot/twaalgos/sccfilter.cc: "only work" ->
      "only works".
      2364ff81
  2. 04 Dec, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      rename src/ as spot/ and use include <spot/...> · f120dd32
      Alexandre Duret-Lutz authored
      * NEWS: Mention the change.
      * src/: Rename as ...
      * spot/: ... this, adjust all headers to include <spot/...> instead of
      "...", and adjust all Makefile.am to search headers from the top-level
      directory.
      * HACKING: Add conventions about #include.
      * spot/sanity/style.test: Add a few more grep to catch cases
      that do not follow these conventions.
      * .gitignore, Makefile.am, README, bench/stutter/Makefile.am,
      bench/stutter/stutter_invariance_formulas.cc,
      bench/stutter/stutter_invariance_randomgraph.cc, configure.ac,
      debian/rules, doc/Doxyfile.in, doc/Makefile.am,
      doc/org/.dir-locals.el.in, doc/org/g++wrap.in, doc/org/init.el.in,
      doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
      doc/org/tut10.org, doc/org/tut20.org, doc/org/tut21.org,
      doc/org/tut22.org, doc/org/tut30.org, iface/ltsmin/Makefile.am,
      iface/ltsmin/kripke.test, iface/ltsmin/ltsmin.cc,
      iface/ltsmin/ltsmin.hh, iface/ltsmin/modelcheck.cc,
      wrap/python/Makefile.am, wrap/python/ajax/spotcgi.in,
      wrap/python/spot_impl.i, wrap/python/tests/ltl2tgba.py,
      wrap/python/tests/randgen.py, wrap/python/tests/run.in: Adjust.
      f120dd32
  3. 20 Oct, 2015 1 commit
  4. 14 Oct, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      scc_filter_states: also remove useless acceptance marks · cd2e5275
      Alexandre Duret-Lutz authored
      * src/twaalgos/sccfilter.hh,
      src/twaalgos/sccfilter.cc (scc_filter_states): Remove useless acceptance
      marks while preserving state-based acceptance.  Add a new argument
      to specify if all useless mark have to be removed, like for scc_filter.
      * src/twaalgos/simulation.cc: Use the new parameter.
      * src/twaalgos/postproc.cc: Likewise.  Also call do_scc_filter even
      after WDBA simplification to cleanup trivial SCCs.  Preserve state-based
      acceptance for weak automata.
      * src/tests/readsave.test: Add one test.
      * src/tests/dstar.test, src/tests/prodor.test, src/tests/remfin.test,
      src/tests/sim3.test, wrap/python/tests/automata.ipynb,
      wrap/python/tests/piperead.ipynb: Adjust expected output.
      * NEWS: Mention the change.
      cd2e5275
  5. 14 Aug, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      sccsimpl: Remove Fin sets between SCCs · 0143f0d4
      Alexandre Duret-Lutz authored
      We do not remove them in rejecting SCCs (as it might make the SCC
      accepting), but we can remove them between SCCs.
      
      Fixes #101.
      
      * src/twaalgos/sccfilter.cc: Here.
      * src/tests/sccsimpl.test: Add test case.
      * NEWS: Mention this.
      0143f0d4
  6. 30 Jun, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      scc_filter: do not remove Fin sets from rejecting SCCs · 5cb19a29
      Alexandre Duret-Lutz authored
      * src/twaalgos/sccfilter.cc (acc_filter_some, acc_filter_all): Merge
      into...
      (acc_filter_mask): ... this single parametrized class, and only
      remove sets that are only used as Inf.
      * src/twa/acc.hh: Add missing operator~.
      * src/tests/sccsimpl.test: Add test case.
      * src/tests/sccdot.test: Adjust.
      * NEWS: Mention the bug.
      5cb19a29
  7. 11 Jun, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      graph: rename num_transitions() as num_edges() · af8634d8
      Alexandre Duret-Lutz authored
      And in fact, rename most "trans*" as "edges*", because that what they
      really are.
      
      * src/bin/autfilt.cc, src/bin/ltlcross.cc, src/bin/randaut.cc,
      src/dstarparse/dra2ba.cc, src/dstarparse/dstarparse.yy,
      src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc,
      src/graph/graph.hh, src/graph/ngraph.hh, src/ltlvisit/exclusive.cc,
      src/parseaut/parseaut.yy, src/tests/complementation.cc,
      src/tests/graph.cc, src/tests/ltl2tgba.cc, src/tests/ngraph.cc,
      src/tests/twagraph.cc, src/twa/twagraph.cc, src/twa/twagraph.hh,
      src/twa/twamask.hh, src/twaalgos/are_isomorphic.cc,
      src/twaalgos/are_isomorphic.hh, src/twaalgos/canonicalize.cc,
      src/twaalgos/cleanacc.cc, src/twaalgos/complete.cc,
      src/twaalgos/compsusp.cc, src/twaalgos/cycles.cc,
      src/twaalgos/degen.cc, src/twaalgos/dot.cc, src/twaalgos/dtbasat.cc,
      src/twaalgos/dtgbacomp.cc, src/twaalgos/dtgbasat.cc,
      src/twaalgos/dupexp.cc, src/twaalgos/emptiness.cc,
      src/twaalgos/isunamb.cc, src/twaalgos/isweakscc.cc,
      src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/mask.hh,
      src/twaalgos/minimize.cc, src/twaalgos/postproc.cc,
      src/twaalgos/powerset.cc, src/twaalgos/product.cc,
      src/twaalgos/randomgraph.cc, src/twaalgos/randomize.cc,
      src/twaalgos/randomize.hh, src/twaalgos/relabel.cc,
      src/twaalgos/remfin.cc, src/twaalgos/safety.cc, src/twaalgos/sbacc.cc,
      src/twaalgos/sccfilter.cc, src/twaalgos/sepsets.cc,
      src/twaalgos/simulation.cc, src/twaalgos/stutter.cc,
      src/twaalgos/totgba.cc: Rename these.
      af8634d8
  8. 13 May, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      scc_info: determine accepting/rejecting-SCCs for any acceptance · 8c32fba8
      Alexandre Duret-Lutz authored
      * src/twaalgos/sccinfo.cc, src/twaalgos/sccinfo.hh
      (determine_unknown_acceptance): New function to call explicitly
      in case one want to know whether the accepting/rejecting status
      of all SCCs regardless of the acceptance.
      * src/twaalgos/dotty.cc src/twaalgos/sccfilter.cc,
      src/twaalgos/sccfilter.hh: Use it.
      * src/tests/unambig.test, src/tests/sccdot.test: Add more tests.
      * doc/org/oaut.org: Adjust doc for --dot=s, orange is not output
      anymore.
      8c32fba8
    • Alexandre Duret-Lutz's avatar
      allow scc_filter() and scc_filter_states() on any TωA · 07ee3d2d
      Alexandre Duret-Lutz authored
      Note however that scc_info does not provide a precise accept/reject
      characterization for SCCs when using Fin acceptance.  However whenever
      it tells that an SCC is rejecting, scc_filter_states() may safely remove
      it.
      
      * src/twaalgos/sccfilter.cc (scc_filter_states): Allow on any TωA.
      (scc_filter): Only use acceptance simplifications on TGBA.
      * src/tests/unambig.test: Add a co-Büchi test.
      07ee3d2d
  9. 22 Apr, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      rename src/tgbaalgos/ as src/twaalgos/ · de529df5
      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.
      de529df5
    • Alexandre Duret-Lutz's avatar
      rename tgba_digraph as twa_graph · e0bd0ad4
      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.
      e0bd0ad4
  10. 18 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      get rid of prop_single_acc_set() and set_single_acc_set() · b803a0ee
      Alexandre Duret-Lutz authored
      Fixes #64.
      
      * src/tgba/tgba.hh: Here.
      * src/tgbaalgos/complete.cc, src/tgbaalgos/degen.cc,
      src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/mask.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/remfin.cc,
      src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc,
      src/tgbaalgos/stutter.cc: Adjust.
      b803a0ee
  11. 03 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      sccinfo: introduce is_rejecting() · ebe4ffc5
      Alexandre Duret-Lutz authored
      Because scc_info does not perform a full emptiness check, it is not
      always able to tell whether an SCC is accepting if the acceptance
      condition use Fin primitives.  This introduce is_rejecting_scc() in
      addition to to is_accepting_scc().  Only one of them may be true, but
      they can both be false if scc_info has no idea whether the SCC is
      accepting.
      
      * src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh: Implement
      is_rejecting_scc().
      * src/bin/ltlcross.cc, src/tgba/acc.cc, src/tgba/acc.hh,
      src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/isweakscc.cc,
      src/tgbaalgos/remfin.cc, src/tgbaalgos/safety.cc,
      src/tgbaalgos/sccfilter.cc: Use it.
      * src/tgbaalgos/dotty.cc: Use is_rejecting_scc() and is_accepting_scc()
      to color SCCs.
      * doc/org/oaut.org: Document the colors used.
      * src/tgbatest/neverclaimread.test, src/tgbatest/readsave.test: Adjust
      tests.
      * src/tgbatest/sccdot.test: New test case.
      * src/tgbatest/Makefile.am: Add it.
      ebe4ffc5
  12. 28 Feb, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      add a stutter-invariant property to automata · 1f0bb428
      Alexandre Duret-Lutz authored
      ... and show it in the HOA output.  Fixes #60.
      
      * src/tgba/tgba.hh: Add is_stutter_invariant().
      * src/tgbaalgos/hoa.cc: Print stutter-invariant
      and inherently-weak.
      * src/tgbaalgos/ltl2tgba_fm.cc: Set both.
      * src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/complete.cc,
      src/tgbaalgos/degen.cc, src/tgbaalgos/dtgbacomp.cc,
      src/tgbaalgos/mask.cc, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/remfin.cc, src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/simulation.cc, src/tgbaalgos/stutter.cc,
      src/tgbatest/hoaparse.test, src/tgbatest/ltldo.test,
      src/tgbatest/monitor.test, src/tgbatest/randomize.test,
      src/tgbatest/remfin.test, src/tgbatest/sbacc.test: Adjust.
      1f0bb428
  13. 26 Feb, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      Prefix many algorithms with runtime_error for unexpected acceptance · f0b1b943
      Alexandre Duret-Lutz authored
      * src/tgba/tgbagraph.cc (merge_transitions): Disable acceptance
      merging if Fin acceptance is used.
      * src/tgbaalgos/degen.cc, src/tgbaalgos/dtbasat.cc,
      src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/isweakscc.cc,
      src/tgbaalgos/lbtt.cc, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/neverclaim.cc, src/tgbaalgos/safety.cc,
      src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc: Throw an
      exception if an unsupported type of acceptance is received.
      f0b1b943
    • Alexandre Duret-Lutz's avatar
      acc: refactor strip() routines · 5b2c7b55
      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().
      5b2c7b55
  14. 23 Feb, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      rename set_acceptance_conditions as set_generalized_buchi · 76c676db
      Alexandre Duret-Lutz authored
      * src/hoaparse/hoaparse.yy, src/tgba/tgbagraph.hh,
      src/tgbaalgos/compsusp.cc, src/tgbaalgos/dtgbasat.cc,
      src/tgbaalgos/mask.cc, src/tgbaalgos/randomgraph.cc,
      src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc,
      src/tgbaalgos/stripacc.cc, src/tgba/tgba.hh: Here.
      76c676db
  15. 03 Jan, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      tgba_digraph: force selection of properties kept on copy · 87c2b291
      Alexandre Duret-Lutz authored
      * src/tgba/tgba.hh: Declare a prop_set to specify the types.
      * src/tgba/tgbagraph.hh: Use prop_set for all copy constructors.
      * iface/ltsmin/ltsmin.cc, src/bin/autfilt.cc, src/bin/randaut.cc,
      src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/closure.cc,
      src/tgbaalgos/complete.cc, src/tgbaalgos/degen.cc,
      src/tgbaalgos/dotty.cc, src/tgbaalgos/dtgbacomp.cc,
      src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
      src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc,
      src/tgbaalgos/stutterize.cc, src/tgbatest/checkpsl.cc,
      src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc,
      wrap/python/spot.i,src/graphtest/tgbagraph.test: Adjust all uses.
      87c2b291
  16. 06 Oct, 2014 1 commit
    • 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
  17. 20 Aug, 2014 1 commit
  18. 15 Aug, 2014 2 commits
    • Alexandre Duret-Lutz's avatar
      tgba: move boolean properties from tgba_digraph to tgba · b43f75e9
      Alexandre Duret-Lutz authored
      * src/tgba/tgbagraph.hh: Remove the set_bprop/get_bprop interface.
      * src/tgba/tgba.cc, src/tgba/tgba.hh: Add a new interface for
      setting/querying/copying the following properties: single_acc_set,
      state_based_acc, inherently_weak, deterministic.
      * src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
      src/neverparse/neverclaimparse.yy, src/saba/sabacomplementtgba.cc,
      src/tgba/tgbagraph.cc, src/tgbaalgos/degen.cc, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/isdet.cc, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/postproc.cc, src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/simulation.cc, src/tgbatest/degenlskip.test,
      src/tgbatest/ltl2tgba.cc: Adjust to the new interface, or use
      it to bypass some useless work.
      b43f75e9
    • Alexandre Duret-Lutz's avatar
      Handle all automata through shared_ptr. (monstro patch) · 51151ab2
      Alexandre Duret-Lutz authored
      A type such as 'const tgba_digraph*' and 'tgba_digraph*' are replaced
      by 'const_tgba_digraph_ptr' and 'tgba_digraph_ptr'.  Additionally 'new
      tgba_digraph(...)' is replaced by 'make_tgba_digraph(...)'.
      
      This convention is followed by all automata types. Those smart
      pointers should normally be passed by const reference as input of
      function to avoid the atomic increments/decrements, but I probably
      missed a few, as this huge patch took me nearly 12h.
      
      * src/kripke/fwd.hh, src/tgba/fwd.hh: New files.
      * src/kripke/Makefile.am, src/tgba/Makefile.am: Adjust.
      * iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc,
      src/bin/common_output.hh, src/bin/dstar2tgba.cc,
      src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc,
      src/bin/ltlfilt.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/kripke/fairkripke.hh, src/kripke/kripke.hh,
      src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh,
      src/kripkeparse/kripkeparse.yy, src/kripkeparse/public.hh,
      src/kripketest/parse_print_test.cc, src/ltlvisit/apcollect.cc,
      src/ltlvisit/apcollect.hh, src/ltlvisit/contain.cc,
      src/ltlvisit/contain.hh, src/neverparse/neverclaimparse.yy,
      src/neverparse/public.hh, src/priv/accmap.hh,
      src/priv/countstates.cc, src/priv/countstates.hh, src/saba/saba.hh,
      src/saba/sabacomplementtgba.cc, src/saba/sabacomplementtgba.hh,
      src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh,
      src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh,
      src/sabatest/sabacomplementtgba.cc, src/ta/ta.hh,
      src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc,
      src/ta/taproduct.hh, 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/dotty.hh,
      src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh,
      src/taalgos/minimize.cc, src/taalgos/minimize.hh,
      src/taalgos/reachiter.cc, src/taalgos/reachiter.hh,
      src/taalgos/statessetbuilder.cc, src/taalgos/statessetbuilder.hh,
      src/taalgos/stats.cc, src/taalgos/stats.hh, src/taalgos/tgba2ta.cc,
      src/taalgos/tgba2ta.hh, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
      src/tgba/formula2bdd.hh, src/tgba/futurecondcol.cc,
      src/tgba/futurecondcol.hh, src/tgba/taatgba.hh, src/tgba/tgba.cc,
      src/tgba/tgba.hh, src/tgba/tgbagraph.hh,
      src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.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/tgba/tgbascc.cc,
      src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh,
      src/tgba/wdbacomp.cc, src/tgba/wdbacomp.hh,
      src/tgbaalgos/bfssteps.cc, src/tgbaalgos/bfssteps.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/dotty.hh, src/tgbaalgos/dottydec.cc,
      src/tgbaalgos/dottydec.hh, 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/gtec/gtec.cc,
      src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/status.cc,
      src/tgbaalgos/gtec/status.hh, src/tgbaalgos/gv04.cc,
      src/tgbaalgos/gv04.hh, src/tgbaalgos/isdet.cc,
      src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.cc,
      src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh,
      src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh,
      src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.cc,
      src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.cc,
      src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.cc,
      src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.cc,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.cc,
      src/tgbaalgos/reducerun.hh, src/tgbaalgos/replayrun.cc,
      src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.cc,
      src/tgbaalgos/rundotdec.hh, src/tgbaalgos/safety.cc,
      src/tgbaalgos/safety.hh, src/tgbaalgos/save.cc,
      src/tgbaalgos/save.hh, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh,
      src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh,
      src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh,
      src/tgbaalgos/se05.cc, src/tgbaalgos/se05.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/tau03.cc, src/tgbaalgos/tau03.hh,
      src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
      src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh,
      src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
      src/tgbatest/complementation.cc, src/tgbatest/explprod.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
      src/tgbatest/maskacc.cc, src/tgbatest/powerset.cc,
      src/tgbatest/randtgba.cc, src/tgbatest/taatgba.cc,
      src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc,
      wrap/python/ajax/spot.in, wrap/python/spot.i,
      wrap/python/tests/interdep.py: Use shared pointers for automata.
      51151ab2
  19. 13 Aug, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      Simplify copying of atomic propositions in new tgba_digraph. · 10e5c623
      Alexandre Duret-Lutz authored
      * src/tgba/bdddict.cc, src/tgba/bdddict.hh
      (register_all_propositions_of): New method.
      * src/tgba/tgbagraph.hh (copy_ap_of): New method.
      * src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
      src/dstarparse/nsa2tgba.cc, src/tgbaalgos/degen.cc,
      src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc,
      src/tgbaalgos/dupexp.cc, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc,
      src/tgbaalgos/stripacc.cc: Simplify using copy_ap_of.
      10e5c623
  20. 12 Aug, 2014 3 commits
    • Alexandre Duret-Lutz's avatar
      remove the sba interface · e9893586
      Alexandre Duret-Lutz authored
      * src/tgba/tgbagraph.hh: Automatize the setting of the SingleAccSet
      property.
      * src/tgbaalgos/minimize.cc: Do not bother setting SingleAccSet.
      * src/tgba/sba.hh: Delete.
      * src/tgba/Makefile.am, wrap/python/spot.i: Adjust.
      * src/taalgos/tgba2ta.cc: Do not include sba.hh.
      * src/neverparse/neverclaimparse.yy: Set the SBA property on the output.
      * src/tgbaalgos/lbtt.cc (lbtt_read_gba): Set the StateBasedAcc property
      on output.
      * src/tgbaalgos/dotty.cc, src/tgbaalgos/neverclaim.cc: Do not rely on
      the sba interface.
      * src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
      src/tgbaalgos/simulation.cc, src/tgbaalgos/sccfilter.cc: Set
      tgba_digraph::StateBasedAcc as appropriate.
      * src/tgbatest/ltl2tgba.cc: Add extra assert.
      e9893586
    • Alexandre Duret-Lutz's avatar
      remove tgba_explicit variants and the old scc_filter · e6ea90e3
      Alexandre Duret-Lutz authored
      * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Delete.
      * src/tgba/Makefile.am: Adjust.
      * src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh:
      Delete these obsoleted algorithms.
      * src/tgbaalgos/Makefile.am: Adjust.
      * src/tgbatest/explicit.cc, src/tgbatest/explicit.test,
      src/tgbatest/explicit2.cc, src/tgbatest/explicit2.test,
      src/tgbatest/explicit3.cc, src/tgbatest/explicit3.test:
      Delete.
      * src/tgbatest/Makefile.am: Adjust.
      * src/bin/ltl2tgba.cc, src/priv/countstates.cc,
      src/tgbaalgos/isweakscc.cc, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/minimize.hh, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/powerset.hh, src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/sccfilter.hh, src/tgbaalgos/simulation.cc,
      src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/powerset.cc, src/tgbatest/tgbaread.cc,
      src/tgbatest/tripprod.cc, wrap/python/ajax/spot.in,
      wrap/python/spot.i: Remove all remaining references to
      tgba_explicit.
      e6ea90e3
    • Alexandre Duret-Lutz's avatar
      replace sba_explicit_* by tgba_digraph, and use tgba_digraph is postproc · 6c9d5e4b
      Alexandre Duret-Lutz authored
      This is a huge patch.  tgba_digraph are equiped with some boolean
      properties that can be used to indicate whether they represent SBA
      (and will carry more informations later).  All algorithms that produce
      or use sba_explicit_* automata are changed to use tgba_digraph.
      postproc has been rewritten using only tgba_digraph, and this required
      changing the return types of many algorithms from tgba* to
      tgba_digraph*.
      
      * src/bin/dstar2tgba.cc, src/bin/ltlfilt.cc, src/dstarparse/dra2ba.cc,
      src/dstarparse/dstar2tgba.cc, src/dstarparse/nra2nba.cc,
      src/dstarparse/nsa2tgba.cc, src/dstarparse/public.hh,
      src/tgba/tgbagraph.hh, src/tgba/tgbasafracomplement.cc,
      src/tgbaalgos/compsusp.cc, src/tgbaalgos/compsusp.hh,
      src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh,
      src/tgbaalgos/dotty.cc, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/minimize.hh, src/tgbaalgos/postproc.cc,
      src/tgbaalgos/postproc.hh, src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/sccinfo.cc, src/tgbaalgos/stripacc.cc,
      src/tgbaalgos/stripacc.hh, src/tgbaalgos/translate.cc,
      src/tgbaalgos/translate.hh, src/tgbatest/ltl2tgba.cc,
      wrap/python/spot.i: Update.
      6c9d5e4b
  21. 11 Aug, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      compsusp: Use new implem of scc_filter to remove suspended variables · 637aeff2
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh: Rewrite all
      composable filters in a way that allow arguments to be passed.
      (scc_filter_susp): New function.
      * src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh (scc_ap_support):
      New method.
      * src/tgbaalgos/compsusp.cc: Adjust to use tgba_digraph, and
      call the new scc_filter_susp().
      637aeff2
  22. 31 Jul, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      Use emplace() for associative containers. · fd5fbda4
      Alexandre Duret-Lutz authored
      * HACKING: Adjust requirements.  g++4.8 is now OK
      for all our targets.
      * iface/dve2/dve2.cc, src/dstarparse/dstarparse.yy
      src/dstarparse/nsa2tgba.cc, src/graph/ngraph.hh,
      src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, src/ltlast/bunop.cc,
      src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlvisit/mark.cc,
      src/ltlvisit/relabel.cc, src/taalgos/emptinessta.cc,
      src/taalgos/tgba2ta.cc, src/tgba/tgbaexplicit.hh, src/tgba/tgbagraph.hh,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbatba.cc,
      src/tgbaalgos/cycles.cc, src/tgbaalgos/degen.cc,
      src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc,
      src/tgbaalgos/emptiness.cc, src/tgbaalgos/gtec/gtec.cc,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/magic.cc,
      src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/reachiter.cc,
      src/tgbaalgos/scc.cc, src/tgbaalgos/sccfilter.cc, src/tgbaalgos/se05.cc,
      src/tgbaalgos/simulation.cc, src/tgbaalgos/tau03.cc,
      src/tgbaalgos/tau03opt.cc, src/tgbaalgos/weight.cc: Use emplace()
      instead of insert(make_pair(...)) or insert(...::value_type(...)).
      fd5fbda4
  23. 10 Jul, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      tgbadigraph: delegate useful graph methods · 1a93166d
      Alexandre Duret-Lutz authored
      * src/tgba/tgbagraph.hh (new_state, new_states, new_transitions, out,
      trans_data): Delegate these useful graph methods so we do not have to
      call get_graph().
      * src/graphtest/tgbagraph.cc, src/tgbaalgos/dtbasat.cc,
      src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dupexp.cc,
      src/tgbaalgos/emptiness.cc, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc,
      src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/sccinfo.cc,src/tgbaalgos/simulation.cc: Simplify.
      1a93166d
  24. 22 Jun, 2014 1 commit
  25. 20 Jun, 2014 3 commits
    • Alexandre Duret-Lutz's avatar
      sccfilter: improve the new version to simplify acceptance sets · af6cb049
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh: Implement
      the acc_filter_simplify filter, and generalize composition to
      be n-ary.
      * src/tgbaalgos/sccfilter.cc (used_acc): New method.
      af6cb049
    • Alexandre Duret-Lutz's avatar
      sccfilter: implement a new version of tgba_digraph · 13673a14
      Alexandre Duret-Lutz authored
      The new version currently supports removal of useless state as well as
      removal of acceptance sets from non-accepting SCCs (the two versions).
      It does not yet support simplifation of acceptance sets and removal of
      suspendable formulae.  However the design, using filters that are
      composed before being applied, should make it easier to implement.
      
      * src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh: Implement
      the new scc_filter and supporting classes.
      * src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Use it.
      The simulation now always return a tgba_digraph.
      * src/tgbatest/sim.test: Adjust.
      13673a14
    • Alexandre Duret-Lutz's avatar
      implement scc_filter_states for tgba_digraph · 9909699c
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/sccfilter.hh (scc_filter_states): New overload taking
      a tgba_digraph and some scc_info.
      9909699c
  26. 12 Feb, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      Replace << "c" by << 'c', and check for it in style.sh · ba5aff24
      Alexandre Duret-Lutz authored
      * src/sanity/style.test: Add a test.
      * iface/dve2/dve2.cc, iface/dve2/dve2check.cc, src/bin/common_output.cc,
      src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/bin/ltlcross.cc,
      src/dstarparse/dra2ba.cc, src/dstarparse/fmterror.cc,
      src/dstarparse/nsa2tgba.cc, src/kripke/kripkeprint.cc,
      src/kripkeparse/fmterror.cc, src/ltlast/atomic_prop.cc,
      src/ltlast/bunop.cc, src/ltltest/ltlrel.cc, src/ltltest/reduc.cc,
      src/ltltest/syntimpl.cc, src/ltlvisit/dotty.cc, src/ltlvisit/lbt.cc,
      src/ltlvisit/randomltl.cc, src/ltlvisit/relabel.cc,
      src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc, src/misc/bitvect.cc,
      src/misc/optionmap.cc, src/misc/timer.cc, src/neverparse/fmterror.cc,
      src/priv/freelist.cc, src/saba/sabacomplementtgba.cc,
      src/sabaalgos/sabadotty.cc, src/taalgos/dotty.cc,
      src/taalgos/minimize.cc, src/tgba/bdddict.cc, src/tgba/bddprint.cc,
      src/tgba/futurecondcol.cc, src/tgba/taatgba.hh,
      src/tgba/tgbakvcomplement.cc, src/tgba/tgbasafracomplement.cc,
      src/tgbaalgos/compsusp.cc, src/tgbaalgos/cycles.cc,
      src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc,
      src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gv04.cc,
      src/tgbaalgos/lbtt.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/powerset.cc, src/tgbaalgos/replayrun.cc,
      src/tgbaalgos/save.cc, src/tgbaalgos/scc.cc, src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/weight.cc, src/tgbaalgos/word.cc,
      src/tgbaparse/fmterror.cc, src/tgbatest/bitvect.cc,
      src/tgbatest/complementation.cc, src/tgbatest/intvcmp2.cc,
      src/tgbatest/intvcomp.cc, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/randtgba.cc: Replace << "c" by << 'c' when
      appropriate.
      ba5aff24
  27. 19 Jun, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix "BDD Error" in scc_filter(). · fc5d4e1a
      Alexandre Duret-Lutz authored
      If all the acceptance set of an SCC but the first one were useless, the
      scc_filter() algorithm could abort with a BDD error because of a bug in
      the logic.
      
      * src/tgbaalgos/sccfilter.cc (scc_filter): Fix.
      * src/tgbatest/sccsimpl.test: Add a test case supplied by Étienne
      Renault.
      fc5d4e1a
  28. 12 May, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Introduce scc_filter_states(). · 6b5b002f
      Alexandre Duret-Lutz authored
      The main motivation is the upcoming patch that introduces
      simulation_sba() and requires this function.
      
      * src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccfilter.cc: Implement it.
      * src/tgbaalgos/postproc.cc: Use it for monitors, because we do not
      care about acceptance conditions.
      * NEWS: Mention it.
      6b5b002f
  29. 27 Apr, 2013 2 commits
  30. 09 Apr, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      sccfilter: ignore more acceptance conditions · c46891ed
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/sccfilter.cc: Compute useless variable SCC-wise, then
      renumber the useful variables so that they can be shared between SCCs.
      * src/tgbatest/sccsimpl.test, src/tgbatest/ltl2ta.test: Adjust test
      cases.
      c46891ed
  31. 12 Oct, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Upgrade GPL v2+ to GPL v3+. · 1551c5d9
      Alexandre Duret-Lutz authored
      * NEWS: Mention this.
      * COPYING: Replace by GPL v3.
      * src/sanity/style.test: Check files with the wrong license,
      in case we forgot to update it during a merge.
      * Makefile.am, bench/Makefile.am, bench/emptchk/Makefile.am,
      bench/emptchk/defs.in, bench/emptchk/ltl-human.sh,
      bench/emptchk/ltl-random.sh, bench/emptchk/pml-clserv.sh,
      bench/emptchk/pml-eeaean.sh, bench/emptchk/pml2tgba.pl,
      bench/ltl2tgba/big, bench/ltl2tgba/defs.in, bench/ltl2tgba/known,
      bench/ltl2tgba/lbtt2csv.pl, bench/ltl2tgba/ltl2baw.in,
      bench/ltl2tgba/parseout.pl, bench/ltl2tgba/small,
      bench/ltlclasses/Makefile.am, bench/ltlclasses/defs.in,
      bench/ltlclasses/run, bench/ltlcounter/Makefile.am,
      bench/ltlcounter/defs.in, bench/ltlcounter/run,
      bench/scc-stats/Makefile.am, bench/scc-stats/stats.cc,
      bench/split-product/Makefile.am, bench/split-product/cutscc.cc,
      bench/split-product/pml2tgba.pl, bench/wdba/Makefile.am,
      bench/wdba/defs.in, bench/wdba/run, configure.ac, doc/Makefile.am,
      doc/dot.in, doc/tl/Makefile.am, iface/Makefile.am,
      iface/dve2/Makefile.am, iface/dve2/defs.in, iface/dve2/dve2.cc,
      iface/dve2/dve2.hh, iface/dve2/dve2check.cc,
      iface/dve2/dve2check.test, iface/dve2/finite.test,
      iface/dve2/kripke.test, iface/gspn/Makefile.am, iface/gspn/common.cc,
      iface/gspn/common.hh, iface/gspn/dcswave.test,
      iface/gspn/dcswaveeltl.test, iface/gspn/dcswavefm.test,
      iface/gspn/dcswaveltl.test, iface/gspn/dottygspn.cc,
      iface/gspn/dottyssp.cc, iface/gspn/gspn.cc, iface/gspn/gspn.hh,
      iface/gspn/ltlgspn.cc, iface/gspn/simple.test, iface/gspn/ssp.cc,
      iface/gspn/ssp.hh, iface/gspn/udcsefm.test, iface/gspn/udcseltl.test,
      iface/gspn/udcsfm.test, iface/gspn/udcsltl.test, src/Makefile.am,
      src/bin/Makefile.am, src/bin/common_cout.cc, src/bin/common_cout.hh,
      src/bin/common_finput.cc, src/bin/common_finput.hh,
      src/bin/common_output.cc, src/bin/common_output.hh,
      src/bin/common_post.cc, src/bin/common_post.hh, src/bin/common_r.cc,
      src/bin/common_r.hh, src/bin/common_range.cc, src/bin/common_range.hh,
      src/bin/common_setup.cc, src/bin/common_setup.hh,
      src/bin/common_sys.hh, src/bin/genltl.cc, src/bin/ltl2tgba.cc,
      src/bin/ltl2tgta.cc, src/bin/ltlfilt.cc, src/bin/man/Makefile.am,
      src/bin/randltl.cc, src/eltlparse/Makefile.am,
      src/eltlparse/eltlparse.yy, src/eltlparse/eltlscan.ll,
      src/eltlparse/fmterror.cc, src/eltlparse/parsedecl.hh,
      src/eltlparse/public.hh, src/eltltest/Makefile.am,
      src/eltltest/acc.cc, src/eltltest/acc.test, src/eltltest/defs.in,
      src/eltltest/nfa.cc, src/eltltest/nfa.test, src/evtgba/Makefile.am,
      src/evtgba/evtgba.cc, src/evtgba/evtgba.hh, src/evtgba/evtgbaiter.hh,
      src/evtgba/explicit.cc, src/evtgba/explicit.hh, src/evtgba/product.cc,
      src/evtgba/product.hh, src/evtgba/symbol.cc, src/evtgba/symbol.hh,
      src/evtgbaalgos/Makefile.am, src/evtgbaalgos/dotty.cc,
      src/evtgbaalgos/dotty.hh, src/evtgbaalgos/reachiter.cc,
      src/evtgbaalgos/reachiter.hh, src/evtgbaalgos/save.cc,
      src/evtgbaalgos/save.hh, src/evtgbaalgos/tgba2evtgba.cc,
      src/evtgbaalgos/tgba2evtgba.hh, src/evtgbaparse/Makefile.am,
      src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll,
      src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh,
      src/evtgbaparse/public.hh, src/evtgbatest/Makefile.am,
      src/evtgbatest/defs.in, src/evtgbatest/explicit.cc,
      src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.cc,
      src/evtgbatest/ltl2evtgba.test, src/evtgbatest/product.cc,
      src/evtgbatest/product.test, src/evtgbatest/readsave.cc,
      src/evtgbatest/readsave.test, src/kripke/Makefile.am,
      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/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh,
      src/kripkeparse/Makefile.am, src/kripkeparse/fmterror.cc,
      src/kripkeparse/kripkeparse.yy, src/kripkeparse/kripkescan.ll,
      src/kripkeparse/parsedecl.hh, src/kripkeparse/public.hh,
      src/kripkeparse/scankripke.ll, src/kripketest/Makefile.am,
      src/kripketest/bad_parsing.test, src/kripketest/defs.in,
      src/kripketest/kripke.test, src/kripketest/parse_print_test.cc,
      src/ltlast/Makefile.am, src/ltlast/allnodes.hh,
      src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
      src/ltlast/automatop.cc, src/ltlast/automatop.hh, src/ltlast/binop.cc,
      src/ltlast/binop.hh, src/ltlast/bunop.cc, src/ltlast/bunop.hh,
      src/ltlast/constant.cc, src/ltlast/constant.hh, src/ltlast/formula.cc,
      src/ltlast/formula.hh, src/ltlast/formula_tree.cc,
      src/ltlast/formula_tree.hh, src/ltlast/multop.cc,
      src/ltlast/multop.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh,
      src/ltlast/predecl.hh, src/ltlast/refformula.cc,
      src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh,
      src/ltlast/visitor.hh, src/ltlenv/Makefile.am, src/ltlenv/declenv.cc,
      src/ltlenv/declenv.hh, src/ltlenv/defaultenv.cc,
      src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh,
      src/ltlparse/Makefile.am, src/ltlparse/fmterror.cc,
      src/ltlparse/ltlfile.cc, src/ltlparse/ltlfile.hh,
      src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll,
      src/ltlparse/parsedecl.hh, src/ltlparse/public.hh,
      src/ltltest/Makefile.am, src/ltltest/consterm.cc,
      src/ltltest/consterm.test, src/ltltest/defs.in, src/ltltest/equals.cc,
      src/ltltest/equals.test, src/ltltest/kind.cc, src/ltltest/kind.test,
      src/ltltest/length.cc, src/ltltest/length.test,
      src/ltltest/lunabbrev.test, src/ltltest/nenoform.test,
      src/ltltest/parse.test, src/ltltest/parseerr.test,
      src/ltltest/readltl.cc, src/ltltest/reduc.cc, src/ltltest/reduc.test,
      src/ltltest/reduccmp.test, src/ltltest/reducpsl.test,
      src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test,
      src/ltltest/tostring.cc, src/ltltest/tostring.test,
      src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test,
      src/ltltest/utf8.test, src/ltltest/uwrm.test,
      src/ltlvisit/Makefile.am, src/ltlvisit/apcollect.cc,
      src/ltlvisit/apcollect.hh, src/ltlvisit/clone.cc,
      src/ltlvisit/clone.hh, src/ltlvisit/contain.cc,
      src/ltlvisit/contain.hh, src/ltlvisit/destroy.cc,
      src/ltlvisit/destroy.hh, src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
      src/ltlvisit/dump.cc, src/ltlvisit/dump.hh, src/ltlvisit/lbt.cc,
      src/ltlvisit/lbt.hh, src/ltlvisit/length.cc, src/ltlvisit/length.hh,
      src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh,
      src/ltlvisit/mark.cc, src/ltlvisit/mark.hh, src/ltlvisit/nenoform.cc,
      src/ltlvisit/nenoform.hh, src/ltlvisit/postfix.cc,
      src/ltlvisit/postfix.hh, src/ltlvisit/randomltl.cc,
      src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.cc,
      src/ltlvisit/reduce.hh, src/ltlvisit/relabel.cc,
      src/ltlvisit/relabel.hh, src/ltlvisit/simpfg.cc,
      src/ltlvisit/simpfg.hh, src/ltlvisit/simplify.cc,
      src/ltlvisit/simplify.hh, src/ltlvisit/snf.cc, src/ltlvisit/snf.hh,
      src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
      src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
      src/ltlvisit/wmunabbrev.cc, src/ltlvisit/wmunabbrev.hh,
      src/misc/Makefile.am, src/misc/acccompl.cc, src/misc/acccompl.hh,
      src/misc/accconv.cc, src/misc/accconv.hh, src/misc/bareword.cc,
      src/misc/bareword.hh, src/misc/bddalloc.cc, src/misc/bddalloc.hh,
      src/misc/bddlt.hh, src/misc/bddop.cc, src/misc/bddop.hh,
      src/misc/casts.hh, src/misc/escape.cc, src/misc/escape.hh,
      src/misc/fixpool.hh, src/misc/freelist.cc, src/misc/freelist.hh,
      src/misc/hash.hh, src/misc/hashfunc.hh, src/misc/intvcmp2.cc,
      src/misc/intvcmp2.hh, src/misc/intvcomp.cc, src/misc/intvcomp.hh,
      src/misc/ltstr.hh, src/misc/memusage.cc, src/misc/memusage.hh,
      src/misc/minato.cc, src/misc/minato.hh, src/misc/modgray.cc,
      src/misc/modgray.hh, src/misc/mspool.hh, src/misc/optionmap.cc,
      src/misc/optionmap.hh, src/misc/random.cc, src/misc/random.hh,
      src/misc/timer.cc, src/misc/timer.hh, src/misc/unique_ptr.hh,
      src/misc/version.cc, src/misc/version.hh, src/neverparse/Makefile.am,
      src/neverparse/fmterror.cc, src/neverparse/neverclaimparse.yy,
      src/neverparse/neverclaimscan.ll, src/neverparse/parsedecl.hh,
      src/neverparse/public.hh, src/saba/Makefile.am,
      src/saba/explicitstateconjunction.cc,
      src/saba/explicitstateconjunction.hh, src/saba/saba.cc,
      src/saba/saba.hh, src/saba/sabacomplementtgba.cc,
      src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh,
      src/saba/sabasucciter.hh, src/sabaalgos/Makefile.am,
      src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh,
      src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh,
      src/sabatest/Makefile.am, src/sabatest/defs.in,
      src/sabatest/sabacomplementtgba.cc, src/sanity/Makefile.am,
      src/sanity/readme.test, src/sanity/style.test, src/ta/Makefile.am,
      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/Makefile.am, src/taalgos/dotty.cc, src/taalgos/dotty.hh,
      src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh,
      src/taalgos/minimize.cc, src/taalgos/minimize.hh,
      src/taalgos/reachiter.cc, src/taalgos/reachiter.hh,
      src/taalgos/statessetbuilder.cc, src/taalgos/statessetbuilder.hh,
      src/taalgos/stats.cc, src/taalgos/stats.hh, src/taalgos/tgba2ta.cc,
      src/taalgos/tgba2ta.hh, src/tgba/Makefile.am, src/tgba/bdddict.cc,
      src/tgba/bdddict.hh, src/tgba/bddprint.cc, src/tgba/bddprint.hh,
      src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh,
      src/tgba/futurecondcol.cc, src/tgba/futurecondcol.hh,
      src/tgba/public.hh, src/tgba/sba.hh, src/tgba/state.hh,
      src/tgba/statebdd.cc, src/tgba/statebdd.hh, src/tgba/succiter.hh,
      src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh,
      src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc,
      src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc,
      src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc,
      src/tgba/tgbabddconcretefactory.hh,
      src/tgba/tgbabddconcreteproduct.cc,
      src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc,
      src/tgba/tgbabddcoredata.hh, src/tgba/tgbabddfactory.hh,
      src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
      src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.hh,
      src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
      src/tgba/tgbascc.cc, src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc,
      src/tgba/tgbasgba.hh, src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
      src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc,
      src/tgba/wdbacomp.hh, src/tgbaalgos/Makefile.am,
      src/tgbaalgos/bfssteps.cc, src/tgbaalgos/bfssteps.hh,
      src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh,
      src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh,
      src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh,
      src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh,
      src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh,
      src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
      src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/eltl2tgba_lacim.hh,
      src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh,
      src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/gtec/Makefile.am,
      src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
      src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
      src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh,
      src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
      src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh,
      src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh, src/tgbaalgos/isdet.cc,
      src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.cc,
      src/tgbaalgos/isweakscc.hh, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.cc,
      src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/magic.cc,
      src/tgbaalgos/magic.hh, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/minimize.hh, src/tgbaalgos/ndfs_result.hxx,
      src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
      src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh,
      src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh,
      src/tgbaalgos/projrun.cc, src/tgbaalgos/projrun.hh,
      src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh,
      src/tgbaalgos/reachiter.cc, src/tgbaalgos/reachiter.hh,
      src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh,
      src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh,
      src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh,
      src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh,
      src/tgbaalgos/safety.cc, src/tgbaalgos/safety.hh,
      src/tgbaalgos/save.cc, src/tgbaalgos/save.hh, src/tgbaalgos/scc.cc,
      src/tgbaalgos/scc.hh, src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/sccfilter.hh, src/tgbaalgos/se05.cc,
      src/tgbaalgos/se05.hh, src/tgbaalgos/simulation.cc,
      src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc,
      src/tgbaalgos/stats.hh, src/tgbaalgos/tau03.cc,
      src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03opt.cc,
      src/tgbaalgos/tau03opt.hh, src/tgbaalgos/weight.cc,
      src/tgbaalgos/weight.hh, src/tgbaparse/Makefile.am,
      src/tgbaparse/fmterror.cc, src/tgbaparse/parsedecl.hh,
      src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
      src/tgbaparse/tgbascan.ll, src/tgbatest/Makefile.am,
      src/tgbatest/babiak.test, src/tgbatest/bddprod.test,
      src/tgbatest/complementation.cc, src/tgbatest/complementation.test,
      src/tgbatest/cycles.test, src/tgbatest/defs.in,
      src/tgbatest/degendet.test, src/tgbatest/degenid.test,
      src/tgbatest/dfs.test, src/tgbatest/dupexp.test,
      src/tgbatest/eltl2tgba.test, src/tgbatest/emptchk.test,
      src/tgbatest/emptchke.test, src/tgbatest/emptchkr.test,
      src/tgbatest/explicit.cc, src/tgbatest/explicit.test,
      src/tgbatest/explicit2.cc, src/tgbatest/explicit2.test,
      src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
      src/tgbatest/explpro4.test, src/tgbatest/explprod.cc,
      src/tgbatest/explprod.test, src/tgbatest/intvcmp2.cc,
      src/tgbatest/intvcomp.cc, src/tgbatest/intvcomp.test,
      src/tgbatest/kv.test, src/tgbatest/ltl2neverclaim.test,
      src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/ltl2tgba.test, src/tgbatest/ltlcounter.test,
      src/tgbatest/ltlprod.cc, src/tgbatest/ltlprod.test,
      src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test,
      src/tgbatest/neverclaimread.test, src/tgbatest/nondet.test,
      src/tgbatest/obligation.test, src/tgbatest/powerset.cc,
      src/tgbatest/randpsl.test, src/tgbatest/randtgba.cc,
      src/tgbatest/randtgba.test, src/tgbatest/readsave.test,
      src/tgbatest/renault.test, src/tgbatest/scc.test,
      src/tgbatest/sccsimpl.test, src/tgbatest/spotlbtt.test,
      src/tgbatest/spotlbtt2.test, src/tgbatest/taatgba.cc,
      src/tgbatest/taatgba.test, src/tgbatest/tgbaread.cc,
      src/tgbatest/tgbaread.test, src/tgbatest/tripprod.cc,
      src/tgbatest/tripprod.test, src/tgbatest/wdba.test,
      src/tgbatest/wdba2.test, wrap/Makefile.am, wrap/python/Makefile.am,
      wrap/python/ajax/Makefile.am, wrap/python/ajax/spot.in,
      wrap/python/buddy.i, wrap/python/spot.i,
      wrap/python/tests/Makefile.am, wrap/python/tests/alarm.py,
      wrap/python/tests/bddnqueen.py, wrap/python/tests/implies.py,
      wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py,
      wrap/python/tests/ltl2tgba.test, wrap/python/tests/ltlparse.py,
      wrap/python/tests/ltlsimple.py, wrap/python/tests/minato.py,
      wrap/python/tests/modgray.py, wrap/python/tests/optionmap.py,
      wrap/python/tests/parsetgba.py, wrap/python/tests/run.in,
      wrap/python/tests/setxor.py: Update licence version, and replace the
      FSF address by a URL.
      1551c5d9