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

5116 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
65e8d16f57 tests: add missing copyright blobs 
* tests/python/remfin.py, tests/python/tra2tba.py: Here.
 2019-06-04 13:58:19 +02:00
Alexandre Duret-Lutz
4a5259d1fa work around another swig4 change 
* python/spot/impl.i: Make sure spot::acc_cond::mark_t::operator<<
exceptions are not ignored.
 2019-06-04 13:58:19 +02:00
Alexandre Duret-Lutz
bae8be9333 work around swig4 regression 
* python/Makefile.am: Here.
 2019-06-04 11:32:50 +02:00
Alexandre Duret-Lutz
05b3007885 work around new import statements generated by swig-4.0 
Those statements are not compatible with the fact that
libtool-generated modules are in .libs/ until they get installed.

* python/spot/__init__.py: Add sys.path to __path__ if SPOT_BUILD is
  set.
* tests/run.in: Set SPOT_BUILD.
 2019-06-04 11:32:46 +02:00
Alexandre Duret-Lutz
428607df1a python: remove the -nofastproxy option 
This was introduced by b893b5597 to work around some IPython 2 issue
(https://github.com/ipython/ipython/issues/7003).

* python/Makefile.am (SWIGFLAGS): Remove obsolete option.
* python/spot/__init__.py: Adjust.
 2019-06-04 11:32:37 +02:00
Alexandre Duret-Lutz
bdd5a0b981 test: add missing copyright boilerplate 
* tests/python/genem.py: Here.
 2019-06-04 11:32:24 +02:00
Alexandre Duret-Lutz
2950833929 translate: relabel_bool was ignored when option_map was not supplied 
* spot/twaalgos/translate.cc: Set relabel_bool_ to 4 by default, not
-1.
* NEWS: Mention the bug.
 2019-06-04 11:31:50 +02:00
Alexandre Duret-Lutz
11e8f9592f dot: replace large labels by "(label too long)" 
Based on a report by Victor Khomenko.

* spot/twaalgos/dot.cc: Here.
* tests/core/readsave.test: Add test case.
* NEWS: Mention it.
 2019-06-04 11:27:47 +02:00
Alexandre Duret-Lutz
09d9e0c52a Bump version to 2.7.4.dev 
* NEWS, configure.ac: Here.
 2019-04-27 06:28:17 +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
ba89cb5db5 * THANKS: Add Victor Khomenko. 2019-04-26 23:01:43 +02:00
Alexandre Duret-Lutz
4d16c0760f formula: b* is siSERE 
Since b[+] and [*0] are siSERE, b* is siSERE as well.
Suggested by Victor Khomenko.

* spot/tl/formula.cc: Implement that for Star and also
in the concatenation rule.
* tests/core/kind.test, tests/core/ltlfilt.test: Adjust.
 2019-04-26 22:40:21 +02:00
Alexandre Duret-Lutz
38f0cfd4c0 formula: fix syntactic-SI detection for ; operator 
Reported by Victor Khomenko.

* spot/tl/formula.cc: Rewrite the siPSL detection for ";".
* tests/core/ltlfilt.test: Add more tests.
* tests/core/kind.test: Adjust.
* NEWS: Mention the bug.
 2019-04-26 16:20:48 +02:00
Alexandre Duret-Lutz
b928d8c82a fix "requires separate Inf and Fin sets" error from ltl2tgba -G 
Report from David Müller.

* spot/twaalgos/simulation.cc: Add wrapper to deal with automata
sharing Fin/Inf sets.
* tests/core/ltl2tgba2.test: New test cases.
* NEWS: Mention the change.
 2019-04-26 11:48:31 +02:00
Alexandre Duret-Lutz
26e2f9cec8 sepsets: fix infinite loop 
* tests/core/sepsets.test: New test case.
* spot/twaalgos/sepsets.cc: Fix the code.
* NEWS: Mention the problem.
 2019-04-26 11:48:31 +02:00
Alexandre Duret-Lutz
936481dcbd * bin/spot-x.cc (ba-simul): Update documentation. 2019-04-26 11:43:02 +02:00
Alexandre Duret-Lutz
e7ac892d32 man: minor fixes 
* bin/man/spot-x.x, bin/man/dstar2tgba.x, bin/spot-x.cc: Cosmetics
changes.
* bin/man/README: New file.
 2019-04-26 11:42:58 +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
9aa5e67384 * NEWS, configure.ac: Bump version to 2.7.3.dev. 2019-04-19 09:00:40 +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
fd073d1df9 tests: fix some examples 
Reported by František Blahoudek.

* tests/python/parity.ipynb: Fix examples and improve some text.
 2019-04-18 14:51:05 +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
c9c98e11c4 * elisp/README: Remove obsolete comment. 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
8c99cffac7 tests: try to work around some frequent time outs in our checks 
* tests/python/ipnbdoctest.py: Augment time limits.
 2019-04-17 17:26:43 +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
b33f32be5a * NEWS: Fix non-existent address 2019-04-02 23:21:36 +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
e70f9d5723 remove_alternation: fix serious typo 
Fixes #382.

* spot/twaalgos/alternation.cc: Here.
* tests/python/alternation.ipynb: Add test case.
* NEWS: Mention it.
 2019-04-02 23:21:36 +02:00
Alexandre Duret-Lutz
e340e61f24 bin: fix handling of \r\n with %> 
Fix issue #380.

* bin/common_finput.cc: Erase a trailing \r.
* tests/core/ltl2tgba2.test: Test it.
* NEWS: Mention the fix.
 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
489444aa4d * NEWS, configure.ac: Bump version to 2.7.2.dev. 2019-03-17 17:19:45 +01:00
Alexandre Duret-Lutz
cf8d711386 Release Spot 2.7.2 
* NEWS, configure.ac, doc/org/setup.org: Bump version.
 2019-03-17 17:19:39 +01:00
Alexandre Duret-Lutz
c63521d67a work around potential null dereference warning 
* spot/twaalgos/ltl2taa.cc: Here.
* NEWS: Mention the issue.
 2019-03-17 17:19:10 +01:00
Alexandre Duret-Lutz
bb51499b11 org: typos 
* doc/org/tut.org, doc/org/tut12.org: Here.
 2019-03-17 15:19:35 +01:00
Alexandre Duret-Lutz
936990a427 org: more hyperlinks 
* doc/org/ltlfilt.org, doc/org/tut12.org: Add links.
 2019-03-16 13:28:50 +01:00
Alexandre Duret-Lutz
262668bbad org: add an example for dealing with LTLf formulas 
Related to issue #377.

* doc/org/tut12.org: New file.
* doc/org/tut.org, doc/Makefile.am, NEWS: Add the new file.
 2019-03-16 13:28:50 +01:00
Alexandre Duret-Lutz
c25a75ea8e * tests/python/twagraph-internals.ipynb: Fix a typo. 2019-03-16 13:28:50 +01:00
Alexandre Duret-Lutz
e3b5552fb8 * NEWS: Add missing entry for previous patch. 2019-03-16 13:28:50 +01:00
Alexandre Duret-Lutz
8512a2d526 org: improve Python formating 
* doc/org/spot.css: Use bold for "def", "from", "import".
* doc/org/init.el.in: Prevent tabs from being inserted when the code
is indented before export.
 2019-03-16 13:28:50 +01:00
Alexandre Duret-Lutz
25133cac28 org: add explicit Kripke structure example 
Fixes #376.

* doc/org/tut52.org: New file.
* doc/org/tut.org, doc/org/tut51.org: Link to it.
* doc/Makefile.am: Add it.
 2019-03-16 13:28:50 +01:00
Alexandre Duret-Lutz
8f7a0c2f7a python: improve kripke_graph bindings 
Related to issue #376.

* spot/kripke/kripkegraph.hh: Avoid indirect type definitions for the
benefit of Swig.
* python/spot/impl.i: Add bindings for iterators over kripke_graph
states and edges.
* tests/python/kripke.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Update.
 2019-03-16 13:28:45 +01:00
Clément Gillard
4ecd066c0e Several typos 
* HACKING: Missing "to", extraneous 's'.
* spot/misc/timer.hh: Extraneous space.
* spot/twa/acc.hh: Extraneous 's', typos.
* spot/twaalgos/genem.hh: Typo.
* spot/twaalgos/sccinfo.cc: Fix indentation.
* spot/twaalgos/sccinfo.hh: Missing 's'.
* tests/python/acc_cond.ipynb: Extraneous 'e', missing comma.
* tests/python/decompose.ipynb: Extraneous 't'.
* tests/python/ltsmin-dve.ipynb: Extraneous verb.
 2019-02-14 16:25:13 +01:00
Alexandre Duret-Lutz
0c32f6b7ae Bump version to 2.7.1.dev 
* configure.ac, NEWS: Here.
 2019-02-14 09:52:38 +01:00
Alexandre Duret-Lutz
8befa3280c Release spot 2.7.1 
* configure.ac, NEWS, doc/org/setup.org: Set version.
 2019-02-14 09:50:25 +01:00
Alexandre Duret-Lutz
f26dd904ff python: better support for explicit Kripke 
Part of issue #376, reported by Hashim Ali.

* python/spot/impl.i: Add bindings for kripke_graph.
* python/spot/__init__.py (automaton): Add a want_kripke option.
* spot/kripke/kripkegraph.hh: Honnor the "state-names" property
when displaying states.
* spot/twaalgos/hoa.cc: Preserve names of Kripke states.
* tests/python/ltsmin-dve.ipynb: Illustrate all the above.
* NEWS: Mention those changes.
* THANKS: Add Hashim.
 2019-02-13 17:47:53 +01:00
Alexandre Duret-Lutz
a86925e20e work around gcc 8.2.1+ bug #89303 
Do not call std::make_shared on classes inheriting from
std::enable_shared_from_this when compiling with g++ 8.2.

* NEWS: Mention the bug.
* spot/misc/common.hh (SPOT_make_shared_enabled__): New macro.
* spot/twa/twagraph.cc, spot/twa/twagraph.hh, spot/twa/twaproduct.hh,
spot/twa/taatgba.hh, spot/twaalgos/couvreurnew.cc,
spot/twaalgos/magic.cc, spot/twaalgos/se05.cc, spot/twaalgos/tau03.cc,
spot/twaalgos/tau03opt.cc, spot/twaalgos/gv04.cc,
spot/ltsmin/ltsmin.cc, spot/twaalgos/gtec/gtec.cc: Use it.
 2019-02-13 16:11:21 +01:00