Commit graph

379 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
2dd134b0aa doc: Jessie -> Stretch
* doc/org/install.org: Update.
2017-06-20 16:29:26 +02:00
Alexandre Duret-Lutz
97e903b13d libtool: surrender to Debian's castrated libtool
The libtool version distributed by Debian is patched to *not* propagate
dependencies (i.e., if libA depends on libB, then linking against libA
will not automatically link against libB, it has to be explicit),
contrary to what the Libtool manual document.  So now we explicitly
link against both libA and libB in such case.

* configure.ac: Remove the workaround that does not work for
MinGW.
* doc/org/compile.org: Mention the issue.
* bin/Makefile.am, tests/Makefile.am, spot/ltsmin/Makefile.am,
doc/org/g++wrap.in: Make the dependencies explicit.
2017-06-11 23:15:20 +02:00
Alexandre Duret-Lutz
52b5491b8e Release Spot 2.3.4
* NEWS, configure.ac, doc/org/setup.org: Update version to 2.3.4.
2017-05-11 10:10:48 +02:00
Alexandre Duret-Lutz
d3d2364ad0 org: list ltlfilt's transformation
* doc/org/ltlfilt.org: A the list of transformation option.
Suggested by Yann Thierry-Mieg.
2017-05-09 14:30:57 +02:00
Alexandre Duret-Lutz
b8065a7947 * doc/org/concepts.org: Typos in property flag names. 2017-04-26 09:08:24 +02:00
Alexandre Duret-Lutz
cbfb79e343 typos: familly -> family
* bench/ltlcounter/README, doc/org/upgrade2.org: Here.
2017-04-26 09:07:34 +02:00
Alexandre Duret-Lutz
6ac9128699 org: typos
* doc/org/concepts.org: Fix some typos.
2017-04-20 22:02:22 +02:00
Alexandre Duret-Lutz
e39e5ac586 Spot 2.3.3
* NEWS, configure.ac, doc/org/setup.org: Bump version number.
2017-04-11 10:43:04 +02:00
Alexandre Duret-Lutz
08c153d3bb genltl: add support for --p-patterns
Fixes #246.

* bin/genltl.cc: Implement it.
* bin/man/genltl.x, doc/org/genltl.org, NEWS: Document it.
* tests/core/ltl2tgba2.test: Test it.
2017-04-07 11:30:31 +02:00
Alexandre Duret-Lutz
4b7a6238b4 genltl: add --hkrss-patterns
Fixes #245.

* bin/genltl.cc: Add the option.
* bin/man/genltl.x: Add reference.
* tests/core/ltl2tgba2.test: Use these patterns.
* doc/org/genltl.org, NEWS: Document the options.
2017-04-07 11:29:49 +02:00
Alexandre Duret-Lutz
276f40602e bin: add shorthands for ltl2dpa ltl2da and ltl2ldba
* bin/common_trans.cc: Here.
* doc/org/ltlcross.org, doc/org/ltldo.org, NEWS: Adjust.
2017-04-07 11:28:39 +02:00
Alexandre Duret-Lutz
1596f0ed75 org: move babel's temporary directory in builddir
Fixes #244, reported by Vincent Tourneur.

* doc/org/.dir-locals.el.in, doc/org/init.el.in: Define
org-babel-temporary-directory and create the directory.
2017-03-22 22:48:16 +01:00
Alexandre Duret-Lutz
0121d278a7 * doc/org/tut11.org: Typo in title. 2017-03-22 22:48:16 +01:00
Alexandre Duret-Lutz
696eba8a29 Release Spot 2.3.2
* configure.ac, NEWS, doc/org/setup.org: Bump version to 2.3.2.
2017-03-15 09:17:10 +01:00
Alexandre Duret-Lutz
b7afef3643 org: misc cosmetics
* doc/org/tut24.org: Add missing section title.
* doc/org/spot.css: Style h3 headings, and remove some useless lines.
2017-03-14 13:35:52 +01:00
Alexandre Duret-Lutz
cd89983ca5 typos: dictionnary -> dictionary
* doc/org/upgrade2.org, tests/python/prodexpt.py,
tests/python/product.ipynb, NEWS: Fix typos.
* tests/sanity/style.test: Add a check for this.
2017-03-08 16:44:30 +01:00
Alexandre Duret-Lutz
28f4e4b9a5 doc: simplify a C++ example
* doc/org/tut10.org: Remove a couple of useless includes.
2017-03-03 22:57:55 +01:00
Alexandre Duret-Lutz
0df785bcde 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 22:57:55 +01:00
Alexandre Duret-Lutz
9defdad2bc 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 22:57:08 +01:00
Alexandre Duret-Lutz
803f9a5dd8 * doc/org/genltl.org: Simplify example. 2017-02-20 12:10:15 +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
7f7d078f2f * doc/org/tut23.org: Typos. 2017-02-12 10:40:34 +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
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
Alexandre Duret-Lutz
cdfa607882 * doc/org/concepts.org: Typo. 2017-02-01 18:50:54 +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
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 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
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
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 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 Duret-Lutz
4b01387817 support for semi-deterministic property
* spot/twa/twa.hh (prop_semi_deterministic): New methods.
* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add support for the
semi-deterministic property.
* doc/org/concepts.org, doc/org/hoa.org: Document it.
* spot/twaalgos/isdet.cc,
spot/twaalgos/isdet.hh (is_semi_deterministic): New function.
* bin/autfilt.cc: Add --is-semi-deterministic.
* bin/common_aoutput.cc: Add --check=semi-deterministic.
* tests/core/semidet.test: New file.
* tests/Makefile.am: Add it.
* tests/core/parseaut.test, tests/core/readsave.test: Adjust.
2016-12-29 16:37:43 +01:00
Alexandre Duret-Lutz
12f6c8cf10 twa_graph: add a merge_univ_dests() method
and call it after parsing

* spot/twa/twagraph.cc, spot/twa/twagraph.hh
(twa_graph::merge_univ_dests): New method.
* spot/parseaut/parseaut.yy: Call it.
* spot/twaalgos/dot.cc: Improve output, now that
several edges can use the same universal destination.
* tests/core/alternating.test, tests/core/complete.test,
tests/core/parseaut.test, tests/python/_altscc.ipynb,
tests/python/alternating.py, tests/python/alternation.ipynb: Adjust
test case.
* doc/org/tut24.org: Adjust example.
2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
3d0a971aa8 org: examples with alternating automata
* doc/org/tut23.org, doc/org/tut24.org, doc/org/tut31.org: New files.
* doc/Makefile.am, doc/org/tut.org: Add them.
* doc/org/hoa.org, doc/org/concepts.org: Adjust for alternation support.
* NEWS: Add links.
2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
87c9d6f039 ltlcross: add support for alternating automata
* bin/ltlcross.cc: Add an alternation-removal pass, and
adjust CSV output.
* doc/org/ltlcross.org: Update.
* tests/core/ltl3dra.test, tests/core/ltl3ba.test: Add more tests.
* tests/Makefile.am: Add tests/core/ltl3ba.test.
* NEWS: Mention it.
2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
fa06cfa303 alternation: implement remove_alternation() for weak alt automata
This mixes the subset construction (for 1-state rejecting SCCs) and
the breakpoint construction (for larger rejecting SCCs).  The
algorithm should probably be rewritten in a cleaner and more efficient
way, but that should do for a first version.  It should be easy to
extend it to support Büchi acceptance (since the breakpoint
construction works for this) when we need it.

* spot/twaalgos/alternation.hh,
spot/twaalgos/alternation.cc (remove_alternation): New function.
* tests/python/alternation.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
2016-12-29 12:57:16 +01:00
Alexandre Duret-Lutz
582d455c23 twa: add support for very-weak property
* spot/twa/twa.hh: Implement the property.
* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add input
and output for it.
* spot/twaalgos/strength.cc,
spot/twaalgos/strength.hh (is_very_weak_automaton): New function.
* tests/core/alternating.test: Add a test for --check=strength
on an alternating automaton.
* tests/core/strength.test, tests/core/parseaut.test: Adjust expected
output.
* NEWS, doc/org/hoa.org, doc/org/concepts.org: Document it.
2016-12-27 12:36:38 +01:00
Alexandre Duret-Lutz
dcd21aaabf org: call set_init_state() in tut22
* doc/org/tut22.org: Here.
2016-12-25 12:27:17 +01:00
Alexandre Duret-Lutz
34ac6f08cc org: ltlcross supports any acceptance condition
* doc/org/ltlcross.org: Also fix the documentation of terminal and
weak SCCs.
2016-12-24 21:08:01 +01:00
Alexandre Duret-Lutz
8e8c6a8cea org: support org >= 8.3
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Load "shell" instead
of "sh" for recent org-mode version.
2016-12-24 21:08:01 +01:00
Alexandre Duret-Lutz
574f47c366 Release Spot 2.2.2
* NEWS, configure.ac, doc/org/setup.org: Update version.
2016-12-16 06:50:59 +01:00
Alexandre Duret-Lutz
341eeb2ba1 strength: fix is_terminal()
Fix #198.  Reported by Maximilien Colange.

* spot/twaalgos/strength.cc (is_terminal): Test that no accepting
transition lead to a rejecting SCC.
* tests/core/strength.test: Add test case.
* spot/twaalgos/strength.hh, spot/twa/twa.hh, doc/org/concepts.org:
Adjust documentation.
* NEWS: Mention the fix.
2016-11-28 18:03:30 +01:00
Alexandre Duret-Lutz
9cf8535578 Release Spot 2.2.1
* NEWS, configure.ac, doc/org/setup.org: Update.
2016-11-21 09:00:51 +01:00
Alexandre Duret-Lutz
dd960dc71c Release Spot 2.2
* configure.ac, doc/org/setup.org, NEWS: Set version number.
2016-11-14 06:02:13 +01:00
Alexandre Duret-Lutz
4bd04fc65c * doc/org/oaut.org: Shorten a long line. 2016-11-13 21:58:37 +01:00