- 26 Oct, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
* NEWS, configure.ac, doc/org/setup.org: Bump version to 2.11.2.
-
- 19 Oct, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
Based on a request from Pierre Ganty. * spot/twaalgos/stats.cc, spot/twaalgos/stats.hh, bin/common_aoutput.cc, bin/common_aoutput.hh: Implement those options. * tests/core/format.test: Add test case. * doc/org/autfilt.org: Update doc. * NEWS: Mention them.
-
- 17 Oct, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
* spot/twaalgos/parity.cc: Implement it. * spot/twaalgos/parity.hh, NEWS: Document it. * tests/python/parity.ipynb: Demonstrate it. This is the only test so far, but more uses are coming.
-
- 13 Oct, 2022 2 commits
-
-
Alexandre Duret-Lutz authored
* spot/tl/relabel.cc (formula_to_fgraph): Do not assume that n-ary operators are Boolean operators. * tests/python/relabel.py: Add a test case found while discussing some expression with Antoine Martin. * NEWS: Mention it.
-
Alexandre Duret-Lutz authored
-
- 10 Oct, 2022 2 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* NEWS, configure.ac, doc/org/setup.org: Update.
-
- 08 Oct, 2022 2 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* NEWS, configure.ac, doc/org/setup.org: Update version.
-
- 05 Oct, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
* spot/twaalgos/translate.cc: When producing Parity output, split LTL as we do in the Generic case. * spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Use acd_transform() and add an "acd" option to disable this. * bin/spot-x.cc, NEWS: Document this. * tests/core/genltl.test, tests/core/minusx.test, tests/core/parity2.test: Adjust test cases for improved outputs.
-
- 04 Oct, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
For issue #512 * README: Update instructions. * configure.ac: Add some code to warn if Python files will be installed in a place that is not searched up by default. Add --with-pythondir support. * NEWS: Mention --with-pythondir.
-
- 23 Sep, 2022 4 commits
-
-
Alexandre Duret-Lutz authored
As LRDE is being renamed LRE, gitlab is one of the first URL to migrate. The old URL is still supported, but we want to only use the new one eventually. * .dir-locals.el, .gitlab-ci.yml, HACKING, NEWS, doc/org/concepts.org, doc/org/install.org, doc/org/setup.org, elisp/Makefile.am, elisp/hoa-mode.el, tests/ltsmin/README: Update to the new gitlab URL.
-
Alexandre Duret-Lutz authored
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Here. * NEWS, bin/spot-x.cc: Mention it. * tests/core/genltl.test: Test it.
-
Alexandre Duret-Lutz authored
Based on a mail from Edmond Irani Liu. The test case also serves for the previous patch. * bin/genltl.cc, spot/gen/formulas.cc, spot/gen/formulas.hh: Add it. * NEWS: Mention it. * tests/core/genltl.test: Test it.
-
Alexandre Duret-Lutz authored
This is motivated by an example sent by Edmond Irani Liu, that will be tested in next patch. * spot/twaalgos/dbranch.cc, spot/twaalgos/dbranch.hh: New files. * python/spot/impl.i, spot/twaalgos/Makefile.am: Add them. * spot/twaalgos/translate.cc: Call delay_branching_here unconditionally. * spot/twa/twagraph.cc (defrag_states): Do not assume that games are alternating. * tests/core/genltl.test: Adjust expected numbers. * tests/python/dbranch.py: New file. * tests/Makefile.am: Add it.
-
- 14 Sep, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
* bin/ltlsynt.cc: Implement these options. * bin/common_aoutput.hh, bin/common_aoutput.cc (automaton_format_opt): Make extern. * NEWS: Mention the new options. * doc/org/ltlsynt.org: Use dot output in documentation. * tests/core/ltlsynt.test: Quick test of the new options.
-
- 13 Sep, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Introduce a merge-states-min option. * bin/spot-x.cc: Document it. * spot/gen/automata.cc, spot/gen/automata.hh, bin/genaut.cc: Add option to generate cyclist test cases. * NEWS: Document the above. * tests/core/included.test: Add test cases that used to be too slow.
-
- 12 Sep, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
* spot/twaalgos/degen.hh, spot/twaalgos/degen.cc: Adjust degeneralize() and degeneralize_tba() to work on generalized-co-Büchi. * NEWS: Mention this. * spot/twaalgos/cobuchi.hh, spot/twaalgos/cobuchi.cc (to_nca): Use degeneralization on generalized-co-Büchi. * spot/twaalgos/postproc.cc: Use degeneralization for generalized co-Büchi as well. * bin/autfilt.cc: Improve chain products of co-Büchi automata by using generalization if too many colors are needed. * tests/core/prodchain.test, tests/python/pdegen.py: Add test cases.
-
- 06 Sep, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
Improve the construction of the above constructions, saving colors. * spot/twaalgos/product.cc: Here. * spot/twaalgos/product.hh, NEWS: Mention it. * tests/core/prodchain.test, tests/core/prodor.test, tests/python/_product_weak.ipynb: Adjust.
-
- 14 Aug, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
* python/spot/impl.i: Make parallel_policy implicitly contractible. * spot/graph/graph.hh (sort_edges_srcfirst_): Pass a parallel_policy explicitly. * spot/twa/twagraph.hh, spot/twa/twagraph.cc (merge_states): Likewise. * spot/misc/common.cc: Remove file. * spot/misc/common.hh (set_nthreads, get_nthreads): Remove, and replace with... (parallel_policy): ... this. * spot/misc/Makefile.am, tests/python/mergedge.py, NEWS: Adjust.
-
- 23 Jul, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
* NEWS: Mention those change. * spot/twaalgos/game.hh (print_pg): New function. (pg_print): Mark as deprecated. * spot/twaalgos/game.cc (pg_print): Redirect to print_pg(). (print_pg): Update to output state names. * python/spot/__init__.py: Teach to_str() about print_pg(). * bin/ltlsynt.cc: Adjust to call print_pg(). * tests/python/games.ipynb: Add an example. * tests/core/ltlsynt.test: Adjust to remove the "INIT" note.
-
- 22 Jul, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
* spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll: Add rules for PGSolver's format. * spot/parseaut/public.hh: PGAME is a new type of output. * tests/core/pgsolver.test: New file. * tests/Makefile.am: Add it. * tests/python/games.ipynb: More exemples. * NEWS: Mention the new feature.
-
- 23 Jun, 2022 3 commits
-
-
Alexandre Duret-Lutz authored
Fixes #509. * spot/parseaut/scanaut.ll: Reset ->str whenever a [ is read, so that we do not attempt to clear ->str while reading garbage. * NEWS: Mention the bug. * tests/core/parseaut.test: Test it.
-
Alexandre Duret-Lutz authored
* spot/twaalgos/dot.cc: Quote identifiers containing a minus. * tests/core/alternating.test: Add test case. * NEWS: Mention the bug.
-
Alexandre Duret-Lutz authored
* spot/graph/graph.hh: Use a temporary array to store the destination vector if the passed range belong to the dests_ vector. Otherwise the passed begin/end risk being invalidated when dests_ is reallocated. * NEWS: Mention the bug.
-
- 22 Jun, 2022 2 commits
-
-
Alexandre Duret-Lutz authored
This was triggered by a question from Pierre Ganty on the mailing list. * spot/twaalgos/contains.hh, spot/twaalgos/contains.cc (contains): Generalize second argument to const_twa_ptr instead of const_twa_graph_ptr. * NEWS: Mention this. * tests/python/ltsmin-pml.ipynb: Show that it work. * THANKS: Mention Pierre.
-
Alexandre Duret-Lutz authored
* bin/common_file.cc, bin/common_file.hh (output_file): Add a force_append option. * bin/ltlsynt.cc: Implement the --from-pgame option, and fix suppot for --csv when multiple inputs are processed. * NEWS: Mention the new option. * tests/core/syfco.test: Add a test case. * tests/core/ltlsynt-pgame.test: New file. * tests/Makefile.am: Add it.
-
- 21 Jun, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
* NEWS, README, doc/org/compile.org: Mention the option and its effect on compilation requirements. * configure.ac: Add the --enable-pthread option, and ENABLE_PTHREAD macro. * doc/org/g++wrap.in, spot/Makefile.am, spot/libspot.pc.in: Compile with -pthread conditionally. * spot/graph/graph.hh, spot/twa/twagraph.cc: Adjust the code to not use thread-local variables, and let the pthread code be optional. * .gitlab-ci.yml: Activate --enable-pthread in two configurations.
-
- 24 May, 2022 1 commit
-
-
Philipp Schlehuber authored
* NEWS: Announce * spot/Makefile.am: Add pthread to use threads * spot/misc/common.cc, spot/misc/common.hh: Add variable + getter/setter * spot/misc/Makefile.am: Add common.cc
-
- 20 May, 2022 2 commits
-
-
Alexandre Duret-Lutz authored
This largely speeds up the computation for conditions like "Rabin n" sharing a lot of subtrees. Also implement options to stop the construction if the shape is wrong. * spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh: Implement the cache and the options. * tests/python/zlktree.ipynb, tests/python/zlktree.py: New tests.
-
Alexandre Duret-Lutz authored
* spot/twaalgos/complete.hh: Adjust documentation. * spot/twaalgos/complete.cc: If the acceptance condition is a tautology, delay the forcing of Büchi acceptance until we are sure it is needed. * NEWS: Mention the change.
-
- 18 May, 2022 5 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* NEWS, configure.ac, doc/org/setup.org: Set version to 2.10.6.
-
Alexandre Duret-Lutz authored
* bin/common_finput.cc (job_processor::process_file): Reset col_to_read. * tests/core/ltlfilt.test: Test it. * NEWS: Mention the bug.
-
Alexandre Duret-Lutz authored
Patch by Shachar Itzhaky. * spot/parseaut/scanaut.ll, spot/parsetl/scantl.ll: Include libc-config.h instead of config.h. * NEWS: Mention the fix. * THANKS: Add Shachar.
-
Alexandre Duret-Lutz authored
Fix #505, Reported by Edmond Irani Liu. * spot/twa/twagraph.cc (copy): Deal with kripke_graph in a better way. * spot/twaalgos/hoa.cc: Do not force the use of named-states since when the input is a kripke_graph. * tests/python/kripke.py: Adjust test cases. * NEWS: Mention the change. * THANKS: Add Edmund.
-
- 17 May, 2022 2 commits
-
-
Alexandre Duret-Lutz authored
* bin/common_finput.cc (job_processor::process_file): Reset col_to_read. * tests/core/ltlfilt.test: Test it. * NEWS: Mention the bug.
-
Alexandre Duret-Lutz authored
Patch by Shachar Itzhaky. * spot/parseaut/scanaut.ll, spot/parsetl/scantl.ll: Include libc-config.h instead of config.h. * NEWS: Mention the fix. * THANKS: Add Shachar.
-
- 09 May, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
Fix #505, Reported by Edmond Irani Liu. * spot/twa/twagraph.cc (copy): Deal with kripke_graph in a better way. * spot/twaalgos/hoa.cc: Do not force the use of named-states since when the input is a kripke_graph. * tests/python/kripke.py: Adjust test cases. * NEWS: Mention the change. * THANKS: Add Edmund.
-
- 03 May, 2022 1 commit
-
-
Alexandre Duret-Lutz authored
-