- 21 Oct, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
* wrap/python/spot.py: Implement it. Also report non-zero exit using CalledProcessError. * wrap/python/tests/automata-io.ipynb, wrap/python/tests/piperead.ipynb: Adjust. * NEWS: Mention the change.
-
- 20 Oct, 2015 3 commits
-
-
Alexandre Duret-Lutz authored
* wrap/python/spot.py: Fix bindings for scc_filter. * wrap/python/tests/remfin.py: Test them.
-
Alexandre Duret-Lutz authored
I have to remember that org-mode does not evaluate something unless it is eventually exported. * doc/org/hoa.org, doc/org/ioltl.org, doc/org/tut21.org, doc/org/tut30.org: Adjust exports commands.
-
Alexandre Duret-Lutz authored
* src/tests/unambig.test: New test case. Reported by Ming-Hsien Tsai. * src/twaalgos/sccfilter.cc: Always create an initial state. * src/twaalgos/isunamb.cc: Speed up on empty languages. * NEWS, THANKS: Update.
-
- 19 Oct, 2015 3 commits
-
-
Alexandre Duret-Lutz authored
* doc/org/tut30.org: New file. * doc/Makefile.am, doc/org/tut.org: Add it.
-
Alexandre Duret-Lutz authored
This simplifies the use of the spot.postprocessor object. * wrap/python/spot.py: Add it. * wrap/python/tests/automata.ipynb: Use it. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
This is a bug: % ltlfilt -f 'a W b' --unabbreviate=WR a U (b | (a W b)) * src/tl/unabbrev.cc: Here. * src/tests/unabbrevwm.test: Harden test case. * wrap/python/tests/randltl.ipynb: Adjust expected output. * NEWS: Mention the fix.
-
- 18 Oct, 2015 4 commits
-
-
Alexandre Duret-Lutz authored
* wrap/python/spot_impl.i (get_name, set_name): New methods for twa. * wrap/python/tests/remfin.py: Test them. * wrap/python/ajax/spotcgi.in: Use set_name(). * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
* doc/org/tut01.org, doc/tl/tl.tex, src/bin/common_r.hh, src/bin/ltlfilt.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc, src/tests/randtgba.cc, src/tests/reduc.cc, src/tests/syntimpl.cc, src/tl/nenoform.cc, src/tl/randomltl.cc, src/tl/randomltl.hh, src/tl/simplify.cc, src/tl/simplify.hh, src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/stutter.cc, src/twaalgos/translate.cc, src/twaalgos/translate.hh, wrap/python/ajax/spotcgi.in, wrap/python/spot.py, wrap/python/tests/interdep.py: Rename ltl_simplifier to tl_simplifier. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* wrap/python/spot.py: Add the unabbreviate() method, and remove unabbrivate_ltl() and get_literal(). * wrap/python/tests/randltl.ipynb: Demonstrate unabbreviate().
-
- 17 Oct, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
* wrap/python/tests/remfin.py: New file. * wrap/python/tests/Makefile.am: Add it. * src/twaalgos/remfin.cc (remove_fin_det_weak): Purge dead states.
-
- 16 Oct, 2015 2 commits
-
-
Alexandre Duret-Lutz authored
* debian/rules: Fix notebooks to use the local mathjax.
-
Alexandre Duret-Lutz authored
* debian/rules: Build for all supported python3 versions. * NEWS: Mention it.
-
- 15 Oct, 2015 5 commits
-
-
Alexandre Duret-Lutz authored
* src/parseaut/parseaut.yy: Add and the a check_version() function. * src/tests/parseaut.test: Test it. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
This additionally fixes #107. * src/bin/ltlgrind.cc: Fix handling for FILEANAME/COL. Document FORMAT in --help. Assume -F for arguments given without options. * src/tests/ltlgrind.test: Add two tests. * NEWS: Mention this.
-
Alexandre Duret-Lutz authored
This is motivated by an email from Fanda. * src/bin/common_post.cc, src/bin/common_post.hh: Add variables to detect when level or pref are sets. * src/bin/autfilt.cc: Adjust default for pref/sets. * src/tests/readsave.test: Add test cases. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
* src/bin/autfilt.cc: Add option --complete. * src/twaalgos/complete.cc: Better handling of 0-edge automata. * src/tests/complement.test: New file. * src/tests/Makefile.am: Add it.
-
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.
-
- 14 Oct, 2015 2 commits
-
-
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 authored
-
- 13 Oct, 2015 2 commits
-
-
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 authored
-
- 08 Oct, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
* wrap/python/spot.py: Use a decorator to extend classes. * wrap/python/tests/formulas.ipynb: Adjust expected help text.
-
- 04 Oct, 2015 2 commits
-
-
Alexandre Duret-Lutz authored
* wrap/python/spot.py: Better docstrings. * wrap/python/tests/formulas.ipynb: Update.
-
Alexandre Duret-Lutz authored
-
- 03 Oct, 2015 13 commits
-
-
Alexandre Duret-Lutz authored
* doc/org/init.el.in: Activate CSS for code fragments. * doc/org/spot.css: Style relevant elements.
-
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 it.
-
Alexandre Duret-Lutz authored
-
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 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 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 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 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 authored
* src/tl/simpfg.cc, src/tl/simpfg.hh: Delete. * src/tl/Makefile.am: Adjust.
-
Alexandre Duret-Lutz authored
-
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 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 authored
-
- 01 Oct, 2015 1 commit
-
-
Alexandre Duret-Lutz authored
It was only needed with Swig versions older than what we have now. * src/misc/common.hh: Here. * src/misc/bitvect.hh, src/misc/common.hh, src/ta/taexplicit.hh, src/ta/taproduct.hh, src/tl/simplify.hh, src/twa/bdddict.hh, src/twa/taatgba.hh, src/twa/twaproduct.hh: Use = delete directly.
-