1. 22 Jun, 2019 1 commit
  2. 12 Jun, 2019 1 commit
  3. 28 May, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      introduce output_aborter, and use it in ltlcross · a8504509
      Alexandre Duret-Lutz authored
      * spot/twaalgos/alternation.cc, spot/twaalgos/alternation.hh,
      spot/twaalgos/complement.cc, spot/twaalgos/complement.hh,
      spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh,
      spot/twaalgos/minimize.cc, spot/twaalgos/minimize.hh,
      spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
      spot/twaalgos/powerset.cc, spot/twaalgos/powerset.hh,
      spot/twaalgos/product.cc, spot/twaalgos/product.hh: Use an
      output_aborter argument to abort if the output is too large.
      * bin/ltlcross.cc: Use complement() with an output_aborter
      so that ltlcross will not attempt to build complement larger
      than 500 states or 5000 edges.  Add --determinize-max-states
      and --determinize-max-edges options.
      * tests/core/ltlcross3.test, tests/core/ltlcrossce2.test,
      tests/core/sccsimpl.test, tests/core/wdba2.test,
      tests/python/stutter-inv.ipynb: Adjust test cases.
      * NEWS: Document this.
      * bin/spot-x.cc: Add documentation for postprocessor's
      det-max-states and det-max-edges arguments.
      * doc/org/ltlcross.org: Update description.
      a8504509
  4. 22 Jun, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      postproc: simplify the acceptance condition · a325de86
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc: Here.
      * spot/twaalgos/cobuchi.cc, spot/twaalgos/totgba.cc: Fix some bug
      uncovered by the new simplified automata.
      * tests/core/satmin2.test, tests/core/sccdot.test,
      tests/core/sim3.test, tests/python/decompose.ipynb,
      tests/python/satmin.ipynb: Update expected results.
      * NEWS: Mention the simplification and the bug.
      a325de86
  5. 11 Jun, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      specialize scc_filter for inherently_weak automata · 95d732e3
      Alexandre Duret-Lutz authored
      Part of issue #351.
      
      * spot/twaalgos/sccfilter.cc, spot/twaalgos/sccfilter.hh: Specialize
      for inherently-weak automata.
      * spot/twaalgos/postproc.cc: Simplify.
      * tests/core/dca2.test, tests/core/parity2.test,
      tests/core/prodor.test, tests/core/randomize.test,
      tests/python/automata.ipynb, tests/python/highlighting.ipynb,
      tests/python/product.ipynb, tests/python/remfin.py,
      tests/python/stutter-inv.ipynb: Adjust.
      * NEWS: Mention it.
      95d732e3
  6. 28 Mar, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      specialized translation for GF(guarantee) and FG(safety) · 7a65bdf6
      Alexandre Duret-Lutz authored
      This is adapted from a proposition in a paper by J. Esparza,
      J. Křentínský, and S. Sickert, submitted to LICS'18.  We should add
      proper references to the code and documentation once that paper is
      accepted.
      
      * spot/twaalgos/gfguarantee.cc, spot/twaalgos/gfguarantee.hh:
      New files.
      * spot/twaalgos/Makefile.am, python/spot/impl.i: Add them.
      * spot/twa/fwd.hh: Add a forward declaration of bdd_dict_ptr.
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Make it
      possible to call finalize() from the translator subclass.  Constify
      all the do_* functions while we are there.
      * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Add
      a "gf-guarantee" option to decide whether to use the new translation.
      * bin/spot-x.cc: Document it.
      * tests/core/dca2.test, tests/core/genltl.test,
      tests/core/ltl2tgba2.test, tests/core/parity2.test,
      tests/core/satmin.test, tests/python/automata.ipynb,
      tests/python/sbacc.py: Adjust test cases.
      * tests/python/except.py: Add a couple more tests.
      7a65bdf6
  7. 21 Feb, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      include config.h in all *.cc files · ac6b0c94
      Alexandre Duret-Lutz authored
      This helps working around missing C functions like strcasecmp that do
      not exist everywhere (e.g. on Cygwin), and for which lib/ supplies a
      replacement.  Unfortunately we do not have such build in our current
      continuous integration suite, so we cannot easily detect files where
      such config.h inclusion would be useful.  Therefore this patch simply
      makes it mandatory to include config.h in *.cc files.  Including this
      in public *.hh file is currently forbidden.
      
      * spot/gen/automata.cc, spot/gen/formulas.cc,
      spot/kripke/fairkripke.cc, spot/kripke/kripke.cc,
      spot/ltsmin/ltsmin.cc, spot/misc/game.cc, spot/parseaut/fmterror.cc,
      spot/parsetl/fmterror.cc, spot/parsetl/parsetl.yy,
      spot/priv/bddalloc.cc, spot/priv/freelist.cc, spot/priv/satcommon.cc,
      spot/priv/trim.cc, spot/priv/weight.cc, spot/ta/ta.cc,
      spot/ta/taexplicit.cc, spot/ta/taproduct.cc, spot/ta/tgtaexplicit.cc,
      spot/ta/tgtaproduct.cc, spot/taalgos/dot.cc,
      spot/taalgos/emptinessta.cc, spot/taalgos/minimize.cc,
      spot/taalgos/reachiter.cc, spot/taalgos/statessetbuilder.cc,
      spot/taalgos/stats.cc, spot/taalgos/tgba2ta.cc, spot/tl/apcollect.cc,
      spot/tl/contain.cc, spot/tl/declenv.cc, spot/tl/defaultenv.cc,
      spot/tl/dot.cc, spot/tl/exclusive.cc, spot/tl/hierarchy.cc,
      spot/tl/length.cc, spot/tl/ltlf.cc, spot/tl/mark.cc,
      spot/tl/mutation.cc, spot/tl/nenoform.cc, spot/tl/print.cc,
      spot/tl/randomltl.cc, spot/tl/relabel.cc, spot/tl/remove_x.cc,
      spot/tl/simplify.cc, spot/tl/snf.cc, spot/tl/unabbrev.cc,
      spot/twa/acc.cc, spot/twa/bdddict.cc, spot/twa/bddprint.cc,
      spot/twa/formula2bdd.cc, spot/twa/taatgba.cc, spot/twa/twa.cc,
      spot/twa/twagraph.cc, spot/twa/twaproduct.cc, spot/twaalgos/aiger.cc,
      spot/twaalgos/alternation.cc, spot/twaalgos/are_isomorphic.cc,
      spot/twaalgos/bfssteps.cc, spot/twaalgos/canonicalize.cc,
      spot/twaalgos/cleanacc.cc, spot/twaalgos/cobuchi.cc,
      spot/twaalgos/complement.cc, spot/twaalgos/complete.cc,
      spot/twaalgos/compsusp.cc, spot/twaalgos/couvreurnew.cc,
      spot/twaalgos/cycles.cc, spot/twaalgos/degen.cc,
      spot/twaalgos/determinize.cc, spot/twaalgos/dot.cc,
      spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc,
      spot/twaalgos/dualize.cc, spot/twaalgos/emptiness.cc,
      spot/twaalgos/gtec/ce.cc, spot/twaalgos/gtec/gtec.cc,
      spot/twaalgos/gtec/sccstack.cc, spot/twaalgos/gtec/status.cc,
      spot/twaalgos/gv04.cc, spot/twaalgos/hoa.cc,
      spot/twaalgos/iscolored.cc, spot/twaalgos/isdet.cc,
      spot/twaalgos/isunamb.cc, spot/twaalgos/isweakscc.cc,
      spot/twaalgos/langmap.cc, spot/twaalgos/lbtt.cc,
      spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc,
      spot/twaalgos/magic.cc, spot/twaalgos/mask.cc,
      spot/twaalgos/minimize.cc, spot/twaalgos/neverclaim.cc,
      spot/twaalgos/parity.cc, spot/twaalgos/postproc.cc,
      spot/twaalgos/powerset.cc, spot/twaalgos/product.cc,
      spot/twaalgos/rabin2parity.cc, spot/twaalgos/randomgraph.cc,
      spot/twaalgos/randomize.cc, spot/twaalgos/reachiter.cc,
      spot/twaalgos/relabel.cc, spot/twaalgos/remfin.cc,
      spot/twaalgos/remprop.cc, spot/twaalgos/sbacc.cc,
      spot/twaalgos/sccfilter.cc, spot/twaalgos/sccinfo.cc,
      spot/twaalgos/se05.cc, spot/twaalgos/sepsets.cc,
      spot/twaalgos/simulation.cc, spot/twaalgos/split.cc,
      spot/twaalgos/stats.cc, spot/twaalgos/strength.cc,
      spot/twaalgos/stripacc.cc, spot/twaalgos/stutter.cc,
      spot/twaalgos/sum.cc, spot/twaalgos/tau03.cc,
      spot/twaalgos/tau03opt.cc, spot/twaalgos/totgba.cc,
      spot/twaalgos/toweak.cc, spot/twaalgos/translate.cc,
      spot/twaalgos/word.cc, tests/core/acc.cc, tests/core/bitvect.cc,
      tests/core/checkpsl.cc, tests/core/checkta.cc, tests/core/consterm.cc,
      tests/core/emptchk.cc, tests/core/equalsf.cc, tests/core/graph.cc,
      tests/core/ikwiad.cc, tests/core/intvcmp2.cc, tests/core/intvcomp.cc,
      tests/core/kind.cc, tests/core/kripkecat.cc, tests/core/length.cc,
      tests/core/ltlrel.cc, tests/core/ngraph.cc, tests/core/parity.cc,
      tests/core/randtgba.cc, tests/core/readltl.cc, tests/core/reduc.cc,
      tests/core/safra.cc, tests/core/sccif.cc, tests/core/syntimpl.cc,
      tests/core/taatgba.cc, tests/core/tostring.cc, tests/core/trival.cc,
      tests/core/twagraph.cc, tests/ltsmin/modelcheck.cc,
      spot/parseaut/scanaut.ll, spot/parsetl/scantl.ll: Include config.h.
      * spot/gen/Makefile.am, spot/graph/Makefile.am,
      spot/kripke/Makefile.am, spot/ltsmin/Makefile.am,
      spot/parseaut/Makefile.am, spot/parsetl/Makefile.am,
      spot/priv/Makefile.am, spot/ta/Makefile.am, spot/taalgos/Makefile.am,
      spot/tl/Makefile.am, spot/twa/Makefile.am, spot/twaalgos/Makefile.am,
      spot/twaalgos/gtec/Makefile.am, tests/Makefile.am: Add the -I lib/
      flags.
      * tests/sanity/includes.test: Catch missing config.h in *.cc, and
      diagnose config.h in *.hh.
      * tests/sanity/style.test: Better diagnostics.
      ac6b0c94
  8. 24 Jan, 2018 1 commit
    • Maximilien Colange's avatar
      Improve IAR construction · 1ebd86de
      Maximilien Colange authored
      spot::iar() was fixed to handle correctly Rabin-like conditions.
      It also now supports Streett-like conditions.
      
      * NEWS, spot/twaalgos/postproc.cc: document it
      * spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh:
        implement it
      * tests/core/rabin2parity.test, tests/python/except.py: test it
      1ebd86de
  9. 16 Jan, 2018 1 commit
    • Maximilien Colange's avatar
      Rabin to parity translation · 7e02aae3
      Maximilien Colange authored
      * spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh:
        implement it
      * spot/twaalgos/postproc.cc: use it
      * spot/twaalgos/Makefile.am: build the new files
      * NEWS: document the new function
      * python/spot/impl.i: Python bindings for the new function
      * tests/Makefile.am, tests/core/rabin2parity.test: test the new function
      7e02aae3
  10. 14 Jan, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      postproc: add support for co-Büchi output · 61b0a542
      Alexandre Duret-Lutz authored
      * spot/twaalgos/cobuchi.cc, spot/twaalgos/cobuchi.hh (to_nca): New
      function.
      (weak_to_cobuchi): New internal function, used in to_nca and to_dca
      when appropriate.
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Implement
      the CoBuchi option.
      * python/spot/__init__.py: Support it in Python.
      * bin/common_post.cc: Add support for --buchi.
      * bin/autfilt.cc: Remove the --dca option.
      * tests/core/dca.test, tests/python/automata.ipynb: Adjust and add
      more tests.  In particular, add more complex persistence and
      recurrence formulas to the list of dca.test.
      * tests/python/dca.test: Adjust and rename to...
      * tests/core/dca2.test: ... this.  Add more tests, to the point
      that this is now failing, as described in issue #317.
      * tests/python/dca.py: Remove.
      * tests/Makefile.am: Adjust.
      61b0a542
  11. 08 Jan, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      postproc: add support for colored-parity · bd6dc7a8
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Add support
      for a colored option.
      * bin/common_post.cc, bin/common_post.hh bin/autfilt.cc,
      bin/ltl2tgba.cc, bin/dstar2tgba.cc: Add support for --colored-parity.
      * bin/ltldo.cc: Adjust as well for consistency, even if --parity and
      --colored-parity is not used here.
      * tests/core/parity2.test: Add tests.
      * doc/org/autfilt.org, doc/org/ltl2tgba.org: Add examples.
      * NEWS: Mention --colored-parity.
      bd6dc7a8
  12. 02 Jan, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      postproc: introduce --parity output · 42ebf8b1
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Add parity
        options.
      * bin/common_post.cc: Add support for --parity.
      * NEWS: Mention it.
      * tests/core/parity2.test: New file.
      * tests/Makefile.am: Add it.
      42ebf8b1
  13. 29 Sep, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      postproc: fix a comment · bd34f3c6
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc: Here.
      bd34f3c6
    • Alexandre Duret-Lutz's avatar
      degen: detect superfluous SCCs and remove them · 900b344c
      Alexandre Duret-Lutz authored
      Suggested by Maximilien Colange.
      
      * spot/twaalgos/degen.cc: If the output has more SCC than the input,
      detect useless SCCs and remove them.
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
      spot/twaalgos/degen.hh: Add support for a degen-remscc option.
      * bin/spot-x.cc, NEWS: Document it.
      * tests/core/degenscc.test: New file.
      * tests/Makefile.am: Add it.
      * tests/core/det.test: Lower some expected size (yay!).
      900b344c
  14. 24 Sep, 2017 1 commit
  15. 27 Mar, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      rename is_deterministic to is_universal · 4a5d7a39
      Alexandre Duret-Lutz authored
      For #212.
      
      * spot/twa/twa.hh: Rename prop_deterministic() as prop_universal(),
      and keep the old name as deprecated.
      * spot/twaalgos/isdet.cc, spot/twaalgos/isdet.hh: Rename
      is_deterministic() as is_universal(), and add a new function
      for is_deterministic().
      * doc/org/concepts.org, doc/org/hoa.org, doc/org/tut21.org,
      spot/tl/hierarchy.cc, spot/twa/twagraph.cc,
      spot/twaalgos/are_isomorphic.cc, spot/twaalgos/determinize.cc,
      spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc,
      spot/twaalgos/hoa.cc, spot/twaalgos/minimize.cc,
      spot/twaalgos/postproc.cc, spot/twaalgos/product.cc,
      spot/twaalgos/randomgraph.cc, spot/twaalgos/remfin.cc,
      spot/twaalgos/simulation.cc, spot/twaalgos/totgba.cc,
      spot/twaalgos/word.cc, tests/python/product.ipynb,
      tests/python/remfin.py: Adjust.
      * NEWS: Mention the change.
      4a5d7a39
  16. 03 Mar, 2017 4 commits
    • Alexandre Duret-Lutz's avatar
      monitor: fix -MD/-M difference in property output · 0621e0e9
      Alexandre Duret-Lutz authored
      Fixes #241.
      
      * spot/twaalgos/postproc.cc: Use the deterministic monitor if it
      has as many states as the non-deterministic one.
      * spot/twaalgos/minimize.cc (minimize_monitor): Quickly check
      for terminal automata.
      * spot/twaalgos/stripacc.cc: Set the weak property.
      * spot/twaalgos/stripacc.hh: Improve documentation.
      * tests/core/monitor.test, tests/core/sbacc.test: Update.
      * NEWS: Mention the issue.
      0621e0e9
    • Alexandre Duret-Lutz's avatar
      postproc: fix monitor code · 9defdad2
      Alexandre Duret-Lutz authored
      Fixes #240.
      
      * spot/twaalgos/postproc.cc: Do not call do_simul on the output of
      minimize_monitor(), and do not skip complete() when PREF_==Any.
      * tests/core/monitor.test: Add a test case.
      * NEWS: Mention the bug.
      * doc/org/ltl2tgba.org: Document complete monitors.
      9defdad2
    • Alexandre Duret-Lutz's avatar
      monitor: fix -MD/-M difference in property output · a66e7704
      Alexandre Duret-Lutz authored
      Fixes #241.
      
      * spot/twaalgos/postproc.cc: Use the deterministic monitor if it
      has as many states as the non-deterministic one.
      * spot/twaalgos/minimize.cc (minimize_monitor): Quickly check
      for terminal automata.
      * spot/twaalgos/stripacc.cc: Set the weak property.
      * spot/twaalgos/stripacc.hh: Improve documentation.
      * tests/core/monitor.test, tests/core/sbacc.test: Update.
      * NEWS: Mention the issue.
      a66e7704
    • Alexandre Duret-Lutz's avatar
      postproc: fix monitor code · 2b9accdf
      Alexandre Duret-Lutz authored
      Fixes #240.
      
      * spot/twaalgos/postproc.cc: Do not call do_simul on the output of
      minimize_monitor(), and do not skip complete() when PREF_==Any.
      * tests/core/monitor.test: Add a test case.
      * NEWS: Mention the bug.
      * doc/org/ltl2tgba.org: Document complete monitors.
      2b9accdf
  17. 12 Feb, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      is_alternating() -> !is_existential() · fefb375d
      Alexandre Duret-Lutz authored
      Part of #212.
      
      * spot/misc/common.hh (SPOT_DEPRECATED): Improve support current
      compilers and options flags.
      * spot/twa/twagraph.hh, spot/graph/graph.hh (is_alternating): Mark it
      as deprecated.
      (is_existential): New method.
      * bin/autfilt.cc, bin/ltlcross.cc, spot/parseaut/parseaut.yy,
      spot/twa/twa.cc, spot/twa/twagraph.cc, spot/twaalgos/alternation.cc,
      spot/twaalgos/are_isomorphic.cc, spot/twaalgos/canonicalize.cc,
      spot/twaalgos/couvreurnew.cc, spot/twaalgos/cycles.cc,
      spot/twaalgos/degen.cc, spot/twaalgos/determinize.cc,
      spot/twaalgos/dot.cc, spot/twaalgos/dtbasat.cc,
      spot/twaalgos/dtwasat.cc, spot/twaalgos/hoa.cc,
      spot/twaalgos/isunamb.cc, spot/twaalgos/isweakscc.cc,
      spot/twaalgos/mask.hh, spot/twaalgos/minimize.cc,
      spot/twaalgos/postproc.cc, spot/twaalgos/product.cc,
      spot/twaalgos/randomize.cc, spot/twaalgos/remfin.cc,
      spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc,
      spot/twaalgos/sccinfo.cc, spot/twaalgos/simulation.cc,
      spot/twaalgos/strength.cc, tests/core/graph.cc, tests/core/ngraph.cc,
      tests/python/alternating.py: Adjust all uses.
      * NEWS: Mention the renaming.
      fefb375d
  18. 06 Jan, 2017 4 commits
    • Alexandre GBAGUIDI AISSE's avatar
      twaalgos: Set 'dicho' algo as default for SAT-based minimization · ef2355a5
      Alexandre GBAGUIDI AISSE authored
      * python/spot/__init__.py: Handle options.
      * spot/twaalgos/dtwasat.cc: Handle options.
      * spot/twaalgos/postproc.cc: Handle options.
      * spot/twaalgos/postproc.hh: Handle options.
      * tests/core/satmin.test: Update tests.
      Now use 'sat-minimize=4' to use the naive algo.
      * tests/core/satmin2.test: Update tests.
      Now use --sat-minimize='naive' to use the naive algo.
      * tests/python/satmin.py: Update tests.
      Now use 'naive=True' to use the naive algo.
      ef2355a5
    • Alexandre GBAGUIDI AISSE's avatar
      spot: Add 'langmap' option with dichotomy (it helps to choose min val) · 67e3a4f2
      Alexandre GBAGUIDI AISSE authored
      * python/spot/__init__.py: Handle 'dicho' option in 'sat_minimize'.
      * spot/priv/satcommon.cc: Implement get_number_of_distinct_vals.
      * spot/priv/satcommon.hh: Declare get_number_of_distinct_vals.
      * spot/twaalgos/dtbasat.cc: Use get_number_of_distinct_vals.
      * spot/twaalgos/dtbasat.hh: Change dichotomy function's prototype.
      * spot/twaalgos/dtwasat.cc: Use get_number_of_distinct_vals.
      * spot/twaalgos/dtwasat.hh: Change dichotomy function's prototype.
      Handle options.
      * spot/twaalgos/postproc.cc: Handle options.
      * spot/twaalgos/postproc.hh: Add dicho_langmap_ var for options.
      * tests/core/satmin2.test: Add tests for dichotomy.
      * tests/core/satmin.test: Add tests for dichotomy.
      * tests/python/satmin.py: Replace 'dichotomy' with 'dicho' option.
      67e3a4f2
    • Alexandre GBAGUIDI AISSE's avatar
      spot: Implement dt*a_sat_minimize_assume(...) methods · 9a204b77
      Alexandre GBAGUIDI AISSE authored
      * python/spot/__init__.py: Add 'assume' option.
      * spot/misc/satsolver.cc: Add function to handle assumptions.
      * spot/misc/satsolver.hh: Declare assumption function.
      * spot/twaalgos/dtbasat.cc: Implement dtba_sat_minimize_assume.
      * spot/twaalgos/dtbasat.hh: Declare it.
      * spot/twaalgos/dtwasat.cc: Implement dtwa_sat_minimize_assume and
      handle options.
      * spot/twaalgos/dtwasat.hh: Declare it.
      * spot/twaalgos/postproc.cc: Handle options.
      * spot/twaalgos/postproc.hh: Use param_ var for incr and assume.
      * tests/core/satmin.test: Add tests for the new function.
      * tests/core/satmin2.test: Add tests for the new function.
      * tests/python/satmin.py: Add tests for the new function.
      9a204b77
    • Alexandre GBAGUIDI AISSE's avatar
      twaalgos: Implement dt*a_sat_minimize_incr(...) functions · ee17c2de
      Alexandre GBAGUIDI AISSE authored
      * python/spot/__init__.py: Add 'incr' boolean argument.
      * spot/twaalgos/dtbasat.cc: Implement dtba_sat_minimize_incr(...).
      * spot/twaalgos/dtbasat.hh: Declare it.
      * spot/twaalgos/dtwasat.cc: Implement dtwa_sat_minimize_incr(...) and
      deal with options.
      * spot/twaalgos/dtwasat.hh: Declare it.
      * spot/twaalgos/postproc.cc: Add option --sat-minimize=incr.
      * spot/twaalgos/postproc.hh: Add incr parameter.
      * tests/core/satmin.test: Add tests for incremental version.
      Update expected result.
      * tests/core/satmin2.test: Add tests for incremental version.
      * tests/python/satmin.py: Add tests for incremental version.
      ee17c2de
  19. 29 Dec, 2016 1 commit
  20. 17 May, 2016 2 commits
  21. 01 May, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      print_hoa: output all registered APs · a1b3b065
      Alexandre Duret-Lutz authored
      Also introduce twa::unregister_ap() and twa_graph::remove_unused_ap()
      so that the methods where this behavior is expected can be fixed.
      
      And fix ltsmin::kripke() which did not register APs.
      
      Part of #170.
      
      * spot/twaalgos/hoa.cc: Use apvars() to print all registerd APs.
      Throw an exception when printing automata using unregistered APs.
      * spot/ltsmin/ltsmin.cc: Call register_ap().
      * spot/twa/twa.cc, spot/twa/twa.hh, spot/twa/twagraph.cc,
      spot/twa/twagraph.hh (twa::unregister_ap, twa_graph::remove_unused_ap):
      New methods.
      * spot/tl/exclusive.cc, spot/twaalgos/postproc.cc,
      spot/twaalgos/remprop.cc, spot/twaalgos/relabel.cc: Use them.
      * tests/core/maskacc.test, tests/core/maskkeep.test,
      tests/core/strength.test: Adjust expected results.
      * NEWS: Mention those changes.
      a1b3b065
    • Alexandre Duret-Lutz's avatar
      print_hoa: output all registered APs · 1c2c914d
      Alexandre Duret-Lutz authored
      Also introduce twa::unregister_ap() and twa_graph::remove_unused_ap()
      so that the methods where this behavior is expected can be fixed.
      
      And fix ltsmin::kripke() which did not register APs.
      
      Part of #170.
      
      * spot/twaalgos/hoa.cc: Use apvars() to print all registerd APs.
      Throw an exception when printing automata using unregistered APs.
      * spot/ltsmin/ltsmin.cc: Call register_ap().
      * spot/twa/twa.cc, spot/twa/twa.hh, spot/twa/twagraph.cc,
      spot/twa/twagraph.hh (twa::unregister_ap, twa_graph::remove_unused_ap):
      New methods.
      * spot/tl/exclusive.cc, spot/twaalgos/postproc.cc,
      spot/twaalgos/remprop.cc, spot/twaalgos/relabel.cc: Use them.
      * tests/core/maskacc.test, tests/core/maskkeep.test,
      tests/core/strength.test: Adjust expected results.
      * NEWS: Mention those changes.
      1c2c914d
  22. 10 Mar, 2016 1 commit
    • Laurent XU's avatar
      sanity: Replace tabulars by spaces in *.cc *.hh *.hxx · f7e7b4f1
      Laurent XU authored
      * bin/autfilt.cc, bin/common_aoutput.cc, bin/common_aoutput.hh,
      bin/common_finput.cc, bin/common_finput.hh, bin/common_hoaread.cc,
      bin/common_output.cc, bin/common_output.hh, bin/common_post.cc,
      bin/common_post.hh, bin/common_r.hh, bin/common_range.cc,
      bin/common_range.hh, bin/common_setup.cc, bin/common_trans.cc,
      bin/common_trans.hh, bin/dstar2tgba.cc, bin/genltl.cc,
      bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc,
      bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randaut.cc, bin/randltl.cc,
      bin/spot-x.cc, spot/graph/graph.hh, spot/graph/ngraph.hh,
      spot/kripke/kripkegraph.hh, spot/ltsmin/ltsmin.cc,
      spot/ltsmin/ltsmin.hh, spot/misc/bareword.cc, spot/misc/bitvect.cc,
      spot/misc/bitvect.hh, spot/misc/common.hh, spot/misc/escape.cc,
      spot/misc/fixpool.hh, spot/misc/formater.cc, spot/misc/hash.hh,
      spot/misc/intvcmp2.cc, spot/misc/intvcmp2.hh, spot/misc/intvcomp.cc,
      spot/misc/intvcomp.hh, spot/misc/location.hh, spot/misc/minato.cc,
      spot/misc/minato.hh, spot/misc/mspool.hh, spot/misc/optionmap.cc,
      spot/misc/optionmap.hh, spot/misc/random.cc, spot/misc/random.hh,
      spot/misc/satsolver.cc, spot/misc/satsolver.hh, spot/misc/timer.cc,
      spot/misc/timer.hh, spot/misc/tmpfile.cc, spot/misc/trival.hh,
      spot/parseaut/fmterror.cc, spot/parseaut/parsedecl.hh,
      spot/parseaut/public.hh, spot/parsetl/fmterror.cc,
      spot/parsetl/parsedecl.hh, spot/priv/accmap.hh, spot/priv/bddalloc.cc,
      spot/priv/freelist.cc, spot/priv/trim.cc, spot/priv/weight.cc,
      spot/priv/weight.hh, spot/ta/taexplicit.cc, spot/ta/taexplicit.hh,
      spot/ta/taproduct.cc, spot/ta/taproduct.hh, spot/ta/tgtaexplicit.cc,
      spot/ta/tgtaexplicit.hh, spot/ta/tgtaproduct.cc,
      spot/ta/tgtaproduct.hh, spot/taalgos/dot.cc, spot/taalgos/dot.hh,
      spot/taalgos/emptinessta.cc, spot/taalgos/emptinessta.hh,
      spot/taalgos/minimize.cc, spot/taalgos/tgba2ta.cc,
      spot/taalgos/tgba2ta.hh, spot/tl/apcollect.cc, spot/tl/contain.cc,
      spot/tl/contain.hh, spot/tl/dot.cc, spot/tl/exclusive.cc,
      spot/tl/exclusive.hh, spot/tl/formula.cc, spot/tl/formula.hh,
      spot/tl/length.cc, spot/tl/mark.cc, spot/tl/mutation.cc,
      spot/tl/mutation.hh, spot/tl/parse.hh, spot/tl/print.cc,
      spot/tl/print.hh, spot/tl/randomltl.cc, spot/tl/randomltl.hh,
      spot/tl/relabel.cc, spot/tl/relabel.hh, spot/tl/remove_x.cc,
      spot/tl/simplify.cc, spot/tl/simplify.hh, spot/tl/snf.cc,
      spot/tl/snf.hh, spot/tl/unabbrev.cc, spot/tl/unabbrev.hh,
      spot/twa/acc.cc, spot/twa/acc.hh, spot/twa/bdddict.cc,
      spot/twa/bdddict.hh, spot/twa/bddprint.cc, spot/twa/formula2bdd.cc,
      spot/twa/formula2bdd.hh, spot/twa/taatgba.cc, spot/twa/taatgba.hh,
      spot/twa/twa.cc, spot/twa/twa.hh, spot/twa/twagraph.cc,
      spot/twa/twagraph.hh, spot/twa/twaproduct.cc, spot/twa/twaproduct.hh,
      spot/twaalgos/are_isomorphic.cc, spot/twaalgos/are_isomorphic.hh,
      spot/twaalgos/bfssteps.cc, spot/twaalgos/bfssteps.hh,
      spot/twaalgos/cleanacc.cc, spot/twaalgos/complete.cc,
      spot/twaalgos/compsusp.cc, spot/twaalgos/compsusp.hh,
      spot/twaalgos/copy.cc, spot/twaalgos/cycles.cc,
      spot/twaalgos/cycles.hh, spot/twaalgos/degen.cc,
      spot/twaalgos/degen.hh, spot/twaalgos/determinize.cc,
      spot/twaalgos/determinize.hh, spot/twaalgos/dot.cc,
      spot/twaalgos/dot.hh, spot/twaalgos/dtbasat.cc,
      spot/twaalgos/dtbasat.hh, spot/twaalgos/dtwasat.cc,
      spot/twaalgos/dtwasat.hh, spot/twaalgos/emptiness.cc,
      spot/twaalgos/emptiness.hh, spot/twaalgos/emptiness_stats.hh,
      spot/twaalgos/gtec/ce.cc, spot/twaalgos/gtec/ce.hh,
      spot/twaalgos/gtec/gtec.cc, spot/twaalgos/gtec/gtec.hh,
      spot/twaalgos/gtec/sccstack.cc, spot/twaalgos/gtec/status.cc,
      spot/twaalgos/gv04.cc, spot/twaalgos/hoa.cc, spot/twaalgos/hoa.hh,
      spot/twaalgos/isdet.cc, spot/twaalgos/isunamb.cc,
      spot/twaalgos/isweakscc.cc, spot/twaalgos/lbtt.cc,
      spot/twaalgos/lbtt.hh, spot/twaalgos/ltl2taa.cc,
      spot/twaalgos/ltl2taa.hh, spot/twaalgos/ltl2tgba_fm.cc,
      spot/twaalgos/ltl2tgba_fm.hh, spot/twaalgos/magic.cc,
      spot/twaalgos/magic.hh, spot/twaalgos/mask.cc, spot/twaalgos/mask.hh,
      spot/twaalgos/minimize.cc, spot/twaalgos/minimize.hh,
      spot/twaalgos/ndfs_result.hxx, spot/twaalgos/neverclaim.cc,
      spot/twaalgos/neverclaim.hh, spot/twaalgos/postproc.cc,
      spot/twaalgos/postproc.hh, spot/twaalgos/powerset.cc,
      spot/twaalgos/powerset.hh, spot/twaalgos/product.cc,
      spot/twaalgos/product.hh, spot/twaalgos/projrun.cc,
      spot/twaalgos/projrun.hh, spot/twaalgos/randomgraph.cc,
      spot/twaalgos/randomgraph.hh, spot/twaalgos/randomize.cc,
      spot/twaalgos/randomize.hh, spot/twaalgos/reachiter.cc,
      spot/twaalgos/reachiter.hh, spot/twaalgos/relabel.cc,
      spot/twaalgos/relabel.hh, spot/twaalgos/remfin.cc,
      spot/twaalgos/remprop.cc, spot/twaalgos/sbacc.cc,
      spot/twaalgos/sccfilter.cc, spot/twaalgos/sccfilter.hh,
      spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh,
      spot/twaalgos/se05.cc, spot/twaalgos/se05.hh,
      spot/twaalgos/sepsets.cc, spot/twaalgos/simulation.cc,
      spot/twaalgos/simulation.hh, spot/twaalgos/stats.cc,
      spot/twaalgos/stats.hh, spot/twaalgos/strength.cc,
      spot/twaalgos/strength.hh, spot/twaalgos/stripacc.cc,
      spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh,
      spot/twaalgos/tau03.cc, spot/twaalgos/tau03opt.cc,
      spot/twaalgos/tau03opt.hh, spot/twaalgos/totgba.cc,
      spot/twaalgos/translate.cc, spot/twaalgos/word.cc, tests/core/acc.cc,
      tests/core/bitvect.cc, tests/core/checkpsl.cc, tests/core/checkta.cc,
      tests/core/consterm.cc, tests/core/emptchk.cc, tests/core/equalsf.cc,
      tests/core/graph.cc, tests/core/ikwiad.cc, tests/core/intvcmp2.cc,
      tests/core/intvcomp.cc, tests/core/kind.cc, tests/core/kripkecat.cc,
      tests/core/ltlrel.cc, tests/core/ngraph.cc, tests/core/randtgba.cc,
      tests/core/readltl.cc, tests/core/reduc.cc, tests/core/safra.cc,
      tests/core/syntimpl.cc, tests/ltsmin/modelcheck.cc: Replace tabulars by
      8 spaces.
      * tests/sanity/style.test: Add checks for no tabulars in *.cc *.hh *.hxx
      f7e7b4f1
  23. 12 Feb, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      postproc: add fine-tuning options for determinization · b066c6f3
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh:
      Add options det-scc, det-simul, det-stutter.
      * bin/spot-x.cc: Document them.
      * doc/org/ltl2tgba.org: Illustrate one of them and link
      to the spot-x man page.
      b066c6f3
    • Alexandre Duret-Lutz's avatar
      postproc: integrate tgba_determinize() · 8568c3b4
      Alexandre Duret-Lutz authored
      * spot/twa/acc.hh: Add a smaller version of is_parity().
      * spot/twaalgos/postproc.cc: Call tgba_determinize() if asked for
      Generic acceptance and Deterministic output.
      * bin/common_post.cc: Add 'G' as a shorthand for --generic.
      * doc/org/ltl2tgba.org: Illustrate =ltl2tgba -G -D=.
      8568c3b4
  24. 13 Jan, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      twa: store property bits as trivals · da391492
      Alexandre Duret-Lutz authored
      * spot/twa/twa.hh: Store property bits as trivals.
      * NEWS: Mention the change.
      * spot/parseaut/parseaut.yy, spot/twaalgos/are_isomorphic.cc,
      spot/twaalgos/complete.cc, spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc,
      spot/twaalgos/isdet.cc, spot/twaalgos/isunamb.cc, spot/twaalgos/lbtt.cc,
      spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/postproc.cc,
      spot/twaalgos/remfin.cc, spot/twaalgos/strength.cc,
      spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh,
      spot/twaalgos/totgba.cc, tests/core/ikwiad.cc,
      tests/python/product.ipynb, tests/python/remfin.py: Adjust.
      * doc/org/hoa.org, doc/org/tut21.org: Update documentation.
      da391492
  25. 18 Dec, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      acc_cond: get rid of generalized_buchi() · fbf5ac0e
      Alexandre Duret-Lutz authored
      It is already in acc_cond::acc_code::generalized_buchi() along with all
      other acceptance condition constructors.
      
      * spot/twa/acc.hh (acc_cond::generalized_buchi): Remove.
      * spot/tests/ikwiad.cc, spot/twaalgos/postproc.cc: Adjust.
      fbf5ac0e
  26. 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
  27. 24 Nov, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      sat: rename dtgbasat as dtwasat · a5ca9dbc
      Alexandre Duret-Lutz authored
      * src/twaalgos/dtgbasat.cc, src/twaalgos/dtgbasat.hh: Rename as...
      * src/twaalgos/dtwasat.cc, src/twaalgos/dtwasat.hh: ... these.
      * src/bin/autfilt.cc, src/tests/ikwiad.cc, src/twaalgos/Makefile.am,
      src/twaalgos/postproc.cc, wrap/python/spot_impl.i: Adjust.
      * NEWS: Mention the renamings.
      a5ca9dbc
  28. 05 Nov, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      twa: rename the is_* getters as prop_* · cbb2e64e
      Alexandre Duret-Lutz authored
      This fixes #116.
      
      * src/twa/twa.hh: Rename those methods.
      * NEWS: Document the renamings.
      * doc/org/hoa.org, doc/org/tut21.org, src/parseaut/parseaut.yy,
      src/tests/ikwiad.cc, src/twa/twagraph.hh,
      src/twaalgos/are_isomorphic.cc, src/twaalgos/complete.cc,
      src/twaalgos/degen.cc, src/twaalgos/dot.cc, src/twaalgos/dtbasat.cc,
      src/twaalgos/dtgbasat.cc, src/twaalgos/hoa.cc, src/twaalgos/isdet.cc,
      src/twaalgos/isunamb.cc, src/twaalgos/lbtt.cc,
      src/twaalgos/minimize.cc, src/twaalgos/postproc.cc,
      src/twaalgos/product.cc, src/twaalgos/randomgraph.cc,
      src/twaalgos/remfin.cc, src/twaalgos/sbacc.cc,
      src/twaalgos/simulation.cc, src/twaalgos/stutter.cc,
      src/twaalgos/totgba.cc: Adjust.
      cbb2e64e
  29. 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
  30. 13 Oct, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      restructure the complementation code · 06d3bc67
      Alexandre Duret-Lutz authored
      The previous code was sometime doing the work of remove_fin() in
      addition to complementing the acceptance conditions.  This separate
      the two operations clearly.  Also the specialized code for
      complementing weak automata is now a specialized code for remove_fin()
      on weak automata.
      
      * src/twaalgos/dtgbacomp.hh, src/twaalgos/dtgbacomp.cc: Rename as ...
      * src/twaalgos/complement.hh, src/twaalgos/complement.cc: ... these.
      * src/twaalgos/Makefile.am: Adjust.
      * src/twaalgos/complement.hh (dtgba_complement): Rename as ...
      (dtwa_complement): ... this, and restrict the purpose to completion
      and accetance complementation.  Further acceptance simplification
      can be done with remove_fin() and to_generalized_buchi().
      * src/twaalgos/remfin.cc (remove_fin): Specialize handling of weak
      automata using the code that was originally in dtgba_complement().
      Also mark the output as state-based when the input has to Inf.
      * src/twaalgos/postproc.cc, src/twaalgos/postproc.hh: Make sure
      scc_filter is always called after to_generalized_buchi().
      * bench/stutter/stutter_invariance_randomgraph.cc,
      src/bin/ltlcross.cc, src/tests/ikwiad.cc, src/twaalgos/minimize.cc,
      src/twaalgos/powerset.cc, src/twaalgos/stutter.cc: Adjust usage.
      * src/tests/dstar.test, src/tests/ltl2dstar4.test,
      src/tests/remfin.test: Adjust expected outputs.
      * wrap/python/spot_impl.i: Export dtwa_complement().
      06d3bc67