|
|
b93fb41af2
|
expansions: fix sort behavior
The previous implementation was wrong and led to segfaults when sorting
large expansions
|
2025-03-12 22:00:11 +01:00 |
|
|
|
980dc72678
|
expansions: make signature canonical
Linear forms are now sorted and duplicates are removed
|
2025-03-08 18:24:27 +01:00 |
|
|
|
4f169ad632
|
expansions: fusion can produce false
let's discard the result if it's false
|
2025-03-08 18:24:27 +01:00 |
|
|
|
1deb2ccb02
|
ltl2tgba_fm: setup switch between bdd and exp
|
2025-03-08 18:24:27 +01:00 |
|
|
|
a2669a160f
|
translate_aa: setup translation choice
|
2025-03-08 18:24:27 +01:00 |
|
|
|
4dce729d22
|
ltl2tgba_fm: switch for expansions
|
2025-03-08 18:24:27 +01:00 |
|
|
|
0e2ebef709
|
expansions: split
|
2025-03-08 18:24:27 +01:00 |
|
|
|
e29aa30c2d
|
expansions: up variants
|
2025-03-08 18:24:27 +01:00 |
|
|
|
d326c17456
|
expansions: expose easy expansion in python
|
2025-03-08 18:24:27 +01:00 |
|
|
|
9faef36529
|
expansions: store as vector of pairs
|
2025-03-08 18:24:27 +01:00 |
|
|
|
0a89377400
|
expansions: US order in pipeline configurable
|
2025-03-08 18:24:27 +01:00 |
|
|
|
975ea0c52a
|
expansions: UniquePrefixSeenOpt
|
2025-03-08 18:24:27 +01:00 |
|
|
|
84d3977c0d
|
expansions: fixes + BDD encode changes + printer
|
2025-03-08 18:05:27 +01:00 |
|
|
|
f5574547ce
|
expansions: simple determinization
|
2025-03-08 18:05:27 +01:00 |
|
|
|
24b71fd8c7
|
expansions: signature merge impl
|
2025-03-08 18:05:27 +01:00 |
|
|
|
2aa7685611
|
expansions: optimize sigma star encoding
|
2025-03-08 18:05:27 +01:00 |
|
|
|
e09f908b89
|
expansions: remove multiple old implementations
|
2025-03-08 18:05:27 +01:00 |
|
|
|
f37be92903
|
expansions: fix first_match case
|
2025-03-08 18:05:27 +01:00 |
|
|
|
bc61b7c30b
|
twaalgos: ltl2tgba_fm: allow disabling SCC trim
|
2025-03-08 18:05:27 +01:00 |
|
|
|
450f38f74d
|
expansions: allow toggling merge_edges off
|
2025-03-08 18:05:27 +01:00 |
|
|
|
7c529eddfd
|
expansions: latest implementation
|
2025-03-08 18:05:27 +01:00 |
|
|
|
31376f804f
|
expansions: multimap version
|
2025-03-08 18:05:27 +01:00 |
|
|
|
2ae5dbb727
|
expansions: determinize only once per state
|
2025-03-08 18:05:27 +01:00 |
|
|
|
728faeba22
|
expansions: fix bdd method
|
2025-03-08 18:05:27 +01:00 |
|
|
|
38fc0c94f3
|
expansions: add BDD method
|
2025-03-08 18:05:27 +01:00 |
|
|
|
7ca9910862
|
expansions: multiple implementations
|
2025-03-08 18:05:27 +01:00 |
|
|
|
7731c7ee54
|
expansions: split-off OrRat case
|
2025-03-08 18:05:27 +01:00 |
|
|
|
0b3f4e5b91
|
expansions: first_match deterministic
|
2025-03-08 18:05:27 +01:00 |
|
|
|
ad3896e7a3
|
expansions: draft
|
2025-03-08 18:05:27 +01:00 |
|
|
|
bbb0c69911
|
derive: add options to control distribution
|
2025-03-08 18:05:27 +01:00 |
|
|
|
9953cacbc6
|
derive: option for some optimisations
|
2025-03-08 18:05:27 +01:00 |
|
|
|
13f953c27f
|
sere_to_tgba: produce state-names
|
2025-03-08 18:05:27 +01:00 |
|
|
|
bc0ef4d5b0
|
ltl2aa: handle edge case in UConcat
If SERE recognizes false, then combined with UConcat the property is
always true.
|
2025-03-08 18:05:27 +01:00 |
|
|
|
9b76e44b97
|
alternation: fix bug introduced in oe_combiner
turns out sometimes we want to account for bddfalse
|
2025-03-08 18:05:27 +01:00 |
|
|
|
3e451c408b
|
ltl2aa: implement EConcat
|
2025-03-08 18:05:27 +01:00 |
|
|
|
af91b0f376
|
ltl2aa: comment
|
2025-03-08 18:05:27 +01:00 |
|
|
|
2e2a3b4544
|
ltl2aa: finalize UConcat
|
2025-03-08 18:05:27 +01:00 |
|
|
|
e4f00229d7
|
ltl2aa: finish SERE aut merging with rhs outedges
|
2025-03-08 18:05:27 +01:00 |
|
|
|
d29c1413bc
|
ltl2aa: fix two bugs in SERE aut merge
|
2025-03-08 18:05:27 +01:00 |
|
|
|
e7df1ac42e
|
ltl2aa: place new state in var_to_state map
|
2025-03-08 18:05:27 +01:00 |
|
|
|
bb7a30f1fd
|
ltl2aa: implem closure
|
2025-03-08 18:05:27 +01:00 |
|
|
|
aba8c9d4fc
|
ltl2aa: share dict between sere and final aut
|
2025-03-08 18:05:27 +01:00 |
|
|
|
7e13cb18e8
|
ltl2aa: fix bdd manipulation in UConcat
|
2025-03-08 18:05:27 +01:00 |
|
|
|
9fd33667c0
|
ltl2aa: fix R & M operators handling
|
2025-03-08 18:05:27 +01:00 |
|
|
|
b1589b293a
|
Add ltl2aa binary to tests/core
|
2025-03-08 18:05:27 +01:00 |
|
|
|
bdf9762498
|
psl not working
|
2025-03-08 18:05:27 +01:00 |
|
|
|
29428bb9f0
|
ltl2aa: factorize self-loop creation
|
2025-03-08 18:05:27 +01:00 |
|
|
|
531fc4c550
|
twaalgos: add LTL to AA translation
|
2025-03-08 18:05:27 +01:00 |
|
|
|
8a6e8fb1d7
|
twaalgos: filter accepting sinks in oe combiner
|
2025-03-08 18:05:27 +01:00 |
|
|
|
f2a3ecab0d
|
graph: filter accepting sinks in univ_dest_mapper
|
2025-03-08 18:05:27 +01:00 |
|
