- 07 Apr, 2017 2 commits
-
-
Thomas Medioni authored
* NEWS: Mention of this modification * spot/twaalgos/complement.cc: Replace dtwa_complement with a call to dualize
-
Thomas Medioni authored
* NEWS: Mention the implementation * python/spot/impl.i: Add dualize() to python interface. * spot/twaalgos/Makefile.am: Add dualize.cc,hh to the build * spot/twaalgos/dualize.cc: Implement dualize() that takes an automaton and returns its dual * spot/twaalgos/dualize.hh: Implement dualize() * tests/Makefile.am: Add dualize tests to the test suite * tests/python/dualize.py: Test cases for dualize
-
- 06 Apr, 2017 1 commit
-
-
Alexandre Duret-Lutz authored
* bin/common_trans.cc: Here. * doc/org/ltlcross.org, doc/org/ltldo.org, NEWS: Adjust.
-
- 05 Apr, 2017 1 commit
-
-
Maximilien Colange authored
* debian/control: Fix URL.
-
- 04 Apr, 2017 1 commit
-
-
Alexandre Duret-Lutz authored
when fin_alone sets where presents (i.e., not really Rabin condition), the rabin_to_buchi_maybe() could fail to notice DBA-typeness. * spot/twaalgos/remfin.cc: Don't set scc_ba_type to false when fin_alone is present. * tests/core/remfin.test: Add a test case.
-
- 03 Apr, 2017 1 commit
-
-
Thomas Medioni authored
* spot/twaalgos/sum.cc: Fix the sum of automatas having universal initial transitions. * tests/core/explsum.test: Add test case testing the handling of universal initial transitions in sum.
-
- 31 Mar, 2017 1 commit
-
-
Thomas Medioni authored
* NEWS: mention this fix. * bench/stutter/stutter_bench.sh, bench/stutter/user.sh: Path to spot binaries would include an inexistant src directory. * bench/stutter/stutter_invariance_formulas.cc: Add override qualifier to satisfy -Wsuggest-override.
-
- 30 Mar, 2017 2 commits
-
-
Alexandre Duret-Lutz authored
* bench/dtgbasat/gen.py, spot/twaalgos/complement.hh: Fix looser->loser and lossing->losing. * tests/sanity/style.test: Catch 'an uni[^n]'. * spot/ta/ta.hh, spot/taalgos/tgba2ta.cc, spot/taalgos/tgba2ta.hh, spot/twa/twagraph.cc, spot/twaalgos/complement.hh, spot/twaalgos/sccinfo.cc, spot/twaalgos/sum.hh: Fix various occurences of this pattern.
-
Alexandre Duret-Lutz authored
* src/kernel.c (bdd_addref): Fix typo documentation. * src/bddop.c (bdd_appall, bdd_appallcomp): Likewise.
-
- 29 Mar, 2017 5 commits
-
-
Maximilien Colange authored
Properly track dependencies of SWIG files to trigger recompilation when appropriate. Closes issue #250. * python/Makefile.am: Track the dependencies of .i files à la automake.
-
Alexandre Duret-Lutz authored
* tests/python/ipnbdoctest.py: Use importlib instead of imp. * tests/python/ltlparse.py: Fix invalid escape sequence.
-
Alexandre Duret-Lutz authored
Related to #212. * python/spot/impl.i: Here.
-
Maximilien Colange authored
* tests/sanity/style.test: improve detection of assert in headers, and of template arguments.
-
Alexandre Duret-Lutz authored
The algorithm had two problems: it was removing only useless destination from universal destination (instead of removing the entire edge), and it was not properly iterating over the entire reachable automaton. * spot/twa/twagraph.cc: Fix it. * spot/twa/twagraph.hh: Adjust documentation. * tests/core/alternating.test: Add more tests. * tests/python/twagraph.py: Adjust. * NEWS: Mention the bug.
-
- 28 Mar, 2017 2 commits
-
-
Alexandre Duret-Lutz authored
* .dir-locals.el: Redefine C-c C-c in sh-mode and python-mode for the tests/ subdirectory.c * HACKING: Mention it.
-
Alexandre Duret-Lutz authored
Because we spent some time with Thomas to re-understand the logic. * spot/twaalgos/complete.cc: Comment the code.
-
- 27 Mar, 2017 2 commits
-
-
Alexandre Duret-Lutz authored
Reported by Thomas Medioni. * spot/twaalgos/complement.cc: Here. * tests/core/complement.test: Add a test case. * NEWS: Mention it.
-
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.
-
- 22 Mar, 2017 4 commits
-
-
Alexandre Duret-Lutz authored
Fixes #247. * bin/genltl.cc: Here. * tests/core/genltl.test: Make sure %F always return a correct pattern name.. * NEWS: Mention the bug.
-
Alexandre Duret-Lutz authored
Fixes #246. * bin/genltl.cc: Implement it. * bin/man/genltl.x, doc/org/genltl.org, NEWS: Document it. * tests/core/ltl2tgba2.test: Test it.
-
Alexandre Duret-Lutz authored
Fixes #245. * bin/genltl.cc: Add the option. * bin/man/genltl.x: Add reference. * tests/core/ltl2tgba2.test: Use these patterns. * doc/org/genltl.org, NEWS: Document the options.
-
Alexandre Duret-Lutz authored
* bin/genltl.cc: Here. * NEWS: Mention it.
-
- 20 Mar, 2017 1 commit
-
-
Alexandre Duret-Lutz authored
* spot/twa/twa.hh: Add support. Make two constructors for prop_set in order to diagnose constructions with 5 arguments. * spot/parseaut/parseaut.yy: Adjust diagnostics for complete and deterministic. * spot/tl/exclusive.cc, spot/twa/twagraph.cc, spot/twaalgos/alternation.cc, spot/twaalgos/complete.cc, spot/twaalgos/complete.hh, spot/twaalgos/degen.cc, spot/twaalgos/determinize.cc, spot/twaalgos/hoa.cc, spot/twaalgos/isdet.cc, spot/twaalgos/mask.cc, spot/twaalgos/minimize.cc, spot/twaalgos/product.cc, spot/twaalgos/remfin.cc, spot/twaalgos/remprop.cc, spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc, spot/twaalgos/simulation.cc, spot/twaalgos/strength.cc, spot/twaalgos/stutter.cc, spot/twaalgos/totgba.cc, tests/core/parseaut.test, tests/python/product.ipynb: Adjust. * NEWS, doc/org/concepts.org, doc/org/hoa.org, doc/org/tut21.org: Document it.
-
- 18 Mar, 2017 1 commit
-
-
Alexandre Duret-Lutz authored
Fixes #244, reported by Vincent Tourneur. * doc/org/.dir-locals.el.in, doc/org/init.el.in: Define org-babel-temporary-directory and create the directory.
-
- 15 Mar, 2017 6 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* spot/parsetl/parsetl.yy: Adjust one diagnostic. * spot/parsetl/scantl.ll: Fix recovering of missing closing brace in lenient mode. * tests/python/declenv.py: Move some tests... * tests/python/ltlparse.py: ... here, and add many more. * NEWS: Mention the lenient mode bug.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* NEWS, configure.ac: Here.
-
Alexandre Duret-Lutz authored
* configure.ac, NEWS, doc/org/setup.org: Bump version to 2.3.2.
-
- 14 Mar, 2017 8 commits
-
-
Alexandre Duret-Lutz authored
Fixes #243. * doc/tl/tl.tex: Here.
-
Alexandre Duret-Lutz authored
Fixes #243. * doc/tl/tl.tex: Here.
-
Alexandre Duret-Lutz authored
* m4/gccwarns.m4: Add -Wno-gnu to workaround a diagnostic from clang 3.9.1 on arch Linux. clang was complaining whtat assert() is using a GNU extension.
-
Alexandre Duret-Lutz authored
* doc/org/tut24.org: Add missing section title. * doc/org/spot.css: Style h3 headings, and remove some useless lines.
-
Alexandre Duret-Lutz authored
* src/bddio.c, src/bddop.c, src/imatrix.c, src/pairs.c: Here.
-
Alexandre Duret-Lutz authored
Fixes #242. * doc/tl/tl.tex: Remove incorrect claim that {r} does not match the PSL semantics.
-
Alexandre Duret-Lutz authored
* m4/gccwarns.m4: Add -Wno-gnu to workaround a diagnostic from clang 3.9.1 on arch Linux. clang was complaining whtat assert() is using a GNU extension.
-
Alexandre Duret-Lutz authored
* doc/org/tut24.org: Add missing section title. * doc/org/spot.css: Style h3 headings, and remove some useless lines.
-
- 13 Mar, 2017 2 commits
-
-
Alexandre Duret-Lutz authored
* src/bddio.c, src/bddop.c, src/imatrix.c, src/pairs.c: Here.
-
Alexandre Duret-Lutz authored
Fixes #242. * doc/tl/tl.tex: Remove incorrect claim that {r} does not match the PSL semantics.
-