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

300 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
05cfbaad1f * doc/org/install.org: Suggest using the stable packages with Ubuntu. 2015-08-25 23:28:31 +02:00
Alexandre Duret-Lutz
daf5a2be05 org: link to tl.pdf 
* doc/org/index.org, doc/org/ioltl.org: Add links.
 2015-08-25 23:23:11 +02:00
Alexandre Duret-Lutz
c8df1ae85d * doc/org/ltldo.org: Another typo. 2015-08-21 23:17:08 +02:00
Alexandre Duret-Lutz
596de181be * doc/org/ltldo.org: Improve English. 2015-08-21 22:11:10 +02:00
Alexandre Duret-Lutz
308833788b unabbreviate: enable removal of R 
This implies learning alternative rules for G, and W as well, since
those would use R.

Fixes #103.  Suggested by Joachim Klein.

* src/ltlvisit/unabbrev.cc, src/ltlvisit/unabbrev.hh: Implement the
new rules.
* doc/tl/tl.tex: Document the rules.
* src/tests/unabbrevwm.test: Test them.
* src/bin/ltlfilt.cc, NEWS: Mention that --unabbreviate accepts R.
 2015-08-21 16:02:52 +02:00
Alexandre Duret-Lutz
f831f729e1 homogenize dstar_parse() and parse_aut() outputs 
* src/dstarparse/dstarparse.yy, src/dstarparse/dstarscan.ll
src/dstarparse/parsedecl.hh, src/dstarparse/public.hh:
Adjust to return the same return types as parse_aut.
* src/dstarparse/fmterror.cc: Delete, we can use
the one of parse_aut.
* src/dstarparse/Makefile.am: Adjust.
* src/tests/ikwiad.cc, src/bin/dstar2tgba.cc,
src/bin/ltldo.cc: Adjust usage.
* src/bin/ltlcross.cc: The the result of dstar_parse() as-is, now that
it is a TωA like those produced by parse_aut().  As a consequence,
get rid of all the code storing statistics about the input
automaton.
* src/tests/ltlcross3.test, src/tests/ltl2dstar.test: Adjust expected
CSV output.
* doc/org/ltlcross.org, src/bin/man/ltlcross.x: Adjust to not
mention that %D performs a tranformation to Büchi.
 2015-08-20 23:21:20 +02:00
Alexandre Duret-Lutz
8a3a07d8a4 * doc/tl/tl.tex: Refine note about {r} vs. r in PSL. 2015-08-19 14:20:17 +02:00
Alexandre Duret-Lutz
5f76f34607 * doc/tl/tl.bib: Properly quote PSL. 2015-08-19 10:59:09 +02:00
Alexandre Duret-Lutz
47824bead6 tl: reorganize section 5 
* doc/tl/tl.tex: Here.
 2015-08-18 11:15:28 +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
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
546304eabc * doc/org/spot.css: Add padding at the bottom 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
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
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
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
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
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
e540eaeee1 document that libraries have their own Debian packages 
* NEWS, doc/org/install.org: Here.
 2015-07-07 15:45:17 +02:00
Alexandre Duret-Lutz
b8c6eb04b3 Release Spot 1.99.1 
* NEWS, configure.ac, doc/org/setup.org: Bump version number.
 2015-06-23 08:35:32 +02:00
Alexandre Duret-Lutz
41a7b906d8 org: improve TOC display and specify viewport 
* doc/org/spot.css: Improve TOC.
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Specify viewport.
 2015-06-22 09:24:32 +02:00
Alexandre Duret-Lutz
c7e6733eb3 * doc/Doxyfile.in: Upgrade to Doxygen 1.8.9.1. 2015-06-21 13:59:26 +02:00
Alexandre Duret-Lutz
813c3799c0 ltl: remove is_eltl_formula() 
* doc/tl/tl.tex, src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/formula.cc,
src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/unop.cc:
Remove is_eltl_formula().
* src/tests/kind.test: Adjust.
 2015-06-20 15:21:31 +02:00
Alexandre Duret-Lutz
ce3ad1e3ff * doc/org/tut20.org: Make sure the cleanup is run. 2015-06-20 14:14:26 +02:00
Alexandre Duret-Lutz
ab83c798f6 * doc/org/syntax.css: Do not set the body colors. 2015-06-20 14:13:16 +02:00
Alexandre Duret-Lutz
27cab60c01 * doc/org/spot.css: Point to new website. 2015-06-19 23:35:39 +02:00
Alexandre Duret-Lutz
c8d964df05 * doc/org/syntax.css: Fix syntax. 2015-06-19 23:35:30 +02:00
Alexandre Duret-Lutz
5b72c5a064 org: really fix the satmin.org example 
* doc/org/satmin.org: Fix export.  We need both 'results: silent' and
'exports: both' for the code to be run and shown.
 2015-06-19 23:14:19 +02:00
Alexandre Duret-Lutz
28c8666cf8 doc: make clean should not need latexmk 
Report from Joachim Klein.

* doc/tl/Makefile.am (mostlyclean-local): Rename as...
(maintainer-clean-local): ... this.
 2015-06-19 17:08:26 +02:00
Alexandre Duret-Lutz
162e114396 org: fix SAT example 
* doc/org/satmin.org: Do not use ":export code" on
code that must be run on export.
 2015-06-19 17:04:10 +02:00
Alexandre Duret-Lutz
9130cfa17f org: Simplify build 
* doc/Makefile.am (org): Remove the useless temporary directory.
 2015-06-19 17:02:19 +02:00
Alexandre Duret-Lutz
95ea1ee075 org: fix recursive compilation 
* doc/Makefile.am (org): Use $(MAKE), not make.
(org-deploy): Remove this obsolete rule.
 2015-06-18 14:31:36 +02:00
Alexandre Duret-Lutz
286775ee68 * doc/org/index.org: Remove up/home links. 2015-06-17 22:33:23 +02:00
Alexandre Duret-Lutz
d8b3062b35 * doc/Doxyfile.in: Fix input encoding. 2015-06-17 11:38:21 +02:00
Alexandre Duret-Lutz
ccd60c8c5e org: link to Doxygen documentation, and to on-line translator 
* doc/org/index.org: Here.
 2015-06-17 11:38:16 +02:00
Alexandre Duret-Lutz
128f105fe5 * doc/mainpage.dox: Update URL. 2015-06-17 00:03:39 +02:00
Alexandre Duret-Lutz
1b3054d8a8 org: simplify calls to ltl2dstar 
* doc/org/satmin.org: Here.
 2015-06-16 22:33:32 +02:00
Alexandre Duret-Lutz
c0aa403867 * doc/org/install.org: Do not use {{{LASTRELEASE}}} in <code>. 2015-06-16 20:25:26 +02:00
Alexandre Duret-Lutz
3e853eedeb org: add utf-8 markers 
* doc/org/index.org, doc/org/ltl2tgta.org, doc/org/randltl.org,
doc/org/satmin.org, doc/org/tut.org, doc/org/tut01.org,
doc/org/tut02.org, doc/org/tut10.org, doc/org/tut20.org,
doc/org/tut21.org, doc/org/tut22.org: Here.
 2015-06-14 23:40:34 +02:00
Alexandre Duret-Lutz
89592881c7 org: new example 
Fixes #14.

* doc/org/tut22.org: New file.
* doc/Makefile.am, doc/org/tut.org: Add it.
 2015-06-12 22:01:30 +02:00
Alexandre Duret-Lutz
562a8d0f20 * doc/org/tut21.org: Show the initial state number. 2015-06-12 21:08:52 +02:00
Alexandre Duret-Lutz
4d848e988c org: new example 
* doc/org/tut21.org: New file.
* doc/Makefile.am, doc/org/tut.org: Add it.
 2015-06-12 00:42:05 +02:00
Alexandre Duret-Lutz
a1ba0a89c5 * doc/org/tut20.org: Cleanup. 2015-06-11 22:36:09 +02:00