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

610 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
454cc73670 doc: use SVG in the doxygen manual 
Suggested in #299.

* doc/Doxyfile.in: Here.
 2017-11-22 12:03:52 +01:00
Alexandre Duret-Lutz
b20687630b org: ltl3hoa -> ltl3tela 
Fixes #296.

* doc/org/ltlcross.org: Here.
 2017-11-07 17:15:13 +01:00
Alexandre Duret-Lutz
010b418583 Merge branch 'master' into next 2017-11-07 07:48:53 +01:00
Alexandre Duret-Lutz
ed5463cf6f Release Spot 2.4.2 
* NEWS, configure.ac, doc/org/setup.org: Update.
 2017-11-07 07:44:27 +01:00
Alexandre Duret-Lutz
75a1d6ac61 bin: add %g options to print acceptance name 
Fixes #289.

* spot/twaalgos/stats.cc, spot/twaalgos/stats.hh,
bin/common_aoutput.cc, bin/common_aoutput.hh: plug %g and %G into
acc_cond::name() when arguments are given as %[arg]g.  or %[arg]G.
* tests/core/acc2.test: Add test case.
* doc/org/randaut.org, NEWS: Document it.
 2017-11-04 07:43:41 +01:00
Alexandre Duret-Lutz
6459877a1a overhaul the stutter-invariance checks 
* spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh: Cleanup and
document the api.
* spot/twa/twa.hh, doc/mainpage.dox: Add a stutter-invariant section.
* tests/python/stutter-inv-states.ipynb: Rename as ...
* tests/python/stutter-inv.ipynb: ... this, and add more comments.
* tests/Makefile.am, doc/org/tut.org: Adjust renaming.
* bench/stutter/stutter_invariance_randomgraph.cc,
bench/stutter/stutter_invariance_formulas.cc,
bench/stutter/Makefile.am: Make it compile again.
* bin/autfilt.cc: Call inplace variants.
* NEWS: Mention the overhaul.
 2017-11-01 10:35:11 +01:00
Alexandre Duret-Lutz
7510743b47 org: update for gpg-signed Debian repository 
* doc/org/install.org: Mention the GPG key.
 2017-10-23 17:59:57 +02:00
Alexandre Duret-Lutz
2222661f98 org: update for gpg-signed Debian repository 
* doc/org/install.org: Mention the GPG key.
 2017-10-23 17:58:32 +02:00
Alexandre Duret-Lutz
d597c58106 org: improve wording 
* doc/org/tut04.org: This tests equivalence, not equality.
 2017-10-19 18:45:55 +02:00
Alexandre Duret-Lutz
bdfa2b3983 org: improve wording 
* doc/org/tut04.org: This tests equivalence, not equality.
 2017-10-19 18:44:37 +02:00
Alexandre Duret-Lutz
1a0dcf4f69 document the recent changes to implication rules 
* doc/tl/tl.tex: This adds the rules implemented in 0a2bca137
for #293.
 2017-10-18 14:53:29 +02:00
Alexandre Duret-Lutz
427c696954 org: fix the example for ltlcross --verbose 
* doc/org/ltlcross.org: Use SPOT_HOA_TOLERANT=1 to work around a bug
in ltl3ba -H1.
 2017-10-18 14:52:30 +02:00
Alexandre Duret-Lutz
308415f88a document the recent changes to implication rules 
* doc/tl/tl.tex: This adds the rules implemented in 0a2bca137
for #293.
 2017-10-17 17:58:59 +02:00
Alexandre Duret-Lutz
fcccd5f425 ltlcross: add support for --reference translators 
Suggested by Tobias Meggendorfer.  Fixes #295.

* bin/ltlcross.cc, bin/common_trans.hh, bin/common_trans.cc: Implement
this --reference option.
* NEWS, doc/org/ltlcross.org: Document it.
* tests/core/ltlcross3.test: Test it.
 2017-10-15 19:35:28 +02:00
Alexandre Duret-Lutz
77c0e76258 org: fix the example for ltlcross --verbose 
* doc/org/ltlcross.org: Use SPOT_HOA_TOLERANT=1 to work around a bug
in ltl3ba -H1.
 2017-10-15 18:48:00 +02:00
Alexandre Duret-Lutz
183ec1fb4e ltlcross, autcross, ltldo: support --fail-on-timeout 
Suggested by Tobias Meggendorfer.  Fixes #294.

* bin/autcross.cc, bin/ltlcross.cc, bin/ltldo.cc: Add the option.
* tests/core/autcross3.test, tests/core/ltlcross3.test,
tests/core/ltldo.test: Test it.
* tests/Makefile.am: Add autcross3.test.
* NEWS, doc/org/autcross.org, doc/org/ltlcross.org, doc/org/ltldo.org:
Mention the option.
* THANKS: Add Tobias.
 2017-10-15 12:22:15 +02:00
Alexandre Duret-Lutz
9b18729721 stutter: detect stutter-invariance at the state level 
* spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh: Implement
stutter-invariance detection at the state level.
* python/spot/impl.i: Instantiate std::vector<bool>
* tests/python/stutter-inv-states.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
 2017-10-11 15:01:29 +02:00
Alexandre Duret-Lutz
584430803d Merge branch 'master' into next 2017-10-05 16:00:07 +02:00
Alexandre Duret-Lutz
5c22db3c73 Release Spot 2.4.1 
* NEWS, configure.ac, doc/org/setup.org: Bump version.
 2017-10-05 15:52:57 +02:00
Alexandre Duret-Lutz
d2c4e596d1 org: fix the dot2tex example 
* doc/org/oaut.org: Fix the call to convert.
 2017-10-05 15:52:57 +02:00
Florian Perlié-Long
89c312cb57 * HACKING, doc/tl/tl.tex, spot/tl/formula.hh: Typos 2017-10-03 16:48:00 +02:00
Florian Perlié-Long
0f023bd0fe * HACKING, doc/tl/tl.tex, spot/tl/formula.hh: Typos 2017-10-03 15:54:48 +02:00
Thibaud Michaud
d6ae7af5f5 ltlsynt: translate winning strategy to AIGER 
* bin/ltlsynt.cc: Here.
* doc/org/ltlsynt.org: Document it.
* tests/core/ltlsynt.test: Test it.
 2017-09-25 12:23:47 +02:00
Thibaud Michaud
f414e9f5f2 parity game: add Zielonka's recursive algorithm 
* spot/misc/game.cc, spot/misc/game.hh: Implement it.
* bin/ltlsynt.cc: Use it.
* doc/org/ltlsynt.org: Document it.
 2017-09-25 12:23:47 +02:00
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
Laurent XU
27982fb80f parity: add spot::change_parity() 
This function changes the parity acceptance of an automaton.

* spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here
* python/spot/impl.i: Add spot/twaalgos/parity.hh
* spot/twaalgos/Makefile.am: Add spot/twaalgos/parity.{cc,hh}
* tests/core/parity.cc, tests/core/parity.test: Add
spot::change_parity() tests
* tests/python/parity.ipynb: Add documentation about
spot::change_parity()
* tests/Makefile.am: Add tests/core/parity.{cc,hh} and
tests/python/parity.ipynb
* doc/org/tut.org: Add the html page of tests/python/parity.ipynb
 2017-09-25 12:10:14 +02:00
Alexandre Duret-Lutz
1941bac22c org: improve dot2tex conversion to png 
* doc/org/oaut.org: Here.
 2017-09-06 11:18:34 +02:00
Alexandre Duret-Lutz
80621557b2 Release Spot 2.4 
* NEWS, configure.ac, doc/org/setup.org: Bump version.
 2017-09-05 21:08:48 +02:00
Alexandre Duret-Lutz
bc626788af dot: make 'x' compatible with 'b'/'r'/'R' 
* spot/twaalgos/dot.cc: Implement.
* doc/org/oaut.org: Illustrate.
* tests/core/dot2tex.test: Add some limited tests.
 2017-09-05 07:45:11 +02:00
Alexandre Duret-Lutz
290d7b56fb * doc/org/oaut.org: Missing word. 2017-09-04 19:57:40 +02:00
Alexandre Duret-Lutz
f726152ebd org: fix one example 
* doc/org/genaut.org: Output the result for the last example.
 2017-09-04 17:23:07 +02:00
Alexandre Duret-Lutz
e7df182a30 gen: rename KS_COBUCHI to KS_NCA for consistency 
* spot/gen/automata.cc, spot/gen/automata.hh, bin/genaut.cc: Rename
the enum, function, and command-line option.
* tests/core/genaut.test, tests/python/gen.ipynb, tests/python/gen.py:
Adjust test cases.
* doc/org/genaut.org: Adjust doc.
 2017-09-03 15:47:27 +02:00
Alexandre Duret-Lutz
e8527d5ae9 Improve simplification of expr[*0..1] 
Fixes #108.

* spot/tl/simplify.cc: Implement the reduction.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/reduccmp.test: Test it.
 2017-09-02 16:35:18 +02:00
Alexandre Duret-Lutz
646c5170ed simplify: some new simplification rules 
For #263, reported by Mikuláš Klokočka.

G(a & Xe1 & F(b & e2)) = G(a & e1 & Fb & e2)
F(a | Xu1 | G(b | u2)) = F(a | u1 | Gb | u2)

* spot/tl/simplify.cc: Implement the rules.
* doc/tl/tl.tex, NEWS: Document them.
* tests/core/reduccmp.test, tests/core/eventuniv.test: Add test cases.
* tests/core/det.test, tests/core/ltl2tgba2.test: Adjust to expect
smaller automata.
* THANKS: Add Mikuláš.
 2017-09-02 11:27:04 +02:00
Alexandre Duret-Lutz
fbb9e4374e dot: add x option for dot2tex 
* spot/twa/acc.cc, spot/twa/acc.hh: Add a LaTeX output for acceptance
conditions.
* spot/twaalgos/dot.cc: Implement the 'x' option and refactor the code
a bit to limit duplication.
* tests/core/dot2tex.test: New test case (requires dot2tex).
* tests/Makefile.am: Add dot2tex.test.
* tests/core/alternating.test, tests/core/readsave.test,
tests/python/automata-io.ipynb: Adjust expected output.
* NEWS, doc/org/oaut.org: Mention the new option.
 2017-08-31 19:50:08 +02:00
Alexandre Duret-Lutz
ed361bb0a9 org: add remark about "%h" 
* doc/org/csv.org: Mention that %h must be double-quoted in CSV output.
 2017-08-29 14:02:28 +02:00
Maximilien Colange
eb91ecf66f Typos 
* NEWS, doc/org/concepts.org, doc/org/hierarchy.org,
  spot/misc/optionmap.hh, spot/twa/acc.hh, spot/twaalgos/ltl2tgba_fm.hh,
  spot/twaalgos/sccinfo.hh, spot/twaalgos/translate.cc: fix typos
 2017-08-28 17:54:21 +02:00
Alexandre Duret-Lutz
f5dce597c6 switch to C++14 compilation 
* configure.ac: Compile in C++14 by default and rename
--enable-c++14 as c++17.
* doc/org/compile.org, doc/org/concepts.org, doc/org/index.org,
doc/org/install.org, doc/org/tut.org, doc/org/upgrade2.org, HACKING,
NEWS, README: Adjust all mentions of C++11.
* spot/twaalgos/stats.hh: Use std::make_unique.
 2017-08-22 18:21:49 +02:00
Alexandre Duret-Lutz
b7d54c8b90 mention autcross in arch.tex 
* doc/org/arch.tex: Add autcross.
* tests/sanity/bin.test: Make sure all binaries appear in arch.tex.
 2017-08-17 15:21:59 +02:00
Alexandre Duret-Lutz
1cc45b2413 dot: display acceptance names 
* spot/twaalgos/dot.cc: Display common acceptance names.
* NEWS: Mention the change.
* doc/org/oaut.org: Adjust text.
* tests/core/alternating.test, tests/core/readsave.test,
tests/python/_altscc.ipynb, tests/python/alternation.ipynb,
tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb,
tests/python/automata.ipynb, tests/python/decompose.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/product.ipynb, tests/python/randaut.ipynb: Adjust test
cases.
 2017-08-17 15:21:59 +02:00
Alexandre Duret-Lutz
a3f5834249 org: update hierarchy 
* doc/org/hierarchy.org: Update with small typos, and
notes about tra2tba.
 2017-08-17 15:21:59 +02:00
Alexandre Duret-Lutz
e041db6101 dot: extend the palette from 9 to 16 colors 
Let's close #212 even if this does not cover the 32 sets.

* spot/twaalgos/dot.cc: Change the palette.
* doc/org/autfilt.org, NEWS: Adjust documentation.
* tests/core/alternating.test, tests/core/readsave.test,
tests/core/tgbagraph.test, tests/python/_altscc.ipynb,
tests/python/alternation.ipynb, tests/python/atva16-fig2a.ipynb,
tests/python/automata-io.ipynb, tests/python/automata.ipynb,
tests/python/decompose.ipynb, tests/python/gen.ipynb,
tests/python/highlighting.ipynb, tests/python/ltsmin-dve.ipynb,
tests/python/piperead.ipynb, tests/python/product.ipynb,
tests/python/randaut.ipynb, tests/python/word.ipynb: Adjust
test cases.
 2017-08-03 14:32:11 +02:00
Alexandre Duret-Lutz
85c23202b7 g++wrap: make it work with --enable-glibcxx-debug 
* doc/org/g++wrap.in: Honor CPPFLAGS.
 2017-08-02 15:26:35 +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
8e685e00c9 deprecate copy() in favor of make_twa_graph() 
Fixes #258.

* spot/twaalgos/copy.cc: Delete, and move the code...
* spot/twa/twagraph.cc: ... in some anonymous namespace here.
* spot/twa/twagraph.hh: Adjust the make_twa_graph() overload.
* spot/twaalgos/copy.hh, NEWS: Mark copy() as deprecated and redirect
to make_twa_graph().
* doc/org/upgrade2.org, doc/org/tut51.org, python/spot/impl.i,
spot/twaalgos/dot.cc, spot/twaalgos/langmap.cc, tests/core/ikwiad.cc:
Adjust callers.
* spot/twaalgos/Makefile.am: Remove copy.cc.
 2017-07-25 11:35:37 +02:00
Alexandre Duret-Lutz
fba3c78206 org: improve recurrence example 
* doc/org/hierarchy.org: When generating DBA from recurrence formulas,
actually use -B instead of --tgba.
 2017-06-30 14:36:00 +02:00
Alexandre Duret-Lutz
efbce454e2 Merge branch 'master' into next 2017-06-22 07:06:29 +02:00
Alexandre Duret-Lutz
af000edbf9 Release Spot 2.3.5 
* NEWS, configure.ac, doc/org/setup.org: Update version.
 2017-06-22 06:58:01 +02:00
Alexandre Duret-Lutz
2dd134b0aa doc: Jessie -> Stretch 
* doc/org/install.org: Update.
 2017-06-20 16:29:26 +02:00
Alexandre Duret-Lutz
85e4cf510c doc: Jessie -> Stretch 
* doc/org/install.org: Update.
 2017-06-19 18:00:10 +02:00