Commit graph

414 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
fba3c78206 org: improve recurrence example
* doc/org/hierarchy.org: When generating DBA from recurrence formulas,
actually use -B instead of --tgba.
2017-06-30 14:36:00 +02:00
Alexandre Duret-Lutz
efbce454e2 Merge branch 'master' into next 2017-06-22 07:06:29 +02:00
Alexandre Duret-Lutz
af000edbf9 Release Spot 2.3.5
* NEWS, configure.ac, doc/org/setup.org: Update version.
2017-06-22 06:58:01 +02:00
Alexandre Duret-Lutz
2dd134b0aa doc: Jessie -> Stretch
* doc/org/install.org: Update.
2017-06-20 16:29:26 +02:00
Alexandre Duret-Lutz
85e4cf510c doc: Jessie -> Stretch
* doc/org/install.org: Update.
2017-06-19 18:00:10 +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
1042a8dae1 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,
spot/gen/Makefile.am, doc/org/g++wrap.in: Make the dependencies
explicit.
2017-06-07 20:34:05 +02:00
Maximilien Colange
4f8a8f7305 Properly handle "simulated-states" property in twagraph::defrag_states.
* spot/twa/twagraph.cc: Implement the change.
* spot/twaalgos/simulation.hh: Improve documentation.
* tests/python/simstate.py: Improve the test.
* doc/org/concepts.org: Typo.
2017-06-05 15:48:36 +02:00
Alexandre Duret-Lutz
93969758ee sanity: catch undocumented named properties
* tests/sanity/namedprop.test: New file.
* tests/Makefile.am: Add it.
* doc/org/concepts.org: Add documentation for degen-levels and
simulated-states.
2017-05-31 20:32:53 +02:00
Alexandre Duret-Lutz
7dfa0ec15d Merge branch 'master' into next 2017-05-11 10:18:00 +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
e089509a0c org: list ltlfilt's transformation
* doc/org/ltlfilt.org: A the list of transformation option.
Suggested by Yann Thierry-Mieg.
2017-05-09 14:29:42 +02:00
Alexandre Duret-Lutz
ec51f976f8 gen: introduce a new automaton family
* spot/gen/automata.cc, spot/gen/automata.hh: Define AUT_L_NBA.
* bin/genaut.cc (--l-nba): New option.
* bin/man/genaut.x, doc/org/genaut.org, NEWS: Document it.
* tests/python/gen.py, tests/core/genaut.test: Test it.
2017-04-28 13:32:42 +02:00
Alexandre Duret-Lutz
540b971355 gen: rename genltl() to ltl_pattern() and introduce ltl_patterns()
* spot/gen/formulas.hh, spot/gen/formulas.cc (genltl): Rename as...
(ltl_pattern): This.
(ltl_pattern_max): New function.
* bin/genltl.cc: Adjust names, and simplify using ltl_pattern_max().
* python/spot/gen.i (ltl_patterns): New function.
* tests/python/gen.py: Test it.
* tests/python/gen.ipynb: New file to document the spot.gen package.
* tests/Makefile.am, doc/org/tut.org: Add gen.ipynb.
2017-04-26 15:06:02 +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
2dc115fe2c * doc/org/concepts.org: Typos in property flag names. 2017-04-26 09:04:27 +02:00
Alexandre Duret-Lutz
8939e0dd50 genltl: move all formula generation code to spot/gen/
Fixes #254.

* spot/gen/formulas.cc, spot/gen/formulas.hh: New files.
* spot/gen/Makefile.am: Add them.
* spot/Makefile.am: Fix build order.
* bin/genltl.cc: Move most code to the above files and adjust.
* bin/Makefile.am: Link genltl with libspotgen.
* doc/org/arch.tex: Adjust picture to show that genltl uses
libspotgen.
* python/spot/gen.i: Include formulas.hh.
* tests/python/gen.py: Make sure genltl() and ltl_pattern_name()
can be called.
2017-04-25 18:14:15 +02:00
Alexandre Duret-Lutz
472cd77098 org: update the architecture diagram
For #254.

* doc/org/arch.tex: Include libspotgen and its python bindings,
genaut, and also the buddy bindings.
* doc/org/concepts.org: Adjust the description.
2017-04-23 19:56:01 +02:00
Alexandre Duret-Lutz
5e8f3ee629 typos: familly -> family
* bench/ltlcounter/README, doc/org/upgrade2.org: Here.
2017-04-23 11:28:28 +02:00
Alexandre Duret-Lutz
22aba2c4e2 genaut: add missing documentation
* bin/man/genaut.x, doc/org/genaut.org: New files.
* bin/man/Makefile.am, doc/Makefile.am: Add them.
* doc/org/tools.org, bin/man/randaut.x, bin/man/randltl.x,
bin/man/genltl.x: Link to them.
2017-04-22 14:19:35 +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
07c2dd3b64 introduce original-states
* spot/twaalgos/degen.cc, spot/twaalgos/degen.hh,
spot/twaalgos/mask.hh: Store original states in "original-states"
properties.
* spot/twaalgos/dot.cc: Add support for option 'd'.
* bin/common_aoutput.cc: Document it.
* doc/org/concepts.org, NEWS: Document "original-states".
* tests/core/readsave.test: Add some tests.
2017-04-20 20:07:30 +02:00
Alexandre Duret-Lutz
e7797b727d org: typos
* doc/org/concepts.org: Fix some typos.
2017-04-20 20:01:18 +02:00
Alexandre Duret-Lutz
334f04b0c4 Merge branch 'master' into next 2017-04-11 11:11:05 +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
Thomas Medioni
152b5d0d30 dtwa_complement: deprecated, use dualize() instead.
* NEWS: Mention of the deprecation
* bench/stutter/stutter_invariance_randomgraph.cc,
  bin/autfilt.cc, bin/ltlcross.cc, spot/twaalgos/langmap.cc,
  spot/twaalgos/minimize.cc, spot/twaalgos/powerset.cc,
  spot/twaalgos/stutter.cc, tests/core/ikwiad.cc,
  tests/python/bugdet.py, tests/python/remfin.py,
  tests/python/sum.py: Refactor calls to dtwa_complement() with calls
  to dualize().
* doc/org/upgrade2.org: Change mention of dtwa_complement with dualize.
* spot/twaalgos/complement.hh: Add deprecation notice.
* python/spot/impl.i: Add deprecation notice for the python bindings.
2017-04-07 17:15:38 +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
cc0e9a5e1e 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-06 14:33:14 +02:00
Alexandre Duret-Lutz
4a5d7a3978 rename is_deterministic to is_universal
For #212.

* spot/twa/twa.hh: Rename prop_deterministic() as prop_universal(),
and keep the old name as deprecated.
* spot/twaalgos/isdet.cc, spot/twaalgos/isdet.hh: Rename
is_deterministic() as is_universal(), and add a new function
for is_deterministic().
* doc/org/concepts.org, doc/org/hoa.org, doc/org/tut21.org,
spot/tl/hierarchy.cc, spot/twa/twagraph.cc,
spot/twaalgos/are_isomorphic.cc, spot/twaalgos/determinize.cc,
spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc,
spot/twaalgos/hoa.cc, spot/twaalgos/minimize.cc,
spot/twaalgos/postproc.cc, spot/twaalgos/product.cc,
spot/twaalgos/randomgraph.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/simulation.cc, spot/twaalgos/totgba.cc,
spot/twaalgos/word.cc, tests/python/product.ipynb,
tests/python/remfin.py: Adjust.
* NEWS: Mention the change.
2017-03-27 19:34:10 +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
fe3b86b306 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-03-22 21:26:16 +01:00
Alexandre Duret-Lutz
1c2a7f3d4f 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-03-22 21:26:16 +01:00
Alexandre Duret-Lutz
0de5f50da9 twa: add support for prop_complete()
* spot/twa/twa.hh: Add support.  Make two constructors for prop_set in
order to diagnose constructions with 5 arguments.
* spot/parseaut/parseaut.yy: Adjust diagnostics for complete and
deterministic.
* spot/tl/exclusive.cc, spot/twa/twagraph.cc,
spot/twaalgos/alternation.cc, spot/twaalgos/complete.cc,
spot/twaalgos/complete.hh, spot/twaalgos/degen.cc,
spot/twaalgos/determinize.cc, spot/twaalgos/hoa.cc,
spot/twaalgos/isdet.cc, spot/twaalgos/mask.cc,
spot/twaalgos/minimize.cc, spot/twaalgos/product.cc,
spot/twaalgos/remfin.cc, spot/twaalgos/remprop.cc,
spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc,
spot/twaalgos/simulation.cc, spot/twaalgos/strength.cc,
spot/twaalgos/stutter.cc, spot/twaalgos/totgba.cc,
tests/core/parseaut.test, tests/python/product.ipynb: Adjust.
* NEWS, doc/org/concepts.org, doc/org/hoa.org,
doc/org/tut21.org: Document it.
2017-03-20 21:07:08 +01:00
Alexandre Duret-Lutz
90a8a912e0 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-18 19:13:30 +01:00
Alexandre Duret-Lutz
270b18ebdb * doc/org/tut11.org: Typo in title. 2017-03-15 14:23:55 +01:00
Alexandre Duret-Lutz
ab8a40cb10 Merge branch 'master' into next 2017-03-15 09:24:37 +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
e851e0f8c0 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 10:44:30 +01:00
Alexandre Duret-Lutz
55a524cf3c org: detect C++ errors
* doc/org/g++wrap.in: Save error messages.
* doc/Makefile.am: Display them at the end of the compilation.
2017-03-10 17:54:01 +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
47e1c9692e 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:10:47 +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