From 684c9c47c43f4a79caaca7e3cba90760f071548a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 30 Dec 2016 10:38:04 +0100 Subject: [PATCH] twa: add prop_set::improve_det Algorithms that remove transitions can turn a non-deterministic automaton into a deterministic one, so we need to be able to specify that determinism can be improved (as opposed to preserved). * spot/twa/twa.hh (twa::prop_set::improve_det): New attribute. (twa::prop_keep, twa::prop_copy): Honor it. * spot/tl/exclusive.cc, spot/twaalgos/alternation.cc, spot/twaalgos/complete.cc, spot/twaalgos/degen.cc, spot/twaalgos/determinize.cc, spot/twaalgos/mask.cc, spot/twaalgos/minimize.cc, spot/twaalgos/remfin.cc, spot/twaalgos/remprop.cc, spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc, spot/twaalgos/simulation.cc, spot/twaalgos/strength.cc, spot/twaalgos/stutter.cc, spot/twaalgos/totgba.cc: Adjust calls to prop_keep() and prop_copy(). --- NEWS | 6 ++++++ spot/tl/exclusive.cc | 2 +- spot/twa/twa.hh | 38 +++++++++++++++++++++++++++++------- spot/twaalgos/alternation.cc | 2 +- spot/twaalgos/complete.cc | 1 + spot/twaalgos/degen.cc | 2 +- spot/twaalgos/determinize.cc | 2 +- spot/twaalgos/mask.cc | 6 +++--- spot/twaalgos/minimize.cc | 4 ++-- spot/twaalgos/remfin.cc | 6 +++--- spot/twaalgos/remprop.cc | 2 +- spot/twaalgos/sbacc.cc | 2 +- spot/twaalgos/sccfilter.cc | 7 ++++--- spot/twaalgos/simulation.cc | 7 +------ spot/twaalgos/strength.cc | 2 +- spot/twaalgos/stutter.cc | 6 +++--- spot/twaalgos/totgba.cc | 2 +- 17 files changed, 62 insertions(+), 35 deletions(-) diff --git a/NEWS b/NEWS index 5112cc2cc..623151421 100644 --- a/NEWS +++ b/NEWS @@ -68,6 +68,12 @@ New in spot 2.2.2.dev (Not yet released) twa::prop_very_weak()/twa::prop_semi_deterministic(), and that can be tested by is_very_weak_automaton()/is_semi_deterministic(). + * twa::prop_set has a new attribute used in twa::prop_copy() and + twa::prop_keep() to indicate that determinism may be improved by + an algorithm. In other words properties like + deterministic/semi-deterministic/unambiguous should be preserved + only if they are positive. + Build: * The configure script has a new option --enable-c++14, to compile in diff --git a/spot/tl/exclusive.cc b/spot/tl/exclusive.cc index 657d1365f..399b2dc28 100644 --- a/spot/tl/exclusive.cc +++ b/spot/tl/exclusive.cc @@ -177,7 +177,7 @@ namespace spot twa_graph_ptr res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); - res->prop_copy(aut, { true, true, true, true }); + res->prop_copy(aut, { true, true, false, true, true }); res->copy_acceptance_of(aut); if (simplify_guards) { diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 7e66f82f6..b6f216159 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -1404,11 +1404,17 @@ namespace spot /// /// This can be used for instance as: /// \code - /// aut->prop_copy(other_aut, {true, false, false, true}); + /// aut->prop_copy(other_aut, {true, false, false, false, true}); /// \endcode /// This would copy the "state-based acceptance" and /// "stutter invariant" properties from \c other_aut to \c code. /// + /// There are two flags for the determinism. If \code + /// deterministic is set, the deterministic, semi-deterministic, + /// and unambiguous properties are copied as-is. If deterministic + /// is unset but improve_det is set, then those properties are + /// only copied if they are positive. + /// /// The reason there is no default value for these flags is that /// whenever we add a new property that do not fall into any of /// these groups, we will be forced to review all algorithm to @@ -1420,7 +1426,8 @@ namespace spot { bool state_based; ///< preserve state-based acceptnace bool inherently_weak; ///< preserve inherently weak, weak, & terminal - bool deterministic; ///< preserve deterministic and unambiguous + bool deterministic; ///< preserve deterministic, semi-det, unambiguous + bool improve_det; ///< improves deterministic, semi-det, unambiguous bool stutter_inv; ///< preserve stutter invariance /// \brief An all-true \c prop_set @@ -1432,7 +1439,7 @@ namespace spot /// properties currently implemented, use an explicit /// /// \code - /// {true, true, true, true} + /// {true, true, true, true, true} /// \endcode /// /// instead of calling \c all(). This way, the day a new @@ -1440,7 +1447,7 @@ namespace spot /// algorithm X, in case that new property is not preserved. static prop_set all() { - return { true, true, true, true }; + return { true, true, true, true, true }; } }; @@ -1471,6 +1478,20 @@ namespace spot prop_semi_deterministic(other->prop_semi_deterministic()); prop_unambiguous(other->prop_unambiguous()); } + else if (p.improve_det) + { + if (other->prop_deterministic().is_true()) + { + prop_deterministic(true); + } + else + { + if (other->prop_semi_deterministic().is_true()) + prop_semi_deterministic(true); + if (other->prop_unambiguous().is_true()) + prop_unambiguous(true); + } + } if (p.stutter_inv) prop_stutter_invariant(other->prop_stutter_invariant()); } @@ -1493,9 +1514,12 @@ namespace spot } if (!p.deterministic) { - prop_deterministic(trival::maybe()); - prop_semi_deterministic(trival::maybe()); - prop_unambiguous(trival::maybe()); + if (!(p.improve_det && prop_deterministic().is_true())) + prop_deterministic(trival::maybe()); + if (!(p.improve_det && prop_semi_deterministic().is_true())) + prop_semi_deterministic(trival::maybe()); + if (!(p.improve_det && prop_unambiguous().is_true())) + prop_unambiguous(trival::maybe()); } if (!p.stutter_inv) prop_stutter_invariant(trival::maybe()); diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index fa4005cb7..710a460aa 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -354,7 +354,7 @@ namespace spot res->copy_ap_of(aut_); // We preserve deterministic-like properties, and // stutter-invariance. - res->prop_copy(aut_, {false, false, true, true}); + res->prop_copy(aut_, {false, false, false, true, true}); res->set_generalized_buchi(has_reject_more_ + reject_1_count_); // We for easier computation of outgoing sets, we will diff --git a/spot/twaalgos/complete.cc b/spot/twaalgos/complete.cc index cef86c619..60018ecaa 100644 --- a/spot/twaalgos/complete.cc +++ b/spot/twaalgos/complete.cc @@ -141,6 +141,7 @@ namespace spot true, // state based true, // inherently_weak true, // deterministic + true, // improve det true, // stutter inv. }); complete_here(res); diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index c47b19836..9256afc1b 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -212,7 +212,7 @@ namespace spot if (want_sba) res->prop_state_acc(true); // Preserve determinism, weakness, and stutter-invariance - res->prop_copy(a, { false, true, true, true }); + res->prop_copy(a, { false, true, true, true, true }); // Create an order of acceptance conditions. Each entry in this // vector correspond to an acceptance set. Each index can diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index c18230d1c..cc7e0cdb9 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -640,7 +640,7 @@ namespace spot res->prop_copy(aut, { false, // state based false, // inherently_weak - false, // deterministic + false, false, // deterministic true // stutter inv }); diff --git a/spot/twaalgos/mask.cc b/spot/twaalgos/mask.cc index dcbbb19f8..c344a0778 100644 --- a/spot/twaalgos/mask.cc +++ b/spot/twaalgos/mask.cc @@ -26,7 +26,7 @@ namespace spot { auto res = make_twa_graph(in->get_dict()); res->copy_ap_of(in); - res->prop_copy(in, { true, true, true, false }); + res->prop_copy(in, { true, true, true, true, false }); unsigned na = in->num_sets(); unsigned tr = to_remove.count(); assert(tr <= na); @@ -54,7 +54,7 @@ namespace spot auto res = make_twa_graph(in->get_dict()); res->copy_ap_of(in); - res->prop_copy(in, { true, true, true, false }); + res->prop_copy(in, { true, true, false, true, false }); res->copy_acceptance_of(in); transform_copy(in, res, [&](unsigned src, bdd& cond, @@ -76,7 +76,7 @@ namespace spot auto res = make_twa_graph(in->get_dict()); res->copy_ap_of(in); - res->prop_copy(in, { true, true, true, false }); + res->prop_copy(in, { true, true, false, true, false }); res->copy_acceptance_of(in); transform_accessible(in, res, [&](unsigned src, bdd& cond, diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index 4bf78f32c..4bb295624 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -486,7 +486,7 @@ namespace spot // final is empty: there is no acceptance condition build_state_set(det_a, non_final); auto res = minimize_dfa(det_a, final, non_final); - res->prop_copy(a, { false, false, false, true }); + res->prop_copy(a, { false, false, false, false, true }); res->prop_deterministic(true); res->prop_weak(true); res->prop_state_acc(true); @@ -591,7 +591,7 @@ namespace spot } auto res = minimize_dfa(det_a, final, non_final); - res->prop_copy(a, { false, false, false, true }); + res->prop_copy(a, { false, false, false, false, true }); res->prop_deterministic(true); res->prop_weak(true); // If the input was terminal, then the output is also terminal. diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 30ff83a75..eaa48f309 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -224,7 +224,7 @@ namespace spot unsigned nst = aut->num_states(); auto res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); - res->prop_copy(aut, { true, false, false, true }); + res->prop_copy(aut, { true, false, false, false, true }); res->new_states(nst); res->set_buchi(); res->set_init_state(aut->get_init_state_number()); @@ -460,7 +460,7 @@ namespace spot { true, // state based true, // inherently weak - true, // determinisitic + true, true, // determinisitic true, // stutter inv. }); scc_info si(res); @@ -664,7 +664,7 @@ namespace spot unsigned nst = aut->num_states(); auto res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); - res->prop_copy(aut, { true, false, false, true }); + res->prop_copy(aut, { true, false, false, false, true }); res->new_states(nst); res->set_acceptance(aut->num_sets() + extra_sets, new_code); res->set_init_state(aut->get_init_state_number()); diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc index f1d5ca53f..8340bef7e 100644 --- a/spot/twaalgos/remprop.cc +++ b/spot/twaalgos/remprop.cc @@ -130,7 +130,7 @@ namespace spot twa_graph_ptr res = make_twa_graph(d); res->copy_ap_of(aut); - res->prop_copy(aut, { true, true, false, false }); + res->prop_copy(aut, { true, true, false, false, false }); res->copy_acceptance_of(aut); for (auto ap: props_exist) diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 11525d38c..7ad03f0ca 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -56,7 +56,7 @@ namespace spot auto res = make_twa_graph(old->get_dict()); res->copy_ap_of(old); res->copy_acceptance_of(old); - res->prop_copy(old, {false, true, true, true}); + res->prop_copy(old, {false, true, true, true, true}); res->prop_state_acc(true); typedef std::pair pair_t; diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index d3f7a1985..9ce0cffee 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -375,7 +375,7 @@ namespace spot else res = scc_filter_apply>>(aut, given_si); - res->prop_copy(aut, { true, true, true, true }); + res->prop_copy(aut, { true, true, false, true, true }); return res; } @@ -415,7 +415,8 @@ namespace spot res->prop_copy(aut, { false, // state-based acceptance is not preserved true, - true, + false, + true, // determinism improved true, }); return res; @@ -449,7 +450,7 @@ namespace spot res->prop_copy(aut, { false, // state-based acceptance is not preserved true, - false, // determinism may not be preserved + false, false, // determinism may not be preserved false, // stutter inv. of suspvars probably altered }); return res; diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index bceb97f42..3db2c06f8 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -594,15 +594,10 @@ namespace spot res->prop_copy(original_, { false, // state-based acc forced below true, // weakness preserved, - true, // determinism checked and overridden below - // and "unambiguous" property preserved + false, true, // determinism improved true, // stutter inv. }); // !unambiguous and !semi-deterministic are not preserved - if (original_->prop_semi_deterministic().is_false()) - res->prop_semi_deterministic(trival::maybe()); - if (original_->prop_unambiguous().is_false()) - res->prop_unambiguous(trival::maybe()); if (!Cosimulation) res->prop_deterministic(nb_minato == nb_satoneset); if (Sba) diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index fcce611db..ef161fbcf 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -277,7 +277,7 @@ namespace spot twa_graph_ptr res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); - res->prop_copy(aut, { true, false, true, false }); + res->prop_copy(aut, { true, false, false, true, false }); if (keep & Strong) res->copy_acceptance_of(aut); diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index 33c9e185c..1dad5a144 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -405,7 +405,7 @@ namespace spot if (num_states != a->num_states()) a->prop_keep({true, // state_based false, // inherently_weak - false, // deterministic + false, false, // deterministic false, // stutter inv. }); a->merge_edges(); @@ -425,7 +425,7 @@ namespace spot { a->prop_keep({false, // state_based false, // inherently_weak - false, // deterministic + false, false, // deterministic false, // stutter inv. }); @@ -505,7 +505,7 @@ namespace spot twa_graph_ptr closure(const const_twa_graph_ptr& a) { - return closure(make_twa_graph(a, {true, true, true, false})); + return closure(make_twa_graph(a, twa::prop_set::all())); } // The stutter check algorithm to use can be overridden via an diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index eb85a291a..33fa52390 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -146,7 +146,7 @@ namespace spot auto out = make_twa_graph(in->get_dict()); out->copy_ap_of(in); - out->prop_copy(in, {false, false, false, true}); + out->prop_copy(in, {false, false, false, false, true}); out->set_generalized_buchi(p); acc_cond::mark_t outall = out->acc().all_sets();