Commit graph

46 commits

Author SHA1 Message Date
Thibaud Michaud
0821c97eb8 add ltlsynt executable
For now, ltlsynt only handles LTL realizability. It uses a reduction to
parity game followed by Calude et al.'s reduction from parity game to
reachability game.

* bin/ltlsynt.cc, bin/Makefile.am, bin/man/ltlsynt.x,
bin/man/Makefile.am, bin/.gitignore: New binary.
* doc/org/arch.tex, doc/Makefile.am, doc/org/tools.org,
doc/org/ltlsynt.org: Document it.
* spot/misc/game.cc, spot/misc/game.hh, spot/misc/Makefile.am: Parity
game wrapper for parity automata + reachability game interface from
Calude et al.'s paper.
2017-09-25 12:23:47 +02:00
Alexandre Duret-Lutz
0cf250d839 bin: introduce autcross
Fixes #252.

* NEWS: Mention it.
* bin/autcross.cc, bin/man/autcross.x, doc/org/autcross.org: New
files.
* bin/Makefile.am, bin/man/Makefile.am, doc/org/tools.org,
doc/Makefile.am: Add them.
* bin/autfilt.cc: Use is_universal() instead of is_deterministic().
* bin/common_hoaread.hh, bin/common_trans.cc, bin/common_trans.hh,
bin/ltlcross.cc, bin/ltldo.cc: Factor some bits common between
ltlcross, ltldo and autcross.
* tests/core/autcross.test, tests/core/autcross2.test: New files.
* tests/Makefile.am: Add them.
* tests/core/dra2dba.test, tests/core/sbacc.test,
tests/core/streett.test: Use autcross.
2017-07-28 10:33:14 +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
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
b439fc674b org: add a citing page
With a reference to the "to appear" ATVA'16 paper.

* doc/org/citing.org: New file.
* doc/Makefile.am: Add it.
* doc/org/index.org, doc/org/tools.org: Link to it.
2016-06-17 15:33:39 +02:00
Alexandre Duret-Lutz
c035ea1822 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:23:01 +02:00
Alexandre Duret-Lutz
d02ee34e10 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 10:41:41 +02:00
Alexandre Duret-Lutz
48e6ef7065 * doc/org/tools.org: Minor tweaks. 2016-05-02 10:06:29 +02:00
Alexandre Duret-Lutz
9d5d1dc8dd 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 17:13:13 +02:00
Alexandre Duret-Lutz
17a18f2890 adjust documentation for the merge of the dstar parser
* NEWS: Mention the changes.
* doc/org/autfilt.org, doc/org/dstar2tgba.org,
doc/org/ltlcross.org, doc/org/tools.org, doc/org/tut20.org,
src/bin/man/dstar2tgba.x, src/bin/man/ltlcross.x: Adjust
documentation.
* src/bin/common_trans.cc: Use %O instead of %D, but keep %D
hidden for backward compatibility.
2015-09-09 00:49:13 +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
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
2e34fa4248 org: add installation instructions
* doc/org/install.org: New file.
* doc/Makefile.am: Add it.
* doc/org/index.org: Link to it.
* doc/org/setup.org: Add macro for
various version numbers.
* doc/org/tools.org: Update version number.
* NEWS, README, bench/ltl2tgba/README, debian/control,
debian/copyright: Update URLs to website.
2015-06-07 23:59:08 +02:00
Alexandre Duret-Lutz
a8f02ed8ca org: add an index page
* doc/org/index.org, doc/org/tut.org: New files.
* doc/Makefile.am: Add them.
* doc/org/setup.org: Adjust HOME link.
* doc/org/tools.org: Adjust UP link.
* debian/spot-doc.doc-base: The root is now index.html.
2015-06-07 16:51:33 +02:00
Alexandre Duret-Lutz
6b28cc9170 org: document HOA support
* doc/org/hoa.org: New file.
* doc/org/oaut.org, doc/org/tools.org: Link to it.
* doc/Makefile.am: Distribute it.
2015-05-30 13:01:43 +02:00
Alexandre Duret-Lutz
96e2da8666 sat-minimize: some documentation and associated fixes
* doc/org/satmin.org: Document the new DTωA-minimization procedure.
* doc/org/tools.org: Fix link.
* src/bin/autfilt.cc: Pass -S to sat_minimize().
* src/twa/twagraph.hh: (state_acc_sets) New method.
* src/twaalgos/dotty.cc: Use it to correctly display co-Büchi automata.
* src/twaalgos/dtbasat.cc: Set the deterministic property on the result.
* src/twaalgos/dtgbasat.cc: Likewise, and preprocess the input automaton
in sat_minimize().
* src/twaalgos/dtgbasat.hh: Fix documentation, and take the state-based
information as an argument.
* src/twaalgos/postproc.cc: Do not call simulation-based reduction
on non-separated acceptances.
* src/tests/satmin2.test: Use -S rather than 'state-based'.
* NEWS: Update.
2015-05-22 00:02:09 +02:00
Alexandre Duret-Lutz
16a8c03143 ltldo: new binary
* src/bin/common_trans.cc, src/bin/common_trans.hh: New files,
extracted from...
* src/bin/ltlcross.cc: ... here, so that ltldo can use them.
* src/bin/ltldo.cc: New file.
* src/bin/Makefile.am: Adjust.
* src/bin/common_aoutput.cc, src/bin/common_aoutput.hh: Make
it possible to add new statistics.
* doc/org/ltldo.org: New file.
* doc/Makefile.am, doc/org/tools.org: Adjust.
* src/bin/man/ltldo.x: New file.
* src/bin/man/Makefile.am: Adjust.
* src/bin/man/ltlcross.x, src/bin/man/ltlfilt.x: Mention ltldo(1).
* src/tgbatest/ltldo.test, src/tgbatest/ltldo2.test: New files.
* src/tgbatest/Makefile.am: Add them.
* NEWS: Mention ltldo.
2015-01-27 08:18:15 +01:00
Alexandre Duret-Lutz
c44b158716 org: declare utf8 everwhere and fix some typos
* doc/org/autfilt.org, doc/org/csv.org, doc/org/dstar2tgba.org,
doc/org/genltl.org, doc/org/ioltl.org, doc/org/ltl2tgba.org,
doc/org/ltlfilt.org, doc/org/ltlgrind.org, doc/org/oaut.org,
doc/org/randaut.org, doc/org/tools.org: Update.
2015-01-25 12:03:15 +01:00
Alexandre Duret-Lutz
ee0c0cd28c * doc/org/tools.org: Adjust colors in text. 2015-01-08 18:33:17 +01:00
Alexandre Duret-Lutz
56ed13a96d org: factor headers into setup.org
* doc/org/setup.org: New file.
* doc/Makefile.am: Distribute it.
* doc/org/autfilt.org, doc/org/csv.org, doc/org/dstar2tgba.org,
doc/org/genltl.org, doc/org/ioltl.org, doc/org/ltl2tgba.org,
doc/org/ltl2tgta.org, doc/org/ltlcross.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: Use
setup.org.
2015-01-07 19:35:30 +01:00
Alexandre Duret-Lutz
f88020035c org: fix EMAIL link
* doc/org/autfilt.org, doc/org/csv.org, doc/org/dstar2tgba.org,
doc/org/genltl.org, doc/org/ioltl.org, doc/org/ltl2tgba.org,
doc/org/ltl2tgta.org, doc/org/ltlcross.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: Here.
2015-01-06 18:23:58 +01:00
Alexandre Duret-Lutz
cbf1e15b01 org: document common output options for automata
* doc/org/oaut.org: New file.
* doc/Makefile.am: Add it.
* doc/org/autfilt.org, doc/org/ltl2tgba.org, doc/org/randaut.org,
doc/org/tools.org: Link to it.
2015-01-04 17:08:39 +01:00
Alexandre Duret-Lutz
d2597854c8 Merge branch 'master' into next
Conflicts:
	NEWS
	configure.ac
	src/kripketest/bad_parsing.test
	src/ltltest/reduccmp.test
	src/neverparse/neverclaimscan.ll
	src/tgba/futurecondcol.cc
	src/tgba/tgbasafracomplement.cc
	src/tgbaalgos/hoa.cc
	src/tgbaalgos/ltl2tgba_fm.cc
	src/tgbatest/neverclaimread.test
	src/tgbatest/readsave.test
2014-12-06 14:02:38 +01:00
Alexandre Duret-Lutz
44b374d1b9 Release Spot 1.2.6.
* NEWS, configure.ac, doc/org/tools.org: Bump version number.
2014-12-06 12:35:05 +01:00
Alexandre Duret-Lutz
e6e416e1e1 document autfilt and randaut
* NEWS: Mention these tools.
* doc/org/autfilt.org, doc/org/randaut.org: New files.
* doc/org/tools.org, doc/Makefile.am: Add them.
2014-11-29 18:03:56 +01:00
Thibaud Michaud
e327f6ea11 Adding ltlgrind as a command-line tool
* src/bin/ltlgrind.cc: New file, command-line tool to get mutations of a
formula.
* src/bin/Makefile.am: Add it.
* src/ltlvisit/mutation.hh, src/ltlvisit/mutation.cc:
New files providing the get_mutations function.
* src/ltlvisit/Makefile.am: Add it.
* src/ltltest/ltlgrind.test: Test it.
* src/ltltest/Makefile.am: Add it.
* src/bin/man/ltlgrind.x: Document it.
* src/bin/man/Makefile.am: Add it.
* doc/org/ltlgrind.org: Document it.
* doc/org/tools.org: Add link to ltlgrind documentation page.
2014-10-06 17:42:30 +02:00
Alexandre Duret-Lutz
290106b0a4 Release Spot 1.2.5.
* configure.ac, doc/org/tools.org, NEWS: Bump version to 1.2.5.
2014-08-21 23:16:39 +02:00
Alexandre Duret-Lutz
c11f15c76c Release Spot 1.2.4
* NEWS, configure.ac, doc/org/tools.org: Bump version.
2014-05-15 11:07:25 +02:00
Alexandre Duret-Lutz
9761703736 doc: update bibliographic references
* doc/org/satmin.org, src/bin/man/dstar2tgba.x, src/bin/man/ltl2tgba.x:
Cite the FORTE'14 paper.
* doc/org/tools.org, src/bin/man/ltl2tgba.x: Replace the VECOS'11
citation by IJCCBS'14.
* src/bin/man/ltl2tgba.x: Cite SPIN'13.
2014-05-14 18:16:12 +02:00
Alexandre Duret-Lutz
2a7d5f5f7f Release Spot 1.2.3
* NEWS, configure.ac, doc/org/tools.org: Update version.
2014-02-11 17:20:58 +01:00
Alexandre Duret-Lutz
35612f3626 Release Spot 1.2.2
* NEWS, configure.ac, doc/org/tools.org: Set version to 1.2.2.
2014-01-24 11:16:07 +01:00
Alexandre Duret-Lutz
4d7638a269 Release Spot 1.2.1.
* NEWS, configure.ac, doc/org/tools.org: Bump version to 1.2.1.
2013-12-11 10:40:33 +01:00
Alexandre Duret-Lutz
846e33b9e5 ltl2tgba: Add a --csv-escape option and document CSV I/O.
* src/bin/common_output.cc, src/bin/common_output.hh:
(output_formula_checked, aut_stat_printer): New.
* src/bin/genltl.cc, src/bin/randltl.cc, src/bin/ltlfilt.cc: Call
output_formula_checked() instead of output_formula().
* src/bin/ltl2tgba.cc: Use aut_stat_printer and add option --csv-escape.
* doc/org/csv.org: New file to document CSV I/O.
* doc/Makefile.am: Add it.
* doc/org/ioltl.org, doc/org/ltlfilt.org, doc/org/ltl2tgba.org,
doc/org/tools.org: Link to csv.org
2013-12-06 11:09:36 +01:00
Alexandre Duret-Lutz
3e3d320de5 doc: add suggestions for bibliographic references
* doc/org/tools.org, src/bin/man/genltl.x, src/bin/man/ltl2tgba.x,
src/bin/man/ltl2tgta.x, src/bin/man/ltlcross.x, src/bin/man/ltlfilt.x,
src/bin/man/randltl.x: Add bibliographic references, mostly to
the ATVA'13 paper.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
c0a845b274 Release Spot 1.2.
* NEWS, configure.ac, doc/org/tools.org: Bump version to 1.2.
2013-10-01 13:23:47 +02:00
Alexandre Duret-Lutz
3076c3da4e org: document SAT-based minimization
* doc/org/satmin.org, doc/org/satmin.tex: New files.
* doc/Makefile.am: Add them.
* doc/org/tools.org: Point to satmin.org.
* NEWS: Mention satmin.html.
2013-09-16 08:39:06 +02:00
Alexandre Duret-Lutz
f704513b6b org: document dstar2tgba.
* doc/org/dstar2tgba.org: New file.
* doc/org/tools.org: Link to it.
* doc/Makefile.am: Distribute it.
* NEWS: Mention the generated web page.
2013-08-26 17:27:39 +02:00
Alexandre Duret-Lutz
9d6d53ed92 Release Spot 1.1.4.
* NEWS, configure.ac, doc/org/tools.org: Update version.
2013-07-29 00:27:59 +02:00
Alexandre Duret-Lutz
026830d159 Release Spot 1.1.3.
* configure.ac, doc/org/tools.org, NEWS: Set version to 1.1.3.
2013-07-09 14:03:07 +02:00
Alexandre Duret-Lutz
424f04ca11 Release Spot 1.1.2.
* configure.ac, NEWS, doc/org/tools.org: Bump version to 1.1.2.
2013-06-09 18:05:20 +02:00
Alexandre Duret-Lutz
27a18a0410 Release Spot 1.1.1
* NEWS, configure.ac, doc/org/tools.org: Bump version.
2013-05-13 16:20:29 +02:00
Alexandre Duret-Lutz
556ba6df9e Release Spot 1.1
* configure.ac, doc/org/tools.org: Bump version number.
* NEWS: Likewise, plus some missing entries.
2013-04-28 16:31:20 +02:00
Alexandre Duret-Lutz
69dcff5ab0 org: Make sure ../../src/bin is searched first.
We used to set PATH in emacs, but because babel executes "sh" via
shell-command, the configuration of the main shell may supersedes ours.

* doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/ltlfilt.org, doc/org/randltl.org, doc/org/tools.org,
doc/org/genltl.org: Move all local-file variable to...
* doc/org/.dir-locals.el: ... here.  And also set the PATH
in org-babel-sh-command.
* doc/org/init.el.in: Set the PATH in org-babel-sh-command.
2013-04-11 19:02:45 +02:00
Alexandre Duret-Lutz
c24270bbf5 org: upgrade to 1.0.2
* doc/org/tools.org: Update to 1.0.2.
* doc/org/ltl2tgba.org: Mention monitors in the intro.
2013-04-09 15:05:56 +02:00
Alexandre Duret-Lutz
d1ad744887 org: update for 1.0.1
* doc/org/ioltl.org: Mention ltl2dstar and the changes to the prefix
parser.
* doc/org/ltlcross.org: Mention bench/ltl2tgba/sum.py.
* doc/org/tools.org: Bump version number.
2013-04-09 15:05:56 +02:00
Alexandre Duret-Lutz
345b8c5b14 doc: add org-mode documentation for user tools
* doc/org/.gitignore, doc/org/genltl.org, doc/org/ioltl.org,
doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/ltlfilt.org, doc/org/randltl.org, doc/org/tools.org: New files.
2013-04-09 15:05:56 +02:00