spot/twa: Add methods to set co-Büchi acceptance
* spot/twa/acc.hh: Add set_generalized_co_buchi() method. * spot/twa/twa.hh: Add set_generalized_co_buchi() and set_co_buchi() wrappers.
This commit is contained in:
parent
75d9e5f624
commit
0957317ad7
2 changed files with 44 additions and 0 deletions
|
|
@ -1027,6 +1027,11 @@ namespace spot
|
||||||
set_acceptance(inf(all_sets()));
|
set_acceptance(inf(all_sets()));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void set_generalized_co_buchi()
|
||||||
|
{
|
||||||
|
set_acceptance(fin(all_sets()));
|
||||||
|
}
|
||||||
|
|
||||||
bool is_generalized_buchi() const
|
bool is_generalized_buchi() const
|
||||||
{
|
{
|
||||||
unsigned s = code_.size();
|
unsigned s = code_.size();
|
||||||
|
|
|
||||||
|
|
@ -963,6 +963,24 @@ namespace spot
|
||||||
acc_.set_generalized_buchi();
|
acc_.set_generalized_buchi();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// \brief Set generalized co-Büchi acceptance
|
||||||
|
///
|
||||||
|
/// \param num the number of acceptance sets to use
|
||||||
|
///
|
||||||
|
/// The acceptance formula of the form
|
||||||
|
/// \code
|
||||||
|
/// Fin(0)&Fin(1)&...&Fin(num-1)
|
||||||
|
/// \endcode
|
||||||
|
/// is generated.
|
||||||
|
///
|
||||||
|
/// In the case where \a num is null, the state-acceptance
|
||||||
|
/// property is automatically turned on.
|
||||||
|
void set_generalized_co_buchi(unsigned num)
|
||||||
|
{
|
||||||
|
set_num_sets_(num);
|
||||||
|
acc_.set_generalized_co_buchi();
|
||||||
|
}
|
||||||
|
|
||||||
/// \brief Set Büchi acceptance.
|
/// \brief Set Büchi acceptance.
|
||||||
///
|
///
|
||||||
/// This declares a single acceptance set, and \c Inf(0)
|
/// This declares a single acceptance set, and \c Inf(0)
|
||||||
|
|
@ -984,6 +1002,27 @@ namespace spot
|
||||||
return acc_.mark(0);
|
return acc_.mark(0);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// \brief Set co-Büchi acceptance.
|
||||||
|
///
|
||||||
|
/// This declares a single acceptance set, and \c Fin(0)
|
||||||
|
/// acceptance. The returned mark \c {0} can be used to tag
|
||||||
|
/// non-accepting transition.
|
||||||
|
///
|
||||||
|
/// Note that this does not mark the automaton as using
|
||||||
|
/// state-based acceptance. If you want to create a co-Büchi
|
||||||
|
/// automaton with state-based acceptance, call
|
||||||
|
/// \code
|
||||||
|
/// prop_state_acc(true)
|
||||||
|
/// \endcode
|
||||||
|
/// in addition.
|
||||||
|
///
|
||||||
|
/// \see prop_state_acc
|
||||||
|
acc_cond::mark_t set_co_buchi()
|
||||||
|
{
|
||||||
|
set_generalized_co_buchi(1);
|
||||||
|
return acc_.mark(0);
|
||||||
|
}
|
||||||
|
|
||||||
private:
|
private:
|
||||||
std::vector<formula> aps_;
|
std::vector<formula> aps_;
|
||||||
bdd bddaps_;
|
bdd bddaps_;
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue