Commit graph

459 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
fb6cc0dff7 * doc/org/concepts.org: Fix reference to BuDDy. 2016-04-10 14:11:49 +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
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
54d6507fc2 Release Spot 1.99.9.
* NEWS, configure.ac, doc/org/setup.org: Bump version.
2016-03-13 16:45:08 +01:00
Alexandre Duret-Lutz
1287525afa * doc/org/autfilt.org: Add missing text. 2016-03-10 18:32:39 +01:00
Alexandre Duret-Lutz
7e2e4df1bb autfilt: add a --reject-word option
* bin/autfilt.cc: Implement --reject-word.
* NEWS, doc/org/autfilt.org: More doc.
* tests/core/acc_word.test: More tests.
2016-03-08 12:14:14 +01:00
Amaury Fauchille
1c82444376 autfilt: add new option --accept-word
Suggested by Matthias Heizmann. Fixes #109.

* NEWS: notify the new option
* THANKS: add Matthias Heizmann
* bin/autfilt.cc: add new option --accept-word=WORD which filters
automata that accept WORD
* doc/org/autfilt.org: add an example of the new option
* tests/Makefile.am: add core/acc_word.test to the list of test files
* tests/core/acc_word.test: test some uses of the new option
2016-03-07 22:19:25 +01:00
Alexandre Duret-Lutz
61b1f200b6 rename tgba_reachable_iterator as twa_reachable_iterator
* spot/twaalgos/reachiter.cc, spot/twaalgos/reachiter.hh: Here.
* spot/twaalgos/stats.cc, spot/twaalgos/lbtt.cc: Adjust.
* doc/org/upgrade2.org, NEWS: Mention the renaming.
2016-03-06 11:40:42 +01:00
Alexandre Duret-Lutz
ad08a585af rename two confusing methods of emptiness_check_instantiator
* spot/twaalgos/emptiness.hh (emptiness_check_instantiator): rename
min_acceptance_conditions and max_acceptance_conditions to
min_sets and max_sets.
* spot/twaalgos/emptiness.cc, python/ajax/spotcgi.in,
tests/core/ikwiad.cc, tests/core/emptchk.cc, tests/core/randtgba.cc:
Adjust.
* doc/org/upgrade2.org, NEWS: Mention the change.
2016-03-03 18:18:39 +01:00
Alexandre Duret-Lutz
e87b271ba5 * doc/org/upgrade2.org: Discuss get_dict(). 2016-03-03 16:46:58 +01:00
Alexandre Duret-Lutz
18d7d0a644 * doc/org/upgrade2.org: More text. 2016-03-03 10:29:12 +01:00
Alexandre Duret-Lutz
892e648970 org: add some help for upgrading old code
* doc/org/upgrade2.org: New file.
* doc/Makefile.am, doc/org/index.org: Add it.
* doc/org/tut22.org: Add some custom id for reference.
* doc/org/spot.css: Style the tables.
* NEWS: Mention the new doc.
2016-03-02 17:44:03 +01:00
Alexandre Duret-Lutz
b2d31b4170 org: Fix a section title.
* doc/org/concepts.org: Fix a mistake reported by František Blahoudek.
2016-03-01 14:27:07 +01:00
Alexandre Duret-Lutz
6b7f0399f4 Release Spot 1.99.8
* NEWS, configure.ac, doc/org/setup.org: Update version number.
2016-02-18 14:28:06 +01:00
Alexandre Duret-Lutz
d30f7e1f0f * doc/org/index.org: Link to spot-sandbox. 2016-02-18 14:24:07 +01:00
Alexandre Duret-Lutz
22f442f758 parsetl: change the interface to return a parsed_formula
This gets the interface of all the functions parsing formula in line
with the interface of the automaton parser: both return a "parsed_*"
object (parsed_formula or parsed_automaton) that contains the said
object and its list of errors.  Doing so avoid having to declare the
parse_error_list in advance.

* spot/tl/parse.hh, spot/parsetl/parsetl.yy: Do the change.
* spot/parsetl/fmterror.cc: Adjust the error printer.
* NEWS: Document it.
* bin/common_finput.cc, bin/common_finput.hh, bin/ltlcross.cc,
bin/ltldo.cc, bin/ltlfilt.cc, doc/org/tut01.org, doc/org/tut02.org,
doc/org/tut10.org, doc/org/tut20.org, python/ajax/spotcgi.in,
python/spot/impl.i, spot/parseaut/parseaut.yy, tests/core/checkpsl.cc,
tests/core/checkta.cc, tests/core/consterm.cc, tests/core/emptchk.cc,
tests/core/equalsf.cc, tests/core/ikwiad.cc, tests/core/kind.cc,
tests/core/length.cc, tests/core/ltlprod.cc, tests/core/ltlrel.cc,
tests/core/randtgba.cc, tests/core/readltl.cc, tests/core/reduc.cc,
tests/core/safra.cc, tests/core/syntimpl.cc, tests/core/tostring.cc,
tests/ltsmin/modelcheck.cc, tests/python/alarm.py,
tests/python/interdep.py, tests/python/ltl2tgba.py,
tests/python/ltlparse.py: Adjust all uses.
2016-02-17 20:31:58 +01:00
Etienne Renault
cf4f58c34b Update paths to please Darwin
Fixes #144.

* doc/org/.dir-locals.el.in,
doc/org/init.el.in,
python/ajax/spotcgi.in,
tests/run.in: Here.
2016-02-17 15:02:41 +01:00
Alexandre Duret-Lutz
1ae0600cae ltlcross: add option --determinize
* bin/ltlcross.cc: Implement it.
* doc/org/ltlcross.org, NEWS: Document it.
* tests/core/ltlcross.test, tests/core/ltlcrossce.test: Test it.
2016-02-15 19:16:45 +01:00
Alexandre Duret-Lutz
26d7264717 org: fix two links
Fixes #150.

* doc/org/tut.org: Fix links to notebooks.
* tests/sanity/ipynb.pl: Catch this type of errors in the future.
2016-02-15 17:17:10 +01:00
Alexandre Duret-Lutz
1b12df46fe ltlfilt: replace --[b]size-max/min by --[b]size
* bin/ltlfilt.cc: Implement the new option, and hide the old
ones.
* doc/org/ltlfilt.org, NEWS: Document these options.
* tests/core/ltl2dstar2.test, tests/core/randpsl.test: Adjust tests
to the new syntax.
2016-02-15 16:10:07 +01:00
Alexandre Duret-Lutz
369c2c537d org: mention the determinization on the main page
Fixes #145.

* doc/org/index.org: Here.
2016-02-13 15:54:27 +01:00
Alexandre Duret-Lutz
b066c6f3f2 postproc: add fine-tuning options for determinization
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh:
Add options det-scc, det-simul, det-stutter.
* bin/spot-x.cc: Document them.
* doc/org/ltl2tgba.org: Illustrate one of them and link
to the spot-x man page.
2016-02-12 14:07:58 +01:00
Alexandre Duret-Lutz
1e52d2a7a8 doc: more doc about determinization
* doc/org/autfilt.org: Here.
2016-02-12 14:07:28 +01:00
Alexandre Duret-Lutz
8568c3b423 postproc: integrate tgba_determinize()
* spot/twa/acc.hh: Add a smaller version of is_parity().
* spot/twaalgos/postproc.cc: Call tgba_determinize() if asked for
Generic acceptance and Deterministic output.
* bin/common_post.cc: Add 'G' as a shorthand for --generic.
* doc/org/ltl2tgba.org: Illustrate =ltl2tgba -G -D=.
2016-02-12 14:07:28 +01:00
Alexandre Duret-Lutz
064ccd5c05 fix paths mentioning buddy/src/.libs
Those had been incorrectly renamed to buddy/spot/.libs when we rename
the main src/ directory into spot/.  This only affected the setting of
DYLD_LIBRARY_PATH, that used to be needed on Darwin.

* doc/org/.dir-locals.el.in, doc/org/init.el.in, python/ajax/spotcgi.in,
tests/run.in: Fix the PATH.
2016-02-12 14:02:47 +01:00
Alexandre Duret-Lutz
77b0b5b3fe dot: add option C(COLOR)
This fixes the output gliches visible in the previous patches,
where highlighting a state would remove its fill color.

* spot/twaalgos/dot.cc, spot/taalgos/dot.cc: Implement option C(COLOR).
* bin/common_aoutput.cc, doc/org/oaut.org: Document it.
* doc/org/.dir-locals.el.in, doc/org/init.el.in,
python/spot/__init__.py: Use it.
* tests/python/automata-io.ipynb, tests/python/automata.ipynb,
tests/python/highlighting.ipynb: Test it.
* tests/core/readsave.test: Adjust.
* NEWS: Mention recent changes.
2016-02-05 19:26:38 +01:00
Alexandre Duret-Lutz
23c2cbf46a python: highlighting functions for edges and states
* python/spot/impl.i (highlight_state, highlight_edge): New function.
* python/spot/__init__.py (highlight_states, highlight_edges): New
functions.
* spot/twaalgos/dot.cc: Add a '#' option.
* spot/taalgos/dot.cc: Ignore '#'.
* tests/python/highlighting.ipynb: New file to illustrate everything.
* tests/Makefile.am, doc/org/tut.org: Add it.
2016-02-05 17:29:30 +01:00
Alexandre Duret-Lutz
2c67c68766 org: adjust PYTHONPATH after recent python changes
Fixes #137.

* doc/org/.dir-locals.el.in, doc/org/init.el.in: Search python modules
in python/spot as well.
2016-02-02 17:38:58 +01:00
Alexandre Duret-Lutz
5a5f83f468 python: add missing bindings for twa_word and twa_run
Fixes #133.

* python/spot/impl.i: Add bindings for twa_word.  Add a __repr__
for twa_run, and instantiate templates for twa_run's members.
* tests/python/word.ipynb: New file with examples.
* tests/Makefile.am, doc/org/tut.org: Add it.
2016-01-31 21:05:44 +01:00
Alexandre Duret-Lutz
5a9b0aa1c1 python: add bindings for ltsmin
* python/spot/ltsmin.i: New file.
* python/Makefile.am: Add it.
* python/spot/impl.i: Add bindings for kripke and fair_kripke.
* tests/python/ltsmin.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* tests/python/ipnbdoctest.py: Make it possible for notebook
to exit(77).
* debian/control: Make the Python package dependent
on libspotltsmin0.
* python/spot/__init__.py: Typo.
2016-01-26 19:20:53 +01:00
Alexandre Duret-Lutz
727d4cc678 * doc/org/concepts.org: Fix a few typos. 2016-01-23 22:11:18 +01:00
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