alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
4145 commits 6 branches 0 tags 36 MiB
Commit graph

4145 commits

This branch
This branch
All branches
Author SHA1 Message Date
Etienne Renault
6be87e5bb9 configure: allows to silent compilation 
* HACKING, configure.ac: here.
 2017-02-16 14:10:25 +01:00
Alexandre Duret-Lutz
fefb375d5f is_alternating() -> !is_existential() 
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.
 2017-02-12 15:56:02 +01:00
Alexandre Duret-Lutz
7f7d078f2f * doc/org/tut23.org: Typos. 2017-02-12 10:40:34 +01:00
Alexandre Duret-Lutz
9609f1e50b configure: fix typos in adl_CHECK_PYTHON 
Fixes #220.

* m4/pypath.m4: Here.
* NEWS: Mention the bug.
 2017-02-12 10:35:00 +01:00
Alexandre Duret-Lutz
15c6fd9562 alternation: fix detection of non-weak automata 
Fixes #218.

* spot/twaalgos/alternation.cc: Adjust check.
* tests/core/alternating.test: Add test case from #218.
* NEWS: Mention the bug.
 2017-02-12 01:37:52 +01:00
Alexandre Duret-Lutz
60bc269fd2 * spot/tl/parse.hh (fix_utf8_locations): Fix documentation. 2017-02-08 10:51:19 +01:00
Alexandre Duret-Lutz
a0366921a5 ltlcross: Adjust color and wording of output 
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.
 2017-02-07 22:33:33 +01:00
Alexandre Duret-Lutz
6e3c7896f8 * HACKING: Typo. 2017-02-06 16:20:38 +01:00
Alexandre Duret-Lutz
fb59cab09f emptiness: allow twa_run::as_twa to preserve names 
* spot/twaalgos/emptiness.cc, spot/twaalgos/emptiness.hh: Here.
* tests/python/ltsmin-dve.ipynb: Add a test.
* NEWS: Mention the change.
 2017-02-04 10:02:23 +01:00
Maximilien Colange
3f5470898d Rework the 'down_cast' macro, closing #196. 
* 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.
 2017-02-02 17:01:40 +01:00
Maximilien Colange
07a76e4d93 Do not warn about static_asserts. 
* tests/sanity/style.test: Filter out static_assert.
 2017-02-02 17:01:12 +01:00
Alexandre Duret-Lutz
6c6660f48f org: plantuml.jar is in the build directory 
Fixes #213.

* doc/org/.dir-locals.el.in, doc/org/init.el.in: Adjust location of
plantuml.jar.
 2017-02-02 10:26:33 +01:00
Etienne Renault
4fdaf0e14e use wget or curl according to what is available 
* doc/Makefile.am, elisp/Makefile.am: here.
* HACKING: add missing requirements.
 2017-02-01 19:43:33 +01:00
Etienne Renault
63116ff79c Fixes #205. 
* tests/core/hierarchy.test: here.
 2017-02-01 19:41:54 +01:00
Alexandre Duret-Lutz
cdfa607882 * doc/org/concepts.org: Typo. 2017-02-01 18:50:54 +01:00
Alexandre Duret-Lutz
33f9e03e83 [buddy] update the warning flags to match Spot's 
* m4/gccwarns.m4: Add more flags taken from Spot.
Also add -Wno-long-long to suppress one warning.
 2017-02-01 18:50:54 +01:00
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