Commit graph

4129 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
a2f174f721 [buddy] fix some -Wpedantic messages
* 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.
2017-02-01 18:50:37 +01:00
Alexandre Duret-Lutz
f0edfdef2b activate -Wpedantic
Fixes #214.

* m4/gccwarn.m4: Add -Wpedantic.
2017-02-01 18:02:40 +01:00
Alexandre Duret-Lutz
d1754123a9 disable [[fallthrough]] until C++17
Fixes #215, reported by Thibaud Michaud.

Also related to GCC bug 79301.

* spot/misc/common.hh: Here.
2017-02-01 18:02:40 +01:00
Alexandre Duret-Lutz
fac610ac48 ltsmin: fix function pointer casts for -Wpedantic
* spot/ltsmin/ltsmin.cc: Here.
2017-02-01 18:02:40 +01:00
Alexandre Duret-Lutz
43d57da7f3 ltsmin: do not use 0-length arrays for -Wpedantic
* spot/ltsmin/ltsmin.cc: Here.
2017-02-01 18:02:40 +01:00
Alexandre Duret-Lutz
825c8a8ad9 remove stray semi-colons reported by -Wpedantic
* spot/priv/weight.cc, spot/priv/weight.hh,
spot/twaalgos/determinize.cc, spot/twaalgos/stats.cc: Here.
2017-02-01 18:02:40 +01:00
Alexandre Duret-Lutz
70c70a63a3 do not use non-standard anonymous structs
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.
2017-02-01 18:02:40 +01:00
Maximilien Colange
954b9d2074 Update doc to reflect changes to Teamcity invokation.
* HACKING: fix command-line invokation of make check for Teamcity.
2017-02-01 16:32:12 +01:00
Alexandre Duret-Lutz
0ada5900de ltldo.org: Fix first examples
Fixes #210.

* doc/org/ltldo.org: Actually execute the code writing sample.ltl, and
remove the file once it is not used anymore.
2017-01-27 20:35:40 +01:00
Alexandre Duret-Lutz
a4b575db1c ltldo: add portfolio options
Fixes #206.

* bin/ltldo.cc: Implement --smallest and --greatest.
* tests/core/ltldo2.test: Test them.
* NEWS, doc/org/ltldo.org: Document them.
2017-01-27 20:35:40 +01:00
Alexandre Duret-Lutz
267f819a9d * doc/org/tut51.org: Typo. 2017-01-27 13:11:20 +01:00
Maximilien Colange
6acb168a5d Do not specify tests extensions as we use a unique runner.
* tests/Makefile.am: Remove TEST_EXTENSIONS + typos.
2017-01-23 09:40:15 +01:00
Alexandre Duret-Lutz
423136a6e0 ltsmin: register dead only if it is an atomic proposition
* spot/ltsmin/ltsmin.cc: Here.  This fixes 5a441e1b.
2017-01-21 18:24:43 +01:00
Alexandre Duret-Lutz
5a441e1b93 fix some incorrect AP registrations
* 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().
2017-01-20 14:41:00 +01:00
Alexandre Duret-Lutz
7f219f2738 * NEWS: Typos. 2017-01-19 14:26:16 +01:00
Alexandre Duret-Lutz
a84f9cddcf Bump version to 2.3.0.dev
* NEWS, configure.ac: Here.
2017-01-19 13:37:52 +01:00
Alexandre Duret-Lutz
6d032597bf Release Spot 2.3
* configure.ac, doc/org/setup.org, NEWS: Bump version to 2.3.
2017-01-19 09:25:22 +01:00
Alexandre Duret-Lutz
21e2d9bb32 org: a few additional links
* doc/org/index.org: Add links to the hierarchy and sat-minimization.
* doc/org/satmin.org: Show how to use glucose.
2017-01-19 09:18:25 +01:00
Alexandre Duret-Lutz
8f9d165cfa * NEWS: Improve for upcoming release. 2017-01-18 22:27:24 +01:00
Alexandre Duret-Lutz
ff4c4a7231 python: render the M&P hierarchy in SVG
* python/spot/__init__.py (show_mp_hierarchy, mp_hierarchy_svg): New
functions.
* tests/python/formulas.ipynb: Illustrate show_mp_hierarchy.
* python/ajax/spotcgi.in: Use mp_hierarchy_svg.
* python/ajax/css/trans.css: Adjust for possible overflows.
* NEWS: Mention this new feature.
2017-01-18 20:58:20 +01:00
Alexandre Duret-Lutz
0e2ab5de53 git rid of std::iterator
Fixes #194.

* spot/graph/graph.hh: Here.
2017-01-18 10:30:10 +01:00
Alexandre Duret-Lutz
d80ca1fb47 sat: reject alternating inputs
* spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc: Here.
2017-01-18 08:08:08 +01:00
Alexandre Duret-Lutz
5939ca4e85 langmap: Add example in notebook
* tests/python/highlighting.ipynb: Add an example of
highlight_languages().
2017-01-17 22:53:20 +01:00
Alexandre Duret-Lutz
0ad62cb97b langmap: adjust to only color non-unique languages
Fixes #203.

* spot/twaalgos/langmap.hh (highlight_languages): Simplify the
interface by only taking the automaton to color.
* spot/twaalgos/langmap.cc (highlight_languages): Only introduce
color for states that have a non-unique language.
* tests/core/highlightstate.test: Update and add more tests.
* tests/python/langmap.py: Keep the tests simple.
* bin/autfilt.cc: Adjust usage and help string.
2017-01-17 21:58:03 +01:00
Alexandre Duret-Lutz
aa457a204d tmpfile: remove deprecated throw specifiers
* spot/misc/tmpfile.cc, spot/misc/tmpfile.hh: Remove throw specifier
to suppress a deprecation warning from g++ 7.
2017-01-16 15:39:05 +01:00
Alexandre GBAGUIDI AISSE
4eebe94a1d TYPOS
* NEWS: typo.
* bench/dtgbasat/config.bench: typo.
* bench/dtgbasat/gen.py: typo.
* bench/dtgbasat/stat-gen.sh: typo.
* doc/org/concepts.org: typo.
2017-01-16 13:38:12 +01:00
Alexandre Duret-Lutz
ebdb198b64 hierarchy: expose mp_class to python
* bin/common_output.cc: Move some of the printing code...
* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: ... here, as new
  variants of mp_class...
* python/spot/impl.i: ... that we can now call from Python.
* python/ajax/spotcgi.in: Use those to simplify and extend
the code printing class membership.
2017-01-14 23:43:01 +01:00
Alexandre Duret-Lutz
a0891fde18 install pkg-config configuration files
Suggested by Jeroen Meijer.

* spot/libspot.pc.in, spot/ltsmin/libspotltsmin.pc.in: New file.
* spot/Makefile.am, spot/ltsmin/Makefile.am: Distribute them, and
install their derived version.
* spot/.gitignore: Ignore *.pc files.
* debian/libbddx-dev.install, debian/libspot-dev.install: Ship
those *.pc files.
* NEWS: Mention it.
2017-01-14 17:56:05 +01:00
Alexandre Duret-Lutz
a9b056baa4 [buddy] install a pkg-config file
* src/libbddx.pc.in: New file.
* src/Makefile.am: Generate libbddx.pc, and install it.
Distribute libbddx.pc.in.
* src/.gitignore: Ignore *.pc.
2017-01-14 17:55:58 +01:00
Alexandre Duret-Lutz
c7141bd189 ltlcross: disable products columns in CSV if --products=0
* bin/ltlcross.cc: Fix it.
* tests/core/ltlcross3.test: Test it.
* NEWS: Mention the bug.
2017-01-14 10:43:35 +01:00
Alexandre Duret-Lutz
b210db8949 sat_minimize: do not complete in the preproc step
Fixes #204.

* spot/twaalgos/dtwasat.cc (sat_minimize): Here.
* tests/core/satmin2.test: Add a test case.
* NEWS: Mention the bug.
2017-01-14 10:18:16 +01:00
Alexandre Duret-Lutz
3ff2acb397 alternation: better detection of non-weak alternating automata
* spot/twaalgos/alternation.cc: Fix the code to also check the
weakness of single-state SCCs.
* tests/core/alternating.test: Add a test from ltl3hoa.
2017-01-14 10:02:37 +01:00
Alexandre Duret-Lutz
7574d6d1e2 debian: distribute static libraries
Suggested by Jeroen Meijer.

* debian/rules: Enable static libraries.
* debian/libbddx-dev.install, debian/libspot-dev.install: Distribute
them.
* THANKS: Add Jeroen.
* NEWS: Mention the change.
2017-01-14 09:29:32 +01:00
Alexandre Duret-Lutz
01838a2456 ltlcross, ltldo: Add support for ltl3hoa.
* bin/common_trans.cc: Add shorthand for ltl3hoa.
* NEWS, doc/org/ltlcross.org, doc/org/ltldo.org: Mention it.
2017-01-13 22:12:43 +01:00
Alexandre Duret-Lutz
43520a3e87 ltlcross, ltldo: add a --relabel option
* bin/common_trans.cc, bin/common_trans.hh: Add the --relabel option.
* bin/ltlcross.cc, bin/ltldo.cc: Implement it.
* doc/org/ltldo.org, NEWS: Document it.
* tests/core/ltl3ba.test: Test it.
2017-01-13 22:12:43 +01:00
Alexandre Duret-Lutz
b0ba6190b7 ltlcross: relabel unsupported atomic propisitions in %s
* bin/ltlcross.cc: Do it.
* bin/common_trans.cc: Adjust documentation.
* tests/core/ltl3ba.test: Test it.
* NEWS: Document it.
2017-01-13 22:12:43 +01:00
Alexandre Duret-Lutz
8754cea2ca org: some doc about the hierarchy
* doc/org/hierarchy.org, doc/org/hierarchy.tex: New files.
* doc/Makefile.am, doc/org/tools.org, NEWS: Add them.
2017-01-12 21:04:38 +01:00
Alexandre Duret-Lutz
cf9ad8ebd1 org: minor tweaks
* doc/org/ltlfilt.org: Update example.
* doc/org/ioltl.org: Explain %s briefly.
2017-01-12 21:04:38 +01:00
Alexandre Duret-Lutz
c9918f6407 minimize_wdba: fix handling of input with useless SCCs
* spot/twaalgos/minimize.cc (minimize_wdba): Diminish the color of
terminal SCCs that are incomplete, as if they had a non-accepting
sink as successor.
* spot/twaalgos/strength.hh, spot/twaalgos/strength.cc
(is_terminal_automaton): Add an option to ignore trivial SCC as we did
before, since it matters for deciding membership to the guarantee
class.
(is_safety_mwdba): Rewrite as ...
(is_safety_automaton): ... generalizating to any acceptance, and
ignoring trivial SCCs.
* bin/ltlfilt.cc, python/ajax/spotcgi.in, spot/tl/hierarchy.cc,
tests/core/ikwiad.cc: Adjust usage of is_terminal_automaton and
is_safety_automaton().
* tests/core/hierarchy.test: Add a problematic formula as test-case.
* NEWS: Mention the bug.
2017-01-12 21:02:56 +01:00
Alexandre Duret-Lutz
7d9ce0d6fc tl: mp_class() and --format=%[vw]h
Tools for deciding the class of a formula.

* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: New files.
* spot/tl/Makefile.am: Add them.
* bin/common_output.cc, bin/common_output.hh: Implement --format=%h.
* tests/core/hierarchy.test: More tests.
* NEWS: Update.
2017-01-10 22:41:11 +01:00
Alexandre Duret-Lutz
de8a248fb2 ltlfilt: add --recurrence and --persistence
* spot/twaalgos/remfin.cc, spot/twaalgos/remfin.hh
(rabin_to_buchi_maybe): Make this function public.
* bin/ltlfilt.cc: Implement the two options.
* tests/core/hierarchy.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the new options.
2017-01-10 16:11:11 +01:00
Alexandre Duret-Lutz
6190e4415b * NEWS: Some rewrites in preparation for the next release. 2017-01-10 11:06:03 +01:00
Alexandre Duret-Lutz
6c9fd5cfaf * .dir-locals.el (magit-branch-adjust-remote-upstream-alist): New. 2017-01-10 10:36:22 +01:00
Alexandre Duret-Lutz
12ecb3febf twagraph: fix purge_dead_states on alternating automata
* tests/core/alternating.test: Run some of the test through
valgrind to exhibit the bug.
* spot/twa/twagraph.cc: Fix it.
2017-01-10 10:29:32 +01:00
Alexandre GBAGUIDI AISSE
042c7a0f5b Update dtgbasat benchmark
* bench/dtgbasat/config.bench: Configuration file sample used by gen.py
* bench/dtgbasat/gen.py: Script that can generate both bench script and
pdf results.
* bench/dtgbasat/stats.sh: Change stat.sh into stat-gen.sh that will be
generated by gen.py script.
* bench/dtgbasat/Makefile.am: Add new files.
* bench/dtgbasat/README: Update README.
* bench/dtgbasat/stat-gen.sh: Add stat script generated by gen.py and
default config.bench file.
2017-01-09 22:46:43 +01:00
Alexandre GBAGUIDI AISSE
823dc56e6b Update NEWS and documentations
* NEWS: Update.
* doc/org/satmin.org: Update satmin page.
* bin/man/spot-x.x: Document SPOT_XCNF and edit SPOT_SATSOLVER.
* bin/spot-x.cc: Update satmin options.
* bin/autfilt.cc: Update satmin related documentations.
* bin/man/autfilt.x: Update autfilt options.
2017-01-06 19:53:21 +01:00
Alexandre GBAGUIDI AISSE
bd37625e49 misc: Add 'SPOT_XCNF' environment variable
* spot/misc/satsolver.cc: Handle xcnf writing.
* spot/misc/satsolver.hh: Handle xcnf writing.
2017-01-06 19:53:21 +01:00
Alexandre GBAGUIDI AISSE
ef2355a542 twaalgos: Set 'dicho' algo as default for SAT-based minimization
* python/spot/__init__.py: Handle options.
* spot/twaalgos/dtwasat.cc: Handle options.
* spot/twaalgos/postproc.cc: Handle options.
* spot/twaalgos/postproc.hh: Handle options.
* tests/core/satmin.test: Update tests.
Now use 'sat-minimize=4' to use the naive algo.
* tests/core/satmin2.test: Update tests.
Now use --sat-minimize='naive' to use the naive algo.
* tests/python/satmin.py: Update tests.
Now use 'naive=True' to use the naive algo.
2017-01-06 19:53:21 +01:00
Alexandre GBAGUIDI AISSE
67e3a4f28e spot: Add 'langmap' option with dichotomy (it helps to choose min val)
* python/spot/__init__.py: Handle 'dicho' option in 'sat_minimize'.
* spot/priv/satcommon.cc: Implement get_number_of_distinct_vals.
* spot/priv/satcommon.hh: Declare get_number_of_distinct_vals.
* spot/twaalgos/dtbasat.cc: Use get_number_of_distinct_vals.
* spot/twaalgos/dtbasat.hh: Change dichotomy function's prototype.
* spot/twaalgos/dtwasat.cc: Use get_number_of_distinct_vals.
* spot/twaalgos/dtwasat.hh: Change dichotomy function's prototype.
Handle options.
* spot/twaalgos/postproc.cc: Handle options.
* spot/twaalgos/postproc.hh: Add dicho_langmap_ var for options.
* tests/core/satmin2.test: Add tests for dichotomy.
* tests/core/satmin.test: Add tests for dichotomy.
* tests/python/satmin.py: Replace 'dichotomy' with 'dicho' option.
2017-01-06 19:53:21 +01:00
Alexandre GBAGUIDI AISSE
7046a49622 bin/autfilt.cc: Add '--highlight-languages' option
* bin/autfilt.cc: Add that option.
* tests/core/highlightstate.test: Add test.
* NEWS: Update.
2017-01-06 19:53:21 +01:00