alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

twa: add prop_set::improve_det

Browse source 
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().
This commit is contained in:
Alexandre Duret-Lutz 2016-12-30 10:38:04 +01:00
parent ada8185361
commit 684c9c47c4
17 changed files with 62 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

6
NEWS
View file

@ -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 twa::prop_very_weak()/twa::prop_semi_deterministic(), and that can
be tested by is_very_weak_automaton()/is_semi_deterministic(). 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: Build:
* The configure script has a new option --enable-c++14, to compile in * The configure script has a new option --enable-c++14, to compile in

2
spot/tl/exclusive.cc
View file

@ -177,7 +177,7 @@ namespace spot
twa_graph_ptr res = make_twa_graph(aut->get_dict()); twa_graph_ptr res = make_twa_graph(aut->get_dict());
res->copy_ap_of(aut); 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); res->copy_acceptance_of(aut);
if (simplify_guards) if (simplify_guards)
{ {

38
spot/twa/twa.hh
View file

@ -1404,11 +1404,17 @@ namespace spot
/// ///
/// This can be used for instance as: /// This can be used for instance as:
/// \code /// \code
/// aut->prop_copy(other_aut, {true, false, false, true}); /// aut->prop_copy(other_aut, {true, false, false, false, true});
/// \endcode /// \endcode
/// This would copy the "state-based acceptance" and /// This would copy the "state-based acceptance" and
/// "stutter invariant" properties from \c other_aut to \c code. /// "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 /// 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 /// whenever we add a new property that do not fall into any of
/// these groups, we will be forced to review all algorithm to /// 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 state_based; ///< preserve state-based acceptnace
bool inherently_weak; ///< preserve inherently weak, weak, & terminal 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 bool stutter_inv; ///< preserve stutter invariance
/// \brief An all-true \c prop_set /// \brief An all-true \c prop_set
@ -1432,7 +1439,7 @@ namespace spot
/// properties currently implemented, use an explicit /// properties currently implemented, use an explicit
/// ///
/// \code /// \code
/// {true, true, true, true} /// {true, true, true, true, true}
/// \endcode /// \endcode
/// ///
/// instead of calling \c all(). This way, the day a new /// 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. /// algorithm X, in case that new property is not preserved.
static prop_set all() 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_semi_deterministic(other->prop_semi_deterministic());
prop_unambiguous(other->prop_unambiguous()); 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) if (p.stutter_inv)
prop_stutter_invariant(other->prop_stutter_invariant()); prop_stutter_invariant(other->prop_stutter_invariant());
} }
@ -1493,9 +1514,12 @@ namespace spot
} }
if (!p.deterministic) if (!p.deterministic)
{ {
prop_deterministic(trival::maybe()); if (!(p.improve_det && prop_deterministic().is_true()))
prop_semi_deterministic(trival::maybe()); prop_deterministic(trival::maybe());
prop_unambiguous(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) if (!p.stutter_inv)
prop_stutter_invariant(trival::maybe()); prop_stutter_invariant(trival::maybe());

2
spot/twaalgos/alternation.cc
View file

@ -354,7 +354,7 @@ namespace spot
res->copy_ap_of(aut_); res->copy_ap_of(aut_);
// We preserve deterministic-like properties, and // We preserve deterministic-like properties, and
// stutter-invariance. // 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_); res->set_generalized_buchi(has_reject_more_ + reject_1_count_);
// We for easier computation of outgoing sets, we will // We for easier computation of outgoing sets, we will

1
spot/twaalgos/complete.cc
View file

@ -141,6 +141,7 @@ namespace spot
true, // state based true, // state based
true, // inherently_weak true, // inherently_weak
true, // deterministic true, // deterministic
true, // improve det
true, // stutter inv. true, // stutter inv.
}); });
complete_here(res); complete_here(res);

2
spot/twaalgos/degen.cc
View file

@ -212,7 +212,7 @@ namespace spot
if (want_sba) if (want_sba)
res->prop_state_acc(true); res->prop_state_acc(true);
// Preserve determinism, weakness, and stutter-invariance // 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 // Create an order of acceptance conditions. Each entry in this
// vector correspond to an acceptance set. Each index can // vector correspond to an acceptance set. Each index can

2
spot/twaalgos/determinize.cc
View file

@ -640,7 +640,7 @@ namespace spot
res->prop_copy(aut, res->prop_copy(aut,
{ false, // state based { false, // state based
false, // inherently_weak false, // inherently_weak
false, // deterministic false, false, // deterministic
true // stutter inv true // stutter inv
}); });

6
spot/twaalgos/mask.cc
View file

@ -26,7 +26,7 @@ namespace spot
{ {
auto res = make_twa_graph(in->get_dict()); auto res = make_twa_graph(in->get_dict());
res->copy_ap_of(in); 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 na = in->num_sets();
unsigned tr = to_remove.count(); unsigned tr = to_remove.count();
assert(tr <= na); assert(tr <= na);
@ -54,7 +54,7 @@ namespace spot
auto res = make_twa_graph(in->get_dict()); auto res = make_twa_graph(in->get_dict());
res->copy_ap_of(in); 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); res->copy_acceptance_of(in);
transform_copy(in, res, [&](unsigned src, transform_copy(in, res, [&](unsigned src,
bdd& cond, bdd& cond,
@ -76,7 +76,7 @@ namespace spot
auto res = make_twa_graph(in->get_dict()); auto res = make_twa_graph(in->get_dict());
res->copy_ap_of(in); 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); res->copy_acceptance_of(in);
transform_accessible(in, res, [&](unsigned src, transform_accessible(in, res, [&](unsigned src,
bdd& cond, bdd& cond,

4
spot/twaalgos/minimize.cc
View file

@ -486,7 +486,7 @@ namespace spot
// final is empty: there is no acceptance condition // final is empty: there is no acceptance condition
build_state_set(det_a, non_final); build_state_set(det_a, non_final);
auto res = minimize_dfa(det_a, final, 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_deterministic(true);
res->prop_weak(true); res->prop_weak(true);
res->prop_state_acc(true); res->prop_state_acc(true);
@ -591,7 +591,7 @@ namespace spot
} }
auto res = minimize_dfa(det_a, final, 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_deterministic(true);
res->prop_weak(true); res->prop_weak(true);
// If the input was terminal, then the output is also terminal. // If the input was terminal, then the output is also terminal.

6
spot/twaalgos/remfin.cc
View file

@ -224,7 +224,7 @@ namespace spot
unsigned nst = aut->num_states(); unsigned nst = aut->num_states();
auto res = make_twa_graph(aut->get_dict()); auto res = make_twa_graph(aut->get_dict());
res->copy_ap_of(aut); 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->new_states(nst);
res->set_buchi(); res->set_buchi();
res->set_init_state(aut->get_init_state_number()); res->set_init_state(aut->get_init_state_number());
@ -460,7 +460,7 @@ namespace spot
{ {
true, // state based true, // state based
true, // inherently weak true, // inherently weak
true, // determinisitic true, true, // determinisitic
true, // stutter inv. true, // stutter inv.
}); });
scc_info si(res); scc_info si(res);
@ -664,7 +664,7 @@ namespace spot
unsigned nst = aut->num_states(); unsigned nst = aut->num_states();
auto res = make_twa_graph(aut->get_dict()); auto res = make_twa_graph(aut->get_dict());
res->copy_ap_of(aut); 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->new_states(nst);
res->set_acceptance(aut->num_sets() + extra_sets, new_code); res->set_acceptance(aut->num_sets() + extra_sets, new_code);
res->set_init_state(aut->get_init_state_number()); res->set_init_state(aut->get_init_state_number());

2
spot/twaalgos/remprop.cc
View file

@ -130,7 +130,7 @@ namespace spot
twa_graph_ptr res = make_twa_graph(d); twa_graph_ptr res = make_twa_graph(d);
res->copy_ap_of(aut); 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); res->copy_acceptance_of(aut);
for (auto ap: props_exist) for (auto ap: props_exist)

2
spot/twaalgos/sbacc.cc
View file

@ -56,7 +56,7 @@ namespace spot
auto res = make_twa_graph(old->get_dict()); auto res = make_twa_graph(old->get_dict());
res->copy_ap_of(old); res->copy_ap_of(old);
res->copy_acceptance_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); res->prop_state_acc(true);
typedef std::pair<unsigned, acc_cond::mark_t> pair_t; typedef std::pair<unsigned, acc_cond::mark_t> pair_t;

7
spot/twaalgos/sccfilter.cc
View file

@ -375,7 +375,7 @@ namespace spot
else else
res = scc_filter_apply<state_filter res = scc_filter_apply<state_filter
<acc_filter_mask<false, true>>>(aut, given_si); <acc_filter_mask<false, true>>>(aut, given_si);
res->prop_copy(aut, { true, true, true, true }); res->prop_copy(aut, { true, true, false, true, true });
return res; return res;
} }
@ -415,7 +415,8 @@ namespace spot
res->prop_copy(aut, res->prop_copy(aut,
{ false, // state-based acceptance is not preserved { false, // state-based acceptance is not preserved
true, true,
true, false,
true, // determinism improved
true, true,
}); });
return res; return res;
@ -449,7 +450,7 @@ namespace spot
res->prop_copy(aut, res->prop_copy(aut,
{ false, // state-based acceptance is not preserved { false, // state-based acceptance is not preserved
true, true,
false, // determinism may not be preserved false, false, // determinism may not be preserved
false, // stutter inv. of suspvars probably altered false, // stutter inv. of suspvars probably altered
}); });
return res; return res;

7
spot/twaalgos/simulation.cc
View file

@ -594,15 +594,10 @@ namespace spot
res->prop_copy(original_, res->prop_copy(original_,
{ false, // state-based acc forced below { false, // state-based acc forced below
true, // weakness preserved, true, // weakness preserved,
true, // determinism checked and overridden below false, true, // determinism improved
// and "unambiguous" property preserved
true, // stutter inv. true, // stutter inv.
}); });
// !unambiguous and !semi-deterministic are not preserved // !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) if (!Cosimulation)
res->prop_deterministic(nb_minato == nb_satoneset); res->prop_deterministic(nb_minato == nb_satoneset);
if (Sba) if (Sba)

2
spot/twaalgos/strength.cc
View file

@ -277,7 +277,7 @@ namespace spot
twa_graph_ptr res = make_twa_graph(aut->get_dict()); twa_graph_ptr res = make_twa_graph(aut->get_dict());
res->copy_ap_of(aut); 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) if (keep & Strong)
res->copy_acceptance_of(aut); res->copy_acceptance_of(aut);

6
spot/twaalgos/stutter.cc
View file

@ -405,7 +405,7 @@ namespace spot
if (num_states != a->num_states()) if (num_states != a->num_states())
a->prop_keep({true, // state_based a->prop_keep({true, // state_based
false, // inherently_weak false, // inherently_weak
false, // deterministic false, false, // deterministic
false, // stutter inv. false, // stutter inv.
}); });
a->merge_edges(); a->merge_edges();
@ -425,7 +425,7 @@ namespace spot
{ {
a->prop_keep({false, // state_based a->prop_keep({false, // state_based
false, // inherently_weak false, // inherently_weak
false, // deterministic false, false, // deterministic
false, // stutter inv. false, // stutter inv.
}); });
@ -505,7 +505,7 @@ namespace spot
twa_graph_ptr twa_graph_ptr
closure(const const_twa_graph_ptr& a) 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 // The stutter check algorithm to use can be overridden via an

2
spot/twaalgos/totgba.cc
View file

@ -146,7 +146,7 @@ namespace spot
auto out = make_twa_graph(in->get_dict()); auto out = make_twa_graph(in->get_dict());
out->copy_ap_of(in); 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); out->set_generalized_buchi(p);
acc_cond::mark_t outall = out->acc().all_sets(); acc_cond::mark_t outall = out->acc().all_sets();