Add several options to CAR
* spot/twa/acc.hh: Remove useless comment. * spot/twaalgos/car.cc: Rewrite the implementation to try multiple algorithms and choose the best, add the possibility to force the order of the colors/pairs in LAR and use propagate_marks_here. * spot/twaalgos/car.hh, tests/python/car.py: Create a new system of options for CAR. * spot/twaalgos/degen.cc, spot/twaalgos/degen.hh: Add the possibility to forbid some marks in is_partially_degeneralizable.
This commit is contained in:
Florian Renkin
parent
6489d6c091
commit
dddc7920e4
6 changed files with 1165 additions and 866 deletions
|
|
@ -592,7 +592,6 @@ namespace spot
|
|||
}
|
||||
if (elements.size() == 2)
|
||||
{
|
||||
// Vaut 1 si si c'est le 2e qui est bon
|
||||
unsigned pos = elements[1].back().sub.op == op
|
||||
&& elements[1][0].mark.count() == 1;
|
||||
if (!(elements[0].back().sub.op == op || pos))
|
||||
|
|
|
|||
1076
spot/twaalgos/car.cc
1076
spot/twaalgos/car.cc
File diff suppressed because it is too large
Load diff
|
|
@ -23,6 +23,23 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
struct car_option
|
||||
{
|
||||
bool search_ex = true;
|
||||
bool use_last = true;
|
||||
bool force_order = true;
|
||||
bool partial_degen = true;
|
||||
bool acc_clean = true;
|
||||
bool parity_equiv = true;
|
||||
bool parity_prefix = true;
|
||||
bool rabin_to_buchi = true;
|
||||
bool reduce_col_deg = false;
|
||||
bool propagate_col = true;
|
||||
bool pretty_print = true;
|
||||
};
|
||||
|
||||
|
||||
|
||||
/// \ingroup twa_acc_transform
|
||||
/// \brief Take an automaton with any acceptance condition and return an
|
||||
/// equivalent parity automaton.
|
||||
|
|
@ -43,17 +60,10 @@ namespace spot
|
|||
/// If \a pretty_print is true, we give a name to the states describing the
|
||||
// state of the aut_ and the permutation.
|
||||
|
||||
SPOT_API twa_graph_ptr
|
||||
remove_false_transitions(const twa_graph_ptr a);
|
||||
SPOT_API twa_graph_ptr
|
||||
remove_false_transitions(const twa_graph_ptr a);
|
||||
|
||||
SPOT_API twa_graph_ptr
|
||||
to_parity(const twa_graph_ptr &aut, const car_option options = car_option());
|
||||
|
||||
SPOT_API twa_graph_ptr
|
||||
car(const twa_graph_ptr &aut,
|
||||
bool search_ex = true,
|
||||
bool partial_degen = true,
|
||||
bool scc_acc_clean = true,
|
||||
bool parity_equiv = true,
|
||||
bool use_last = true,
|
||||
bool parity_prefix = true,
|
||||
bool rabin_to_buchi = true,
|
||||
bool pretty_print = false);
|
||||
} // namespace spot
|
||||
|
|
@ -846,7 +846,8 @@ namespace spot
|
|||
|
||||
acc_cond::mark_t
|
||||
is_partially_degeneralizable(const const_twa_graph_ptr& aut,
|
||||
bool allow_inf, bool allow_fin)
|
||||
bool allow_inf, bool allow_fin,
|
||||
std::vector<acc_cond::mark_t> forbid)
|
||||
{
|
||||
auto& code = aut->get_acceptance();
|
||||
|
||||
|
|
@ -881,15 +882,21 @@ namespace spot
|
|||
case acc_cond::acc_op::FinNeg:
|
||||
pos -= 2;
|
||||
if (allow_fin)
|
||||
if (update(code[pos].mark))
|
||||
{
|
||||
auto m = code[pos].mark;
|
||||
if (!std::count(forbid.begin(), forbid.end(), m) && update(m))
|
||||
return res;
|
||||
}
|
||||
break;
|
||||
case acc_cond::acc_op::Inf:
|
||||
case acc_cond::acc_op::InfNeg:
|
||||
pos -= 2;
|
||||
if (allow_inf)
|
||||
if (update(code[pos].mark))
|
||||
{
|
||||
auto m = code[pos].mark;
|
||||
if (!std::count(forbid.begin(), forbid.end(), m) && update(m))
|
||||
return res;
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -151,7 +151,8 @@ namespace spot
|
|||
SPOT_API acc_cond::mark_t
|
||||
is_partially_degeneralizable(const const_twa_graph_ptr& aut,
|
||||
bool allow_inf = true,
|
||||
bool allow_fin = true);
|
||||
bool allow_fin = true,
|
||||
std::vector<acc_cond::mark_t> forbid = {});
|
||||
|
||||
/// \ingroup twa_algorithms
|
||||
/// \brief Propagate marks around the automaton
|
||||
|
|
|
|||
|
|
@ -20,31 +20,83 @@
|
|||
|
||||
import spot
|
||||
|
||||
no_option = spot.car_option()
|
||||
no_option.search_ex = False
|
||||
no_option.use_last = False
|
||||
no_option.force_order = False
|
||||
no_option.partial_degen = False
|
||||
no_option.acc_clean = False
|
||||
no_option.parity_equiv = False
|
||||
no_option.parity_prefix = False
|
||||
no_option.rabin_to_buchi = False
|
||||
no_option.propagate_col = False
|
||||
|
||||
acc_clean_search_opt = spot.car_option()
|
||||
acc_clean_search_opt.force_order = False
|
||||
acc_clean_search_opt.partial_degen = False
|
||||
acc_clean_search_opt.parity_equiv = False
|
||||
acc_clean_search_opt.parity_prefix = False
|
||||
acc_clean_search_opt.rabin_to_buchi = False
|
||||
acc_clean_search_opt.propagate_col = False
|
||||
|
||||
partial_degen_opt = spot.car_option()
|
||||
partial_degen_opt.search_ex = False
|
||||
partial_degen_opt.force_order = False
|
||||
partial_degen_opt.parity_equiv = False
|
||||
partial_degen_opt.parity_prefix = False
|
||||
partial_degen_opt.rabin_to_buchi = False
|
||||
partial_degen_opt.propagate_col = False
|
||||
|
||||
parity_equiv_opt = spot.car_option()
|
||||
parity_equiv_opt.search_ex = False
|
||||
parity_equiv_opt.use_last = False
|
||||
parity_equiv_opt.force_order = False
|
||||
parity_equiv_opt.partial_degen = False
|
||||
parity_equiv_opt.parity_prefix = False
|
||||
parity_equiv_opt.rabin_to_buchi = False
|
||||
parity_equiv_opt.propagate_col = False
|
||||
|
||||
rab_to_buchi_opt = spot.car_option()
|
||||
rab_to_buchi_opt.use_last = False
|
||||
rab_to_buchi_opt.force_order = False
|
||||
rab_to_buchi_opt.partial_degen = False
|
||||
rab_to_buchi_opt.parity_equiv = False
|
||||
rab_to_buchi_opt.parity_prefix = False
|
||||
rab_to_buchi_opt.propagate_col = False
|
||||
|
||||
# Force to use CAR or IAR for each SCC
|
||||
use_car_opt = spot.car_option()
|
||||
use_car_opt.partial_degen = False
|
||||
use_car_opt.parity_equiv = False
|
||||
use_car_opt.parity_prefix = False
|
||||
use_car_opt.rabin_to_buchi = False
|
||||
use_car_opt.propagate_col = False
|
||||
|
||||
all_opt = spot.car_option()
|
||||
all_opt.pretty_print = True
|
||||
|
||||
|
||||
options = [
|
||||
# No option
|
||||
[False, False, False, False, False, False, False, False],
|
||||
# Only acc clean and …
|
||||
# … search last
|
||||
[True, False, True, False, True, False, False, False],
|
||||
# … partial degen
|
||||
[False, True, True, False, False, False, False, False],
|
||||
# … parity equiv
|
||||
[False, False, True, True, False, False, False, False],
|
||||
# … parity prefix
|
||||
[False, False, True, False, False, True, False, False],
|
||||
# … rabin to buchi
|
||||
[False, False, True, False, False, False, True, False],
|
||||
no_option,
|
||||
acc_clean_search_opt,
|
||||
partial_degen_opt,
|
||||
parity_equiv_opt,
|
||||
rab_to_buchi_opt,
|
||||
use_car_opt,
|
||||
spot.car_option(),
|
||||
]
|
||||
|
||||
i = 1
|
||||
|
||||
def test(aut):
|
||||
global i
|
||||
for se, par, cl, parity, last, pref, rab, pri in options:
|
||||
p = spot.car(aut, se, par, cl, parity, last, pref, rab, pri)
|
||||
for opt in options:
|
||||
try:
|
||||
p = spot.to_parity(aut, opt)
|
||||
assert(spot.are_equivalent(aut, p))
|
||||
print(f"OK {i}")
|
||||
i += 1
|
||||
except:
|
||||
# Are equivalent can raise exception
|
||||
assert(False)
|
||||
|
||||
|
||||
test(spot.automaton("""HOA: v1
|
||||
|
|
@ -154,10 +206,10 @@ explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4}
|
|||
4 [!0&!1] 1 {2 4} State: 5 [!0&1] 4 --END--
|
||||
"""))
|
||||
|
||||
for f in spot.randltl(15, 1000):
|
||||
for f in spot.randltl(15, 2000):
|
||||
test(spot.translate(f, "det", "G"))
|
||||
|
||||
for f in spot.randltl(5, 10000):
|
||||
for f in spot.randltl(5, 25000):
|
||||
test(spot.translate(f))
|
||||
|
||||
test(spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det'))
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue