81a635c831
expansions: optimize sigma star encoding
2023-06-01 22:27:44 +02:00
aeba9ff674
expansions: remove multiple old implementations
2023-06-01 22:27:44 +02:00
564e3af5dd
expansions: fix first_match case
2023-06-01 22:27:44 +02:00
2c4f85f687
twaalgos: ltl2tgba_fm: allow disabling SCC trim
2023-06-01 22:27:44 +02:00
d410435adc
expansions: allow toggling merge_edges off
2023-06-01 22:27:44 +02:00
0168efea60
expansions: latest implementation
2023-06-01 22:27:44 +02:00
22f76b7e1c
expansions: multimap version
2023-06-01 22:27:44 +02:00
66761b3980
expansions: determinize only once per state
2023-06-01 22:27:44 +02:00
b62945b5de
expansions: fix bdd method
2023-06-01 22:27:44 +02:00
f4b2637c04
expansions: add BDD method
2023-06-01 22:27:44 +02:00
806b7319b9
expansions: multiple implementations
2023-06-01 22:27:44 +02:00
2e40892fd6
expansions: split-off OrRat case
2023-06-01 22:27:44 +02:00
bd8b5b4b51
expansions: first_match deterministic
2023-06-01 22:27:44 +02:00
16fd28d29b
expansions: draft
2023-06-01 22:27:44 +02:00
4ce9c483c1
derive: add options to control distribution
2023-06-01 22:27:44 +02:00
b2b80831ca
derive: option for some optimisations
2023-06-01 22:27:44 +02:00
2ef0ea00f4
sere_to_tgba: produce state-names
2023-06-01 22:27:44 +02:00
8abad2b4f7
ltl2aa: handle edge case in UConcat
...
If SERE recognizes false, then combined with UConcat the property is
always true.
2023-06-01 22:27:44 +02:00
2d11d907ef
alternation: fix bug introduced in oe_combiner
...
turns out sometimes we want to account for bddfalse
2023-06-01 22:27:44 +02:00
66f0ab85d0
ltl2aa: implement EConcat
2023-06-01 22:27:44 +02:00
3744d0cbed
ltl2aa: comment
2023-06-01 22:27:44 +02:00
36b09fa1f6
ltl2aa: finalize UConcat
2023-06-01 22:27:44 +02:00
88914c58c7
ltl2aa: finish SERE aut merging with rhs outedges
2023-06-01 22:27:44 +02:00
87c99cb38f
ltl2aa: fix two bugs in SERE aut merge
2023-06-01 22:27:44 +02:00
2af19a485b
ltl2aa: place new state in var_to_state map
2023-06-01 22:27:44 +02:00
44568b5622
ltl2aa: implem closure
2023-06-01 22:27:44 +02:00
85b8717c05
ltl2aa: share dict between sere and final aut
2023-06-01 22:27:44 +02:00
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
