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

513 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
55a524cf3c org: detect C++ errors 
* doc/org/g++wrap.in: Save error messages.
* doc/Makefile.am: Display them at the end of the compilation.
 2017-03-10 17:54:01 +01:00
Alexandre Duret-Lutz
47e1c9692e typos: dictionnary -> dictionary 
* doc/org/upgrade2.org, tests/python/prodexpt.py,
tests/python/product.ipynb, NEWS: Fix typos.
* tests/sanity/style.test: Add a check for this.
 2017-03-08 16:10:47 +01:00
Alexandre Duret-Lutz
3699e6cd0c doc: simplify a C++ example 
* doc/org/tut10.org: Remove a couple of useless includes.
 2017-03-03 17:58:31 +01:00
Alexandre Duret-Lutz
bb23ea9978 doc: add an example about how to build monitor in shell/python/C++ 
Part of #239.

* doc/org/tut11.org: New file.
* doc/org/ltl2tgba.org, doc/org/hierarchy.org: Add some anchors we can
link to in tut11.org.
* doc/org/tut.org, doc/Makefile.am: Add tut11.org.
* NEWS: Mention the new page.
 2017-03-03 17:57:31 +01:00
Alexandre Duret-Lutz
2b9accdf58 postproc: fix monitor code 
Fixes #240.

* spot/twaalgos/postproc.cc: Do not call do_simul on the output of
minimize_monitor(), and do not skip complete() when PREF_==Any.
* tests/core/monitor.test: Add a test case.
* NEWS: Mention the bug.
* doc/org/ltl2tgba.org: Document complete monitors.
 2017-03-03 14:39:55 +01:00
Clément Gillard
da051e112d decompose_scc: Update 'decompose' notebook 
* tests/python/decompose.ipynb: Add about `decompose_scc`.
* doc/org/tut.org: Update description.
 2017-02-21 21:36:26 +01:00
Alexandre Duret-Lutz
803f9a5dd8 * doc/org/genltl.org: Simplify example. 2017-02-20 12:10:15 +01:00
Alexandre Duret-Lutz
b08da14e04 Release Spot 2.3.1 
* configure.ac, NEWS, doc/org/setup.org: Bump version numbers.
 2017-02-20 07:51:53 +01:00
Alexandre Duret-Lutz
7f7d078f2f * doc/org/tut23.org: Typos. 2017-02-12 10:40:34 +01:00
Alexandre Duret-Lutz
a0366921a5 ltlcross: Adjust color and wording of output 
Suggested by Akim Demaille.

* bin/ltlcross.cc: Change the colors, and add ':' at
the end of some error message.
* NEWS: Mention the color change.
* doc/org/ltlcross.org: Adjust examples.
 2017-02-07 22:33:33 +01:00
Alexandre Duret-Lutz
6c6660f48f org: plantuml.jar is in the build directory 
Fixes #213.

* doc/org/.dir-locals.el.in, doc/org/init.el.in: Adjust location of
plantuml.jar.
 2017-02-02 10:26:33 +01:00
Etienne Renault
4fdaf0e14e use wget or curl according to what is available 
* doc/Makefile.am, elisp/Makefile.am: here.
* HACKING: add missing requirements.
 2017-02-01 19:43:33 +01:00
Alexandre Duret-Lutz
cdfa607882 * doc/org/concepts.org: Typo. 2017-02-01 18:50:54 +01:00
Alexandre Duret-Lutz
0ada5900de ltldo.org: Fix first examples 
Fixes #210.

* doc/org/ltldo.org: Actually execute the code writing sample.ltl, and
remove the file once it is not used anymore.
 2017-01-27 20:35:40 +01:00
Alexandre Duret-Lutz
a4b575db1c ltldo: add portfolio options 
Fixes #206.

* bin/ltldo.cc: Implement --smallest and --greatest.
* tests/core/ltldo2.test: Test them.
* NEWS, doc/org/ltldo.org: Document them.
 2017-01-27 20:35:40 +01:00
Alexandre Duret-Lutz
267f819a9d * doc/org/tut51.org: Typo. 2017-01-27 13:11:20 +01:00
Alexandre Duret-Lutz
6d032597bf Release Spot 2.3 
* configure.ac, doc/org/setup.org, NEWS: Bump version to 2.3.
 2017-01-19 09:25:22 +01:00
Alexandre Duret-Lutz
21e2d9bb32 org: a few additional links 
* doc/org/index.org: Add links to the hierarchy and sat-minimization.
* doc/org/satmin.org: Show how to use glucose.
 2017-01-19 09:18:25 +01:00
Alexandre GBAGUIDI AISSE
4eebe94a1d TYPOS 
* NEWS: typo.
* bench/dtgbasat/config.bench: typo.
* bench/dtgbasat/gen.py: typo.
* bench/dtgbasat/stat-gen.sh: typo.
* doc/org/concepts.org: typo.
 2017-01-16 13:38:12 +01:00
Alexandre Duret-Lutz
01838a2456 ltlcross, ltldo: Add support for ltl3hoa. 
* bin/common_trans.cc: Add shorthand for ltl3hoa.
* NEWS, doc/org/ltlcross.org, doc/org/ltldo.org: Mention it.
 2017-01-13 22:12:43 +01:00
Alexandre Duret-Lutz
43520a3e87 ltlcross, ltldo: add a --relabel option 
* bin/common_trans.cc, bin/common_trans.hh: Add the --relabel option.
* bin/ltlcross.cc, bin/ltldo.cc: Implement it.
* doc/org/ltldo.org, NEWS: Document it.
* tests/core/ltl3ba.test: Test it.
 2017-01-13 22:12:43 +01: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
cf9ad8ebd1 org: minor tweaks 
* doc/org/ltlfilt.org: Update example.
* doc/org/ioltl.org: Explain %s briefly.
 2017-01-12 21:04:38 +01:00
Alexandre GBAGUIDI AISSE
823dc56e6b Update NEWS and documentations 
* NEWS: Update.
* doc/org/satmin.org: Update satmin page.
* bin/man/spot-x.x: Document SPOT_XCNF and edit SPOT_SATSOLVER.
* bin/spot-x.cc: Update satmin options.
* bin/autfilt.cc: Update satmin related documentations.
* bin/man/autfilt.x: Update autfilt options.
 2017-01-06 19:53:21 +01:00
Alexandre Duret-Lutz
4b01387817 support for semi-deterministic property 
* spot/twa/twa.hh (prop_semi_deterministic): New methods.
* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add support for the
semi-deterministic property.
* doc/org/concepts.org, doc/org/hoa.org: Document it.
* spot/twaalgos/isdet.cc,
spot/twaalgos/isdet.hh (is_semi_deterministic): New function.
* bin/autfilt.cc: Add --is-semi-deterministic.
* bin/common_aoutput.cc: Add --check=semi-deterministic.
* tests/core/semidet.test: New file.
* tests/Makefile.am: Add it.
* tests/core/parseaut.test, tests/core/readsave.test: Adjust.
 2016-12-29 16:37:43 +01:00
Alexandre Duret-Lutz
12f6c8cf10 twa_graph: add a merge_univ_dests() method 
and call it after parsing

* spot/twa/twagraph.cc, spot/twa/twagraph.hh
(twa_graph::merge_univ_dests): New method.
* spot/parseaut/parseaut.yy: Call it.
* spot/twaalgos/dot.cc: Improve output, now that
several edges can use the same universal destination.
* tests/core/alternating.test, tests/core/complete.test,
tests/core/parseaut.test, tests/python/_altscc.ipynb,
tests/python/alternating.py, tests/python/alternation.ipynb: Adjust
test case.
* doc/org/tut24.org: Adjust example.
 2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
3d0a971aa8 org: examples with alternating automata 
* doc/org/tut23.org, doc/org/tut24.org, doc/org/tut31.org: New files.
* doc/Makefile.am, doc/org/tut.org: Add them.
* doc/org/hoa.org, doc/org/concepts.org: Adjust for alternation support.
* NEWS: Add links.
 2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
87c9d6f039 ltlcross: add support for alternating automata 
* bin/ltlcross.cc: Add an alternation-removal pass, and
adjust CSV output.
* doc/org/ltlcross.org: Update.
* tests/core/ltl3dra.test, tests/core/ltl3ba.test: Add more tests.
* tests/Makefile.am: Add tests/core/ltl3ba.test.
* NEWS: Mention it.
 2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
fa06cfa303 alternation: implement remove_alternation() for weak alt automata 
This mixes the subset construction (for 1-state rejecting SCCs) and
the breakpoint construction (for larger rejecting SCCs).  The
algorithm should probably be rewritten in a cleaner and more efficient
way, but that should do for a first version.  It should be easy to
extend it to support Büchi acceptance (since the breakpoint
construction works for this) when we need it.

* spot/twaalgos/alternation.hh,
spot/twaalgos/alternation.cc (remove_alternation): New function.
* tests/python/alternation.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
 2016-12-29 12:57:16 +01:00
Alexandre Duret-Lutz
582d455c23 twa: add support for very-weak property 
* spot/twa/twa.hh: Implement the property.
* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add input
and output for it.
* spot/twaalgos/strength.cc,
spot/twaalgos/strength.hh (is_very_weak_automaton): New function.
* tests/core/alternating.test: Add a test for --check=strength
on an alternating automaton.
* tests/core/strength.test, tests/core/parseaut.test: Adjust expected
output.
* NEWS, doc/org/hoa.org, doc/org/concepts.org: Document it.
 2016-12-27 12:36:38 +01:00
Alexandre Duret-Lutz
dcd21aaabf org: call set_init_state() in tut22 
* doc/org/tut22.org: Here.
 2016-12-25 12:27:17 +01:00
Alexandre Duret-Lutz
34ac6f08cc org: ltlcross supports any acceptance condition 
* doc/org/ltlcross.org: Also fix the documentation of terminal and
weak SCCs.
 2016-12-24 21:08:01 +01:00
Alexandre Duret-Lutz
8e8c6a8cea org: support org >= 8.3 
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Load "shell" instead
of "sh" for recent org-mode version.
 2016-12-24 21:08:01 +01:00
Alexandre Duret-Lutz
574f47c366 Release Spot 2.2.2 
* NEWS, configure.ac, doc/org/setup.org: Update version.
 2016-12-16 06:50:59 +01:00
Alexandre Duret-Lutz
341eeb2ba1 strength: fix is_terminal() 
Fix #198.  Reported by Maximilien Colange.

* spot/twaalgos/strength.cc (is_terminal): Test that no accepting
transition lead to a rejecting SCC.
* tests/core/strength.test: Add test case.
* spot/twaalgos/strength.hh, spot/twa/twa.hh, doc/org/concepts.org:
Adjust documentation.
* NEWS: Mention the fix.
 2016-11-28 18:03:30 +01:00
Alexandre Duret-Lutz
9cf8535578 Release Spot 2.2.1 
* NEWS, configure.ac, doc/org/setup.org: Update.
 2016-11-21 09:00:51 +01:00
Alexandre Duret-Lutz
dd960dc71c Release Spot 2.2 
* configure.ac, doc/org/setup.org, NEWS: Set version number.
 2016-11-14 06:02:13 +01:00
Alexandre Duret-Lutz
4bd04fc65c * doc/org/oaut.org: Shorten a long line. 2016-11-13 21:58:37 +01:00
Alexandre Duret-Lutz
e91073a9f1 org: document %r and %R 
* doc/org/oaut.org (Timing): New section.
* NEWS: Link to it.
 2016-11-13 14:30:12 +01:00
Alexandre Duret-Lutz
c225747749 twa: introduce intersects() and friends 
* spot/twa/twa.hh, spot/twa/twa.cc (intersects, intersecting_run,
intersecting_word): New functions.
* NEWS: Mention them.
* doc/org/tut51.org, tests/python/bugdet.py: Use them.
 2016-11-13 11:23:12 +01:00
Alexandre Duret-Lutz
fe1f754d2e * doc/tl/tl.tex: Typo. 2016-11-05 12:11:00 +01:00
Alexandre Duret-Lutz
b0c60e799a Release Spot 2.1.2 
* NEWS, configure.ac, doc/org/setup.org: Bump version.
 2016-10-14 17:18:23 +02:00
Alexandre Duret-Lutz
3b5fa22a3b ltlcross: add option --strength and --ambiguous 
Suggested by František Blahoudek.

* bin/ltlcross.cc: Implement the two options.
* doc/org/ltlcross.org, NEWS: Document them.
* tests/core/complementation.test: Adjust test case.
* tests/core/ltlcross3.test, tests/core/unambig.test: More tests.
 2016-10-13 15:41:49 +02:00
Alexandre Duret-Lutz
ad502eb324 * doc/org/citing.org: Update references. 2016-10-13 12:04:54 +02:00
Alexandre Duret-Lutz
062643cc88 * doc/org/tut51.org: Typos. 2016-10-12 10:53:03 +02:00
Alexandre Duret-Lutz
a2575e0d3e org: really hide the plantuml logo 
Fix a5d6aa2.

* doc/org/.dir-locals.el.in, doc/org/init.el.in: Use
-Djava.awt.headless=true, not -Djava.awt.headless.
 2016-10-10 15:40:19 +02:00
Alexandre Duret-Lutz
fa80571d44 org: avoid displaying the plantuml log during builds 
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Make sure plantuml is
started via "java -Djava.awt.headless".
 2016-10-07 15:29:41 +02:00
Alexandre Duret-Lutz
e2b4d38ade more file to ignore 
* bin/.gitignore, doc/org/.gitignore: Here.
 2016-10-03 16:15:35 +02:00
Alexandre Duret-Lutz
959e757a22 org: cleanup some temporary 
* doc/org/concepts.org: Here.
 2016-10-03 15:27:09 +02:00
Alexandre Duret-Lutz
6528d75339 simplify: rewrite GF(a & GFb) as G(Fa & Fb) 
Fixes #185.

* spot/tl/simplify.cc: Implement the new rule.
* NEWS, doc/tl/tl.tex: Document it.
* tests/core/reduccmp.test: Test it.
 2016-09-22 17:37:55 +02:00