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

898 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
6f37ff8ed0 ltlcross, autcross: add --quiet/-q option 
* bin/autcross.cc, bin/ltlcross.cc: Implement it.
* doc/org/autcross.org, doc/org/ltlcross.org, NEWS: Document it.
* doc/org/spot.css: Add colors for Makefile snippets.
* tests/core/autcross4.test, tests/core/ltlcross3.test,
tests/core/ltlcrossce.test: Add test cases.
 2019-07-17 17:34:01 +02:00
Alexandre Duret-Lutz
738515d7fd org: work around emacs/gnutls interaction bug 
* doc/org/init.el.in: Set gnutls-algorithm-priority when needed.
* NEWS: Mention the issue.
 2019-07-17 09:16:04 +02:00
Alexandre Duret-Lutz
b4cced9ba8 genltl: add --pps-arbiter-{strict,standard} 
* spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement
this.
* NEWS, bin/man/genltl.x, doc/spot.bib: Add documentation.
* tests/core/genltl.test, tests/core/ltlfilt.test: Add some tests.
 2019-07-12 16:48:10 +02:00
Alexandre Duret-Lutz
1f8a777e1f * doc/org/install.org: Debian stable is now Buster. 2019-07-10 14:22:54 +02:00
Alexandre Duret-Lutz
85b2d426d9 Release Spot 2.8 
* configure.ac, doc/org/setup.org, NEWS: Bump version to Spot 2.8.
 2019-07-10 06:13:19 +02:00
Alexandre Duret-Lutz
396dcabd7d * doc/spot.bib: Fix some urls. 2019-07-09 16:09:20 +02:00
Alexandre Duret-Lutz
5af4612eda genem: cite our ATVA'19 paper 
* doc/spot.bib (baier.19.atva): New reference.
* spot/twaalgos/genem.hh: Cite it.
 2019-07-09 16:09:20 +02:00
Alexandre Duret-Lutz
0d9cc29b46 tl: eight new simplification rules 
* NEWS, doc/tl/tl.tex: Document the rules.
* spot/tl/simplify.cc: Implement them.
* tests/core/reduccmp.test: Test them.
* tests/core/det.test, tests/core/ltl2tgba2.test,
tests/python/stutter-inv.ipynb, tests/core/385.test: Adjust.
 2019-07-09 16:09:15 +02:00
Alexandre Duret-Lutz
caad07cfa4 * doc/tl/tl.tex: Typo. 2019-06-30 19:06:50 +02:00
Alexandre Duret-Lutz
ad2f5524bb doc: add tut90.org about bdd_dict 
Fixes #372.

* doc/org/tut90.org: New file.
* doc/Makefile.am, doc/org/tut.org: Add it.
* NEWS: Mention it.
* python/spot/__init__.py: Allow make_twa_graph with
default bdd_dict.
 2019-06-27 10:50:19 +02:00
Alexandre Duret-Lutz
8c13d7209e ltlsynt: misc typos 
* doc/org/ltlsynt.org: Fix example.
* bin/ltlsynt.cc: Fix --help text.
 2019-06-18 19:12:42 +02:00
Alexandre Duret-Lutz
da5d23f0a2 simplify: GF(f)=GF(dnf(f)) FG(f)=FG(cnf(f)) 
These rules come from Delag's paper, and help some cases
in issue #385.

* spot/tl/simplify.cc: Implement the simplification.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/385.test: New file.
* tests/Makefile.am: Add it.
* tests/core/reduccmp.test: More tests.
* tests/core/ltl2tgba2.test: Adjust one improved case.
* tests/python/automata.ipynb, tests/python/twagraph-internals.ipynb:
Adjust expected output, as the cnf/dnf reorder some subformulas.
 2019-06-18 10:03:56 +02:00
Alexandre Duret-Lutz
df326e032b use a bibtex file to collect all references in Doxygen 
* doc/tl/tl.bib: Move ...
* doc/spot.bib: ... here, and augment it with all references that
appeared verbatim in Doxygen comments.
* doc/Makefile.am, doc/tl/Makefile.am
doc/tl/tl.tex: Adjust for the move.
* doc/Doxyfile.in: Point to spot.bib.
* spot/gen/automata.hh, spot/gen/formulas.hh, spot/misc/game.hh,
spot/misc/minato.hh spot/taalgos/emptinessta.hh,
spot/taalgos/minimize.hh, spot/taalgos/tgba2ta.hh, spot/tl/formula.hh,
spot/tl/remove_x.hh, spot/tl/simplify.hh, spot/tl/snf.hh,
spot/twaalgos/cobuchi.hh, spot/twaalgos/cycles.hh,
spot/twaalgos/dualize.hh, spot/twaalgos/gtec/gtec.hh,
spot/twaalgos/gv04.hh, spot/twaalgos/ltl2taa.hh,
spot/twaalgos/ltl2tgba_fm.hh, spot/twaalgos/magic.hh,
spot/twaalgos/minimize.hh, spot/twaalgos/parity.hh,
spot/twaalgos/powerset.hh, spot/twaalgos/randomgraph.hh,
spot/twaalgos/se05.hh, spot/twaalgos/simulation.hh,
spot/twaalgos/strength.hh, spot/twaalgos/stutter.hh,
spot/twaalgos/tau03.hh, spot/twaalgos/totgba.hh,
spot/twaalgos/toweak.hh: Use \cite instead of a verbatim bibtex entry.
 2019-06-14 21:02:27 +02:00
Alexandre Duret-Lutz
b4da0cf660 hierarchy: add a new way to check DBA-realizability via DPA 
* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Here.
* tests/core/hierarchy.test: Test it.
* bin/man/spot-x.x: Document SPOT_PR_CHECK.
* doc/org/hierarchy.org, NEWS: Update.
 2019-06-12 23:38:17 +02:00
Alexandre Duret-Lutz
cba012328e genaut: introduce --m-nba 
* bin/genaut.cc: Implement the --m-nba option.
* spot/gen/automata.hh, spot/gen/automata.cc: Add the generation code.
* NEWS, bin/man/genaut.x: Document it.
* doc/org/genaut.org: Update.
* tests/core/genaut.test, tests/core/parity2.test: Add some tests.
 2019-06-07 14:16:42 +02:00
Alexandre Duret-Lutz
435fec89b0 Merge branch 'master' into next 2019-06-05 08:12:35 +02:00
Alexandre Duret-Lutz
e9fb50114f Release Spot 2.7.5 
* NEWS, configure.ac, doc/org/setup.org: Bump version.
 2019-06-05 08:05:24 +02:00
Alexandre Duret-Lutz
58389bdb80 tl: extend F[n:m] and G[n:m] to the case of m=$ 
Suggested by Victor Khomenko.

* spot/tl/formula.cc, spot/tl/formula.hh, spot/parsetl/parsetl.yy:
Implement this.
* NEWS, doc/tl/tl.tex: Document it.
* tests/core/sugar.test, tests/python/ltlparse.py: Add some tests.
 2019-06-02 14:39:21 +02:00
Alexandre Duret-Lutz
a85045091b introduce output_aborter, and use it in ltlcross 
* spot/twaalgos/alternation.cc, spot/twaalgos/alternation.hh,
spot/twaalgos/complement.cc, spot/twaalgos/complement.hh,
spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh,
spot/twaalgos/minimize.cc, spot/twaalgos/minimize.hh,
spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/powerset.cc, spot/twaalgos/powerset.hh,
spot/twaalgos/product.cc, spot/twaalgos/product.hh: Use an
output_aborter argument to abort if the output is too large.
* bin/ltlcross.cc: Use complement() with an output_aborter
so that ltlcross will not attempt to build complement larger
than 500 states or 5000 edges.  Add --determinize-max-states
and --determinize-max-edges options.
* tests/core/ltlcross3.test, tests/core/ltlcrossce2.test,
tests/core/sccsimpl.test, tests/core/wdba2.test,
tests/python/stutter-inv.ipynb: Adjust test cases.
* NEWS: Document this.
* bin/spot-x.cc: Add documentation for postprocessor's
det-max-states and det-max-edges arguments.
* doc/org/ltlcross.org: Update description.
 2019-05-28 14:27:30 +02:00
Alexandre Duret-Lutz
90a88d0b5a tl: fix handling of f##[0:0]g, and of ##[0:n]g 
The first issue was reported by Victor Khomenko.

* spot/tl/formula.cc: Introduce a single-argument
version of sugar_delay().
* spot/parsetl/parsetl.yy: Use it.
* doc/tl/tl.tex, spot/tl/formula.hh: Adjust doc.
* tests/core/ltlfilt.test, tests/core/sugar.test: More tests.
 2019-05-20 20:59:33 +02:00
Alexandre Duret-Lutz
66a3b6f7cb tl: fix the definition of ##[i:j] 
Reported by Victor Khomenko.

* NEWS, doc/tl/tl.tex, spot/tl/formula.cc: Fix the definition.
* tests/core/ltl2tgba.test: Add some test cases.
 2019-05-19 09:16:42 +02:00
Alexandre Duret-Lutz
f476483f4a tl: add support for ##[+] and ##[*] 
Suggested by Victor Khomenko.

* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Implement them.
* NEWS, doc/tl/tl.tex: Document them.
* tests/core/sugar.test: Add a couple of tests.
 2019-05-18 12:06:35 +02:00
Alexandre Duret-Lutz
b726d78cbd tl: new simplification rules 
Related to issue #385.

* doc/tl/tl.tex, NEWS: Document the rules.
* spot/tl/simplify.cc: Implement the rules.
* tests/core/reduccmp.test, tests/core/ltl2tgba2.test: Add tests.
* tests/core/degenscc.test: Adjust.
 2019-05-18 11:39:09 +02:00
Alexandre Duret-Lutz
e325289a12 simplify: more rules for first_match 
* spot/tl/simplify.cc: Implement the rules.
* tests/core/reduccmp.test: Test them.
* doc/tl/tl.tex: Document them.
 2019-05-11 14:10:57 +02:00
Alexandre Duret-Lutz
c6605e951d tl: add some simplifications for first_match 
Following a discussion with Victor Khomenko.

* doc/tl/tl.tex: Document those rules.
* spot/tl/simplify.cc: Implement them.
* tests/core/reduccmp.test: Test them.
 2019-05-08 15:08:31 +02:00
Alexandre Duret-Lutz
ef8de879dc tut03: add missing operators 
* doc/org/tut03.org: Here.
 2019-05-06 15:16:09 +02:00
Alexandre Duret-Lutz
6fac026454 implement SVA's first_match operator 
* NEWS, doc/tl/tl.tex, doc/tl/tl.bib: Document it.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse it.
* spot/tl/formula.cc, spot/tl/formula.hh, spot/tl/dot.cc,
spot/tl/mutation.cc, spot/tl/print.cc, spot/tl/randomltl.cc,
spot/twaalgos/ltl2tgba_fm.cc: Adjust to support first_match.
* spot/tl/mark.cc, spot/tl/simplify.cc, spot/tl/snf.cc,
spot/tl/unabbrev.cc, spot/twa/formula2bdd.cc,
spot/twaalgos/ltl2taa.cc: Ignore it.
* tests/core/acc_word.test, tests/core/randpsl.test: Add more tests.
* tests/core/rand.test, tests/core/unambig.test,
tests/python/randltl.ipynb: Adjust.
* tests/python/formulas.ipynb: Show first_match.
 2019-05-06 15:11:30 +02:00
Alexandre Duret-Lutz
caf1eaa4ce tl.pdf: add missing precedence and grammar rules 
* doc/tl/tl.tex: Here.
 2019-05-05 14:26:10 +02:00
Alexandre Duret-Lutz
60d488b30c tl: add support for ##n and ##[i:j] from SVA 
* spot/tl/formula.cc, spot/tl/formula.hh (formula::sugar_delay): New
function to implement this operator as syntactic sugar.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse it.
* doc/tl/tl.tex: Document the syntactic sugar rules and precedence.
* tests/core/sugar.test: Add tests.
* NEWS: Mention this new feature.
 2019-05-04 22:03:13 +02:00
Alexandre Duret-Lutz
00f70257db Merge branch 'master' into next 2019-04-27 06:30:08 +02:00
Alexandre Duret-Lutz
90e5f6ed7d Release Spot 2.7.4 
* doc/org/setup.org, configure.ac, NEWS: Update version.
 2019-04-27 06:25:21 +02:00
Alexandre Duret-Lutz
d66eb84643 org: better sitemap 
* doc/org/init.el.in: List pages in a nested list according to
HTML_LINK_UP links.
 2019-04-26 16:21:12 +02:00
Alexandre Duret-Lutz
f3657a6763 * doc/org/ltlcross.org: Fix ltlcross.csv example. 2019-04-26 11:42:52 +02:00
Alexandre Duret-Lutz
54e25e38d1 * doc/org/ltlcross.org: Fix ltlcross.csv example. 2019-04-19 17:19:39 +02:00
Alexandre Duret-Lutz
cb72191642 Merge branch 'master' into next 2019-04-19 09:04:29 +02:00
Alexandre Duret-Lutz
eb826185f5 Release spot 2.7.3 
* NEWS, configure.ac, doc/org/setup.org: Set version.
 2019-04-19 08:56:41 +02:00
Alexandre Duret-Lutz
80456fcf8f org: reverse part of 7dfeda8e7 
* doc/org/satmin.org: Get the old description of the CSV example.  The
new description installed by 7dfeda8e7 only apply to the next major
release.
 2019-04-19 08:54:55 +02:00
Alexandre Duret-Lutz
339dac62d0 org: add a quick dirty comparison of 3 translators 
* doc/org/ltldo.org: Here.
* doc/org/spot.css: Add table-pre style.
 2019-04-17 17:31:03 +02:00
Alexandre Duret-Lutz
bbbe6ab8f9 org: better display for CSV tables 
* doc/org/.dir-locals.el.in,
doc/org/init.el.in (org-html-table-header-tags): Define.
* doc/org/spot.css: Style the tables.
 2019-04-17 17:31:03 +02:00
Alexandre Duret-Lutz
7dfeda8e77 org: simplify babel blocks using #+PROPERTY: header-args 
This feature is in Org 9, which is already required.

* doc/org/autcross.org, doc/org/autfilt.org, doc/org/compile.org,
doc/org/concepts.org, doc/org/csv.org, doc/org/dstar2tgba.org,
doc/org/genaut.org, doc/org/genltl.org, doc/org/hierarchy.org,
doc/org/hoa.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/ltlsynt.org,
doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org,
doc/org/satmin.org, doc/org/setup.org, doc/org/tools.org,
doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut04.org, doc/org/tut10.org, doc/org/tut11.org,
doc/org/tut12.org, doc/org/tut20.org, doc/org/tut21.org,
doc/org/tut22.org, doc/org/tut23.org, doc/org/tut24.org,
doc/org/tut30.org, doc/org/tut31.org, doc/org/tut50.org,
doc/org/upgrade2.org: Simplify SRC block setups for sh, python and
C++.  Also fix a few typos and examples along the way.
 2019-04-17 17:30:56 +02:00
Alexandre Duret-Lutz
d3cdabeb6e org: add a quick dirty comparison of 3 translators 
* doc/org/ltldo.org: Here.
* doc/org/spot.css: Add table-pre style.
 2019-04-17 17:01:26 +02:00
Alexandre Duret-Lutz
14f5d1ec65 org: better display for CSV tables 
* doc/org/.dir-locals.el.in,
doc/org/init.el.in (org-html-table-header-tags): Define.
* doc/org/spot.css: Style the tables.
 2019-04-17 11:41:33 +02:00
Alexandre Duret-Lutz
8a96828d85 org: simplify babel blocks using #+PROPERTY: header-args 
This feature is in Org 9, which is already required.

* doc/org/autcross.org, doc/org/autfilt.org, doc/org/compile.org,
doc/org/concepts.org, doc/org/csv.org, doc/org/dstar2tgba.org,
doc/org/genaut.org, doc/org/genltl.org, doc/org/hierarchy.org,
doc/org/hoa.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/ltlsynt.org,
doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org,
doc/org/satmin.org, doc/org/setup.org, doc/org/tools.org,
doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut04.org, doc/org/tut10.org, doc/org/tut11.org,
doc/org/tut12.org, doc/org/tut20.org, doc/org/tut21.org,
doc/org/tut22.org, doc/org/tut23.org, doc/org/tut24.org,
doc/org/tut30.org, doc/org/tut31.org, doc/org/tut50.org,
doc/org/upgrade2.org: Simplify SRC block setups for sh, python and
C++.  Also fix a few typos and examples along the way.
 2019-04-17 11:41:33 +02:00
Alexandre Duret-Lutz
1150b7012a * doc/org/tut22.org: Add missing call to prop_state_acc(True). 2019-04-03 10:48:04 +02:00
Alexandre Duret-Lutz
7e3232e3a3 org: explain how to build automata with state-based acceptance 
* doc/org/tut22.org: Here.  Suggested by Yannick Molinghen.
* THANKS: Add him.
 2019-04-03 10:48:04 +02:00
Alexandre Duret-Lutz
8c4f93d6c9 * doc/org/tut22.org: Add missing call to prop_state_acc(True). 2019-04-02 23:25:29 +02:00
Alexandre Duret-Lutz
f6467bea69 org: fix description of remove_fin 
* doc/org/dstar2tgba.org: The RA2BA is not for state-based acceptance
only.
 2019-04-02 23:21:36 +02:00
Alexandre Duret-Lutz
1d0db88073 org: suggest python-dev for installing Python headers 
* doc/org/install.org: Mention python-dev and libpython3-dev.
Suggested by Tereza Šťastná.
* THANKS: Add her.
 2019-04-02 23:18:27 +02:00
Alexandre Duret-Lutz
20563d8a00 org: explain how to build automata with state-based acceptance 
* doc/org/tut22.org: Here.  Suggested by Yannick Molinghen.
* THANKS: Add him.
 2019-04-02 23:14:26 +02:00
Alexandre Duret-Lutz
76517d9cd2 org: adjust text for simplified example for dstar2tgba 
* doc/org/dstar2tgba.org: Simplify example now that the automaton is
further reduced.
 2019-04-02 16:35:01 +02:00