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

437 commits

Author SHA1 Message Date
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
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
d597c58106 org: improve wording 
* doc/org/tut04.org: This tests equivalence, not equality.
 2017-10-19 18:45:55 +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
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
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
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
Alexandre Duret-Lutz
97e903b13d libtool: surrender to Debian's castrated libtool 
The libtool version distributed by Debian is patched to *not* propagate
dependencies (i.e., if libA depends on libB, then linking against libA
will not automatically link against libB, it has to be explicit),
contrary to what the Libtool manual document.  So now we explicitly
link against both libA and libB in such case.

* configure.ac: Remove the workaround that does not work for
MinGW.
* doc/org/compile.org: Mention the issue.
* bin/Makefile.am, tests/Makefile.am, spot/ltsmin/Makefile.am,
doc/org/g++wrap.in: Make the dependencies explicit.
 2017-06-11 23:15:20 +02:00
Alexandre Duret-Lutz
1042a8dae1 libtool: surrender to Debian's castrated libtool 
The libtool version distributed by Debian is patched to *not* propagate
dependencies (i.e., if libA depends on libB, then linking against libA
will not automatically link against libB, it has to be explicit),
contrary to what the Libtool manual document.  So now we explicitly
link against both libA and libB in such case.

* configure.ac: Remove the workaround that does not work for
MinGW.
* doc/org/compile.org: Mention the issue.
* bin/Makefile.am, tests/Makefile.am, spot/ltsmin/Makefile.am,
spot/gen/Makefile.am, doc/org/g++wrap.in: Make the dependencies
explicit.
 2017-06-07 20:34:05 +02:00
Maximilien Colange
4f8a8f7305 Properly handle "simulated-states" property in twagraph::defrag_states. 
* spot/twa/twagraph.cc: Implement the change.
* spot/twaalgos/simulation.hh: Improve documentation.
* tests/python/simstate.py: Improve the test.
* doc/org/concepts.org: Typo.
 2017-06-05 15:48:36 +02:00
Alexandre Duret-Lutz
93969758ee sanity: catch undocumented named properties 
* tests/sanity/namedprop.test: New file.
* tests/Makefile.am: Add it.
* doc/org/concepts.org: Add documentation for degen-levels and
simulated-states.
 2017-05-31 20:32:53 +02:00
Alexandre Duret-Lutz
7dfa0ec15d Merge branch 'master' into next 2017-05-11 10:18:00 +02:00
Alexandre Duret-Lutz
52b5491b8e Release Spot 2.3.4 
* NEWS, configure.ac, doc/org/setup.org: Update version to 2.3.4.
 2017-05-11 10:10:48 +02:00
Alexandre Duret-Lutz
d3d2364ad0 org: list ltlfilt's transformation 
* doc/org/ltlfilt.org: A the list of transformation option.
Suggested by Yann Thierry-Mieg.
 2017-05-09 14:30:57 +02:00
Alexandre Duret-Lutz
e089509a0c org: list ltlfilt's transformation 
* doc/org/ltlfilt.org: A the list of transformation option.
Suggested by Yann Thierry-Mieg.
 2017-05-09 14:29:42 +02:00
Alexandre Duret-Lutz
ec51f976f8 gen: introduce a new automaton family 
* spot/gen/automata.cc, spot/gen/automata.hh: Define AUT_L_NBA.
* bin/genaut.cc (--l-nba): New option.
* bin/man/genaut.x, doc/org/genaut.org, NEWS: Document it.
* tests/python/gen.py, tests/core/genaut.test: Test it.
 2017-04-28 13:32:42 +02:00
Alexandre Duret-Lutz
540b971355 gen: rename genltl() to ltl_pattern() and introduce ltl_patterns() 
* spot/gen/formulas.hh, spot/gen/formulas.cc (genltl): Rename as...
(ltl_pattern): This.
(ltl_pattern_max): New function.
* bin/genltl.cc: Adjust names, and simplify using ltl_pattern_max().
* python/spot/gen.i (ltl_patterns): New function.
* tests/python/gen.py: Test it.
* tests/python/gen.ipynb: New file to document the spot.gen package.
* tests/Makefile.am, doc/org/tut.org: Add gen.ipynb.
 2017-04-26 15:06:02 +02:00
Alexandre Duret-Lutz
b8065a7947 * doc/org/concepts.org: Typos in property flag names. 2017-04-26 09:08:24 +02:00
Alexandre Duret-Lutz
cbfb79e343 typos: familly -> family 
* bench/ltlcounter/README, doc/org/upgrade2.org: Here.
 2017-04-26 09:07:34 +02:00
Alexandre Duret-Lutz
2dc115fe2c * doc/org/concepts.org: Typos in property flag names. 2017-04-26 09:04:27 +02:00
Alexandre Duret-Lutz
8939e0dd50 genltl: move all formula generation code to spot/gen/ 
Fixes #254.

* spot/gen/formulas.cc, spot/gen/formulas.hh: New files.
* spot/gen/Makefile.am: Add them.
* spot/Makefile.am: Fix build order.
* bin/genltl.cc: Move most code to the above files and adjust.
* bin/Makefile.am: Link genltl with libspotgen.
* doc/org/arch.tex: Adjust picture to show that genltl uses
libspotgen.
* python/spot/gen.i: Include formulas.hh.
* tests/python/gen.py: Make sure genltl() and ltl_pattern_name()
can be called.
 2017-04-25 18:14:15 +02:00
Alexandre Duret-Lutz
472cd77098 org: update the architecture diagram 
For #254.

* doc/org/arch.tex: Include libspotgen and its python bindings,
genaut, and also the buddy bindings.
* doc/org/concepts.org: Adjust the description.
 2017-04-23 19:56:01 +02:00
Alexandre Duret-Lutz
5e8f3ee629 typos: familly -> family 
* bench/ltlcounter/README, doc/org/upgrade2.org: Here.
 2017-04-23 11:28:28 +02:00
Alexandre Duret-Lutz
22aba2c4e2 genaut: add missing documentation 
* bin/man/genaut.x, doc/org/genaut.org: New files.
* bin/man/Makefile.am, doc/Makefile.am: Add them.
* doc/org/tools.org, bin/man/randaut.x, bin/man/randltl.x,
bin/man/genltl.x: Link to them.
 2017-04-22 14:19:35 +02:00
Alexandre Duret-Lutz
6ac9128699 org: typos 
* doc/org/concepts.org: Fix some typos.
 2017-04-20 22:02:22 +02:00
Alexandre Duret-Lutz
07c2dd3b64 introduce original-states 
* spot/twaalgos/degen.cc, spot/twaalgos/degen.hh,
spot/twaalgos/mask.hh: Store original states in "original-states"
properties.
* spot/twaalgos/dot.cc: Add support for option 'd'.
* bin/common_aoutput.cc: Document it.
* doc/org/concepts.org, NEWS: Document "original-states".
* tests/core/readsave.test: Add some tests.
 2017-04-20 20:07:30 +02:00
Alexandre Duret-Lutz
e7797b727d org: typos 
* doc/org/concepts.org: Fix some typos.
 2017-04-20 20:01:18 +02:00
Alexandre Duret-Lutz
334f04b0c4 Merge branch 'master' into next 2017-04-11 11:11:05 +02:00
Alexandre Duret-Lutz
e39e5ac586 Spot 2.3.3 
* NEWS, configure.ac, doc/org/setup.org: Bump version number.
 2017-04-11 10:43:04 +02:00