Commit graph

4177 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
2c9f201c0d twa_graph: fix set_univ_init_state() with initializer_list
Reported by Thomas Medioni.

* spot/twa/twagraph.hh (set_univ_init_state): Remove the bogus
template parameter.
* tests/core/twagraph.cc, tests/core/tgbagraph.test: Test the method.
* NEWS: Mention the bug.
2017-03-07 13:36:49 +01:00
Alexandre Duret-Lutz
a66e7704d8 monitor: fix -MD/-M difference in property output
Fixes #241.

* spot/twaalgos/postproc.cc: Use the deterministic monitor if it
has as many states as the non-deterministic one.
* spot/twaalgos/minimize.cc (minimize_monitor): Quickly check
for terminal automata.
* spot/twaalgos/stripacc.cc: Set the weak property.
* spot/twaalgos/stripacc.hh: Improve documentation.
* tests/core/monitor.test, tests/core/sbacc.test: Update.
* NEWS: Mention the issue.
2017-03-03 18:37:32 +01:00
Alexandre Duret-Lutz
3699e6cd0c doc: simplify a C++ example
* doc/org/tut10.org: Remove a couple of useless includes.
2017-03-03 17:58:31 +01:00
Alexandre Duret-Lutz
bb23ea9978 doc: add an example about how to build monitor in shell/python/C++
Part of #239.

* doc/org/tut11.org: New file.
* doc/org/ltl2tgba.org, doc/org/hierarchy.org: Add some anchors we can
link to in tut11.org.
* doc/org/tut.org, doc/Makefile.am: Add tut11.org.
* NEWS: Mention the new page.
2017-03-03 17:57:31 +01:00
Alexandre Duret-Lutz
2b9accdf58 postproc: fix monitor code
Fixes #240.

* spot/twaalgos/postproc.cc: Do not call do_simul on the output of
minimize_monitor(), and do not skip complete() when PREF_==Any.
* tests/core/monitor.test: Add a test case.
* NEWS: Mention the bug.
* doc/org/ltl2tgba.org: Document complete monitors.
2017-03-03 14:39:55 +01:00
Alexandre Duret-Lutz
cf5d2c2b32 acc: make mark_t::operator bool() explicit
This avoids a few conversion problems, and also made the bug of
sbacc (fixed by 37fc948be4) obvious.

Reported by Thomas Medioni.

* spot/twa/acc.hh (mark_t::operator bool): Make it explicit.
* spot/twaalgos/remfin.cc: Adjust.
2017-03-03 13:35:31 +01:00
Alexandre Duret-Lutz
37fc948be4 sbacc: fix a typo and remove some useless code
* spot/twaalgos/sbacc.cc: Do not assign to one_in twice, and
fix the value of init_acc.
* tests/core/sbacc.test: Add a test case.
* NEWS: Mention the bug.
2017-03-03 11:55:00 +01:00
Alexandre Duret-Lutz
1eb5be543d acc: implement min_set() and max_set() using gcc builtins
Fixes #238.

* spot/twa/acc.hh (max_set): Add a version using __builtin_clz().
(min_set): New method.
* tests/core/acc.cc, tests/core/acc.test: Add some tests.
2017-03-02 14:17:06 +01:00
Alexandre Duret-Lutz
22a3d1c393 remove options -! and -" from genltl
Fixes #237.

* bin/genltl.cc: Fix the numbering of options.
* NEWS: Mention the bugs.
2017-03-01 16:18:12 +01:00
Alexandre Duret-Lutz
18283d6907 add options to %x to list atomic propositions
* bin/common_aoutput.cc, bin/common_aoutput.hh, bin/common_output.cc,
bin/common_output.hh: Add options to %x to list atomic propositions
with various quoting scheme.  Deprecate --format=%a in favor of the
new --format=%x for consistency with --stats=%x.
* tests/core/format.test, tests/core/remprop.test: Adjust and add more
tests.
* NEWS: Mention these changes.
2017-03-01 16:02:09 +01:00
Alexandre Duret-Lutz
68ad391948 correct handling of --stats=%P
Fixes #236.

* bin/common_aoutput.cc: Fix it.
* tests/core/format.test: Improve test cases.
* NEWS: Mention the bug.
2017-02-28 17:02:06 +01:00
Alexandre Duret-Lutz
d2e9515c10 skip divine tests when divine does not understand compile --help
Fixes #235, reported by Henrich Lauko.

* python/spot/ltsmin.i: Catch CalledProcessError.
* NEWS: Mention the bug.
* THANKS: Add Henrich.
2017-02-28 17:02:06 +01:00
Alexandre Duret-Lutz
0d00ab24d2 bin: --stats=%x to count atomic propositions
* bin/common_aoutput.cc, bin/common_aoutput.hh: Implement %x and %X.
* tests/core/remprop.test: Test them.
* NEWS: Mention them.
2017-02-28 17:02:06 +01:00
Alexandre Duret-Lutz
dd5a820863 * spot/priv/satcommon.cc: Fix include. 2017-02-28 17:02:06 +01:00
Alexandre Duret-Lutz
ac39c1db3c powerset: minor simplifications
* spot/twaalgos/powerset.cc (tgba_powerset): Use twa::ap() to simplify
the code.
(number_of_variables): Remove.
2017-02-28 17:01:15 +01:00
Alexandre Duret-Lutz
58abbc7399 * AUTHORS: Add Clément Gillard 2017-02-28 16:49:48 +01:00
Clément Gillard
da051e112d decompose_scc: Update 'decompose' notebook
* tests/python/decompose.ipynb: Add about `decompose_scc`.
* doc/org/tut.org: Update description.
2017-02-21 21:36:26 +01:00
Clément Gillard
5d143cc1f8 decompose_scc: factor autfilt into decompose_acc_scc
Put what is done by `autfilt` in a new function, `decompose_acc_scc`.

* bin/autfilt.cc: Move code from here...
* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh: To here.
* tests/python/decompose_scc.py: Test python binding.
2017-02-21 21:33:15 +01:00
Clément Gillard
c0eeea2c5f autfilt: Add '--decompose-scc' option
See #172.

* bin/autfilt.cc: Add option.
* tests/core/strength.test: Remove ambiguity with
'--decompose-strength'.
* NEWS: Mention it.
* tests/core/scc.test: Test it.
2017-02-21 21:33:14 +01:00
Clément Gillard
164135d3d7 Add a decompose_scc() function
See #172.
While at it, fix typo in doxygen comment.

* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh: New function.
* tests/python/decompose_scc.py, tests/Makefile.am: Test python
binding.

* spot/twaalgos/mask.hh: Fix typo.
2017-02-21 21:32:11 +01:00
Alexandre Duret-Lutz
289b2383ad scc_info: add Python bindings
Related to #172, where we discussed that scc_info bindings were
missing.

* spot/twaalgos/sccinfo.hh (spot::scc_info::scc_node): Move...
(spot::scc_info_node): ... here to help Swig.
* python/spot/impl.i: Add bindings for scc_info.
* tests/python/sccinfo.py: New file.
* tests/Makefile.am: Add it.
2017-02-20 14:31:16 +01:00
Alexandre Duret-Lutz
803f9a5dd8 * doc/org/genltl.org: Simplify example. 2017-02-20 12:10:15 +01:00
Alexandre Duret-Lutz
93dad61571 * NEWS: Bump version number. 2017-02-20 09:42:37 +01:00
Alexandre Duret-Lutz
36c53ece2a * configure.ac: Bump version to 2.3.1.dev. 2017-02-20 08:04:34 +01:00
Alexandre Duret-Lutz
b08da14e04 Release Spot 2.3.1
* configure.ac, NEWS, doc/org/setup.org: Bump version numbers.
2017-02-20 07:51:53 +01:00
Alexandre Duret-Lutz
1c96afb1d0 genltl: --kv-phi is in fact --kv-psi
* bin/genltl.cc: Change the name and add the bibtex entry.
* bin/man/genltl.x: Replace LNCS by LNAI.
* tests/core/genltl.test: Also test the %F output.
2017-02-18 10:49:36 +01:00
Alexandre Duret-Lutz
a14abf27fb genltl: typos and shorter descriptions
* bin/genltl.cc: Shorten the descriptions of
the three new LTL families.
* NEWS: Mention those.
2017-02-17 17:45:11 +01:00
Alexandre Duret-Lutz
16e71b5093 * AUTHORS: Add Vincent & Arthur. 2017-02-17 13:15:41 +01:00
Vincent Tourneur
fc2831bf24 genltl: Add 3 families of LTL formulas from a paper
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.
2017-02-16 18:59:34 +01:00
Arthur Remaud
f7bbfd2812 autfilt: Better display of cluster when universal edge loops in it
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
2017-02-16 18:53:18 +01:00
Arthur Remaud
34859568cd autfilt: add option (y) to --dot to split universal transitions
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
2017-02-16 18:52:37 +01:00
Etienne Renault
5516209d8c ltsmin: more information for MacOS users
* tests/ltsmin/README: this fixes #230.
2017-02-16 14:10:33 +01:00
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