twa: no default argument for property setters
This is a preliminary for the renaming suggested in #116. * src/twa/twa.hh (prop_state_based_acc, prop_inherently_weak, prop_deterministic, prop_unambiguous, prop_stutter_invariant, prop_stutter_sensitive): Do not default the argument to true. * src/parseaut/parseaut.yy, src/twaalgos/degen.cc, src/twaalgos/dtbasat.cc, src/twaalgos/dtgbasat.cc, src/twaalgos/minimize.cc, src/twaalgos/randomgraph.cc, src/twaalgos/remfin.cc, src/twaalgos/sbacc.cc, src/twaalgos/simulation.cc, src/twaalgos/totgba.cc, wrap/python/tests/remfin.py: Adjust.
This commit is contained in:
parent
bf5749189e
commit
8ea5f73c1a
12 changed files with 38 additions and 38 deletions
|
|
@ -1158,8 +1158,8 @@ dstar_header: dstar_sizes
|
||||||
res.h->aut->new_states(res.states);;
|
res.h->aut->new_states(res.states);;
|
||||||
res.info_states.resize(res.states);
|
res.info_states.resize(res.states);
|
||||||
}
|
}
|
||||||
res.h->aut->prop_state_based_acc();
|
res.h->aut->prop_state_based_acc(true);
|
||||||
res.h->aut->prop_deterministic();
|
res.h->aut->prop_deterministic(true);
|
||||||
// res.h->aut->prop_complete();
|
// res.h->aut->prop_complete();
|
||||||
fill_guards(res);
|
fill_guards(res);
|
||||||
res.cur_guard = res.guards.end();
|
res.cur_guard = res.guards.end();
|
||||||
|
|
@ -1303,7 +1303,7 @@ dstar_states:
|
||||||
|
|
||||||
never: "never" { res.namer = res.h->aut->create_namer<std::string>();
|
never: "never" { res.namer = res.h->aut->create_namer<std::string>();
|
||||||
res.h->aut->set_buchi();
|
res.h->aut->set_buchi();
|
||||||
res.h->aut->prop_state_based_acc();
|
res.h->aut->prop_state_based_acc(true);
|
||||||
res.acc_state = State_Acc;
|
res.acc_state = State_Acc;
|
||||||
res.pos_acc_sets = res.h->aut->acc().all_sets();
|
res.pos_acc_sets = res.h->aut->acc().all_sets();
|
||||||
}
|
}
|
||||||
|
|
@ -1560,7 +1560,7 @@ lbtt-header-states: LBTT
|
||||||
lbtt-header: lbtt-header-states INT_S
|
lbtt-header: lbtt-header-states INT_S
|
||||||
{
|
{
|
||||||
res.acc_mapper = new spot::acc_mapper_int(res.h->aut, $2);
|
res.acc_mapper = new spot::acc_mapper_int(res.h->aut, $2);
|
||||||
res.h->aut->prop_state_based_acc();
|
res.h->aut->prop_state_based_acc(true);
|
||||||
res.acc_state = State_Acc;
|
res.acc_state = State_Acc;
|
||||||
}
|
}
|
||||||
| lbtt-header-states INT
|
| lbtt-header-states INT
|
||||||
|
|
@ -1869,7 +1869,7 @@ static void fix_properties(result_& r)
|
||||||
//r.h->aut->prop_complete(r.complete);
|
//r.h->aut->prop_complete(r.complete);
|
||||||
if (r.acc_style == State_Acc ||
|
if (r.acc_style == State_Acc ||
|
||||||
(r.acc_style == Mixed_Acc && !r.trans_acc_seen))
|
(r.acc_style == Mixed_Acc && !r.trans_acc_seen))
|
||||||
r.h->aut->prop_state_based_acc();
|
r.h->aut->prop_state_based_acc(true);
|
||||||
}
|
}
|
||||||
|
|
||||||
static void check_version(const result_& r)
|
static void check_version(const result_& r)
|
||||||
|
|
|
||||||
|
|
@ -706,7 +706,7 @@ namespace spot
|
||||||
set_num_sets_(num);
|
set_num_sets_(num);
|
||||||
acc_.set_acceptance(c);
|
acc_.set_acceptance(c);
|
||||||
if (num == 0)
|
if (num == 0)
|
||||||
prop_state_based_acc();
|
prop_state_based_acc(true);
|
||||||
}
|
}
|
||||||
|
|
||||||
/// \brief Copy the acceptance condition of another tgba.
|
/// \brief Copy the acceptance condition of another tgba.
|
||||||
|
|
@ -715,7 +715,7 @@ namespace spot
|
||||||
acc_ = a->acc();
|
acc_ = a->acc();
|
||||||
unsigned num = acc_.num_sets();
|
unsigned num = acc_.num_sets();
|
||||||
if (num == 0)
|
if (num == 0)
|
||||||
prop_state_based_acc();
|
prop_state_based_acc(true);
|
||||||
}
|
}
|
||||||
|
|
||||||
void copy_ap_of(const const_twa_ptr& a)
|
void copy_ap_of(const const_twa_ptr& a)
|
||||||
|
|
@ -730,7 +730,7 @@ namespace spot
|
||||||
set_num_sets_(num);
|
set_num_sets_(num);
|
||||||
acc_.set_generalized_buchi();
|
acc_.set_generalized_buchi();
|
||||||
if (num == 0)
|
if (num == 0)
|
||||||
prop_state_based_acc();
|
prop_state_based_acc(true);
|
||||||
}
|
}
|
||||||
|
|
||||||
acc_cond::mark_t set_buchi()
|
acc_cond::mark_t set_buchi()
|
||||||
|
|
@ -810,7 +810,7 @@ namespace spot
|
||||||
return is.state_based_acc;
|
return is.state_based_acc;
|
||||||
}
|
}
|
||||||
|
|
||||||
void prop_state_based_acc(bool val = true)
|
void prop_state_based_acc(bool val)
|
||||||
{
|
{
|
||||||
is.state_based_acc = val;
|
is.state_based_acc = val;
|
||||||
}
|
}
|
||||||
|
|
@ -825,7 +825,7 @@ namespace spot
|
||||||
return is.inherently_weak;
|
return is.inherently_weak;
|
||||||
}
|
}
|
||||||
|
|
||||||
void prop_inherently_weak(bool val = true)
|
void prop_inherently_weak(bool val)
|
||||||
{
|
{
|
||||||
is.inherently_weak = val;
|
is.inherently_weak = val;
|
||||||
}
|
}
|
||||||
|
|
@ -835,7 +835,7 @@ namespace spot
|
||||||
return is.deterministic;
|
return is.deterministic;
|
||||||
}
|
}
|
||||||
|
|
||||||
void prop_deterministic(bool val = true)
|
void prop_deterministic(bool val)
|
||||||
{
|
{
|
||||||
is.deterministic = val;
|
is.deterministic = val;
|
||||||
}
|
}
|
||||||
|
|
@ -845,7 +845,7 @@ namespace spot
|
||||||
return is.unambiguous;
|
return is.unambiguous;
|
||||||
}
|
}
|
||||||
|
|
||||||
void prop_unambiguous(bool val = true)
|
void prop_unambiguous(bool val)
|
||||||
{
|
{
|
||||||
is.unambiguous = val;
|
is.unambiguous = val;
|
||||||
}
|
}
|
||||||
|
|
@ -860,12 +860,12 @@ namespace spot
|
||||||
return is.stutter_sensitive;
|
return is.stutter_sensitive;
|
||||||
}
|
}
|
||||||
|
|
||||||
void prop_stutter_invariant(bool val = true)
|
void prop_stutter_invariant(bool val)
|
||||||
{
|
{
|
||||||
is.stutter_invariant = val;
|
is.stutter_invariant = val;
|
||||||
}
|
}
|
||||||
|
|
||||||
void prop_stutter_sensitive(bool val = true)
|
void prop_stutter_sensitive(bool val)
|
||||||
{
|
{
|
||||||
is.stutter_sensitive = val;
|
is.stutter_sensitive = val;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -207,7 +207,7 @@ namespace spot
|
||||||
res->copy_ap_of(a);
|
res->copy_ap_of(a);
|
||||||
res->set_buchi();
|
res->set_buchi();
|
||||||
if (want_sba)
|
if (want_sba)
|
||||||
res->prop_state_based_acc();
|
res->prop_state_based_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 });
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -640,8 +640,8 @@ namespace spot
|
||||||
a->copy_ap_of(aut);
|
a->copy_ap_of(aut);
|
||||||
acc_cond::mark_t acc = a->set_buchi();
|
acc_cond::mark_t acc = a->set_buchi();
|
||||||
if (state_based)
|
if (state_based)
|
||||||
a->prop_state_based_acc();
|
a->prop_state_based_acc(true);
|
||||||
a->prop_deterministic();
|
a->prop_deterministic(true);
|
||||||
a->new_states(satdict.cand_size);
|
a->new_states(satdict.cand_size);
|
||||||
|
|
||||||
unsigned last_aut_trans = -1U;
|
unsigned last_aut_trans = -1U;
|
||||||
|
|
|
||||||
|
|
@ -1026,8 +1026,8 @@ namespace spot
|
||||||
auto a = make_twa_graph(autdict);
|
auto a = make_twa_graph(autdict);
|
||||||
a->copy_ap_of(aut);
|
a->copy_ap_of(aut);
|
||||||
if (state_based)
|
if (state_based)
|
||||||
a->prop_state_based_acc();
|
a->prop_state_based_acc(true);
|
||||||
a->prop_deterministic();
|
a->prop_deterministic(true);
|
||||||
a->set_acceptance(satdict.cand_nacc, satdict.cand_acc);
|
a->set_acceptance(satdict.cand_nacc, satdict.cand_acc);
|
||||||
a->new_states(satdict.cand_size);
|
a->new_states(satdict.cand_size);
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -122,7 +122,7 @@ namespace spot
|
||||||
auto dict = a->get_dict();
|
auto dict = a->get_dict();
|
||||||
auto res = make_twa_graph(dict);
|
auto res = make_twa_graph(dict);
|
||||||
res->copy_ap_of(a);
|
res->copy_ap_of(a);
|
||||||
res->prop_state_based_acc();
|
res->prop_state_based_acc(true);
|
||||||
|
|
||||||
// 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
|
||||||
|
|
@ -481,9 +481,9 @@ namespace spot
|
||||||
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, true });
|
||||||
res->prop_deterministic();
|
res->prop_deterministic(true);
|
||||||
res->prop_inherently_weak();
|
res->prop_inherently_weak(true);
|
||||||
res->prop_state_based_acc();
|
res->prop_state_based_acc(true);
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -582,8 +582,8 @@ 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, true });
|
||||||
res->prop_deterministic();
|
res->prop_deterministic(true);
|
||||||
res->prop_inherently_weak();
|
res->prop_inherently_weak(true);
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -130,9 +130,9 @@ namespace spot
|
||||||
throw std::invalid_argument("random_graph() requires n>0 states");
|
throw std::invalid_argument("random_graph() requires n>0 states");
|
||||||
auto res = make_twa_graph(dict);
|
auto res = make_twa_graph(dict);
|
||||||
if (deterministic)
|
if (deterministic)
|
||||||
res->prop_deterministic();
|
res->prop_deterministic(true);
|
||||||
if (state_acc)
|
if (state_acc)
|
||||||
res->prop_state_based_acc();
|
res->prop_state_based_acc(true);
|
||||||
|
|
||||||
int props_n = ap->size();
|
int props_n = ap->size();
|
||||||
int* props = new int[props_n];
|
int* props = new int[props_n];
|
||||||
|
|
|
||||||
|
|
@ -468,8 +468,8 @@ namespace spot
|
||||||
// We will modify res in place, and the resulting
|
// We will modify res in place, and the resulting
|
||||||
// automaton will only have one acceptance set.
|
// automaton will only have one acceptance set.
|
||||||
acc_cond::mark_t all_acc = res->set_buchi();
|
acc_cond::mark_t all_acc = res->set_buchi();
|
||||||
res->prop_state_based_acc();
|
res->prop_state_based_acc(true);
|
||||||
res->prop_deterministic();
|
res->prop_deterministic(true);
|
||||||
|
|
||||||
unsigned sink = res->num_states();
|
unsigned sink = res->num_states();
|
||||||
for (unsigned src = 0; src < sink; ++src)
|
for (unsigned src = 0; src < sink; ++src)
|
||||||
|
|
@ -746,7 +746,7 @@ namespace spot
|
||||||
|
|
||||||
// If the input had no Inf, the output is a state-based automaton.
|
// If the input had no Inf, the output is a state-based automaton.
|
||||||
if (allinf == 0U)
|
if (allinf == 0U)
|
||||||
res->prop_state_based_acc();
|
res->prop_state_based_acc(true);
|
||||||
|
|
||||||
res->purge_dead_states();
|
res->purge_dead_states();
|
||||||
trace << "before cleanup: " << res->get_acceptance() << '\n';
|
trace << "before cleanup: " << res->get_acceptance() << '\n';
|
||||||
|
|
|
||||||
|
|
@ -33,7 +33,7 @@ namespace spot
|
||||||
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});
|
||||||
res->prop_state_based_acc();
|
res->prop_state_based_acc(true);
|
||||||
|
|
||||||
typedef std::pair<unsigned, acc_cond::mark_t> pair_t;
|
typedef std::pair<unsigned, acc_cond::mark_t> pair_t;
|
||||||
std::map<pair_t, unsigned> s2n;
|
std::map<pair_t, unsigned> s2n;
|
||||||
|
|
|
||||||
|
|
@ -640,9 +640,9 @@ namespace spot
|
||||||
true, // stutter inv.
|
true, // stutter inv.
|
||||||
});
|
});
|
||||||
if (nb_minato == nb_satoneset && !Cosimulation)
|
if (nb_minato == nb_satoneset && !Cosimulation)
|
||||||
res->prop_deterministic();
|
res->prop_deterministic(true);
|
||||||
if (Sba)
|
if (Sba)
|
||||||
res->prop_state_based_acc();
|
res->prop_state_based_acc(true);
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -334,10 +334,10 @@ namespace spot
|
||||||
assert(cnf.front().mark == 0U);
|
assert(cnf.front().mark == 0U);
|
||||||
res = make_twa_graph(aut->get_dict());
|
res = make_twa_graph(aut->get_dict());
|
||||||
res->set_init_state(res->new_state());
|
res->set_init_state(res->new_state());
|
||||||
res->prop_state_based_acc();
|
res->prop_state_based_acc(true);
|
||||||
res->prop_inherently_weak();
|
res->prop_inherently_weak(true);
|
||||||
res->prop_deterministic();
|
res->prop_deterministic(true);
|
||||||
res->prop_stutter_invariant();
|
res->prop_stutter_invariant(true);
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -18,7 +18,7 @@ State: 2
|
||||||
[t] 2
|
[t] 2
|
||||||
--END--
|
--END--
|
||||||
""")
|
""")
|
||||||
aut.prop_inherently_weak()
|
aut.prop_inherently_weak(True)
|
||||||
aut = spot.dtwa_complement(aut)
|
aut = spot.dtwa_complement(aut)
|
||||||
aut1 = spot.scc_filter_states(aut)
|
aut1 = spot.scc_filter_states(aut)
|
||||||
assert(aut1.to_str('hoa') == """HOA: v1
|
assert(aut1.to_str('hoa') == """HOA: v1
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue