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

4968 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
92369d68c6 solve build issue on Debian unstable i386 
* tests/python/_product_weak.ipynb: Split large loop in two cells.
 2018-10-15 21:42:44 +02:00
Alexandre Duret-Lutz
4b2562a33f Bump version to 2.6.2.dev 
* NEWS, configure.ac: Here.
 2018-09-28 10:12:36 +02:00
Alexandre Duret-Lutz
2828e229bd Release Spot 2.6.2 
* NEWS, configure.ac, doc/org/setup.org: Bump version number.
 2018-09-28 10:04:39 +02:00
Alexandre Duret-Lutz
5172b9c7d9 org: adjust link to online translator 
* doc/org/index.org: Here.
 2018-09-28 10:04:17 +02:00
Alexandre Duret-Lutz
3eb26704d6 more gcc-snapshot warnings 
* spot/misc/game.hh: Here.
 2018-09-27 10:22:49 +02:00
Alexandre Duret-Lutz
438d9e6d02 * NEWS: Describe more fixed bugs. 2018-09-26 17:58:01 +02:00
Alexandre Duret-Lutz
406e3b4f22 exclusive_ap::constrain does not improve determism 
Fixes #363.

* spot/tl/exclusive.cc: Fix the prop_copy() call.
* tests/core/exclusive-tgba.test: Test it.
* NEWS: Mention the issue.
 2018-09-26 17:54:09 +02:00
Alexandre Duret-Lutz
1b92a8e605 * .gitlab-ci.yml: Fix docker names. 2018-09-26 17:54:09 +02:00
Alexandre Duret-Lutz
87ef2822df print_dot: add xlabel to colored states if too many colors in use 
Based on a report from Andreas Tollkötter.

* spot/twaalgos/dot.cc (highlight_states_show_num_): New option,
turned on implicitly when more than 8 colors are used.
* tests/core/highlightstate.test: Test it.
* NEWS: Mention it.
* THANKS: Add Andreas.
 2018-09-26 17:53:56 +02:00
Alexandre Duret-Lutz
c5abf1b334 * debian/copyright: Fix syntax. 2018-09-26 17:53:15 +02:00
Alexandre Duret-Lutz
a69ea2a9cb remove more references to the old cgi-based translator 
* debian/source/lintian-overrides, python/.gitignore: Here
 2018-09-26 17:53:15 +02:00
Alexandre Duret-Lutz
7a2e5d8bce debian: add missing build dependency 
* debian/control (Build-Depends): Add dh-python.
 2018-09-26 17:53:15 +02:00
Alexandre Duret-Lutz
32a39c3f1a debiam: fix the regex from previous patches 
* debian/rules: Here.
 2018-09-26 17:53:15 +02:00
Alexandre Duret-Lutz
3adc9e18cc debian: apply the mathjax regex to org output as well 
* debian/rules: Here.
 2018-09-26 17:53:15 +02:00
Alexandre Duret-Lutz
9c356bfff6 * doc/org/setup.org: Typo. 2018-09-26 17:53:15 +02:00
Alexandre Duret-Lutz
89b55b7d8d debian: another mathjax regex 
* debian/rules: mathjax is also fetched from cdnjs.cloudflare.com.
 2018-09-26 17:53:15 +02:00
Alexandre Duret-Lutz
a455a277ca debian: adjust the mathjax regex 
* debian/rules: Here.
 2018-09-26 17:53:15 +02:00
Alexandre Duret-Lutz
e7f11b8884 * debian/control: Typo. 2018-09-26 17:53:15 +02:00
Alexandre Duret-Lutz
0076b8f240 * HACKING: R is now required to build from git. 2018-09-26 17:53:15 +02:00
Alexandre Duret-Lutz
816e5752fb fix --disable-doxygen and --disable-c++17 
Reported by Yuri Victorovich.

* configure.ac (enable_doxygen, enable_c++17): Use $enableval instead
of "yes".
* THANKS: Add Yuri.
 2018-09-26 17:53:15 +02:00
Alexandre Duret-Lutz
10d94d9ff9 gcc-snapshot warnings 
* spot/kripke/kripkegraph.hh, spot/priv/bddalloc.hh,
spot/priv/freelist.hh, spot/priv/satcommon.hh, spot/ta/taexplicit.cc
spot/twa/bdddict.cc, spot/twa/twagraph.hh,
spot/twaalgos/alternation.hh, spot/twaalgos/dtwasat.cc,
spot/twaalgos/ltl2taa.cc, spot/twaalgos/stutter.cc,
tests/core/ngraph.cc: Add default constructors, copy constructors, or
remove useless destructors.
 2018-09-26 17:53:15 +02:00
Alexandre Duret-Lutz
eb30d147d8 Adjust to Automake 1.16 
* python/Makefile.am: Adjust for Automake 1.16.
 2018-09-26 17:53:15 +02:00
Alexandre Duret-Lutz
1be313ef0b get rid of the Python-based CGI translator 
We now have a separate project for its replacement at
https://gitlab.lrde.epita.fr/spot/spot-web-app/

* python/ajax/: Remove directory.
* python/Makefile.am, configure.ac, README: Adjust.
* NEWS: Mention this.
 2018-09-26 17:53:11 +02:00
Alexandre Duret-Lutz
22ad9f5ed2 org: show some useful R operations on ltlcross output 
* doc/org/ltlcross.org: Here.
* doc/org/init.el.in, doc/org/.dir-locals.el.in: Enable R,
and install ess.
 2018-09-26 17:52:16 +02:00
Alexandre Duret-Lutz
90f529918b * NEWS, configure.ac: Bump version number. 2018-08-04 08:56:38 +02:00
Alexandre Duret-Lutz
d743674729 Release Spot 2.6.1 
* NEWS, configure.ac, doc/org/setup.org: Update version number.
 2018-08-04 08:54:45 +02:00
Alexandre Duret-Lutz
5c8cf1bc47 fix python bindings for spot::parsed_formula::f getter 
* python/spot/impl.i: Add a typemap.
* tests/python/ltlsimple.py: Add a test case for an issue.
* NEWS: Mention the bug.
 2018-08-03 08:27:35 +02:00
Alexandre Duret-Lutz
701a3b1c6a contains: fix the semantics 
spot::contains(a, b) should test a⊇b.  It was testing a⊆b instead.

* NEWS: Mention the bug.
* spot/twaalgos/contains.cc, spot/twaalgos/contains.hh: Fix the
code and documentation.
* tests/python/contains.ipynb: Adjust description and expected
results.
* python/spot/__init__.py: Also swap the argument of
language_containment_checker.contains()
* bin/autfilt.cc: Adjust usage.
 2018-08-02 13:54:17 +02:00
Alexandre Duret-Lutz
126d392355 tl: add some implication-based rewritings for "<->", "->", and "xor" 
This prevents an exception from being raised if NNF is not performed
on Boolean properties and implication-based checks are used.

* NEWS: Mention the issue.
* spot/tl/simplify.cc, doc/tl/tl.tex: Add some rules.
* tests/python/ltlsimple.py: Test them.
 2018-08-02 13:54:17 +02:00
Maximilien Colange
d8419db618 * spot/twa/acc.hh: fix constness 2018-08-02 13:54:17 +02:00
Alexandre Duret-Lutz
483b05c550 * spot/twaalgos/translate.cc: Typos in comments. 2018-08-02 13:54:17 +02:00
Alexandre Duret-Lutz
b2e51545f9 scc_info: fix split_on_sets 
* spot/twaalgos/sccinfo.cc (split_on_sets): Correctly register APs.
* tests/python/sccsplit.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
 2018-08-02 13:54:17 +02:00
Alexandre Duret-Lutz
2d8292c02e * .gitlab-ci.yml (debpkg-stable): Typo. 2018-08-02 13:54:17 +02:00
Alexandre Duret-Lutz
79a62ae1c9 ltlfilt: introduce --suspendable 
* bin/ltlfilt.cc: Add the option.
* tests/core/ltlfilt.test: Use it.
* NEWS: Mention it.
 2018-08-02 13:54:17 +02:00
Alexandre Duret-Lutz
d5ffdb60b5 * spot/twa/twa.cc: Typo. 2018-08-02 13:53:12 +02:00
Etienne Renault
85eff247b2 HACKING: directory has moved 
* HACKING: Here.
 2018-08-02 13:53:12 +02:00
Etienne Renault
e0b10d847a remove duplicated includes 
* spot/graph/graph.hh,
spot/taalgos/tgba2ta.cc,
spot/tl/formula.hh,
spot/twaalgos/dot.cc,
spot/twaalgos/ltl2tgba_fm.cc,
spot/twaalgos/ndfs_result.hxx,
spot/twaalgos/powerset.cc,
spot/twaalgos/stutter.cc: Here.
 2018-08-02 13:53:12 +02:00
Etienne Renault
acf254243b remove useless forward declaration 
* spot/ta/taexplicit.hh,
spot/twaalgos/compsusp.hh,
spot/twaalgos/isunamb.hh,
spot/twaalgos/word.hh: Here.
 2018-08-02 13:53:12 +02:00
Alexandre Duret-Lutz
b33a88d8bb escape_rfc4180: document relation with std::quote 
* spot/misc/escape.hh: Here.
 2018-08-02 13:53:12 +02:00
Alexandre Duret-Lutz
1edb47ad5b fix two issues related to jupyter notebook execution 
* tests/python/ipnbdoctest.py: Invert diffs inputs.
* tests/run.in: Run notebooks with
PYTHONIOENCODING=utf-8:surrogateescape to avoid exceptions when trying
to display utf-8 characters on ascii terminals.
 2018-08-02 13:53:12 +02:00
Alexandre Duret-Lutz
b8aae428e5 org: add missing documentation for prop_complete 
* doc/org/concepts.org: Here.
 2018-08-02 13:53:12 +02:00
Antoine Martin
8d475780d2 * HACKING: typos 2018-08-02 13:53:12 +02:00
Alexandre Duret-Lutz
8edd064859 * doc/tl/tl.tex: Convert to utf-8. 2018-08-02 13:53:12 +02:00
Alexandre Duret-Lutz
2616ea7c80 org: do not define the viewport twice 
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Do not set the
viewport, org already does it.
 2018-07-05 13:54:21 +02:00
Alexandre Duret-Lutz
db19141f7a Bump version to 2.6.0.dev 
* NEWS, configure.ac: Here.
 2018-07-04 17:11:24 +02:00
Alexandre Duret-Lutz
215b0dcbf0 Release Spot 2.6 
* NEWS, configure.ac, doc/org/setup.org: Bump version to 2.6.
 2018-07-04 17:07:09 +02:00
Alexandre Duret-Lutz
70b212d8b8 org: add instructions for install RPM packages 
* doc/org/install.org: Here.
* NEWS: Mention that we have RPM packages.
 2018-07-04 16:00:00 +02:00
Alexandre Duret-Lutz
0a9c1d3347 * spot.spec.in: Use --disable-devel --enable-optimizations. 2018-07-04 16:00:00 +02:00
Alexandre Duret-Lutz
0d2b8aacd1 Fix GITPATCH computation 
Since the introduction of the syntcomp2018-submission tag (on a
separate branch), that computation of GITPATCH was based on this
tag because it was the last one (even if it is not on next).
We did not see it on the Debian packages, because they clone
only one branch of the repository, but the RPM packages had a
different GITPATCH.

* configure.ac (GITPATCH): Compute the number of commits since the
last "spot-*" tag.
 2018-07-04 16:00:00 +02:00
Alexandre Duret-Lutz
0411099506 trival: prefer a global operator== relying on implicit conversion 
Hopefully fixes #359.

* spot/misc/trival.hh: Declare a global operator==(trival,trival) that
replace the specialized operator==(bool,trival), and the in class
trival::operator(trival), thanks to the implicit construction from
bool to trival.  Make the repr_t/value_t constructor explicit, are
those are mostly internal to the library and may cause conflicts.
* spot/twa/twa.hh: Adjust to construct trival explicitly.
* python/spot/impl.i: Since Swig/Python does not support global
comparison operators, implement a member version, supporting
only __eq__(trival,bool) as before.
* tests/python/setacc.py: Adjust erroneous code.
* tests/python/trival.py: Add test cases.
 2018-07-04 16:00:00 +02:00