1. 15 Oct, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      fix crash of randaut -Q0 · 6cf807da
      Alexandre Duret-Lutz authored
      * src/twaalgos/randomgraph.cc: Replace an assertion by an exception.
      * src/bin/randaut.cc: Diagnose -Q0.
      * src/tests/randaut.test: Test it.
      * NEWS: Mention the bug.
  2. 14 Oct, 2015 2 commits
    • 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.
    • Alexandre Duret-Lutz's avatar
  3. 13 Oct, 2015 2 commits
    • 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().
    • Alexandre Duret-Lutz's avatar
      * src/bin/ltlcross.cc: Typo. · fb642c6d
      Alexandre Duret-Lutz authored
  4. 08 Oct, 2015 1 commit
  5. 04 Oct, 2015 2 commits
  6. 03 Oct, 2015 13 commits
    • Alexandre Duret-Lutz's avatar
      org: better syntax highlighting · 24a8affb
      Alexandre Duret-Lutz authored
      * doc/org/init.el.in: Activate CSS for code fragments.
      * doc/org/spot.css: Style relevant elements.
    • Alexandre Duret-Lutz's avatar
      python: implement formula.__format__ · 5bfd0267
      Alexandre Duret-Lutz authored
      Fixes #105.
      * src/bin/common_trans.cc (quote_shell_string): Move ...
      * src/misc/escape.cc, src/misc/escape.hh (quote_shell_string):
      ... here.
      * wrap/python/spot_impl.i: Wrap escape.hh.
      * wrap/python/spot.py: Implement formula.__format__.
      * wrap/python/tests/ltlsimple.py: Test it.
      * NEWS, doc/org/tut01.org, wrap/python/tests/formulas.ipynb: Document
    • Alexandre Duret-Lutz's avatar
      * NEWS: Summarize recent changes. · 20bb1719
      Alexandre Duret-Lutz authored
    • Alexandre Duret-Lutz's avatar
      Work around weird Python 3.5 generator/iterator interaction · 6ff4fa97
      Alexandre Duret-Lutz authored
      * wrap/python/spot.py: Python 3.5 reports some unexpected SystemError
      messages when the stack of iterator(...(iterator(generator))) we build
      for random LTL generation raises a StopIteration.  The messages are
      attached either to delete_formula or delete_randltlgenerator, claiming
      that these functions exit with an error; but I have checked that they
      do not.  I've been unable to understand the cause of the issue.
      Replacing the generator by an iterator at least fixes the problem in a
      way that is transparent for our API.
      * wrap/python/tests/randltl.ipynb: Adjust expected formulas.
    • Alexandre Duret-Lutz's avatar
      python: do not crash when a function returns a null formula · 5f2d55ab
      Alexandre Duret-Lutz authored
      * wrap/python/spot_impl.i: Map null formulas to None.
      * wrap/python/tests/randgen.py: New file.
      * wrap/python/tests/Makefile.am: Add it.
    • Alexandre Duret-Lutz's avatar
      bdddict: remove dead code · 24ef5a0b
      Alexandre Duret-Lutz authored
      * src/twa/bdddict.cc,
      src/twa/bdddict.hh (unregister_all_typed_variables, oneacc_to_formula,
      register_acceptance_variables): Remove these unused methods.
    • Alexandre Duret-Lutz's avatar
      postproc: default to an empty formula · 2fa9c275
      Alexandre Duret-Lutz authored
      * src/twaalgos/postproc.hh: Allow the formula not to be specified.  The
      code already support that, as it is called with an explicit nullptr in
      autfilt (for example), but not requiring the nullptr is better for the
      Python bindings.
    • Alexandre Duret-Lutz's avatar
      tgba_complete: rename as complete and export in Python · 5e07e838
      Alexandre Duret-Lutz authored
      * src/twaalgos/complete.cc, src/twaalgos/complete.hh
      (tgba_complete, tgba_complete_here): Rename as...
      (complete, complete_here): ... these.  Also fix useless output of
      acceptance marks on transition leading to the sink when the automaton
      does not use state-based acceptance.
      * src/tests/ikwiad.cc, src/twaalgos/dtgbacomp.cc,
      src/twaalgos/dtgbasat.cc, src/twaalgos/postproc.cc,
      src/twaalgos/product.cc: Adjust.
      * wrap/python/spot_impl.i: Export these function.
      * wrap/python/tests/automata.ipynb: Test spot.complete().
    • Alexandre Duret-Lutz's avatar
      simpfg: remove this unused function · afe5b2a1
      Alexandre Duret-Lutz authored
      * src/tl/simpfg.cc, src/tl/simpfg.hh: Delete.
      * src/tl/Makefile.am: Adjust.
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      Add noexcept to various constructors related to graphs. · 54935cb9
      Alexandre Duret-Lutz authored
      * m4/gccwarn.m4: Enable -Wnoexcept.
      * src/graph/graph.hh, src/twa/acc.hh, src/twa/twagraph.hh: Add noexcept
      to various constructors.
    • Alexandre Duret-Lutz's avatar
      Enable -Wmissing-declarations in development mode. · 20365e53
      Alexandre Duret-Lutz authored
      * m4/gccwarn.m4: Add -Wmissing-declarations.
      * iface/ltsmin/ltsmin.cc, iface/ltsmin/modelcheck.cc,
      src/bin/common_trans.cc, src/bin/genltl.cc, src/bin/ltlgrind.cc,
      src/tests/acc.cc, src/tests/bitvect.cc, 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/graph.cc, src/tests/ikwiad.cc, src/tests/intvcmp2.cc,
      src/tests/intvcomp.cc, src/tests/kind.cc, src/tests/length.cc,
      src/tests/ltlprod.cc, src/tests/ltlrel.cc, src/tests/ngraph.cc,
      src/tests/randtgba.cc, src/tests/readltl.cc, src/tests/reduc.cc,
      src/tests/syntimpl.cc, src/tests/tostring.cc, src/tests/twagraph.cc,
      src/tl/contain.cc, src/twaalgos/dtgbacomp.cc, src/twaalgos/minimize.cc:
      Add "static" and move in anonymous namespace when appropriate.
    • Alexandre Duret-Lutz's avatar
  7. 01 Oct, 2015 5 commits
  8. 30 Sep, 2015 8 commits
  9. 29 Sep, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      doxygen: improve formula documentation · dcb9d7e8
      Alexandre Duret-Lutz authored
      * doc/Doxyfile.in: Adjust to hide SPOT_API.
      * doc/mainpage.dox: Adjust like to parse_infix_psl().
      * src/tl/formula.hh: Document most methods of formula,
      and fix the definition of the comparisons operator.
      * src/ltlparse/public.hh, src/tl/apcollect.hh, src/tl/declenv.hh,
      src/tl/defaultenv.hh, src/tl/dot.hh, src/tl/environment.hh,
      src/tl/length.hh, src/tl/mark.hh, src/tl/nenoform.hh, src/tl/print.hh,
      src/tl/randomltl.hh, src/tl/relabel.hh, src/tl/simpfg.hh,
      src/tl/simplify.hh, src/tl/unabbrev.hh: Adjust doxygen group.
    • Alexandre Duret-Lutz's avatar
      bddprint: do not store a global shared_ptr to the bdd_dict · ca95e4d1
      Alexandre Duret-Lutz authored
      * src/twa/bddprint.cc: Do not store a global shared_ptr to the bdddict
      used for printing (a simple pointer is enough), otherwise it risks being
      the last shared_ptr to be destroyed, and it might be destroyed after the
      unicity maps of the formulas.
  10. 28 Sep, 2015 4 commits
    • Alexandre Duret-Lutz's avatar
      doc: more examples of the formula interface · c67540db
      Alexandre Duret-Lutz authored
      * src/tl/formula.hh, src/tl/formula.cc: Add an operator<< to print
      * doc/org/tut01.org, doc/org/tut02.org: Adjust.
      * doc/org/tut03.org: New file.
      * doc/org/tut.org, doc/Makefile.am: Add it.
    • Alexandre Duret-Lutz's avatar
      kill the ltl namespace · cb392101
      Alexandre Duret-Lutz authored
      * NEWS: Mention it.
      * bench/stutter/stutter_invariance_formulas.cc,
      bench/stutter/stutter_invariance_randomgraph.cc, doc/mainpage.dox,
      doc/org/tut01.org, doc/org/tut02.org, doc/org/tut10.org, doc/tl/tl.tex,
      iface/ltsmin/ltsmin.cc, iface/ltsmin/ltsmin.hh,
      iface/ltsmin/modelcheck.cc, src/bin/autfilt.cc,
      src/bin/common_aoutput.cc, src/bin/common_aoutput.hh,
      src/bin/common_finput.cc, src/bin/common_finput.hh,
      src/bin/common_output.cc, src/bin/common_output.hh, src/bin/common_r.hh,
      src/bin/common_trans.cc, src/bin/common_trans.hh, src/bin/dstar2tgba.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/randaut.cc, src/bin/randltl.cc,
      src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/kripkeparse/kripkeparse.yy, src/kripkeparse/public.hh,
      src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy,
      src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
      src/ltlparse/public.hh, src/parseaut/parseaut.yy,
      src/parseaut/public.hh, 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/parse.test,
      src/tests/parse_print_test.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/tostring.test,
      src/tl/apcollect.cc, src/tl/apcollect.hh, src/tl/contain.cc,
      src/tl/contain.hh, src/tl/declenv.cc, src/tl/declenv.hh,
      src/tl/defaultenv.cc, src/tl/defaultenv.hh, src/tl/dot.cc,
      src/tl/dot.hh, src/tl/environment.hh, src/tl/exclusive.cc,
      src/tl/exclusive.hh, src/tl/formula.cc, src/tl/formula.hh,
      src/tl/length.cc, src/tl/length.hh, src/tl/mark.cc, src/tl/mark.hh,
      src/tl/mutation.cc, src/tl/mutation.hh, src/tl/nenoform.cc,
      src/tl/nenoform.hh, src/tl/print.cc, src/tl/print.hh,
      src/tl/randomltl.cc, src/tl/randomltl.hh, src/tl/relabel.cc,
      src/tl/relabel.hh, src/tl/remove_x.cc, src/tl/remove_x.hh,
      src/tl/simpfg.cc, src/tl/simpfg.hh, src/tl/simplify.cc,
      src/tl/simplify.hh, src/tl/snf.cc, src/tl/snf.hh, src/tl/unabbrev.cc,
      src/tl/unabbrev.hh, src/twa/bdddict.cc, src/twa/bdddict.hh,
      src/twa/bddprint.cc, src/twa/formula2bdd.cc, src/twa/formula2bdd.hh,
      src/twa/taatgba.cc, src/twa/taatgba.hh, src/twa/twa.hh,
      src/twa/twagraph.cc, src/twa/twagraph.hh, src/twaalgos/compsusp.cc,
      src/twaalgos/compsusp.hh, src/twaalgos/ltl2taa.cc,
      src/twaalgos/ltl2taa.hh, src/twaalgos/ltl2tgba_fm.cc,
      src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/minimize.cc,
      src/twaalgos/minimize.hh, src/twaalgos/neverclaim.cc,
      src/twaalgos/postproc.cc, src/twaalgos/postproc.hh,
      src/twaalgos/powerset.cc, src/twaalgos/powerset.hh,
      src/twaalgos/randomgraph.cc, src/twaalgos/randomgraph.hh,
      src/twaalgos/relabel.cc, src/twaalgos/relabel.hh,
      src/twaalgos/remprop.cc, src/twaalgos/remprop.hh, src/twaalgos/stats.cc,
      src/twaalgos/stats.hh, src/twaalgos/stutter.cc, src/twaalgos/stutter.hh,
      src/twaalgos/translate.cc, src/twaalgos/translate.hh,
      wrap/python/spot_impl.i: Remove the ltl namespace.
    • 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.
    • Alexandre Duret-Lutz's avatar
      python: work around old swig version · 3e10dba9
      Alexandre Duret-Lutz authored
      Swig 3.0.2 (currently installed by Debian), install strongly typed
      enumerator in the main namespace instead of in its own namespace.
      This is fixed in latter versions of Swig.
      * wrap/python/spot.py: If spot.op does not exists, populated it with all
      operators from the spot namespace.
      * wrap/python/tests/ltlsimple.py: Use operators from spot.op.