Commit b43f75e9 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

tgba: move boolean properties from tgba_digraph to tgba

* src/tgba/tgbagraph.hh: Remove the set_bprop/get_bprop interface.
* src/tgba/tgba.cc, src/tgba/tgba.hh: Add a new interface for
setting/querying/copying the following properties: single_acc_set,
state_based_acc, inherently_weak, deterministic.
* src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
src/neverparse/neverclaimparse.yy, src/saba/sabacomplementtgba.cc,
src/tgba/tgbagraph.cc, src/tgbaalgos/degen.cc, src/tgbaalgos/dotty.cc,
src/tgbaalgos/isdet.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/postproc.cc, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/simulation.cc, src/tgbatest/degenlskip.test,
src/tgbatest/ltl2tgba.cc: Adjust to the new interface, or use
it to bypass some useless work.
parent e3b5119f
...@@ -231,10 +231,11 @@ namespace spot ...@@ -231,10 +231,11 @@ namespace spot
realizable_(realizable) realizable_(realizable)
{ {
out_->copy_ap_of(a->aut); out_->copy_ap_of(a->aut);
out_->set_bprop(tgba_digraph::StateBasedAcc); out_->prop_state_based_acc();
acc_ = out_->set_single_acceptance_set(); acc_ = out_->set_single_acceptance_set();
out_->new_states(num_states_ * (a->accpair_count + 1)); out_->new_states(num_states_ * (a->accpair_count + 1));
out_->set_init_state(a->aut->get_init_state_number()); out_->set_init_state(a->aut->get_init_state_number());
} }
tgba_digraph_ptr tgba_digraph_ptr
......
...@@ -46,7 +46,7 @@ namespace spot ...@@ -46,7 +46,7 @@ namespace spot
{ {
out_->copy_ap_of(aut); out_->copy_ap_of(aut);
out_->set_single_acceptance_set(); out_->set_single_acceptance_set();
out_->set_bprop(tgba_digraph::StateBasedAcc); out_->prop_state_based_acc();
out_->new_states(num_states_ * (d_->accpair_count + 1)); out_->new_states(num_states_ * (d_->accpair_count + 1));
auto i = aut->get_init_state(); auto i = aut->get_init_state();
......
...@@ -303,7 +303,7 @@ namespace spot ...@@ -303,7 +303,7 @@ namespace spot
tgba_digraph_ptr result = make_tgba_digraph(dict); tgba_digraph_ptr result = make_tgba_digraph(dict);
auto namer = result->create_namer<std::string>(); auto namer = result->create_namer<std::string>();
result->set_single_acceptance_set(); result->set_single_acceptance_set();
result->set_bprop(tgba_digraph::SBA); result->prop_state_based_acc();
neverclaimyy::parser parser(error_list, env, result, namer, fcache); neverclaimyy::parser parser(error_list, env, result, namer, fcache);
parser.set_debug_level(debug); parser.set_debug_level(debug);
......
...@@ -186,7 +186,7 @@ namespace spot ...@@ -186,7 +186,7 @@ namespace spot
: automaton_(automaton), the_acceptance_cond_(the_acceptance_cond), : automaton_(automaton), the_acceptance_cond_(the_acceptance_cond),
origin_(origin) origin_(origin)
{ {
assert(automaton->get_bprop(tgba_digraph::SBA)); assert(automaton->is_sba());
// If state not accepting or rank is even // If state not accepting or rank is even
if (((origin_->get_rank() & 1) == 0) || if (((origin_->get_rank() & 1) == 0) ||
!automaton_->state_is_accepting(origin_->get_state())) !automaton_->state_is_accepting(origin_->get_state()))
......
...@@ -29,6 +29,7 @@ namespace spot ...@@ -29,6 +29,7 @@ namespace spot
last_support_conditions_input_(0), last_support_conditions_input_(0),
num_acc_(-1) num_acc_(-1)
{ {
props = 0U;
} }
tgba::~tgba() tgba::~tgba()
......
...@@ -251,6 +251,89 @@ namespace spot ...@@ -251,6 +251,89 @@ namespace spot
private: private:
mutable bdd last_support_conditions_output_; mutable bdd last_support_conditions_output_;
mutable int num_acc_; mutable int num_acc_;
protected:
// Boolean properties. Beware: true means that the property
// holds, but false means the property is unknown.
struct bprop
{
bool single_acc_set:1; // A single acceptance set.
bool state_based_acc:1; // State-based acceptance.
bool inherently_weak:1; // Weak automaton.
bool deterministic:1; // Deterministic automaton.
};
union
{
unsigned props;
bprop is;
};
public:
bool has_single_acc_set() const
{
return is.single_acc_set;
}
void prop_single_acc_set(bool val = true)
{
is.single_acc_set = val;
}
bool has_state_based_acc() const
{
return is.state_based_acc;
}
void prop_state_based_acc(bool val = true)
{
is.state_based_acc = val;
}
bool is_sba() const
{
return has_state_based_acc() && has_single_acc_set();
}
bool is_inherently_weak() const
{
return is.inherently_weak;
}
void prop_inherently_weak(bool val = true)
{
is.inherently_weak = val;
}
bool is_deterministic() const
{
return is.deterministic;
}
void prop_deterministic(bool val = true)
{
is.deterministic = val;
}
// This is no default value here on purpose. This way any time we
// add a new property we cannot to update every call to prop_copy().
void prop_copy(const const_tgba_ptr& other,
bool state_based,
bool single_acc,
bool inherently_weak,
bool deterministic)
{
if (state_based)
prop_state_based_acc(other->has_state_based_acc());
if (single_acc)
prop_single_acc_set(other->has_single_acc_set());
if (inherently_weak)
prop_inherently_weak(other->is_inherently_weak());
if (deterministic)
prop_deterministic(other->is_deterministic());
}
}; };
/// \addtogroup tgba_representation TGBA representations /// \addtogroup tgba_representation TGBA representations
......
...@@ -39,10 +39,7 @@ namespace spot ...@@ -39,10 +39,7 @@ namespace spot
all_acceptance_conditions_ = all_acceptance_conditions_ =
compute_all_acceptance_conditions(neg_acceptance_conditions_); compute_all_acceptance_conditions(neg_acceptance_conditions_);
if (number_of_acceptance_conditions() == 1) prop_single_acc_set(number_of_acceptance_conditions() == 1);
set_bprop(tgba_digraph::SingleAccSet);
else
clear_bprop(tgba_digraph::SingleAccSet);
} }
bdd tgba_digraph::set_single_acceptance_set() bdd tgba_digraph::set_single_acceptance_set()
...@@ -50,7 +47,8 @@ namespace spot ...@@ -50,7 +47,8 @@ namespace spot
if (all_acceptance_conditions_ != bddfalse) if (all_acceptance_conditions_ != bddfalse)
dict_->unregister_all_typed_variables(bdd_dict::acc, this); dict_->unregister_all_typed_variables(bdd_dict::acc, this);
set_bprop(tgba_digraph::SingleAccSet); prop_single_acc_set();
int accvar = int accvar =
dict_->register_acceptance_variable(ltl::constant::true_instance(), dict_->register_acceptance_variable(ltl::constant::true_instance(),
this); this);
......
...@@ -390,34 +390,9 @@ namespace spot ...@@ -390,34 +390,9 @@ namespace spot
/// extremities and acceptance. /// extremities and acceptance.
void merge_transitions(); void merge_transitions();
protected:
unsigned bprops_ = 0;
public:
enum bprop {
StateBasedAcc = 1,
SingleAccSet = 2,
SBA = StateBasedAcc | SingleAccSet,
};
bool get_bprop(bprop p) const
{
return (bprops_ & p) == p;
}
void set_bprop(bprop p)
{
bprops_ |= p;
}
void clear_bprop(bprop p)
{
bprops_ &= ~p;
}
bool state_is_accepting(unsigned s) const bool state_is_accepting(unsigned s) const
{ {
assert(get_bprop(StateBasedAcc)); assert(has_state_based_acc());
for (auto& t: g_.out(s)) for (auto& t: g_.out(s))
// Stop at the first transition, since the remaining should be // Stop at the first transition, since the remaining should be
// labeled identically. // labeled identically.
......
...@@ -264,7 +264,9 @@ namespace spot ...@@ -264,7 +264,9 @@ namespace spot
res->copy_ap_of(a); res->copy_ap_of(a);
res->set_single_acceptance_set(); res->set_single_acceptance_set();
if (want_sba) if (want_sba)
res->set_bprop(tgba_digraph::StateBasedAcc); res->prop_state_based_acc();
// Preserve determinism and weakness
res->prop_copy(a, false, false, 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
...@@ -624,8 +626,8 @@ namespace spot ...@@ -624,8 +626,8 @@ namespace spot
{ {
// If this already a degeneralized digraph, there is nothing we // If this already a degeneralized digraph, there is nothing we
// can improve. // can improve.
if (auto d = std::dynamic_pointer_cast<const tgba_digraph>(a)) if (a->is_sba())
if (d->get_bprop(tgba_digraph::SBA)) if (auto d = std::dynamic_pointer_cast<const tgba_digraph>(a))
return std::const_pointer_cast<tgba_digraph>(d); return std::const_pointer_cast<tgba_digraph>(d);
return degeneralize_aux<true>(a, use_z_lvl, use_cust_acc_orders, return degeneralize_aux<true>(a, use_z_lvl, use_cust_acc_orders,
...@@ -639,8 +641,8 @@ namespace spot ...@@ -639,8 +641,8 @@ namespace spot
{ {
// If this already a degeneralized digraph, there is nothing we // If this already a degeneralized digraph, there is nothing we
// can improve. // can improve.
if (auto d = std::dynamic_pointer_cast<const tgba_digraph>(a)) if (a->has_single_acc_set())
if (d->get_bprop(tgba_digraph::SingleAccSet)) if (auto d = std::dynamic_pointer_cast<const tgba_digraph>(a))
return std::const_pointer_cast<tgba_digraph>(d); return std::const_pointer_cast<tgba_digraph>(d);
return degeneralize_aux<false>(a, use_z_lvl, use_cust_acc_orders, return degeneralize_aux<false>(a, use_z_lvl, use_cust_acc_orders,
......
...@@ -129,10 +129,7 @@ namespace spot ...@@ -129,10 +129,7 @@ namespace spot
{ {
if (!dd) if (!dd)
dd = dotty_decorator::instance(); dd = dotty_decorator::instance();
if (auto gd = dynamic_cast<const tgba_digraph*>(g.get())) dotty_bfs d(os, g, assume_sba || g->has_state_based_acc(), dd);
assume_sba |= gd->get_bprop(tgba_digraph::StateBasedAcc);
dotty_bfs d(os, g, assume_sba, dd);
d.run(); d.run();
return os; return os;
} }
......
...@@ -25,9 +25,10 @@ namespace spot ...@@ -25,9 +25,10 @@ namespace spot
{ {
namespace namespace
{ {
template<bool count>
static static
unsigned unsigned
count_nondet_states_aux(const const_tgba_ptr& aut, bool count = true) count_nondet_states_aux(const const_tgba_ptr& aut)
{ {
unsigned res = 0; unsigned res = 0;
typedef std::deque<const state*> todo_list; typedef std::deque<const state*> todo_list;
...@@ -82,13 +83,15 @@ namespace spot ...@@ -82,13 +83,15 @@ namespace spot
unsigned unsigned
count_nondet_states(const const_tgba_ptr& aut) count_nondet_states(const const_tgba_ptr& aut)
{ {
return count_nondet_states_aux(aut); return count_nondet_states_aux<true>(aut);
} }
bool bool
is_deterministic(const const_tgba_ptr& aut) is_deterministic(const const_tgba_ptr& aut)
{ {
return !count_nondet_states_aux(aut, false); if (aut->is_deterministic())
return true;
return !count_nondet_states_aux<false>(aut);
} }
bool bool
......
...@@ -79,13 +79,13 @@ namespace spot ...@@ -79,13 +79,13 @@ namespace spot
all_acc_conds_(a->all_acceptance_conditions()), all_acc_conds_(a->all_acceptance_conditions()),
acs_(all_acc_conds_), acs_(all_acc_conds_),
sba_format_(sba_format), sba_format_(sba_format),
// Check if the automaton can be converted into a sba_(nullptr)
// tgba_digraph. This makes the state_is_accepting()
// function more efficient.
sba_(std::dynamic_pointer_cast<const tgba_digraph>(a))
{ {
if (sba_ && !sba_->get_bprop(tgba_digraph::SBA)) // Check if the automaton can be converted into a
sba_ = nullptr; // tgba_digraph. This makes the state_is_accepting() function
// more efficient.
if (a->is_sba())
sba_ = std::dynamic_pointer_cast<const tgba_digraph>(a);
} }
bool bool
...@@ -243,7 +243,7 @@ namespace spot ...@@ -243,7 +243,7 @@ namespace spot
auto aut = make_tgba_digraph(dict); auto aut = make_tgba_digraph(dict);
acc_mapper_int acc_b(aut, num_acc, envacc); acc_mapper_int acc_b(aut, num_acc, envacc);
aut->new_states(num_states); aut->new_states(num_states);
aut->set_bprop(tgba_digraph::StateBasedAcc); aut->prop_state_based_acc();
for (unsigned n = 0; n < num_states; ++n) for (unsigned n = 0; n < num_states; ++n)
{ {
......
...@@ -122,7 +122,7 @@ namespace spot ...@@ -122,7 +122,7 @@ namespace spot
auto dict = a->get_dict(); auto dict = a->get_dict();
auto res = make_tgba_digraph(dict); auto res = make_tgba_digraph(dict);
res->copy_ap_of(a); res->copy_ap_of(a);
res->set_bprop(tgba_digraph::StateBasedAcc); res->prop_state_based_acc();
// For each set, create a state in the resulting automaton. // For each set, create a state in the resulting automaton.
// For a state s, state_num[s] is the number of the state in the minimal // For a state s, state_num[s] is the number of the state in the minimal
...@@ -499,8 +499,10 @@ namespace spot ...@@ -499,8 +499,10 @@ namespace spot
// non_final contain all states. // non_final contain all states.
// 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);
return minimize_dfa(det_a, final, non_final); res->prop_deterministic();
res->prop_inherently_weak();
return res;
} }
tgba_digraph_ptr minimize_wdba(const const_tgba_ptr& a) tgba_digraph_ptr minimize_wdba(const const_tgba_ptr& a)
...@@ -599,7 +601,10 @@ namespace spot ...@@ -599,7 +601,10 @@ namespace spot
} }
} }
return minimize_dfa(det_a, final, non_final); auto res = minimize_dfa(det_a, final, non_final);
res->prop_deterministic();
res->prop_inherently_weak();
return res;
} }
tgba_digraph_ptr tgba_digraph_ptr
...@@ -618,6 +623,11 @@ namespace spot ...@@ -618,6 +623,11 @@ namespace spot
return std::const_pointer_cast<tgba_digraph>(aut_f); return std::const_pointer_cast<tgba_digraph>(aut_f);
} }
// If the input automaton was already weak and deterministic, the
// output is necessary correct.
if (aut_f->is_inherently_weak() && aut_f->is_deterministic())
return min_aut_f;
// if f is a syntactic obligation formula, the WDBA minimization // if f is a syntactic obligation formula, the WDBA minimization
// must be correct. // must be correct.
if (f && f->is_syntactic_obligation()) if (f && f->is_syntactic_obligation())
......
...@@ -44,7 +44,7 @@ namespace spot ...@@ -44,7 +44,7 @@ namespace spot
comments_(comments), all_acc_conds_(a->all_acceptance_conditions()), comments_(comments), all_acc_conds_(a->all_acceptance_conditions()),
sba_(std::dynamic_pointer_cast<const tgba_digraph>(a)) sba_(std::dynamic_pointer_cast<const tgba_digraph>(a))
{ {
assert(!sba_ || sba_->get_bprop(tgba_digraph::StateBasedAcc)); assert(!sba_ || sba_->has_state_based_acc());
} }
void void
......
...@@ -195,10 +195,11 @@ namespace spot ...@@ -195,10 +195,11 @@ namespace spot
{ {
bool reject_bigger = (PREF_ == Small) && (level_ == Medium); bool reject_bigger = (PREF_ == Small) && (level_ == Medium);
dba = minimize_obligation(a, f, 0, reject_bigger); dba = minimize_obligation(a, f, 0, reject_bigger);
if (dba == a || !dba) // Minimization failed. if (dba && dba->is_inherently_weak() && dba->is_deterministic())
dba = nullptr;
else
dba_is_minimal = dba_is_wdba = true; dba_is_minimal = dba_is_wdba = true;
else
// Minimization failed.
dba = nullptr;
// The WDBA is a BA, so no degeneralization is required. // The WDBA is a BA, so no degeneralization is required.
} }
......
...@@ -498,10 +498,8 @@ namespace spot ...@@ -498,10 +498,8 @@ namespace spot
tgba_digraph_ptr tgba_digraph_ptr
scc_filter_states(const const_tgba_digraph_ptr& aut, scc_info* given_si) scc_filter_states(const const_tgba_digraph_ptr& aut, scc_info* given_si)
{ {
bool sb = aut->get_bprop(tgba_digraph::StateBasedAcc);
auto res = scc_filter_apply<state_filter<>>(aut, given_si); auto res = scc_filter_apply<state_filter<>>(aut, given_si);
if (sb) res->prop_copy(aut, true, true, true, true);
res->set_bprop(tgba_digraph::StateBasedAcc);
return res; return res;
} }
...@@ -519,6 +517,11 @@ namespace spot ...@@ -519,6 +517,11 @@ namespace spot
<acc_filter_some <acc_filter_some
<acc_filter_simplify<>>>>(aut, given_si); <acc_filter_simplify<>>>>(aut, given_si);
res->merge_transitions(); res->merge_transitions();
res->prop_copy(aut,
false, // state-based acceptance is not preserved
true,
true,
true);
return res; return res;
} }
...@@ -545,6 +548,11 @@ namespace spot ...@@ -545,6 +548,11 @@ namespace spot
ignoredvars, ignoredvars,
early_susp); early_susp);
res->merge_transitions(); res->merge_transitions();
res->prop_copy(aut,
false, // state-based acceptance is not preserved
true,
true,
false); // determinism may not be preserved
return res; return res;
} }
......
...@@ -526,15 +526,6 @@ namespace spot ...@@ -526,15 +526,6 @@ namespace spot
} }
} }
bool result_is_deterministic() const
{
assert(stat.states != 0);
return res_is_deterministic;
}
// Build the minimal resulting automaton. // Build the minimal resulting automaton.
tgba_digraph_ptr build_result() tgba_digraph_ptr build_result()
{ {
...@@ -550,7 +541,7 @@ namespace spot ...@@ -550,7 +541,7 @@ namespace spot
res->copy_ap_of(a_); res->copy_ap_of(a_);
res->set_acceptance_conditions(all_acceptance_conditions_); res->set_acceptance_conditions(all_acceptance_conditions_);
if (Sba) if (Sba)
res->set_bprop(tgba_digraph::StateBasedAcc); res->prop_state_based_acc();
bdd sup_all_acc = bdd_support(all_acceptance_conditions_); bdd sup_all_acc = bdd_support(all_acceptance_conditions_);
// Non atomic propositions variables (= acc and class) // Non atomic propositions variables (= acc and class)
...@@ -691,7 +682,15 @@ namespace spot ...@@ -691,7 +682,15 @@ namespace spot
} }
delete gb; delete gb;
res_is_deterministic = nb_minato == nb_satoneset; res->prop_copy(original_,
false, // state-based acc forced below
false, // single acc is set by set_acceptance_conditions
true, // weakness preserved,
false); // determinism checked and set below
if (nb_minato == nb_satoneset)
res->prop_deterministic();
if (Sba)
res->prop_state_based_acc();
return res; return res;
} }
...@@ -779,8 +778,6 @@ namespace spot ...@@ -779,8 +778,6 @@ namespace spot
const_tgba_ptr original_; const_tgba_ptr original_;
bdd all_acceptance_conditions_; bdd all_acceptance_conditions_;
bool res_is_deterministic;
}; };
// For now, we don't try to handle cosimulation.