Commit graph

3750 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
125ca7df7a tests: reset CFLAGS
* tests/run.in: Here.  This helps when spins is installed an the tests
actually compile code; we do not want to inherit the -std=c11
-fvisibility=hidden set for compiling Spot.
2016-06-14 16:03:32 +02:00
Alexandre Duret-Lutz
91e8ced372 * tests/Makefile.am: Distribute elevator2.1.pm. 2016-06-14 16:03:32 +02:00
Alexandre Duret-Lutz
bb47d13fcd fix a few copyright headers
* tests/core/ltlcrossgrind.test, tests/core/ltlgrind.test,
tests/core/ltlrel.test: Here.
2016-06-14 11:32:26 +02:00
Alexandre Duret-Lutz
dc5237c7e7 relabel: fix infinite recursion in relabel_bse()
Reported by František Blahoudek.

* spot/tl/relabel.cc: Fix.
* tests/core/ltlrel.test: Add test case.
* NEWS: Mention the bug.
2016-06-14 10:11:15 +02:00
Alexandre Duret-Lutz
1c8c86914f * doc/org/tut.org: Typo. 2016-05-25 11:06:19 +02:00
Alexandre Duret-Lutz
1f9b18f54a org: fix sat-minimize example
Fixes #178.

* doc/org/satmin.org: Use a different example, where tba-det does not
work.  Also adjust the text to automatically adjust to the size of the
produced automata.
2016-05-17 22:18:44 +02:00
Alexandre Duret-Lutz
2d304f3dcf org: fix never claim example
* doc/org/concepts.org: Enlarge the width of the output of pr so that
the output is not truncated.  It add a missing closing brace.
2016-05-17 22:18:43 +02:00
Alexandre Duret-Lutz
0605181c7a * spot/twaalgos/postproc.cc: Typo. 2016-05-17 15:41:12 +02:00
Alexandre Duret-Lutz
c94787b7d9 * doc/org/ltlcross.org: Fix explanation. 2016-05-11 16:19:13 +02:00
Alexandre Duret-Lutz
1780208961 ajax: add <h1> title
Final part of #176.

* python/ajax/trans.html: Here.
2016-05-10 10:48:33 +02:00
Alexandre Duret-Lutz
86287be2ef org: disable postamble in html export
* doc/org/init.el.in, doc/org/.dir-locals.el.in: Here.
2016-05-10 10:48:33 +02:00
Alexandre Duret-Lutz
bb2c697072 org: add a description for each page
Part of #176.

* doc/org/autfilt.org, doc/org/compile.org, doc/org/concepts.org,
doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genltl.org,
doc/org/hoa.org, doc/org/install.org, doc/org/ioltl.org,
doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/ltldo.org, doc/org/ltlfilt.org, doc/org/ltlgrind.org,
doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org,
doc/org/satmin.org, doc/org/tools.org, doc/org/tut.org,
doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut10.org, doc/org/tut20.org, doc/org/tut21.org,
doc/org/tut22.org, doc/org/tut30.org, doc/org/upgrade2.org: Here.
* doc/org/index.org: Also add keywords in case it is useful, and
use a more descripting title for search engines.
2016-05-10 10:48:33 +02:00
Alexandre Duret-Lutz
e75605529a attempt to fix clang++ compilation error
Seen on arch linux when clang++ 3.7.1 uses GCC's 6.1.1 tuple header.

* spot/twaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::succ): Build the return
type explicitly.
* NEWS: Mention the issue.
2016-05-10 10:48:13 +02:00
Alexandre Duret-Lutz
d4c1db287b * NEWS: Update for next version. 2016-05-09 13:13:02 +02:00
Alexandre Duret-Lutz
bd5ac37e7c * configure.ac: Bump version number. 2016-05-09 09:42:20 +02:00
Alexandre Duret-Lutz
cfd4a1b98d Release Spot 2.0.1
* NEWS, configure.ac, doc/org/setup.org: Update.
2016-05-09 09:33:24 +02:00
Alexandre Duret-Lutz
4cc6df102a bench: fix bench/ltl2tgba for new bin location
* bench/ltl2tgba/Makefile.am, bench/ltl2tgba/defs.in:
Update location of tools.
* NEWS: Mention the fix.
2016-05-05 19:40:23 +02:00
Alexandre Duret-Lutz
465fda2b35 * bin/man/genltl.x: Typo. 2016-05-05 19:40:23 +02:00
Alexandre Duret-Lutz
9149724617 doc: add a spot(7) man page
Suggested by Akim Demaille.  Fixes #171.

* bin/man/spot.x, bin/spot.cc: New files.
* bin/man/Makefile.am, bin/Makefile.am: Add them.
* doc/org/tools.org, NEWS: Mention the new page.
2016-05-02 14:40:45 +02:00
Alexandre Duret-Lutz
d6e491a761 doc: fix css to not highlight table row in man pages
* doc/org/spot.css: Here.
2016-05-02 14:40:45 +02:00
Alexandre Duret-Lutz
5e6d096e0f * doc/org/tools.org: Minor tweaks. 2016-05-02 14:40:45 +02:00
Alexandre Duret-Lutz
52e722c818 * spot/misc/tmpfile.hh: Disallow copy. 2016-05-01 18:59:47 +02:00
Alexandre Duret-Lutz
a1b3b065fa print_hoa: output all registered APs
Also introduce twa::unregister_ap() and twa_graph::remove_unused_ap()
so that the methods where this behavior is expected can be fixed.

And fix ltsmin::kripke() which did not register APs.

Part of #170.

* spot/twaalgos/hoa.cc: Use apvars() to print all registerd APs.
Throw an exception when printing automata using unregistered APs.
* spot/ltsmin/ltsmin.cc: Call register_ap().
* spot/twa/twa.cc, spot/twa/twa.hh, spot/twa/twagraph.cc,
spot/twa/twagraph.hh (twa::unregister_ap, twa_graph::remove_unused_ap):
New methods.
* spot/tl/exclusive.cc, spot/twaalgos/postproc.cc,
spot/twaalgos/remprop.cc, spot/twaalgos/relabel.cc: Use them.
* tests/core/maskacc.test, tests/core/maskkeep.test,
tests/core/strength.test: Adjust expected results.
* NEWS: Mention those changes.
2016-05-01 15:09:06 +02:00
Alexandre Duret-Lutz
dad17b36b8 honor ap() when counting transitions
Fixing this bug alone revealed another bug: parsing never claim or LBTT
automata did not register APs.  So this fixes both bugs.

This is the first part of #170.

* spot/twa/twa.hh (register_aps_from_dict): New method.
* spot/parseaut/parseaut.yy: Call it for never claim and LBTT files.
* spot/twaalgos/stats.cc: Simplify using ap_vars().
* tests/core/ltl2tgba.test: Add a test case.
* NEWS: Mention the bugs.
2016-05-01 15:06:21 +02:00
Alexandre Duret-Lutz
4f913c7fb5 autfilt: fix simpification of exclusive AP
* bin/autfilt.cc: Here.
* tests/core/exclusive-tgba.test: Test it.
* NEWS: Mention the fix.
2016-05-01 15:06:21 +02:00
Alexandre Duret-Lutz
0b05a8f98b * tests/python/ltsmin.ipynb: Remove some debugging code. 2016-04-22 20:22:55 +02:00
Alexandre Duret-Lutz
1d739d766f python: export tgba_determinize
* python/spot/impl.i: Here.
* tests/python/automata.ipynb: Use it.
* NEWS: Mention it.
2016-04-22 20:22:55 +02:00
Etienne Renault
fcbb950c0f Update list of dependencies.
* HACKING: Here.
2016-04-22 20:22:55 +02:00
Alexandre Duret-Lutz
6acd03a142 doc: ltlcross is not only about Büchi anymore
* bin/man/ltlcross.x, doc/org/ltlcross.org, doc/org/tools.org: Fix
one-line summaries.
2016-04-21 19:41:11 +02:00
Alexandre Duret-Lutz
2b5516ba66 * bin/autfilt.cc: Typos in --help. 2016-04-21 19:40:59 +02:00
Alexandre Duret-Lutz
370ac51b6b docyment make_emptiness_check_instantiator()
Fixes #161, reported by Yann Thierry-Mieg.

* spot/twaalgos/emptiness.hh: Here.
* NEWS: Mention it.
2016-04-21 08:58:44 +02:00
Alexandre Duret-Lutz
adb99869cc bitvect: tweak to please icc
This allows bitvect.hh to compile with icpc 16.0.2, but the whole
project does not yet compile due to a bug in 16.0.2 that prevents
compilation of unordered_map::emplace() from the STL shipped with GCC
5.3.1.

* spot/misc/bitvect.hh: adjust friend declarations.
2016-04-21 08:58:38 +02:00
Alexandre Duret-Lutz
7c7f0df8a8 check_strength(): also check negated properties
The test is in the patch introducing HOA 1.1 output.

* spot/twaalgos/strength.cc: Here.
* NEWS: Mention the bug.
2016-04-20 15:27:28 +02:00
Alexandre Duret-Lutz
f50486b4cf parseaut: fix parsing of /*****/
* spot/parseaut/scanaut.ll: Here.
* tests/core/strength.test: Add a test.
* NEWS: Mention the bug.
2016-04-20 15:27:28 +02:00
Alexandre Duret-Lutz
134982c08b Typo in --help output
* bin/common_aoutput.cc: Fix --help output for -Hk.
* NEWS: Mention it.
2016-04-18 21:20:38 +02:00
Alexandre Duret-Lutz
5185844d8a * NEWS, configure.ac: Bump version number. 2016-04-18 21:16:46 +02:00
Alexandre Duret-Lutz
96a2a13c85 Release Spot 2.0
* configure.ac, doc/org/setup.org, NEWS: Update version number.
2016-04-11 06:52:12 +02:00
Alexandre Duret-Lutz
ab20585180 * spot/graph/graph.hh: Typo in comment. 2016-04-10 18:05:46 +02:00
Alexandre Duret-Lutz
a6afaf3d9d adjust for recent renaming of valid_trans()
* spot/kripke/kripkegraph.hh, spot/twa/twagraph.hh: Call
is_valid_edge() instead.
* NEWS: Mention the renaming.
2016-04-10 17:22:26 +02:00
Alexandre Duret-Lutz
fb6cc0dff7 * doc/org/concepts.org: Fix reference to BuDDy. 2016-04-10 14:11:49 +02:00
Alexandre Duret-Lutz
9d6941f038 * spot/graph/graph.hh: More Doxygen comments. 2016-04-10 14:11:36 +02:00
Alexandre Duret-Lutz
5e47d4df38 update some URLs to skip permanent redirections
* doc/org/concepts.org, doc/org/ltlcross.org, doc/org/ltldo.org,
python/ajax/trans.html, tools/man2html.pl: Update URLs.
2016-04-10 12:16:28 +02:00
Alexandre Duret-Lutz
868f2634f8 org: document automata properties
Fixes #157.

* doc/org/concepts.org: Document the properties.
* doc/org/hoa.org: Link to it.
* NEWS: Mention the change.
2016-04-10 11:33:46 +02:00
Alexandre Duret-Lutz
4299517c8d org: add picture for the architecture
* doc/org/arch.tex: New file.
* doc/Makefile.am: Compile it.
* doc/org/concepts.org: Show it.
2016-04-10 10:04:14 +02:00
Alexandre Duret-Lutz
949638930b * NEWS: Mention recent python changes. 2016-04-09 10:14:31 +02:00
Alexandre Duret-Lutz
59e1f6a339 ltlfilt: implement --reject-word and --accept-word
* bin/common_range.hh: Store the common definition of words.
* bin/autfilt.cc: Use it.
* bin/ltlfilt.cc: Likewise, and implement those two options.
* tests/core/acc_word.test: Test them.
* doc/org/autfilt.org: Augment the last example to point out
that it can now be done with ltlfilt.
* NEWS: Mention the new options.
2016-04-09 10:10:41 +02:00
Alexandre Duret-Lutz
901f287032 python: add prints for atomic_prop_set
Fixes #159.

* python/spot/ltsmin.i: Here.
* python/spot/impl.i: Disable duplicate instantiation.
* tests/python/ltsmin.ipynb: Test it.
2016-04-08 23:01:07 +02:00
Alexandre Duret-Lutz
e429e2f056 * tests/sanity/style.test: Cancel set -x. 2016-04-08 22:34:17 +02:00
Alexandre Duret-Lutz
ed3b58c99c let ltsmin.model.kripke() take the output of atomic_prop_collect()
Fixes #160.

* spot/tl/formula.hh (formula::ap): New specialization.
* tests/python/ltsmin.ipynb: Test it.
2016-04-08 22:33:48 +02:00
Alexandre Duret-Lutz
a4f111f342 * spot/tl/formula.hh: More doxygen comments for fnode. 2016-04-01 18:26:27 +02:00