1. 16 Jul, 2020 1 commit
    • Alexandre Duret-Lutz's avatar
      build in C++17 mode by default · 4f230976
      Alexandre Duret-Lutz authored
      * configure.ac: Activate C++17, and replace --enable-c++17 by
      --enable-c++20.
      * NEWS: Mention the news.
      * .gitlab-ci.yml: Use C++20 for the former C++17 builds.
      * HACKING, README, doc/org/compile.org, doc/org/concepts.org,
      doc/org/index.org, doc/org/install.org, doc/org/tut.org,
      doc/org/upgrade2.org, spot/misc/escape.hh: Adjust mentions
      of C++14.
      4f230976
  2. 10 Jun, 2020 1 commit
  3. 03 Jun, 2020 5 commits
    • Etienne Renault's avatar
      bricks: move into spot directory · 01cceef2
      Etienne Renault authored
      * bricks/brick-assert, bricks/brick-bitlevel,
      bricks/brick-hash, bricks/brick-hashset,
      bricks/brick-shmem, bricks/brick-types: Rename as .. .
      * spot/bricks/brick-assert, spot/bricks/brick-bitlevel,
      spot/bricks/brick-hash, spot/bricks/brick-hashset,
      spot/bricks/brick-shmem, spot/bricks/brick-types: ... this
      * Makefile.am, README, debian/copyright,
      debian/libspot-dev.install, m4/bricks.m4,
      spot/Makefile.am, spot/ltsmin/spins_kripke.hh,
      spot/ltsmin/spins_kripke.hxx, spot/mc/bloemen.hh
      spot/mc/deadlock.hh, tests/Makefile.am,
      tests/core/bricks.cc: here.
      01cceef2
    • Etienne Renault's avatar
      bricks: add bricks for concurrent hashmap · 458f5063
      Etienne Renault authored
      * Makefile.am, README, bricks/brick-assert.h,
      bricks/brick-bitlevel.h, bricks/brick-hash.h,
      bricks/brick-hashset.h, bricks/brick-shmem.h,
      bricks/brick-types.h, configure.ac,
      debian/copyright, debian/libspot-dev.install,
      m4/bricks.m4, tests/Makefile.am,
      tests/core/.gitignore, tests/core/bricks.cc: here.
      458f5063
    • Etienne Renault's avatar
      reachability: sequential reachability for kripkecube · 94492ffa
      Etienne Renault authored
      * README, configure.ac, spot/mc/Makefile.am,
      spot/mc/reachability.hh: here.
      94492ffa
    • Etienne Renault's avatar
      convert: BDD to cube conversions · 8d57700d
      Etienne Renault authored
      * README, configure.ac, spot/Makefile.am,
      spot/twacube_algos/Makefile.am, spot/twacube_algos/convert.cc
      spot/twacube_algos/convert.hh, tests/core/cube.cc,
      tests/core/cube.test: here.
      8d57700d
    • Etienne Renault's avatar
      Introduce cube data structure · 7c3fdd6b
      Etienne Renault authored
      * README, configure.ac, spot/Makefile.am,
      spot/twacube/Makefile.am, spot/twacube/cube.cc,
      spot/twacube/cube.hh, tests/Makefile.am,
      tests/core/.gitignore, tests/core/cube.cc,
      tests/core/cube.test: here.
      7c3fdd6b
  4. 26 Jan, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      doc: add some troubleshooting help · 056ec02b
      Alexandre Duret-Lutz authored
      Inspired by #375.
      
      * README: Add a section about troubleshooting installations.  Mention
      GraphViz as optional dependency.
      * doc/org/install.org: Mention the troubleshooting section from INSTALL.
      056ec02b
  5. 26 Sep, 2018 1 commit
  6. 11 Aug, 2018 1 commit
  7. 24 May, 2018 1 commit
  8. 22 Nov, 2017 1 commit
  9. 22 Aug, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      switch to C++14 compilation · f5dce597
      Alexandre Duret-Lutz authored
      * configure.ac: Compile in C++14 by default and rename
      --enable-c++14 as c++17.
      * doc/org/compile.org, doc/org/concepts.org, doc/org/index.org,
      doc/org/install.org, doc/org/tut.org, doc/org/upgrade2.org, HACKING,
      NEWS, README: Adjust all mentions of C++11.
      * spot/twaalgos/stats.hh: Use std::make_unique.
      f5dce597
  10. 21 Apr, 2017 1 commit
    • Maximilien Colange's avatar
      Add a new library to generate formulas and automata. · d90e38eb
      Maximilien Colange authored
      This library, called libspotgen, gathers functions to generate classes
      of automata found in the literature.
      Related to #254.
      
      * NEWS, README: Mention the modification.
      * Makefile.am, debian/control, debian/libspotgen0.install: Build the new
        library in a separate package.
      * spot/gen/automata.hh, spot/gen/automata.cc: Add a family of co-Büchi
        automata.
      * configure.ac, spot/Makefile.am, spot/gen/Makefile.am: Build the new
        library.
      d90e38eb
  11. 06 Jan, 2017 1 commit
    • Alexandre GBAGUIDI AISSE's avatar
      spot: Add Picosat to Spot library & Update satsolver class · 32f040fa
      Alexandre GBAGUIDI AISSE authored
      * Makefile.am: Add picosat to subdirs.
      * configure.ac: Add picosat/Makefile to AC_CONFIG_FILES.
      * README: Add picosat/ in the list of directories.
      * debian/copyright: Add picosat licence and details.
      * picosat/Makefile.am: Implement Makefile.am in picosat directory.
      * spot/Makefile.am: Tell the compiler to add libpico.la into libspot.la.
      * picosat/LICENSE: Add picosat licence.
      * picosat/NEWS: Add picosat NEWS.
      * picosat/VERSION: Add picosat VERSION.
      * picosat/picosat.c: Add picosat c file.
      * picosat/picosat.h: Add picosat header file.
      * spot/misc/satsolver.cc: Update functions.
      * spot/misc/satsolver.hh: Add documentation, clean code, change
      some functions visibility and separate templates functions.
      * spot/twaalgos/dtbasat.cc: Update dtba_to_sat function.
      * spot/twaalgos/dtwasat.cc: Update dtwa_to_sat function.
      32f040fa
  12. 25 Oct, 2016 1 commit
  13. 24 Jul, 2016 1 commit
  14. 05 Jan, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      move the sanity tests in tests/sanity/ · 6e854b6d
      Alexandre Duret-Lutz authored
      * spot/sanity/: Move ...
      * tests/sanity/: ... here.
      * spot/sanity/Makefile.am: Merge with...
      * tests/Makefile.am: ... this.
      * tests/run.in: Learn to run perl tests.
      * README, configure.ac, spot/Makefile.am: Adjust.
      * spot/tl/mark.hh: Add missing SPOT_API detected by
      fixed private.test.
      
      * spot/twaalgos/weight.cc, spot/twaalgos/weight.hh: Move...
      * spot/priv/weight.cc, spot/priv/weight.hh: ... here, as
      suggested by fixed private.test.
      * spot/twaalgos/tau03opt.cc, spot/twaalgos/Makefile.am,
      spot/priv/Makefile.am: Adjust.
      6e854b6d
    • Alexandre Duret-Lutz's avatar
      move ltsmin tests to tests/ltsmin/ · ddc424f5
      Alexandre Duret-Lutz authored
      * spot/ltsmin/defs.in: Delete.
      * spot/ltsmin/README, spot/ltsmin/beem-peterson.4.dve,
      spot/ltsmin/check.test, spot/ltsmin/elevator2.1.pm,
      spot/ltsmin/finite.dve, spot/ltsmin/finite.pm, spot/ltsmin/finite.test,
      spot/ltsmin/finite2.test, spot/ltsmin/kripke.test,
      spot/ltsmin/modelcheck.cc: Move...
      * tests/ltsmin/: ... here.
      * spot/ltsmin/README: Point to tests/ltsmin/README.
      * README, configure.ac, spot/ltsmin/Makefile.am, tests/.gitignore,
      tests/Makefile.am, tests/core/defs.in: Adjust.
      ddc424f5
  15. 04 Jan, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      Merge the core and python tests in the tests/ directory · 5cb94a1a
      Alexandre Duret-Lutz authored
      * tests/: Rename as...
      * tests/core/: ... this.
      * python/tests/: Rename as...
      * tests/python/: ... this.
      * python/tests/run.in: Move as...
      * tests/run.in: This, and adjust.
      * tests/Makefile.am: Adjust to run both core and python tests.
      * configure.ac, README, debian/python3-spot.examples, debian/rules,
      doc/org/tut.org, python/Makefile.am, spot/ltsmin/Makefile.am,
      spot/ltsmin/kripke.test, spot/sanity/ipynb.test: Adjust.
      5cb94a1a
  16. 27 Dec, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      move spot/bin/ and spot/tests/ up by one level · 134dfc73
      Alexandre Duret-Lutz authored
      * spot/bin/: Move...
      * bin/: ... here.
      * spot/tests/: Move...
      * tests/: ... here.
      * Makefile.am, README, bench/stutter/Makefile.am,
      bench/stutter/stutter_invariance_formulas.cc, doc/Makefile.am,
      configure.ac, debian/rules, spot/Makefile.am, spot/ltsmin/Makefile.am,
      spot/ltsmin/kripke.test, spot/sanity/style.test, python/tests/run.in:
      Adjust.
      134dfc73
  17. 25 Dec, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      Move spot-if/ltsmin/ to spot/ltsmin/ · 6fb4df43
      Alexandre Duret-Lutz authored
      * spot-if/ltsmin/: Rename as...
      * spot/ltsmin/: ... this.
      * spot-if/: Delete.
      * Makefile.am, NEWS, README, configure.ac, debian/libspot-dev.install,
      doc/Doxyfile.in, spot/Makefile.am, spot/sanity/80columns.test,
      spot/sanity/style.test: Adjust.
      6fb4df43
    • Alexandre Duret-Lutz's avatar
      rename wrap/python/ to python/ · 34c3c1ce
      Alexandre Duret-Lutz authored
      * wrap/python/: Rename to...
      * python/: ... this.
      * wrap/: Delete.
      * Makefile.am, README, configure.ac, debian/python3-spot.examples,
      debian/rules, doc/org/.dir-locals.el.in, doc/org/init.el.in,
      spot/sanity/ipynb.test: Adjust.
      34c3c1ce
  18. 07 Dec, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      rename iface/ as spot-if/ · b519c7d3
      Alexandre Duret-Lutz authored
      So that instead of having to do
        #incluce <spot/iface/ltsmin/ltsmin.hh>
      for using installed the installed header, and
        #incluce <iface/ltsmin/ltsmin.hh>
      for using the non-installed version, we now do
        #incluce <spot-if/ltsmin/ltsmin.hh>
      in both cases.
      
      * iface/: Rename as...
      * spot-if/: ... this.
      * doc/Doxyfile.in, README, configure.ac, Makefile.am,
      spot/sanity/80columns.test, spot/sanity/style.test: Adjust.
      * NEWS: Mention the change.
      * spot-if/ltsmin/Makefile.am: Install headers in $includedir/spot-if.
      * debian/libspot-dev.install: Distribute that directory as well.
      b519c7d3
  19. 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
  20. 28 Nov, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      rewrite explicit Kripke structures and their parser · afbaa54d
      Alexandre Duret-Lutz authored
      Fixes #4 and fixes #5.
      
      * NEWS: Mention the change.
      * src/kripkeparse/: Delete.
      * README, src/Makefile.am, configure.ac: Adjust.
      * src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh: Delete.
      * src/kripke/kripkegraph.hh: New file.
      * src/kripke/Makefile.am: Adjust.
      * src/parseaut/parseaut.yy, src/parseaut/public.hh: Add
      an option to read kripke structures.
      * src/tests/bad_parsing.test: Delete.
      * src/tests/Makefile.am: Adjust.
      * src/tests/kripke.test, src/tests/parse_print_test.cc: Rewrite.
      * src/tests/ikwiad.cc, src/tests/parseaut.test,
      iface/ltsmin/modelcheck.cc, wrap/python/spot_impl.i: Adjust.
      afbaa54d
  21. 20 Nov, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      org: syntax-highlight the HOA outputs · 5aba246f
      Alexandre Duret-Lutz authored
      * elisp/hoa-mode.el, elisp/Makefile.am, elisp/README: New files.
      * debian/copyright, configure.ac, README, Makefile.am: Adjust.
      * doc/org/init.el.in: Adjust to load hoa-mode.el.
      * doc/org/spot.css: Add entries for HOA mode.
      * doc/org/hoa.org, doc/org/ltldo.org, doc/org/oaut.org,
      doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.org,
      doc/org/tut30.org: Make the HOA outputs as HOA.
      5aba246f
  22. 21 Oct, 2015 1 commit
  23. 30 Sep, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      ltlparse: move in parsetl/, and declare in tl/parse.hh · ae6cd921
      Alexandre Duret-Lutz authored
      * src/ltlparse/public.hh: Rename as...
      * src/tl/parse.hh: ... this.
      * src/ltlparse/: Rename as...
      * src/parsetl/: ... this.
      * NEWS: Mention the change.
      * README, configure.ac, doc/org/tut01.org, doc/org/tut02.org,
      doc/org/tut03.org, doc/org/tut10.org, src/Makefile.am,
      src/bin/common_finput.cc, src/bin/common_finput.hh, src/bin/ltl2tgta.cc,
      src/kripkeparse/kripkeparse.yy, src/parseaut/parseaut.yy,
      src/tests/checkpsl.cc, src/tests/checkta.cc,
      src/tests/complementation.cc, src/tests/consterm.cc,
      src/tests/emptchk.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc,
      src/tests/kind.cc, src/tests/length.cc, src/tests/ltlprod.cc,
      src/tests/ltlrel.cc, src/tests/randtgba.cc, src/tests/readltl.cc,
      src/tests/reduc.cc, src/tests/syntimpl.cc, src/tests/tostring.cc,
      src/tl/Makefile.am, src/twaalgos/lbtt.cc, wrap/python/spot_impl.i,
      iface/ltsmin/modelcheck.cc: Adjust.
      ae6cd921
  24. 28 Sep, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      merge ltlvisit/ ltlast/ ltlenv/ into a single tl/ directory · 6ded5e75
      Alexandre Duret-Lutz authored
      The ltl prefix does not make a lot of sens anymore (since we
      support psl as well).  ltlast/ and ltlenv/ were almost empty.
      And ltlvisit/ did not contain any visitor anymore.
      
      * src/ltlvisit/, src/ltlast/, src/ltlenv/: Merge into...
      * src/tl/: ...this.
      * NEWS: Mention the change.
      * README, bench/stutter/stutter_invariance_formulas.cc,
      bench/stutter/stutter_invariance_randomgraph.cc, configure.ac,
      doc/org/tut01.org, doc/org/tut02.org, doc/org/tut10.org, doc/tl/tl.tex,
      iface/ltsmin/ltsmin.hh, iface/ltsmin/modelcheck.cc, src/Makefile.am,
      src/bin/autfilt.cc, src/bin/common_output.cc, src/bin/common_output.hh,
      src/bin/common_r.hh, src/bin/common_trans.cc, src/bin/genltl.cc,
      src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc,
      src/bin/ltldo.cc, src/bin/ltlfilt.cc, src/bin/ltlgrind.cc,
      src/bin/randltl.cc, src/kripke/kripkeexplicit.hh,
      src/kripkeparse/public.hh, src/parseaut/public.hh, src/priv/accmap.hh,
      src/ta/taexplicit.hh, src/ta/tgtaexplicit.hh, src/tests/equalsf.cc,
      src/tests/ikwiad.cc, src/tests/length.cc, src/tests/ltlrel.cc,
      src/tests/randtgba.cc, src/tests/readltl.cc, src/tests/reduc.cc,
      src/tests/syntimpl.cc, src/tests/taatgba.cc, src/tests/tostring.cc,
      src/tests/twagraph.cc, src/twa/acc.hh, src/twa/bdddict.cc,
      src/twa/bdddict.hh, src/twa/bddprint.cc, src/twa/taatgba.cc,
      src/twa/taatgba.hh, src/twa/twa.hh, src/twa/twagraph.cc,
      src/twa/twagraph.hh, src/twa/twasafracomplement.cc,
      src/twaalgos/compsusp.cc, src/twaalgos/compsusp.hh,
      src/twaalgos/dtgbasat.cc, src/twaalgos/hoa.cc,
      src/twaalgos/isweakscc.cc, src/twaalgos/lbtt.cc,
      src/twaalgos/ltl2taa.cc, src/twaalgos/ltl2taa.hh,
      src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/ltl2tgba_fm.hh,
      src/twaalgos/minimize.hh, src/twaalgos/neverclaim.cc,
      src/twaalgos/randomgraph.hh, src/twaalgos/relabel.hh,
      src/twaalgos/remprop.hh, src/twaalgos/stats.cc, src/twaalgos/stutter.cc,
      src/twaalgos/translate.hh, wrap/python/spot_impl.i,
      src/ltlparse/ltlparse.yy, src/ltlparse/public.hh: Adjust.
      6ded5e75
  25. 08 Sep, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      parseaut: swallow the dstarparser · 209e89a9
      Alexandre Duret-Lutz authored
      Note that the parser is still not able to reader multiple dstar
      automata.
      
      * src/dstarparse/: Delete.
      * configure.ac, src/Makefile.am, README: Adjust.
      * src/parseaut/parseaut.yy, src/parseaut/scanaut.ll: Merge in the
      dstarparser rules.
      * src/bin/common_trans.cc, src/bin/common_trans.hh,
      src/bin/dstar2tgba.cc, src/bin/ltlcross.cc, src/bin/ltldo.cc,
      src/tests/ikwiad.cc: Adjust usage.
      * src/tests/parseaut.test: Adjust expected output.
      209e89a9
  26. 11 Jun, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      hoaparse: rename to parseaut · a86391ab
      Alexandre Duret-Lutz authored
      Because this parser is not specific to HOA anymore.
      
      * src/hoaparse/Makefile.am, src/hoaparse/fmterror.cc,
      src/hoaparse/hoaparse.yy, src/hoaparse/parsedecl.hh,
      src/parseaut/public.hh, src/hoaparse/hoascan.ll,
      src/tests/hoaparse.test: Rename to...
      * src/parseaut/Makefile.am, src/parseaut/fmterror.cc,
      src/parseaut/parseaut.yy, src/parseaut/parsedecl.hh,
      src/hoaparse/public.hh, src/parseaut/scanaut.ll,
      src/tests/parseaut.test: ... these, and also adjust the name internally.
      For instance hoa_aut_ptr is now parsed_aut_ptr; hoa_stream_parser is now
      automaton_stream_parser, and hoa_parse() has become parse_aut().
      * NEWS, README, configure.ac, doc/org/tut20.org, src/Makefile.am,
      src/bin/autfilt.cc, src/bin/common_aoutput.cc,
      src/bin/common_aoutput.hh, src/bin/common_conv.cc,
      src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tests/Makefile.am,
      src/tests/complementation.cc, src/tests/ltl2tgba.cc,
      src/tests/readsave.test, wrap/python/ajax/spot.in,
      wrap/python/spot.py, wrap/python/spot_impl.i,
      wrap/python/tests/automata-io.ipynb, wrap/python/tests/parsetgba.py:
      Adjust.
      a86391ab
  27. 07 Jun, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      org: add installation instructions · 2e34fa42
      Alexandre Duret-Lutz authored
      * doc/org/install.org: New file.
      * doc/Makefile.am: Add it.
      * doc/org/index.org: Link to it.
      * doc/org/setup.org: Add macro for
      various version numbers.
      * doc/org/tools.org: Update version number.
      * NEWS, README, bench/ltl2tgba/README, debian/control,
      debian/copyright: Update URLs to website.
      2e34fa42
  28. 24 Apr, 2015 2 commits
    • Etienne Renault's avatar
      Merge kripketest, graphtest and ltltest into tests · 66bd8f34
      Etienne Renault authored
      * README, configure.ac, iface/ltsmin/Makefile.am,
      src/tests/defs.in, src/tests/.gitignore, src/tests/Makefile.am,
      src/Makefile.am: update references.
      * src/kripketest/.gitignore, src/kripketest/Makefile.am,
      src/kripketest/defs.in, src/graphtest/.gitignore,
      src/graphtest/Makefile.am,
      src/graphtest/defs.in, src/ltltest/.cvsignore,
      src/ltltest/.gitignore, src/ltltest/Makefile.am,
      src/ltltest/defs.in:: remove files.
      * src/kripketest/bad_parsing.test, src/kripketest/kripke.test,
      src/kripketest/origin, src/kripketest/parse_print_test.cc,
      src/ltltest/bare.test, src/ltltest/consterm.cc,
      src/ltltest/consterm.test, src/tests/defs.in,
      src/ltltest/equals.test, src/ltltest/equalsf.cc,
      src/ltltest/eventuniv.test, src/ltltest/exclusive-ltl.test,
      src/graphtest/graph.cc, src/graphtest/graph.test,
      src/ltltest/isop.test, src/ltltest/kind.cc,
      src/ltltest/kind.test, src/ltltest/latex.test,
      src/ltltest/lbt.test, src/ltltest/length.cc,
      src/ltltest/length.test, src/ltltest/lenient.test,
      src/ltltest/ltlcrossgrind.test, src/ltltest/ltlfilt.test,
      src/ltltest/ltlgrind.test, src/ltltest/ltlrel.cc,
      src/ltltest/ltlrel.test, src/ltltest/lunabbrev.test,
      src/ltltest/nenoform.test, src/graphtest/ngraph.cc,
      src/graphtest/ngraph.test, src/ltltest/parse.test,
      src/ltltest/parseerr.test, src/ltltest/rand.test,
      src/ltltest/readltl.cc, src/ltltest/reduc.cc,
      src/ltltest/reduc.test, src/ltltest/reduc0.test,
      src/ltltest/reduccmp.test, src/ltltest/reducpsl.test,
      src/ltltest/remove_x.test, src/ltltest/stutter-ltl.test,
      src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test,
      src/graphtest/tgbagraph.test, src/ltltest/tostring.cc,
      src/ltltest/tostring.test, src/ltltest/tunabbrev.test,
      src/ltltest/tunenoform.test, src/graphtest/twagraph.cc,
      src/ltltest/unabbrevwm.test,src/ltltest/utf8.test,
      src/ltltest/uwrm.test: rename as...
      * src/tests/bad_parsing.test, src/tests/kripke.test,
      src/tests/origin, src/tests/parse_print_test.cc,
      src/tests/bare.test, src/tests/consterm.cc,
      src/tests/consterm.test, src/tests/equals.test,
      src/tests/equalsf.cc, src/tests/eventuniv.test,
      src/tests/exclusive-ltl.test, src/tests/graph.cc,
      src/tests/graph.test, src/tests/isop.test,
      src/tests/kind.cc, src/tests/kind.test,
      src/tests/latex.test, src/tests/lbt.test,
      src/tests/length.cc, src/tests/length.test,
      src/tests/lenient.test, src/tests/ltlcrossgrind.test,
      src/tests/ltlfilt.test, src/tests/ltlgrind.test,
      src/tests/ltlrel.cc, src/tests/ltlrel.test,
      src/tests/lunabbrev.test, src/tests/nenoform.test,
      src/tests/ngraph.cc, src/tests/ngraph.test,
      src/tests/parse.test, src/tests/parseerr.test,
      src/tests/rand.test, src/tests/readltl.cc,
      src/tests/reduc.cc, src/tests/reduc.test,
      src/tests/reduc0.test, src/tests/reduccmp.test,
      src/tests/reducpsl.test, src/tests/remove_x.test,
      src/tests/stutter-ltl.test, src/tests/syntimpl.cc,
      src/tests/syntimpl.test, src/tests/tgbagraph.test,
      src/tests/tostring.cc, src/tests/tostring.test,
      src/tests/tunabbrev.test, src/tests/tunenoform.test,
      src/tests/twagraph.cc, src/tests/unabbrevwm.test,
      src/tests/utf8.test, src/tests/uwrm.test: ...these!
      66bd8f34
    • Etienne Renault's avatar
      Rename tgbatest into tests. · bd57f7a9
      Etienne Renault authored
      * src/Makefile.am, README, configure.ac: update references.
      * src/tgbatest/: rename as...
      * src/tests/: ...this!
      bd57f7a9
  29. 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 files as twa · 703fbd0e
      Alexandre Duret-Lutz authored
      Automatic mass renaming.
      
      * src/graphtest/tgbagraph.cc, src/tgba/acc.cc, src/tgba/acc.hh,
      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/fwd.hh, src/tgba/Makefile.am,
      src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc,
      src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh, src/tgba/tgba.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/.cvsignore: Rename as...
      * src/graphtest/twagraph.cc, src/twa/acc.cc, src/twa/acc.hh,
      src/twa/bdddict.cc, src/twa/bdddict.hh, src/twa/bddprint.cc,
      src/twa/bddprint.hh, src/twa/formula2bdd.cc, src/twa/formula2bdd.hh,
      src/twa/fwd.hh, src/twa/Makefile.am, src/twa/taatgba.cc,
      src/twa/taatgba.hh, src/twa/twa.cc, src/twa/twagraph.cc,
      src/twa/twagraph.hh, src/twa/twa.hh, src/twa/twamask.cc,
      src/twa/twamask.hh, src/twa/twaproduct.cc, src/twa/twaproduct.hh,
      src/twa/twaproxy.cc, src/twa/twaproxy.hh,
      src/twa/twasafracomplement.cc, src/twa/twasafracomplement.hh,
      src/twa/.cvsignore: ... these.
      * README, bench/stutter/stutter_invariance_randomgraph.cc,
      configure.ac, iface/ltsmin/modelcheck.cc, src/Makefile.am,
      src/bin/common_aoutput.cc, src/bin/common_conv.hh,
      src/bin/common_trans.hh, src/bin/dstar2tgba.cc, src/bin/ltl2tgta.cc,
      src/bin/randaut.cc, src/dstarparse/dra2ba.cc,
      src/dstarparse/public.hh, src/graphtest/Makefile.am,
      src/graphtest/ngraph.cc, src/hoaparse/hoaparse.yy,
      src/hoaparse/public.hh, src/kripke/fairkripke.hh,
      src/kripke/kripkeexplicit.cc, src/kripke/kripkeprint.cc,
      src/kripkeparse/kripkeparse.yy, src/ltlvisit/apcollect.cc,
      src/ltlvisit/apcollect.hh, src/ltlvisit/exclusive.hh,
      src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
      src/priv/accmap.hh, src/ta/ta.hh, src/ta/taexplicit.cc,
      src/ta/taexplicit.hh, src/ta/tgta.hh, src/ta/tgtaexplicit.cc,
      src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh, src/taalgos/dotty.cc,
      src/taalgos/emptinessta.cc, src/taalgos/minimize.cc,
      src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh,
      src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh,
      src/tgbaalgos/bfssteps.cc, src/tgbaalgos/canonicalize.cc,
      src/tgbaalgos/canonicalize.hh, src/tgbaalgos/cleanacc.hh,
      src/tgbaalgos/complete.hh, src/tgbaalgos/compsusp.cc,
      src/tgbaalgos/compsusp.hh, src/tgbaalgos/degen.cc,
      src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/dotty.hh, src/tgbaalgos/dtbasat.cc,
      src/tgbaalgos/dtbasat.hh, 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/sccstack.hh, src/tgbaalgos/gtec/status.hh,
      src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh, src/tgbaalgos/hoa.cc,
      src/tgbaalgos/hoa.hh, src/tgbaalgos/isdet.hh, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.hh,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh,
      src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, src/tgbaalgos/mask.hh,
      src/tgbaalgos/minimize.hh, src/tgbaalgos/ndfs_result.hxx,
      src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
      src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/powerset.hh, src/tgbaalgos/product.cc,
      src/tgbaalgos/product.hh, src/tgbaalgos/projrun.cc,
      src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.cc,
      src/tgbaalgos/randomgraph.hh, src/tgbaalgos/randomize.hh,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.cc,
      src/tgbaalgos/reducerun.hh, src/tgbaalgos/relabel.hh,
      src/tgbaalgos/remfin.hh, src/tgbaalgos/remprop.hh,
      src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh,
      src/tgbaalgos/sbacc.hh, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh,
      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.hh,
      src/tgbaalgos/stutter.cc, src/tgbaalgos/stutter.hh,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
      src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
      src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh,
      src/tgbaalgos/weight.hh, src/tgbaalgos/word.cc, src/tgbatest/acc.cc,
      src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/taatgba.cc,
      wrap/python/spot_impl.i: Adjust.
      703fbd0e
  30. 01 Apr, 2015 1 commit
  31. 28 Feb, 2015 1 commit
  32. 04 Feb, 2015 1 commit