GitLab

Fixes #80.

* bin/genltl.cc: Add --kr-n2, --kr-nlogn and --kr-n.
* bin/man/genltl.x: Add the paper in the documentation.
* tests/core/genltl.test: Test them.

Fixes #208

* NEWS: Informations about the modifications
* spot/twaalgos/dot.cc (print): Gestion of cluster for
universal transitions
* tests/core/alternating.test: tests added
* tests/core/neverclaimread.test: tests changed for
new dot format
* tests/core/readsave.test: tests changed
* tests/core/sccdot.test: tests changed
* tests/python/_altscc.ipynb: tests changed
* tests/python/decompose.ipynb: tests changed

Fixes #207

* NEWS: Informations about the option 'y' for --dot added
* bin/common_aoutput.cc: Documentation for the option 'y'
for --dot added
* spot/twaalgos/dot.cc (print_dst, process_link): Functions
modified for the new option
* tests/core/alternating.test: Tests added

* tests/ltsmin/README: this fixes #230.

* HACKING, configure.ac: here.

Part of #212.

* spot/misc/common.hh (SPOT_DEPRECATED): Improve support current
compilers and options flags.
* spot/twa/twagraph.hh, spot/graph/graph.hh (is_alternating): Mark it
as deprecated.
(is_existential): New method.
* bin/autfilt.cc, bin/ltlcross.cc, spot/parseaut/parseaut.yy,
spot/twa/twa.cc, spot/twa/twagraph.cc, spot/twaalgos/alternation.cc,
spot/twaalgos/are_isomorphic.cc, spot/twaalgos/canonicalize.cc,
spot/twaalgos/couvreurnew.cc, spot/twaalgos/cycles.cc,
spot/twaalgos/degen.cc, spot/twaalgos/determinize.cc,
spot/twaalgos/dot.cc, spot/twaalgos/dtbasat.cc,
spot/twaalgos/dtwasat.cc, spot/twaalgos/hoa.cc,
spot/twaalgos/isunamb.cc, spot/twaalgos/isweakscc.cc,
spot/twaalgos/mask.hh, spot/twaalgos/minimize.cc,
spot/twaalgos/postproc.cc, spot/twaalgos/product.cc,
spot/twaalgos/randomize.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc,
spot/twaalgos/sccinfo.cc, spot/twaalgos/simulation.cc,
spot/twaalgos/strength.cc, tests/core/graph.cc, tests/core/ngraph.cc,
tests/python/alternating.py: Adjust all uses.
* NEWS: Mention the renaming.

Fixes #220.

* m4/pypath.m4: Here.
* NEWS: Mention the bug.

Fixes #218.

* spot/twaalgos/alternation.cc: Adjust check.
* tests/core/alternating.test: Add test case from #218.
* NEWS: Mention the bug.

Suggested by Akim Demaille.

* bin/ltlcross.cc: Change the colors, and add ':' at
the end of some error message.
* NEWS: Mention the color change.
* doc/org/ltlcross.org: Adjust examples.

* spot/twaalgos/emptiness.cc, spot/twaalgos/emptiness.hh: Here.
* tests/python/ltsmin-dve.ipynb: Add a test.
* NEWS: Mention the change.

* spot/misc/casts.hh: New inline functions and compile-time checks.
* spot/kripke/kripkegraph.hh, spot/ta/taexplicit.cc,
  spot/ta/taproduct.cc, spot/ta/tgtaproduct.cc, spot/taalgos/tgba2ta.cc,
  spot/twa/taatgba.hh, spot/twa/taatgba.cc, spot/twa/twagraph.hh,
  spot/twa/twaproduct.cc, spot/twaalgos/emptiness.cc,
  spot/twaalgos/stutter.cc, spot/ltsmin/ltsmin.cc, tests/core/ikwiad.cc,
  tests/core/ngraph.cc: Remove downcast checks from code.

* tests/sanity/style.test: Filter out static_assert.

Fixes #213.

* doc/org/.dir-locals.el.in, doc/org/init.el.in: Adjust location of
plantuml.jar.

* doc/Makefile.am, elisp/Makefile.am: here.
* HACKING: add missing requirements.

* tests/core/hierarchy.test: here.

* m4/gccwarns.m4: Add more flags taken from Spot.
Also add -Wno-long-long to suppress one warning.

* src/bddop.c: Empty macro arguments are undefined ISO C90 and
ISO C++98.  Use '+' when calling APPLY_SHORTCUTS.
* src/fdd.c, src/kernel.c: Avoid constructs invalid in C90.
* src/bddop.c, src/bddx.h, src/kernel.c, src/kernel.h,
examples/cmilner/cmilner.c: Remove C++ comments.

Fixes #214.

* m4/gccwarn.m4: Add -Wpedantic.

Fixes #215, reported by Thibaud Michaud.

Also related to GCC bug 79301.

* spot/misc/common.hh: Here.

* spot/ltsmin/ltsmin.cc: Here.

* spot/ltsmin/ltsmin.cc: Here.

* spot/priv/weight.cc, spot/priv/weight.hh,
spot/twaalgos/determinize.cc, spot/twaalgos/stats.cc: Here.

For #214, as observed by Thibaud Michaud.

* spot/twa/acc.hh: Name the anonymous struct.
* spot/twa/acc.hh, spot/twa/acc.cc, spot/parseaut/parseaut.yy,
spot/twaalgos/dtwasat.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/sepsets.cc, spot/twaalgos/totgba.cc: Adjust all usages.
* NEWS: Mention the renaming.

* HACKING: fix command-line invokation of make check for Teamcity.

Fixes #210.

* doc/org/ltldo.org: Actually execute the code writing sample.ltl, and
remove the file once it is not used anymore.

Fixes #206.

* bin/ltldo.cc: Implement --smallest and --greatest.
* tests/core/ltldo2.test: Test them.
* NEWS, doc/org/ltldo.org: Document them.

* tests/Makefile.am: Remove TEST_EXTENSIONS + typos.

* spot/ltsmin/ltsmin.cc: Here.  This fixes 5a441e1b.

* spot/ltsmin/ltsmin.cc: Do not forget to register dead.
* spot/twa/twaproduct.cc: Use copy_ap_of() instead of
register_all_propositions_of() because the latter does
do update ap().

* NEWS, configure.ac: Here.

* configure.ac, doc/org/setup.org, NEWS: Bump version to 2.3.

* doc/org/index.org: Add links to the hierarchy and sat-minimization.
* doc/org/satmin.org: Show how to use glucose.