|
|
fface984ca
|
sonf: fix recursion of rewriting, was only called on operand
* spot/tl/sonf.cc: Here.
|
2025-10-15 12:52:55 +02:00 |
|
|
|
8efea81c75
|
merge
|
2025-03-17 16:11:36 +01:00 |
|
|
|
059c5072df
|
nix: provide package in release tarballs
|
2025-03-17 16:11:36 +01:00 |
|
|
|
c5746ef5cf
|
expansions: fix bogus false pairs in linear forms
|
2025-03-17 16:11:36 +01:00 |
|
|
|
42221100dd
|
nix: setup Nix Flake file
* flake.nix, flake.lock: here
|
2025-03-17 16:11:36 +01:00 |
|
|
|
3d3f311733
|
expansions: remove unused lambda capture
|
2025-03-17 16:11:36 +01:00 |
|
|
|
939942af30
|
expansions: fix sort behavior
The previous implementation was wrong and led to segfaults when sorting
large expansions
|
2025-03-17 16:11:36 +01:00 |
|
|
|
37b814c750
|
expansions: make signature canonical
Linear forms are now sorted and duplicates are removed
|
2025-03-17 16:11:36 +01:00 |
|
|
|
7fa1973613
|
expansions: fusion can produce false
let's discard the result if it's false
|
2025-03-17 16:11:36 +01:00 |
|
|
|
a32431c341
|
ltl2tgba_fm: setup switch between bdd and exp
|
2025-03-17 16:11:36 +01:00 |
|
|
|
dfa828739b
|
translate_aa: setup translation choice
|
2025-03-17 16:11:36 +01:00 |
|
|
|
f687ef7bbb
|
ltl2tgba_fm: switch for expansions
|
2025-03-17 16:11:36 +01:00 |
|
|
|
7cbf544d33
|
expansions: split
|
2025-03-17 16:11:36 +01:00 |
|
|
|
b15c0818c5
|
expansions: up variants
|
2025-03-17 16:11:36 +01:00 |
|
|
|
ed3d1ef4aa
|
expansions: expose easy expansion in python
|
2025-03-17 16:11:36 +01:00 |
|
|
|
90ea02d42a
|
expansions: store as vector of pairs
|
2025-03-17 16:11:36 +01:00 |
|
|
|
d760d2cb3b
|
expansions: US order in pipeline configurable
|
2025-03-17 16:11:36 +01:00 |
|
|
|
e50be0692d
|
expansions: UniquePrefixSeenOpt
|
2025-03-17 16:11:36 +01:00 |
|
|
|
29e0b22c2a
|
expansions: fixes + BDD encode changes + printer
|
2025-03-17 16:11:36 +01:00 |
|
|
|
f09c1dd7f3
|
expansions: simple determinization
|
2025-03-17 16:11:36 +01:00 |
|
|
|
931d39e739
|
expansions: signature merge impl
|
2025-03-17 16:11:36 +01:00 |
|
|
|
bbbcdc331a
|
expansions: optimize sigma star encoding
|
2025-03-17 16:11:36 +01:00 |
|
|
|
a4091ffc37
|
expansions: remove multiple old implementations
|
2025-03-17 16:11:36 +01:00 |
|
|
|
77d25d87a1
|
expansions: fix first_match case
|
2025-03-17 16:11:36 +01:00 |
|
|
|
382c57923c
|
twaalgos: ltl2tgba_fm: allow disabling SCC trim
|
2025-03-17 16:11:36 +01:00 |
|
|
|
b5f11f7366
|
expansions: allow toggling merge_edges off
|
2025-03-17 16:11:36 +01:00 |
|
|
|
518c58fe52
|
expansions: latest implementation
|
2025-03-17 16:11:36 +01:00 |
|
|
|
003230ed19
|
expansions: multimap version
|
2025-03-17 16:11:36 +01:00 |
|
|
|
ce9a94f224
|
expansions: determinize only once per state
|
2025-03-17 16:11:36 +01:00 |
|
|
|
faaefa7424
|
expansions: fix bdd method
|
2025-03-17 16:11:36 +01:00 |
|
|
|
12a8d5382d
|
expansions: add BDD method
|
2025-03-17 16:11:36 +01:00 |
|
|
|
9361116431
|
expansions: multiple implementations
|
2025-03-17 16:11:36 +01:00 |
|
|
|
3c6929829d
|
expansions: split-off OrRat case
|
2025-03-17 16:11:36 +01:00 |
|
|
|
1240fec39b
|
expansions: first_match deterministic
|
2025-03-17 16:11:36 +01:00 |
|
|
|
b9f461c025
|
expansions: draft
|
2025-03-17 16:11:36 +01:00 |
|
|
|
0fdd3c31f4
|
derive: add options to control distribution
|
2025-03-17 16:11:36 +01:00 |
|
|
|
89543e6a73
|
derive: option for some optimisations
|
2025-03-17 16:11:36 +01:00 |
|
|
|
e80c98751d
|
sere_to_tgba: produce state-names
|
2025-03-17 16:11:36 +01:00 |
|
|
|
7b936819cc
|
ltl2aa: handle edge case in UConcat
If SERE recognizes false, then combined with UConcat the property is
always true.
|
2025-03-17 16:11:36 +01:00 |
|
|
|
07a283498f
|
alternation: fix bug introduced in oe_combiner
turns out sometimes we want to account for bddfalse
|
2025-03-17 16:11:36 +01:00 |
|
|
|
465b135f44
|
ltl2aa: implement EConcat
|
2025-03-17 16:11:36 +01:00 |
|
|
|
e5d7ba9e22
|
ltl2aa: comment
|
2025-03-17 16:11:36 +01:00 |
|
|
|
dec854ee07
|
ltl2aa: finalize UConcat
|
2025-03-17 16:11:36 +01:00 |
|
|
|
0957c11c94
|
ltl2aa: finish SERE aut merging with rhs outedges
|
2025-03-17 16:11:36 +01:00 |
|
|
|
eca0bd4590
|
ltl2aa: fix two bugs in SERE aut merge
|
2025-03-17 16:11:36 +01:00 |
|
|
|
93c50e1610
|
ltl2aa: place new state in var_to_state map
|
2025-03-17 16:11:36 +01:00 |
|
|
|
58965475fb
|
ltl2aa: implem closure
|
2025-03-17 16:11:36 +01:00 |
|
|
|
4153ce0655
|
ltl2aa: share dict between sere and final aut
|
2025-03-17 16:11:36 +01:00 |
|
|
|
0c76e6dd21
|
ltl2aa: fix bdd manipulation in UConcat
|
2025-03-17 16:11:36 +01:00 |
|
|
|
8e8e44c5f9
|
ltl2aa: fix R & M operators handling
|
2025-03-17 16:11:36 +01:00 |
|
