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

4317 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
e0d3291881 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 16:58:31 +01:00
Alexandre Duret-Lutz
905af90459 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 16:58:26 +01:00
Alexandre Duret-Lutz
6c218e4828 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 16:58:23 +01:00
Alexandre Duret-Lutz
0f7008d98c * spot/priv/satcommon.cc: Fix include. 2017-02-28 16:58:20 +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
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