Commit graph

276 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
78fd7beaaf org: Add a Concepts page.
* doc/org/concepts.org: New file.
* doc/Makefile.am: Add it.
* doc/org/oaut.org: Add anchor.
* doc/org/index.org, doc/org/tut.org: Add links to concepts.org.
* doc/org/spot.css: Set up boxes for implementation details.
* NEWS: Mention the new page.
2016-01-23 17:49:32 +01:00
Alexandre Duret-Lutz
73b1a0901e * doc/org/.gitignore: Add sitemap.org. 2016-01-21 19:07:48 +01:00
Alexandre Duret-Lutz
ad8b964520 org: generate a sitemap
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Enable sitemap
generation.
2016-01-18 16:57:26 +01:00
Alexandre Duret-Lutz
5b82978449 * doc/org/setup.org: Disable html postamble. 2016-01-18 16:57:06 +01:00
Alexandre Duret-Lutz
f466320b4a Release Spot 1.99.7
* NEWS, configure.ac, doc/org/setup.org: Bump version to 1.99.7.
2016-01-15 11:30:16 +01:00
Alexandre Duret-Lutz
0f39da9ed6 * doc/org/compile.org: Typos. 2016-01-15 08:39:08 +01:00
Alexandre Duret-Lutz
da391492f3 twa: store property bits as trivals
* spot/twa/twa.hh: Store property bits as trivals.
* NEWS: Mention the change.
* spot/parseaut/parseaut.yy, spot/twaalgos/are_isomorphic.cc,
spot/twaalgos/complete.cc, spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc,
spot/twaalgos/isdet.cc, spot/twaalgos/isunamb.cc, spot/twaalgos/lbtt.cc,
spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/postproc.cc,
spot/twaalgos/remfin.cc, spot/twaalgos/strength.cc,
spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh,
spot/twaalgos/totgba.cc, tests/core/ikwiad.cc,
tests/python/product.ipynb, tests/python/remfin.py: Adjust.
* doc/org/hoa.org, doc/org/tut21.org: Update documentation.
2016-01-13 17:57:54 +01:00
Alexandre Duret-Lutz
d0b38156f3 bin: make HOA the default output
* bin/common_aoutput.cc: Make HOA the default output.
* NEWS: Mention this.
* doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/hoa.org,
doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/ltldo.org, doc/org/oaut.org, doc/org/randaut.org,
doc/org/satmin.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut20.org, doc/org/tut21.org, doc/org/tut30.org,
tests/core/dstar.test, tests/core/ltldo2.test, tests/core/monitor.test,
tests/python/piperead.ipynb: Adjust.
2016-01-08 13:42:57 +01:00
Alexandre Duret-Lutz
cca2022e90 bin: add -d as a shorthand for --dot
* bin/common_aoutput.cc: Here.
* NEWS, doc/org/oaut.org: Mention it.
* tests/core/readsave.test: Use it once.
2016-01-06 16:27:59 +01:00
Alexandre Duret-Lutz
ea5f52ddbb randaut: rename -d as -e
This is so that we can have -d as an alias for --dot everywhere.

* bin/randaut.cc: Rename -d as -e.
* NEWS: Mention the change.
* doc/org/autfilt.org, doc/org/oaut.org, doc/org/randaut.org,
tests/core/parseaut.test, tests/core/readsave.test: Adjust.
2016-01-06 15:54:11 +01:00
Alexandre Duret-Lutz
8c04e31a35 org: fix definition of PATH
* doc/org/.dir-locals.el.in, doc/org/init.el.in: bin/ is no longer in
spot/.
2016-01-06 15:43:36 +01:00
Alexandre Duret-Lutz
5cb94a1a3f Merge the core and python tests in the tests/ directory
* tests/: Rename as...
* tests/core/: ... this.
* python/tests/: Rename as...
* tests/python/: ... this.
* python/tests/run.in: Move as...
* tests/run.in: This, and adjust.
* tests/Makefile.am: Adjust to run both core and python tests.
* configure.ac, README, debian/python3-spot.examples, debian/rules,
doc/org/tut.org, python/Makefile.am, spot/ltsmin/Makefile.am,
spot/ltsmin/kripke.test, spot/sanity/ipynb.test: Adjust.
2016-01-04 16:02:30 +01:00
Alexandre Duret-Lutz
8483f7fc50 * doc/org/tut.org: Minor fixes. 2015-12-27 20:20:42 +01:00
Alexandre Duret-Lutz
34c3c1cedc rename wrap/python/ to python/
* wrap/python/: Rename to...
* python/: ... this.
* wrap/: Delete.
* Makefile.am, README, configure.ac, debian/python3-spot.examples,
debian/rules, doc/org/.dir-locals.el.in, doc/org/init.el.in,
spot/sanity/ipynb.test: Adjust.
2015-12-25 12:38:25 +01:00
Alexandre Duret-Lutz
74ec9c54c4 show how to implement product in Python
* wrap/python/tests/product.ipynb: New file.
* wrap/python/tests/Makefile.am, doc/org/tut.org: Add it.
* wrap/python/tests/ipnbdoctest.py: Ignore %timeit results.
* wrap/python/spot_impl.i: Add bindings for
set_state_names()/get_state_names().
* spot/twaalgos/product.cc: Fix computation of properties.
* doc/org/hoa.org: Name.
* NEWS: Update.
2015-12-24 19:47:15 +01:00
Alexandre Duret-Lutz
2927cf38ac python: add some doc & tests for the acceptance bindings
* wrap/python/tests/acc_cond.ipynb: New file.
* wrap/python/tests/Makefile.am, doc/org/tut.org: Add it.
* wrap/python/spot_impl.i: Add printer for acc_cond::mark_t.
2015-12-16 19:06:20 +01:00
Alexandre Duret-Lutz
c39d35d068 python: port the tut22.org example to Python
* wrap/python/spot_impl.i: Extend acc_cond::mark_t to with a constructor
that takes a vector.
* doc/org/tut22.org: Add a Python version.
* doc/org/tut.org: Adjust the list, we don't have any C++-specific
example.
* NEWS: Mention it.
2015-12-15 19:01:33 +01:00
Alexandre Duret-Lutz
9313222e95 python: allow iterating over the successors of a state
Fixes #118.

* spot/twa/twagraph.hh: Avoid using graph_t::state to help Swig.
* wrap/python/spot_impl.i: Add a __str__ function for acc_cond::mark_t.
* doc/org/tut21.org: Add the Python version.
* doc/org/tut.org: Move tut21.org to the Python/C++ section.
* NEWS: Update.
2015-12-14 11:51:57 +01:00
Alexandre Duret-Lutz
2d3e7cecf5 org: update Spot description on index page
* doc/org/index.org: Here.
2015-12-08 22:43:42 +01:00
Alexandre Duret-Lutz
1f2260f971 introduce is_inherently_weak_automaton()
* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh
(is_inherently_weak_automaton): New function.
(is_type_automaton): Adjust to implement the above and
set prop_inherently_weak().
* spot/twaalgos/isweakscc.cc, spot/twaalgos/isweakscc.hh:
Rewrite is_inherently_weak_scc() to not enumerate cycles.
* spot/bin/autfilt.cc: Add a --is-inherently-weak option.
* spot/tests/readsave.test: More tests.
* spot/tests/strength.test: Adjust expected output.
* doc/org/hoa.org: Adjust documentation of --check.
* NEWS: Mention those changes.
2015-12-08 18:13:19 +01:00
Alexandre Duret-Lutz
690b8f51c7 org: some documentation about compiling C++
* doc/org/compile.org: New file.
* doc/Makefile.am: Add it.
* NEWS: Mention it.
* doc/org/tut.org, doc/org/tut01.org: Link to it.
2015-12-05 11:29:02 +01:00
Alexandre Duret-Lutz
f120dd3206 rename src/ as spot/ and use include <spot/...>
* NEWS: Mention the change.
* src/: Rename as ...
* spot/: ... this, adjust all headers to include <spot/...> instead of
"...", and adjust all Makefile.am to search headers from the top-level
directory.
* HACKING: Add conventions about #include.
* spot/sanity/style.test: Add a few more grep to catch cases
that do not follow these conventions.
* .gitignore, Makefile.am, README, bench/stutter/Makefile.am,
bench/stutter/stutter_invariance_formulas.cc,
bench/stutter/stutter_invariance_randomgraph.cc, configure.ac,
debian/rules, doc/Doxyfile.in, doc/Makefile.am,
doc/org/.dir-locals.el.in, doc/org/g++wrap.in, doc/org/init.el.in,
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, iface/ltsmin/Makefile.am,
iface/ltsmin/kripke.test, iface/ltsmin/ltsmin.cc,
iface/ltsmin/ltsmin.hh, iface/ltsmin/modelcheck.cc,
wrap/python/Makefile.am, wrap/python/ajax/spotcgi.in,
wrap/python/spot_impl.i, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/randgen.py, wrap/python/tests/run.in: Adjust.
2015-12-04 20:13:59 +01:00
Alexandre Duret-Lutz
af96afac82 Release Spot 1.99.6
* NEWS, configure.ac, doc/org/setup.org: Update version and date.
2015-12-04 08:12:34 +01:00
Alexandre Duret-Lutz
cff79b063b * doc/org/hoa.org: Simplify wording in property table. 2015-11-29 02:51:32 +01:00
Alexandre Duret-Lutz
745fda1a4f print_hoa: add option "k"
* src/twaalgos/hoa.cc, src/twaalgos/hoa.hh: Implement it.
* NEWS, doc/org/hoa.org, src/bin/common_aoutput.cc: Document it.
* src/tests/readsave.test: Test it.
2015-11-28 02:18:13 +01:00
Alexandre Duret-Lutz
6237bf4cd6 org: more language tooltips in HTML output
* doc/org/spot.css: add tooltips for Python and C++.
2015-11-20 14:50:25 +01:00
Alexandre Duret-Lutz
5aba246ff0 org: syntax-highlight the HOA outputs
* elisp/hoa-mode.el, elisp/Makefile.am, elisp/README: New files.
* debian/copyright, configure.ac, README, Makefile.am: Adjust.
* doc/org/init.el.in: Adjust to load hoa-mode.el.
* doc/org/spot.css: Add entries for HOA mode.
* doc/org/hoa.org, doc/org/ltldo.org, doc/org/oaut.org,
doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.org,
doc/org/tut30.org: Make the HOA outputs as HOA.
2015-11-20 14:28:51 +01:00
Alexandre Duret-Lutz
c1bfc5d59b doc: two typos
* doc/mainpage.dox, doc/org/tut01.org: Here.
2015-11-17 18:18:50 +01:00
Alexandre Duret-Lutz
104a372c41 Add a notebook illustrating decompose_strength()
* wrap/python/tests/decompose.ipynb: New file.
* wrap/python/tests/Makefile.am: Add it.
* src/twaalgos/strength.cc: Fix corner cases.
* src/tests/strength.test: Adjust corner case.
* NEWS, doc/org/tut.org: Mention the notebook.
2015-11-08 22:07:43 +01:00
Alexandre Duret-Lutz
3428fb32cd Add support for --check=strength
* src/twaalgos/strength.cc, src/twaalgos/strength.hh (check_strength):
New function.
* src/bin/common_aoutput.cc: Add --check=strength.
* src/tests/strength.test: New file.
* src/tests/Makefile.am: Add it.
* doc/org/hoa.org, NEWS: Document it.
2015-11-07 21:40:04 +01:00
Alexandre Duret-Lutz
0c5f87b442 add support for the "terminal" property
* src/twa/twa.hh: Store the terminal property.
* src/twaalgos/hoa.cc, src/parseaut/parseaut.yy: Add I/O for "terminal".
* src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/minimize.cc: Set terminal
as apropriate.
* src/twaalgos/safety.cc: Use it.
* doc/org/tut21.org, doc/org/hoa.org, NEWS: Document it.
* src/tests/complement.test, src/tests/monitor.test,
wrap/python/tests/automata-io.ipynb: Adjust.
2015-11-07 14:04:44 +01:00
Alexandre Duret-Lutz
654888718c add support for the weak property
This fixes #119.

* doc/org/tut21.org, doc/org/hoa.org, NEWS: Document it.
* src/twa/twa.hh: Support it in automata.
* src/twaalgos/hoa.cc, src/parseaut/parseaut.yy: Add I/O support.
* src/twaalgos/minimize.cc, src/twaalgos/totgba.cc: Set weak
automata on output.
* src/tests/complement.test, src/tests/parseaut.test,
src/tests/readsave.test, src/tests/remfin.test, src/tests/sccsimpl.test,
src/tests/wdba2.test, wrap/python/tests/automata-io.ipynb: Adjust.
2015-11-06 21:51:48 +01:00
Alexandre Duret-Lutz
eecd201273 org: more examples of accessing properties
For the first part of #118.

* doc/org/tut21.org: Here.
2015-11-06 16:15:34 +01:00
Alexandre Duret-Lutz
33c234da11 hoa: output "unambiguous" only for non-deterministic automata by default
* src/twaalgos/hoa.cc: Output do not output "unambiguous" if the
automaton is deterministic.  Add option "v" to cancel this restriction,
and also output "no-univ-branch".
* src/twaalgos/hoa.hh: Document the "v" option.
* src/tests/readsave.test: Test it.
* src/tests/unambig.test: Adjust for unambiguous not being output
if the automaton is deterministic.
* src/bin/common_aoutput.cc, NEWS: Document it.
* doc/org/hoa.org: Add a summary table about how properties are handled.
* src/twa/twa.hh (prop_deterministic): Setting this should also
set the unambiguous property.
* src/twaalgos/isunamb.cc: Simplify the property check.
2015-11-05 19:42:08 +01:00
Alexandre Duret-Lutz
30037b9905 org: update description of support for HOA properties
* doc/org/hoa.org: Here.  Also mention --trust-hoa.
2015-11-05 17:16:54 +01:00
Alexandre Duret-Lutz
cbb2e64e7c twa: rename the is_* getters as prop_*
This fixes #116.

* src/twa/twa.hh: Rename those methods.
* NEWS: Document the renamings.
* doc/org/hoa.org, doc/org/tut21.org, src/parseaut/parseaut.yy,
src/tests/ikwiad.cc, src/twa/twagraph.hh,
src/twaalgos/are_isomorphic.cc, src/twaalgos/complete.cc,
src/twaalgos/degen.cc, src/twaalgos/dot.cc, src/twaalgos/dtbasat.cc,
src/twaalgos/dtgbasat.cc, src/twaalgos/hoa.cc, src/twaalgos/isdet.cc,
src/twaalgos/isunamb.cc, src/twaalgos/lbtt.cc,
src/twaalgos/minimize.cc, src/twaalgos/postproc.cc,
src/twaalgos/product.cc, src/twaalgos/randomgraph.cc,
src/twaalgos/remfin.cc, src/twaalgos/sbacc.cc,
src/twaalgos/simulation.cc, src/twaalgos/stutter.cc,
src/twaalgos/totgba.cc: Adjust.
2015-11-05 09:51:53 +01:00
Alexandre Duret-Lutz
f08b658f04 Release Spot 1.99.5
* NEWS, configure.ac, doc/org/setup.org: Update version.
2015-11-03 13:42:27 +01:00
Alexandre Duret-Lutz
a28ead2dce org: simply calls to parse_aut()
* doc/org/tut20.org, doc/org/tut21.org, doc/org/tut30.org: Simplify
the calls to parse_aut.
2015-11-03 11:58:40 +01:00
Alexandre Duret-Lutz
71979840cb bin: factor handling of -B/-C/-D/... output options
* src/bin/common_post.cc: Handle the options
for BA/TGBA/Monitor as well as Complete/SBAcc here,
and in the same group.  Rename "Translation intent"
and "Optimization level" to "Simplification goal" and
"Simplification level" so that it makes sense even
in autfilt.
* src/bin/autfilt.cc, src/bin/dstar2tgba.cc,
src/bin/ltl2tgba.cc: Remove common code.
* doc/org/autfilt.org, doc/org/dstar2tgba.org,
doc/org/ltl2tgba.org: Adjust sed invocations.
2015-10-26 20:28:06 +01:00
Alexandre Duret-Lutz
dee73ee342 parse_aut: simplify the interface
* src/parseaut/public.hh, src/parseaut/parseaut.yy,
src/parseaut/fmterror.cc: Add a raise_errors options.  Remove the
parse_strict() method.  Store parse errors and filename in the output
parsed_aut to simplify usage.
* doc/org/tut20.org, doc/org/tut21.org, doc/org/tut30.org,
src/bin/autfilt.cc, src/bin/common_hoaread.cc, src/bin/dstar2tgba.cc,
src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tests/complementation.cc,
src/tests/ikwiad.cc, src/tests/ltlcross3.test, src/tests/ltldo.test,
wrap/python/spot.py, wrap/python/tests/parsetgba.py: Adjust usage.
* NEWS: Mention the changes.
2015-10-26 20:28:06 +01:00
Alexandre Duret-Lutz
84f9be9e8e doc: show more metadata about automata
* src/twa/bdddict.hh (varnum): New method.
* doc/org/tut21.org: Show more metadata.
2015-10-23 13:58:27 +02:00
Alexandre Duret-Lutz
64607af7ab propagate the new minimum version of python
* README, doc/org/install.org, m4/pypath.m4: We now require Python 3.3
or later.
2015-10-21 14:27:18 +02:00
Alexandre Duret-Lutz
c7d063aaa0 org: fix multiple examples
I have to remember that org-mode does not evaluate something unless it
is eventually exported.

* doc/org/hoa.org, doc/org/ioltl.org, doc/org/tut21.org,
doc/org/tut30.org: Adjust exports commands.
2015-10-20 14:53:57 +02:00
Alexandre Duret-Lutz
61bf5daab4 Add code example using the postprocessor.
* doc/org/tut30.org: New file.
* doc/Makefile.am, doc/org/tut.org: Add it.
2015-10-19 23:15:52 +02:00
Alexandre Duret-Lutz
176c9e2e17 tl: rename ltl_simplifier to tl_simplifier
* doc/org/tut01.org, doc/tl/tl.tex, src/bin/common_r.hh,
src/bin/ltlfilt.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc,
src/tests/randtgba.cc, src/tests/reduc.cc, src/tests/syntimpl.cc,
src/tl/nenoform.cc, src/tl/randomltl.cc, src/tl/randomltl.hh,
src/tl/simplify.cc, src/tl/simplify.hh, src/twaalgos/ltl2tgba_fm.cc,
src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/stutter.cc,
src/twaalgos/translate.cc, src/twaalgos/translate.hh,
wrap/python/ajax/spotcgi.in, wrap/python/spot.py,
wrap/python/tests/interdep.py: Rename ltl_simplifier to tl_simplifier.
* NEWS: Mention it.
2015-10-18 13:35:23 +02:00
Alexandre Duret-Lutz
24a8affbc5 org: better syntax highlighting
* doc/org/init.el.in: Activate CSS for code fragments.
* doc/org/spot.css: Style relevant elements.
2015-10-03 17:14:52 +02:00
Alexandre Duret-Lutz
5bfd0267e7 python: implement formula.__format__
Fixes #105.

* src/bin/common_trans.cc (quote_shell_string): Move ...
* src/misc/escape.cc, src/misc/escape.hh (quote_shell_string):
... here.
* wrap/python/spot_impl.i: Wrap escape.hh.
* wrap/python/spot.py: Implement formula.__format__.
* wrap/python/tests/ltlsimple.py: Test it.
* NEWS, doc/org/tut01.org, wrap/python/tests/formulas.ipynb: Document
it.
2015-10-03 15:46:05 +02:00
Alexandre Duret-Lutz
59685eada0 Spot 1.99.4
* NEWS, configure.ac, doc/org/setup.org: Bump version.
* doc/org/index.org: Better wording of a link.
2015-10-01 07:39:02 +02:00
Alexandre Duret-Lutz
7c5f345d68 * doc/org/tut03.org: Fix typos. 2015-09-30 18:50:57 +02:00
Alexandre Duret-Lutz
ae6cd92142 ltlparse: move in parsetl/, and declare in tl/parse.hh
* src/ltlparse/public.hh: Rename as...
* src/tl/parse.hh: ... this.
* src/ltlparse/: Rename as...
* src/parsetl/: ... this.
* NEWS: Mention the change.
* README, configure.ac, doc/org/tut01.org, doc/org/tut02.org,
doc/org/tut03.org, doc/org/tut10.org, src/Makefile.am,
src/bin/common_finput.cc, src/bin/common_finput.hh, src/bin/ltl2tgta.cc,
src/kripkeparse/kripkeparse.yy, src/parseaut/parseaut.yy,
src/tests/checkpsl.cc, src/tests/checkta.cc,
src/tests/complementation.cc, src/tests/consterm.cc,
src/tests/emptchk.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc,
src/tests/kind.cc, src/tests/length.cc, src/tests/ltlprod.cc,
src/tests/ltlrel.cc, src/tests/randtgba.cc, src/tests/readltl.cc,
src/tests/reduc.cc, src/tests/syntimpl.cc, src/tests/tostring.cc,
src/tl/Makefile.am, src/twaalgos/lbtt.cc, wrap/python/spot_impl.i,
iface/ltsmin/modelcheck.cc: Adjust.
2015-09-30 17:38:06 +02:00