Commit graph

6482 commits

Author SHA1 Message Date
c1a0b5aa46 ltl2aa: fix bdd manipulation in UConcat 2023-06-01 22:27:44 +02:00
7eacf99f76 ltl2aa: fix R & M operators handling 2023-06-01 22:27:44 +02:00
11c469648f Add ltl2aa binary to tests/core 2023-06-01 22:27:44 +02:00
8f4ba3ec1a psl not working 2023-06-01 22:27:44 +02:00
be45ccd46d ltl2aa: factorize self-loop creation 2023-06-01 22:27:44 +02:00
06f21899b1 twaalgos: add LTL to AA translation 2023-06-01 22:27:44 +02:00
382acca320 twaalgos: filter accepting sinks in oe combiner 2023-06-01 22:27:44 +02:00
abe3da54fb graph: filter accepting sinks in univ_dest_mapper 2023-06-01 22:27:44 +02:00
f2063b7fc3 derive: use first 2023-06-01 22:27:44 +02:00
0d6c3cd6e9 derive: handle AndNLM 2023-06-01 22:27:44 +02:00
6882611d25 derive: extract AndNLM rewriting 2023-06-01 22:27:44 +02:00
2c89e09a47 derive: no nullptr handling 2023-06-01 22:27:44 +02:00
90be62be3d derive: use from_finite 2023-06-01 22:27:44 +02:00
d2667d48f6 twaalgos: add from_finite
* spot/twaalgos/remprop.cc, spot/twaalgos/remprop.hh: add a from_finite
  function to perform the opposite operation to to_finite
2023-06-01 22:27:44 +02:00
04112b26cc twaalgos: extract internal sere2dfa 2023-06-01 22:27:44 +02:00
1092e6c0c2 tl: implement SERE derivation 2023-06-01 22:27:44 +02:00
f0e4efa238 twagraph: merge_edges supports finite automata
* spot/twa/twagraph.cc: don't remove false-labeled edges if the
  automaton uses state-based acceptance and the edge is a self loop
2023-06-01 22:27:44 +02:00
d2bc100656 nix: provide package in release tarballs 2023-06-01 22:20:11 +02:00
4535b4a915 nix: setup Nix Flake file
* flake.nix, flake.lock: here
2023-06-01 22:20:11 +02:00
Florian Renkin
7868115a8b parity_type_to_parity: Add missing cases
* spot/twaalgos/toparity.cc: Correct some cases where the solution was
not detected.
* tests/python/toparity.py: Update tests.
2023-05-24 20:05:43 +02:00
Alexandre Duret-Lutz
abe7222973 bitvect: work around incorrect warning from gcc
* spot/misc/bitvect.hh: Don't free the old ptr if realloc() returns
NULL, as this confuse GCC who warns that we are freeing something that
has already been freed.   Instead, let the ~bitvect() destructor
handle this.
2023-05-15 09:43:46 +02:00
Alexandre Duret-Lutz
134da9209c genem: Add yet another version of the algorithm
* spot/twa/acc.hh, spot/twa/acc.cc (fin_unit_one_split_improved): New
function.
* python/spot/impl.i: Add bindings for fin_unit_one_split_improved.
* spot/twaalgos/genem.cc: Add the spot212 version.
* tests/python/genem.py: Test it.
2023-05-15 09:43:46 +02:00
Alexandre Duret-Lutz
747ec8b1c5 debian: add missing build dependencies
* debian/control: Add Build-Depends on graphviz, jupyter-nbconvert,
doxygen.
2023-05-15 09:43:43 +02:00
Alexandre Duret-Lutz
b487ff4190 Merge branch 'master' into next 2023-04-20 09:50:23 +02:00
Alexandre Duret-Lutz
d0ae0dfc38 * NEWS, configure.ac: Bump version to 2.11.5.dev. 2023-04-20 09:48:22 +02:00
Alexandre Duret-Lutz
b6c076ce19 release Spot 2.11.5
* NEWS, configure.ac, doc/org/setup.org: Update version.
2023-04-20 09:45:41 +02:00
Alexandre Duret-Lutz
184aa9931e org: replace version references with org-babel blocks
This way we have fewer lines to edit multiple when making releases.

* doc/org/index.org, doc/org/init.el.in, doc/org/install.org,
doc/org/setup.org, doc/org/tools.org: Use org-babel instead of macros
for release version and links.
2023-04-19 09:07:02 +02:00
Alexandre Duret-Lutz
eb80f5d5af powerset: fix segfault when the initial state is a sink
Reported by Raven Beutner.

* spot/twaalgos/minimize.cc: Improve comment.
* spot/twaalgos/powerset.cc: Fix handling of an initial state that
is also a sink.
* tests/core/wdba2.test: Add test case.
* NEWS: Mention the bug.
2023-04-19 09:06:58 +02:00
Alexandre Duret-Lutz
eb0f40b9d6 twa_run: let as_twa work on the result of intersecting_run
Reported by Philipp Schlehuber-Caissier.

* spot/twaalgos/emptiness.cc (as_twa): Simplify considerably.  Don't
try to replay the run, and don't merge identical states.
* spot/twaalgos/word.hh, spot/twaalgos/emptiness.hh: Improve
documentation.
* tests/python/intrun.py: Add a test case.
* NEWS: Mention the bug.
2023-04-19 09:06:55 +02:00
Philipp Schlehuber-Caissier
993695a2c4 Fix parity solver if edgevector is not contiguous
Validity of strategies was tested relying on
num_edges() which might be smaller than the edge_number

* spot/twaalgos/game.cc: Fix here
* tests/python/game.py: Test here
2023-04-19 09:06:25 +02:00
Alexandre Duret-Lutz
0c8093eded correctly fails if emacs needed and missing
Fixes #528.

* configure.ac: Define EMACS using tools/missing.
* NEWS: Mention the bug.
2023-04-19 09:06:01 +02:00
Alexandre Duret-Lutz
646b6e546f fix spurious test-case failure when Python is not installed
Fixes #530.

* tests/core/ltlsynt2.test: Skip when PYTHON is empty.
* NEWS: Mention the fix.
2023-04-19 09:05:42 +02:00
Alexandre Duret-Lutz
1a0b1f235d * doc/tl/tl.tex: Typo in firstmatch semantics. 2023-04-19 09:04:16 +02:00
Philipp Schlehuber
5714ecce32 Ignore ltargz.m4
* .gitignore: Ignore it
* m4/ltargz.m4: Remove it
2023-04-19 09:04:11 +02:00
Alexandre Duret-Lutz
dcd4759896 org: fix rendering of R examples for recent ESS/Org
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Newer ESS version
need to be taught to use default-directory instead of the project
directory.
* doc/org/ltlcross.org: Use "result file" to render the output.
2023-04-19 09:04:07 +02:00
Alexandre Duret-Lutz
a146457ea1 * doc/org/tut03.org: Typos. 2023-04-19 09:04:02 +02:00
Alexandre Duret-Lutz
d3013b072d org: do not require org-install
org-install has been obsolete for a long time, and has been removed
from Org 9.6.

* doc/org/init.el.in: Remove org-install.
2023-04-19 09:03:53 +02:00
Alexandre Duret-Lutz
c12b0622b4 org: replace version references with org-babel blocks
This way we have fewer lines to edit multiple when making releases.

* doc/org/index.org, doc/org/init.el.in, doc/org/install.org,
doc/org/setup.org, doc/org/tools.org: Use org-babel instead of macros
for release version and links.
2023-04-18 22:18:16 +02:00
Alexandre Duret-Lutz
0e54a85310 powerset: fix segfault when the initial state is a sink
Reported by Raven Beutner.

* spot/twaalgos/minimize.cc: Improve comment.
* spot/twaalgos/powerset.cc: Fix handling of an initial state that
is also a sink.
* tests/core/wdba2.test: Add test case.
* NEWS: Mention the bug.
2023-04-18 22:18:16 +02:00
Alexandre Duret-Lutz
ae10361bdd twa_run: let as_twa work on the result of intersecting_run
Reported by Philipp Schlehuber-Caissier.

* spot/twaalgos/emptiness.cc (as_twa): Simplify considerably.  Don't
try to replay the run, and don't merge identical states.
* spot/twaalgos/word.hh, spot/twaalgos/emptiness.hh: Improve
documentation.
* tests/python/intrun.py: Add a test case.
* NEWS: Mention the bug.
2023-04-18 22:18:16 +02:00
Philipp Schlehuber-Caissier
d152b3a316 Fix parity solver if edgevector is not contiguous
Validity of strategies was tested relying on
num_edges() which might be smaller than the edge_number

* spot/twaalgos/game.cc: Fix here
* tests/python/game.py: Test here
2023-03-31 15:17:57 +02:00
Alexandre Duret-Lutz
0c34152a33 correctly fails if emacs needed and missing
Fixes #528.

* configure.ac: Define EMACS using tools/missing.
* NEWS: Mention the bug.
2023-03-29 17:01:13 +02:00
Alexandre Duret-Lutz
039cd756d5 fix spurious test-case failure when Python is not installed
Fixes #530.

* tests/core/ltlsynt2.test: Skip when PYTHON is empty.
* NEWS: Mention the fix.
2023-03-29 16:20:51 +02:00
Alexandre Duret-Lutz
7a97a6080c * doc/tl/tl.tex: Typo in firstmatch semantics. 2023-03-29 16:16:06 +02:00
Philipp Schlehuber
7a91cf78ec Ignore ltargz.m4
* .gitignore: Ignore it
* m4/ltargz.m4: Remove it
2023-03-23 09:02:32 +01:00
Philipp Schlehuber
e7e23d5ffc Adding option to solve parity games globally
Parity games have been solved semi-locally so far.
We deduced a strategy for the reachable part of the arena
This lead to some inconsistencies when not all state were
rachable.
Now you can chose to solve parity games truely globally.

* spot/twaalgos/game.cc, spot/twaalgos/game.hh: Here
* tests/python/games.ipynb: Test
2023-03-23 09:02:09 +01:00
Alexandre Duret-Lutz
146942953a org: fix rendering of R examples for recent ESS/Org
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Newer ESS version
need to be taught to use default-directory instead of the project
directory.
* doc/org/ltlcross.org: Use "result file" to render the output.
2023-03-03 15:36:31 +01:00
Alexandre Duret-Lutz
f117159ec4 * doc/org/tut03.org: Typos. 2023-02-24 11:26:12 +01:00
Alexandre Duret-Lutz
66839b1a29 bdd_to_formula: add CNF variant
* spot/twa/formula2bdd.hh,
spot/twa/formula2bdd.cc (bdd_to_cnf_formula): New function.
* python/spot/__init__.py: Add a default dictionary for convenience.
* tests/python/bdditer.py: Add test cases.
* NEWS: Mention it.
2023-02-24 11:26:12 +01:00
Alexandre Duret-Lutz
8a5b86521c * NEWS: Remove duplicate entries. 2023-02-16 17:48:49 +01:00