- 29 Jul, 2020 2 commits
-
-
Alexandre Duret-Lutz authored
* spot/twaalgos/toparity.cc: Do not call prpagate_marks_here twice if the automaton was not degeneralized. * spot/twaalgos/toparity.hh: Typo in comment.
-
Alexandre Duret-Lutz authored
Fixes #403. * spot/twaalgos/cleanacc.cc (simplify_complementary_marks_here): Assume that two colors are complementary in a broad sense, i.e., on is present if (but not only if) the other is missing before applying those rewritings. Technically, this is usually not necessary, because the changes done in #418 will cause such "covering-the-full-automaton" pair of colors to be disjoint so complementary in a strict sense. It might make a difference (this is not tested) in presence of reused colors which #418 cannot remove. In any case, it's simply less code to implement the broad sense. * tests/python/toparity.py: Add test case from #403, which is reduced to two states with recent optimizations.
-
- 28 Jul, 2020 4 commits
-
-
Alexandre Duret-Lutz authored
This fixes issue #418. * spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::acc_code::useless_colors_patterns): New method to detect patterns of colors allowing other colors to be added or removed at will. * spot/twaalgos/cleanacc.cc (simplify_acceptance_here): Use the above patterns to remove some useless colors from transitions and hope that this can help simplify the acceptance condition. * spot/twaalgos/degen.cc (propagate_marks_vector): Use the pattern to add more colors. * tests/core/ltl2tgba2.test: Add the test case from issue #418. * tests/core/ltl2dstar4.test, tests/core/satmin3.test, tests/core/sccdot.test, tests/core/sim3.test, tests/python/automata.ipynb, tests/python/decompose.ipynb, tests/python/merge.py, tests/python/pdegen.py, tests/python/remfin.py, tests/python/toparity.py, tests/python/tra2tba.py: Adjust all test cases. * NEWS: Mention this new feature.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* spot/twaalgos/cleanacc.cc (merge_identical_marks_here, merge_mark, included_marks): Fuse these into ... (simplify_included_marks_here): ... this new function. * NEWS: Mention the fix of issue #406.
-
Alexandre Duret-Lutz authored
* lib/argp-help.c (hol_entry_help): Handle cases with option description is larger than RMARGIN.
-
- 27 Jul, 2020 4 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* doc/org/spot.css: Display input and output closer and separate them with dash.
-
Alexandre Duret-Lutz authored
* spot/twaalgos/remfin.cc: Actually use propmarks. * tests/core/det.test, tests/core/remfin.test, tests/python/automata.ipynb, tests/python/remfin.py, tests/python/tra2tba.py: Adjust test cases.
-
Alexandre Duret-Lutz authored
-
- 25 Jul, 2020 1 commit
-
-
Florian Renkin authored
This fixes #406. * spot/twaalgos/cleanacc.cc: Add the simplification. * tests/core/remfin.test, tests/python/automata.ipynb, tests/python/remfin.py: Update tests. * tests/python/simplacc.py: Update and add tests.
-
- 24 Jul, 2020 3 commits
-
-
Alexandre Duret-Lutz authored
* spot/twaalgos/remfin.cc (tra_to_tba): Implement the same optimization has in the generic remove_fin transformation. * tests/python/tra2tba.py: Adjust.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
Do not clone transitions that are necessarily part of on accepting cycle in the main copy of the automaton. * spot/twaalgos/remfin.cc: Use propagate_marks_vector to ignore more edges. * tests/core/remfin.test, tests/python/remfin.py, tests/python/automata.ipynb: Adjust. * tests/sanity/style.test: Do not choke on C++17 if statements with initializer.
-
- 23 Jul, 2020 1 commit
-
-
Alexandre Duret-Lutz authored
* doc/org/hierarchy.tex: Draw the shadow manually, so that it is part of the bounding box when we extract the SVG.
-
- 22 Jul, 2020 5 commits
-
-
Alexandre Duret-Lutz authored
This fixes #412. * spot/twaalgos/translate.cc: Add the quick syntactic simplification. * spot/twaalgos/relabel.cc: Do not register old unused APs. * tests/core/ltl2tgba2.test: Add test case. * tests/core/bdd.test, tests/python/automata.ipynb: Adjust. * NEWS: Mention this.
-
Alexandre Duret-Lutz authored
Under that option, !(a ^ b) was converted to (!a <=> !b) instead of simply (a <=> b). * spot/tl/simplify.cc (equiv_or_xor): Improve rewriting. * tests/core/ltl2tgba2.test, tests/python/simstate.py: Adjust test cases.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* configure.ac, NEWS, doc/org/setup.org: Set version to 2.9.3.
-
- 21 Jul, 2020 9 commits
-
-
Alexandre Duret-Lutz authored
* doc/org/autcross.org, doc/org/autfilt.org, doc/org/citing.org, doc/org/compile.org, doc/org/concepts.org, doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genaut.org, doc/org/genltl.org, doc/org/hierarchy.org, doc/org/hoa.org, doc/org/index.org, doc/org/install.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltlfilt.org, doc/org/ltlgrind.org, doc/org/ltlsynt.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org, doc/org/satmin.org, doc/org/tut.org, doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org, doc/org/tut04.org, doc/org/tut10.org, doc/org/tut11.org, doc/org/tut12.org, doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.org, doc/org/tut23.org, doc/org/tut24.org, doc/org/tut30.org, doc/org/tut31.org, doc/org/tut50.org, doc/org/tut51.org, doc/org/tut52.org, doc/org/tut90.org, doc/org/upgrade2.org: Run ispell-buffer on all these. * bin/autfilt.cc, python/spot/__init__.py: Fix typos in help texts noticed while spell-checking the org files.
-
Alexandre Duret-Lutz authored
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Set the SPOT_UNINSTALLED envvar, as we already do in the test suite.
-
Alexandre Duret-Lutz authored
Reported by Salomon Sickert. * bin/ltlcross.cc: Also call determinize_unknown_acceptance() for positive automata. * tests/core/ltlcross3.test: Add another test case. * NEWS: Mention the fix.
-
Alexandre Duret-Lutz authored
* doc/org/autcross.org, doc/org/autfilt.org, doc/org/citing.org, doc/org/compile.org, doc/org/concepts.org, doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genaut.org, doc/org/genltl.org, doc/org/hierarchy.org, doc/org/hoa.org, doc/org/index.org, doc/org/install.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltlfilt.org, doc/org/ltlgrind.org, doc/org/ltlsynt.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org, doc/org/satmin.org, doc/org/tut.org, doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org, doc/org/tut04.org, doc/org/tut10.org, doc/org/tut11.org, doc/org/tut12.org, doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.org, doc/org/tut23.org, doc/org/tut24.org, doc/org/tut30.org, doc/org/tut31.org, doc/org/tut50.org, doc/org/tut51.org, doc/org/tut52.org, doc/org/tut90.org, doc/org/upgrade2.org: Run ispell-buffer on all these. * bin/autfilt.cc, python/spot/__init__.py: Fix typos in help texts noticed while spell-checking the org files.
-
Alexandre Duret-Lutz authored
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Set the SPOT_UNINSTALLED envvar, as we already do in the test suite.
-
Alexandre Duret-Lutz authored
Reported by Salomon Sickert. * bin/ltlcross.cc: Also call determinize_unknown_acceptance() for positive automata. * tests/core/ltlcross3.test: Add another test case. * NEWS: Mention the fix.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* configure.ac, NEWS, doc/org/setup.org: Set version to 2.9.2.
-
- 20 Jul, 2020 4 commits
-
-
Alexandre Duret-Lutz authored
Fixes #420 reported by Salomon Sickert. * bin/ltlcross.cc: Call determine_unknown_acceptance(). * spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Document that one_accepting_scc()==-1 can mean "don't know", and update determine_unknown_acceptance() to set one_acc_scc_. * tests/core/ltlcross3.test: Add test case. * NEWS: Mention the fixes.
-
Alexandre Duret-Lutz authored
* spot/tl/formula.hh (formula::operator bool): Mark as noexcept. * bin/common_trans.hh, bin/common_trans.cc: Use std::atomic instead of volatile.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
Fixes #420 reported by Salomon Sickert. * bin/ltlcross.cc: Call determine_unknown_acceptance(). * spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Document that one_accepting_scc()==-1 can mean "don't know", and update determine_unknown_acceptance() to set one_acc_scc_. * tests/core/ltlcross3.test: Add test case. * NEWS: Mention the fixes.
-
- 17 Jul, 2020 2 commits
-
-
Etienne Renault authored
* configure.ac: Here.
-
Alexandre Duret-Lutz authored
* spot/tl/formula.hh (formula::operator bool): Make it explicit. When compiling in C++20 mode with g++ 10.1, this bool operator was used instead of the comparison operators while looking up a std::pair<formula,formula> in a hash map, causing many test suite failures. This problem does not occur with clang++ 10.0, so it might just be a bug in g++ 10.1. But having explicit operator bool is good practice anyway.
-
- 16 Jul, 2020 5 commits
-
-
Alexandre Duret-Lutz authored
With GCC 10.1 all comparisons that default to the <=> C++20 comparison operator emit a spurious zero-as-null-pointer-constant warning, which is an error in our configuration. This is due to an implementation choice in the libstdc++ library, so it also causes warning from clang++ 10.0 when using the same libstdc++ library. A fix for GCC PR95242 was committed in g++ (not in libstdc++), so while g++ 10.2 might be fixed, clang++ will need a similar fix. I've seen those failures on Arch linux with gcc 10.1.0-2 and clang 10.0.0-3. On Debian sid, g++ 10.1.0-4 seems to already include the fix. * m4/gccwarn.m4: Include a string comparison in the test code so that -Wzero-as-null-pointer-constant is not enabled if it would produce warnings on such statements.
-
Alexandre Duret-Lutz authored
* spot/tl/formula.hh (formula::operator bool): Mark as noexcept. * bin/common_trans.hh, bin/common_trans.cc: Use std::atomic instead of volatile.
-
Alexandre Duret-Lutz authored
* configure.ac: Activate C++17, and replace --enable-c++17 by --enable-c++20.
-
Alexandre Duret-Lutz authored
* configure.ac: Activate C++17, and replace --enable-c++17 by --enable-c++20. * NEWS: Mention the news. * .gitlab-ci.yml: Use C++20 for the former C++17 builds. * HACKING, README, doc/org/compile.org, doc/org/concepts.org, doc/org/index.org, doc/org/install.org, doc/org/tut.org, doc/org/upgrade2.org, spot/misc/escape.hh: Adjust mentions of C++14.
-
Alexandre Duret-Lutz authored
-