|
|
b04c4d7fd9
|
expansions: expose easy expansion in python
|
2023-10-12 15:04:40 +02:00 |
|
|
|
49f3c18ae3
|
expansions: store as vector of pairs
|
2023-10-12 15:04:06 +02:00 |
|
|
|
0199ebd592
|
expansions: US order in pipeline configurable
|
2023-10-12 04:13:47 +02:00 |
|
|
|
de2025298e
|
expansions: UniquePrefixSeenOpt
|
2023-09-21 08:51:58 +02:00 |
|
|
|
46aee256eb
|
expansions: fixes + BDD encode changes + printer
|
2023-07-04 07:21:20 +02:00 |
|
|
|
094fa85b02
|
expansions: simple determinization
|
2023-06-01 22:27:44 +02:00 |
|
|
|
189dde38d3
|
expansions: signature merge impl
|
2023-06-01 22:27:44 +02:00 |
|
|
|
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 |
|
