Commit graph

3340 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
47824bead6 tl: reorganize section 5
* doc/tl/tl.tex: Here.
2015-08-18 11:15:28 +02:00
Alexandre Duret-Lutz
ce9b2369ed more final keywords
* src/ltlvisit/mutation.cc, src/ltlvisit/relabel.cc,
src/ltlvisit/remove_x.cc: Add final keyword to final classes.
2015-08-18 09:46:13 +02:00
Alexandre Duret-Lutz
0689aa165b silence diagnostics from gcc-snapshot
(Upcoming GCC 6.)

* src/misc/intvcmp2.cc: Here.
* NEWS: Mention it.
2015-08-17 18:56:36 +02:00
Alexandre Duret-Lutz
56cbc3c813 ltlfilt: add --unabbreviate
* src/bin/ltlfilt.cc: Add option --unabbreviate.
* src/tests/ltlfilt.test: Add a test case.
* NEWS: Mention it.
2015-08-17 17:38:47 +02:00
Alexandre Duret-Lutz
d1f915c748 merge tunnabrev/lunnabrev/wmunabbrev into a single function
* src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh,
src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
src/ltlvisit/wmunabbrev.cc, src/ltlvisit/wmunabbrev.hh: Delete.
* src/ltlvisit/unabbrev.cc, src/ltlvisit/unabbrev.hh: New files.
* src/ltlvisit/Makefile.am: Adjust.
* src/ltlvisit/print.cc, src/tests/equalsf.cc, src/tests/Makefile.am,
src/twaalgos/ltl2taa.cc, wrap/python/spot_impl.i, src/bin/ltlfilt.cc:
Adjust callers.
* src/ltlvisit/contain.cc, src/tests/syntimpl.cc: Remove useless
include.
* wrap/python/tests/formulas.ipynb: New test cases.
* doc/tl/tl.tex: Group all rules in a single section.
* NEWS: Mention it.
2015-08-17 17:38:47 +02:00
Alexandre Duret-Lutz
314a016547 * doc/org/spot.css: improve style for printing. 2015-08-17 11:06:02 +02:00
Alexandre Duret-Lutz
59202bd5de do not rewrite <-> and -> for Spin LTL output
Fixes #39, reported by Joachim Klein.

* src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Take an option
to specify which of xor/equiv/implies should be rewritten.
* src/ltlvisit/print.cc (print_spin): Rewrite only xor.
* src/tests/ltlfilt.test: Add a test case.
* NEWS: Mention this.
2015-08-14 20:33:56 +02:00
Alexandre Duret-Lutz
ac6b042e2c remove a GCC 4.6 workaround
* src/twa/twagraph.hh (namer): Use a template alias instead
of a trait.
* src/twa/twagraph.cc, src/parseaut/parseaut.yy,
src/twaalgos/ltl2tgba_fm.cc: Adjust.
2015-08-14 15:34:28 +02:00
Alexandre Duret-Lutz
304f2496ea bdddict: remove register_clone_acc
* src/twa/bdddict.cc, src/twa/bdddict.hh: Here.
2015-08-14 15:16:26 +02:00
Alexandre Duret-Lutz
c50d5a82ac fix a spurious assertion
* src/twaalgos/totgba.cc: Here.
* NEWS: Mention it.
2015-08-14 14:13:57 +02:00
Alexandre Duret-Lutz
0143f0d435 sccsimpl: Remove Fin sets between SCCs
We do not remove them in rejecting SCCs (as it might make the SCC
accepting), but we can remove them between SCCs.

Fixes #101.

* src/twaalgos/sccfilter.cc: Here.
* src/tests/sccsimpl.test: Add test case.
* NEWS: Mention this.
2015-08-14 11:42:28 +02:00
Alexandre Duret-Lutz
2eab0344b9 fix latex escaping
* src/ltlvisit/print.cc: Property output the double
quotes in latex mode, not only sclatex.
* src/misc/escape.cc: Fix LaTeX escape to work in math mode.
* src/tests/latex.test: Add a test.
* wrap/python/tests/formulas.ipynb: Adjust expected output
* NEWS: Mention the fix.
2015-08-13 17:25:00 +02:00
Alexandre Duret-Lutz
21ff2d0415 org: Add link to the Python notebooks.
Fixes #100.

* doc/org/tut.org: Link to the notebook.
* src/sanity/ipynb.test: New test, to make sure we do not forget
to document ipython notebook when we add some.
* src/sanity/Makefile.am: Add it and run it.
* NEWS: Mention it.
2015-08-13 16:50:15 +02:00
Alexandre Duret-Lutz
868cabe4f6 * src/bin/man/ltlcross.x: Document %N, %T, %H. 2015-08-13 16:50:15 +02:00
Alexandre Duret-Lutz
546304eabc * doc/org/spot.css: Add padding at the bottom of man pages. 2015-08-13 16:50:15 +02:00
Alexandre Duret-Lutz
b8445846ce * tools/man2html.pl: Fix interlinking of man pages. 2015-08-13 16:50:15 +02:00
Alexandre Duret-Lutz
490b0b1584 * doc/org/tools.org: Add links to man pages. 2015-08-13 16:50:15 +02:00
Alexandre Duret-Lutz
288a4ff33c * src/bin/man/ltl2tgba.x: Remove superfluous directory. 2015-08-13 15:13:44 +02:00
Alexandre Duret-Lutz
d2c0105224 * HACKING: Mention that we now need groff. 2015-08-13 12:05:18 +02:00
Alexandre Duret-Lutz
3897c8dc9a org: include the man pages in the generated userdoc
* doc/Makefile.am (org-man): New target.
* tools/man2html.pl: Adjust to distinguish source and destination
directories.  Use relative links in genated files.
* NEWS: Mention the html man pages.
2015-08-13 09:06:21 +02:00
Alexandre Duret-Lutz
f7b65001e9 man: improve typesetting and prepare for html output
* src/bin/man/autfilt.x, src/bin/man/dstar2tgba.x,
src/bin/man/ltl2tgba.x, src/bin/man/ltlcross.x,
src/bin/man/ltlgrind.x, src/bin/man/randltl.x, src/bin/man/spot-x.x:
Improve typesetting and cross-references.
* tools/help2man: Adjust to better detect the optional arguments.
Detect options that are not separated from their description by two
spaces.  Argp output some of those.
* tools/man2html.pl: New file.
* Makefile.am: Distribute it.
* src/bin/ltlfilt.cc: Fix description of --define.
* src/bin/ltlgrind.cc: Fix duplicate description for --help and
--version.  Reorder --help output slightly.
* NEWS: Mention the few fixes.
2015-08-13 09:06:21 +02:00
Alexandre Duret-Lutz
5b75ad5abd fix detection of ipython
* configure.ac: Use AC_CHECK_PROGS instead of AC_CHECK_PROG.
2015-08-08 16:44:52 +02:00
Alexandre Duret-Lutz
29fc0f5caa org: use optipng to compress png files
* doc/Makefile.am: If optipng is present, run it in dist-hook.
2015-08-07 18:23:54 +02:00
Alexandre Duret-Lutz
659dfe95e1 org: cleanup css files
* doc/org/syntax.css: Delete this useless file.
* doc/org/spot.css: Cleanup.
* doc/org/init.el.in, doc/org/.dir-locals.el.in: Only load spot.css.
* doc/Makefile.am: Only distribute spot.css.
2015-08-07 16:41:12 +02:00
Alexandre Duret-Lutz
86e16af97c debian: Distribute the html version of the ipython notebooks
* configure.ac: Check for ipython.
* wrap/python/tests/Makefile.am (nb-html): New rule, using ipython.
* debian/control: Depend on ipython.
* debian/rules: Run nb-html.
* debian/python3-spot.examples: Install the genrated html files.
2015-08-07 15:09:29 +02:00
Alexandre Duret-Lutz
fb8a16ffcc * wrap/python/ajax/spotcgi.in: Output .hoa as text/x-hoa. 2015-08-07 12:06:01 +02:00
Alexandre Duret-Lutz
be847372de * NEWS: Summarize recent changes. 2015-08-07 11:22:22 +02:00
Alexandre Duret-Lutz
62fb48ea6e cgi: add a HOA output
* wrap/python/ajax/spotcgi.in: In addition to dot & svg, provide a HOA
output.
2015-08-07 11:22:18 +02:00
Alexandre Duret-Lutz
33afd9f0e2 cgi: Display a message for weak TGBA.
* wrap/python/ajax/spotcgi.in: If a weak BA is output as a TGBA, add a
hint that this is pointless.
2015-08-07 10:49:32 +02:00
Alexandre Duret-Lutz
7efe8c1c6c cgi: force transition-based acceptance output for TGBA
* wrap/python/ajax/spotcgi.in: Force transition-based acceptance in the
output when a TGBA is required, even if the WDBA-minimization return a
BA.
2015-08-07 10:42:34 +02:00
Alexandre Duret-Lutz
254910ed7c * wrap/python/ajax/trans.html: Remove some debugging statements. 2015-08-07 10:30:33 +02:00
Alexandre Duret-Lutz
c0b77b2e62 cgi: do not display Inf(0) for state-based BA
* wrap/python/ajax/spotcgi.in: If the output is a state-based BA, i.e.,
displayed with double circles, then do not output "Inf(0)" as acceptance
condition as that is confusing.  Print "Büchi" instead.
2015-08-06 16:29:55 +02:00
Alexandre Duret-Lutz
3edd55fcd5 print_hoa: diagnose unknown options
* src/twaalgos/hoa.cc: Here.
* src/tests/readsave.test: Test it.
* NEWS: Mention it.
* src/twaalgos/dot.cc, src/twaalgos/neverclaim.cc: Fix the
error message.
2015-07-24 23:23:55 +02:00
Alexandre Duret-Lutz
5cd8c1b8cc * src/twa/twasafracomplement.cc: Remove two unused methods. 2015-07-23 18:05:46 +02:00
Alexandre Duret-Lutz
e76596e1bf acc: fix detection of generalized-Rabin
Fixes #99.

* src/tests/parseaut.test: New test case.
* src/twa/acc.cc (is_generalized_rabin): Fix detection
of Fin(0)|Fin(1)|Fin(2)&Inf(3).
* NEWS: Mention it.
2015-07-23 17:56:42 +02:00
Alexandre Duret-Lutz
ed4629a2ad * NEWS, configure.ac: Bump version to 1.99.2a. 2015-07-18 09:12:35 +02:00
Alexandre Duret-Lutz
ff57e3ef4c Release Spot 1.99.2
* NEWS, configure.ac, doc/org/setup.org: Bump version number.
2015-07-18 00:37:45 +02:00
Alexandre Duret-Lutz
4e025ecd2b org: Really fix example generation
* doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/hoa.org,
doc/org/ltlcross.org: Fix several typos.  In particular ":results" and
":exports" both end with s.
2015-07-17 23:43:01 +02:00
Alexandre Duret-Lutz
67d3553b12 org: fix example generation
* doc/org/autfilt.org, doc/org/dstar2tgba.org: Here.  Many examples
failed because the code generating the input was not run.
2015-07-17 19:04:40 +02:00
Alexandre Duret-Lutz
fd16383e70 org: simplify the calls to ltl2dstar
* doc/org/dstar2tgba.org, doc/org/satmin.org: Here.
2015-07-17 18:00:05 +02:00
Alexandre Duret-Lutz
750d352fb6 Fix many dead links.
Also change http:// to https:// for url that would automatically
redirect to the later.

* doc/mainpage.dox, doc/org/dstar2tgba.org, doc/org/ltl2tgba.org,
doc/org/ltlcross.org, doc/org/satmin.org, doc/org/tools.org,
src/ltlvisit/dot.hh, src/misc/hashfunc.hh, wrap/python/ajax/trans.html:
Here.
2015-07-17 17:55:15 +02:00
Alexandre Duret-Lutz
44bc1d7e39 * NEWS: Reorganize. 2015-07-17 14:57:11 +02:00
Alexandre Duret-Lutz
c9109335b3 org: more typos
* doc/org/setup.org: Fix link to tarball.
* doc/org/ltlcross.org: Missing s.
2015-07-17 10:06:49 +02:00
Alexandre Duret-Lutz
da0f863d64 debian: fix dependency between libspot-dev and libspotltlsmin0
* debian/control: Here.
2015-07-17 09:51:36 +02:00
Alexandre Duret-Lutz
29052c4619 bin: better shell quoting for ltlcross and ltldo
* src/bin/common_trans.cc: Use double-quotes when single-quotes
cannot do.
* src/tests/ltlcross3.test: Add a test case.
* NEWS: Mention it.
2015-07-16 22:39:26 +02:00
Alexandre Duret-Lutz
31f5ea75b2 bin: document %% for ltldo and ltlcross
I had no idea this was working...
Reported by Joachim Klein.

* src/bin/common_trans.cc: Document it.
* src/tests/ltlcross3.test: Test it.
2015-07-16 20:01:24 +02:00
Alexandre Duret-Lutz
a39ebcc8cc org: fix broken links to GraphViz
* doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org:
Here.
2015-07-16 20:01:20 +02:00
Alexandre Duret-Lutz
c37fedb011 org: typos
Reported by Joachim Klein.

* doc/org/ltl2tgba.org: Broken link.
* doc/org/ltlcross.org: Two typos.
2015-07-16 17:52:45 +02:00
Alexandre Duret-Lutz
dafeda6fff bin: make it clear that -B produces state-based acceptance
* src/bin/autfilt.cc, src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc: Here.
2015-07-16 17:49:21 +02:00
Alexandre Duret-Lutz
e6a5a743f7 remfin: avoid some loops in SCC that do not intersect any Fin
* src/twaalgos/remfin.cc: Here.
2015-07-16 12:07:40 +02:00