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

* spot/twa/acc.hh: More documentation.

parent c20f49ae
Pipeline #5056 failed with stages
in 101 minutes and 24 seconds
......@@ -44,16 +44,42 @@ namespace spot
};
}
/// \ingroup twa_essentials
/// @{
/// \brief An acceptance condition
///
/// This represent an acceptance condition in the HOA sense, that
/// is, an acceptance formula plus a number of acceptance sets. The
/// acceptance formula is expected to use a subset of the acceptance
/// sets. (It usually uses *all* sets, otherwise that means that
/// some of the sets have no influence on the automaton language and
/// could be removed.)
class SPOT_API acc_cond
{
#ifndef SWIG
private:
[[noreturn]] static void report_too_many_sets();
[[noreturn]] static void report_too_many_sets();
#endif
public:
/// \brief An acceptance mark
///
/// This type is used to represent a set of acceptance sets. It
/// works (and is implemented) like a bit vector where bit at
/// index i represents the membership to the i-th acceptance set.
///
/// Typically, each transition of an automaton is labeled by a
/// mark_t that represents the membership of the transition to
/// each of the acceptance sets.
///
/// For efficiency reason, the maximum number of acceptance sets
/// (i.e., the size of the bit vector) supported is a compile-time
/// constant. It can be changed by passing an option to the
/// configure script of Spot.
struct mark_t :
public internal::_32acc<SPOT_MAX_ACCSETS == 8*sizeof(unsigned)>
public internal::_32acc<SPOT_MAX_ACCSETS == 8*sizeof(unsigned)>
{
private:
// configure guarantees that SPOT_MAX_ACCSETS % (8*sizeof(unsigned)) == 0
......@@ -66,9 +92,11 @@ namespace spot
}
public:
/// Initialize an empty mark_t.
mark_t() = default;
#ifndef SWIG
/// Create a mark_t from a range of set numbers.
template<class iterator>
mark_t(const iterator& begin, const iterator& end)
: mark_t(_value_t::zero())
......@@ -77,6 +105,7 @@ namespace spot
set(*i);
}
/// Create a mark_t from a list of set numbers.
mark_t(std::initializer_list<unsigned> vals)
: mark_t(vals.begin(), vals.end())
{
......@@ -106,6 +135,11 @@ namespace spot
return SPOT_MAX_ACCSETS;
}
/// \brief A mark_t with all bits set to one.
///
/// Beware that *all* bits are sets, not just the bits used in
/// the acceptance condition. This class is unaware of the
/// acceptance condition.
static mark_t all()
{
return mark_t(_value_t::mone());
......@@ -289,25 +323,30 @@ namespace spot
return xv;
}
/// \brief Whether the set of bits represented by *this is a
/// subset of those represented by \a m.
bool subset(mark_t m) const
{
return !((*this) - m);
}
/// \brief Whether the set of bits represented by *this is a
/// proper subset of those represented by \a m.
bool proper_subset(mark_t m) const
{
return *this != m && this->subset(m);
}
// Number of bits sets.
/// \brief Number of bits sets.
unsigned count() const
{
return id.count();
}
// Return the number of the highest set used plus one.
// If no set is used, this returns 0,
// If the sets {1,3,8} are used, this returns 9.
/// \brief The number of the highest set used plus one.
///
/// If no set is used, this returns 0,
/// If the sets {1,3,8} are used, this returns 9.
unsigned max_set() const
{
if (id)
......@@ -316,9 +355,10 @@ namespace spot
return 0;
}
// Return the number of the lowest set used plus one.
// If no set is used, this returns 0.
// If the sets {1,3,8} are used, this returns 2.
/// \brief The number of the lowest set used plus one.
///
/// If no set is used, this returns 0.
/// If the sets {1,3,8} are used, this returns 2.
unsigned min_set() const
{
if (id)
......@@ -327,13 +367,18 @@ namespace spot
return 0;
}
// Return the lowest acceptance mark
/// \brief A mark_t where all bits have been removed except the
/// lowest one.
///
/// For instance if this contains {1,3,8}, the output is {1}.
mark_t lowest() const
{
return id & -id;
}
// Remove n bits that where set
/// \brief Remove n bits that where set.
///
/// If there are less than n bits set, the output is empty.
mark_t& remove_some(unsigned n)
{
while (n--)
......@@ -341,6 +386,7 @@ namespace spot
return *this;
}
/// \brief Fill a container with the indices of the bits that are set.
template<class iterator>
void fill(iterator here) const
{
......@@ -355,16 +401,24 @@ namespace spot
}
}
// Returns some iterable object that contains the used sets.
/// Returns some iterable object that contains the used sets.
spot::internal::mark_container sets() const;
SPOT_API
friend std::ostream& operator<<(std::ostream& os, mark_t m);
};
// This encodes either an operator or set of acceptance sets.
/// \brief Operators for acceptance formulas.
enum class acc_op : unsigned short
{ Inf, Fin, InfNeg, FinNeg, And, Or };
/// \brief A "node" in an acceptance formulas.
///
/// Acceptance formulas are stored as a vector of acc_word in a
/// kind of reverse polish notation. Each acc_word is either an
/// operator, or a set of acceptance sets. Operators come with a
/// size that represent the number of words in the subtree,
/// current operator excluded.
union acc_word
{
mark_t mark;
......@@ -375,6 +429,18 @@ namespace spot
} sub;
};
/// \brief An acceptance formulas.
///
/// Acceptance formulas are stored as a vector of acc_word in a
/// kind of reverse polish notation. The motivation for this
/// design was that we could evaluate the acceptance condition
/// using a very simple stack-based interpreter; however it turned
/// out that such a stack-based interpretation would prevent us
/// from doing short-circuit evaluation, so we are not evaluating
/// acceptance conditions this way, and maybe the implementation
/// of acc_code could change in the future. It's best not to rely
/// on the fact that formulas are stored as vectors. Use the
/// provided methods instead.
struct SPOT_API acc_code: public std::vector<acc_word>
{
bool operator==(const acc_code& other) const
......@@ -475,20 +541,38 @@ namespace spot
return !(*this == other);
}
/// \brief Is this the "true" acceptance condition?
///
/// This corresponds to "t" in the HOA format. Under this
/// acceptance condition, all runs are accepting.
bool is_t() const
{
// We store "t" as an empty condition, or as Inf({}).
unsigned s = size();
return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
&& !((*this)[s - 2].mark));
}
/// \brief Is this the "false" acceptance condition?
///
/// This corresponds to "f" in the HOA format. Under this
/// acceptance condition, no runs is accepting. Obviously, this
/// has very few practical application, except as neutral
/// element in some construction.
bool is_f() const
{
// We store "f" as Fin({}).
unsigned s = size();
return s > 1
&& (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
}
/// \brief Construct the "false" acceptance condition.
///
/// This corresponds to "f" in the HOA format. Under this
/// acceptance condition, no runs is accepting. Obviously, this
/// has very few practical application, except as neutral
/// element in some construction.
static acc_code f()
{
acc_code res;
......@@ -499,11 +583,22 @@ namespace spot
return res;
}
/// \brief Construct the "true" acceptance condition.
///
/// This corresponds to "t" in the HOA format. Under this
/// acceptance condition, all runs are accepting.
static acc_code t()
{
return {};
}
/// \brief Construct a generalized co-Büchi acceptance
///
/// For the input m={1,8,9}, this constructs Fin(1)|Fin(8)|Fin(9).
///
/// Internally, such a formula is stored using a single word
/// Fin({1,8,9}).
/// @{
static acc_code fin(mark_t m)
{
acc_code res;
......@@ -518,7 +613,24 @@ namespace spot
{
return fin(mark_t(vals));
}
/// @}
/// \brief Construct a generalized co-Büchi acceptance for
/// complemented sets.
///
/// For the input `m={1,8,9}`, this constructs
/// `Fin(!1)|Fin(!8)|Fin(!9)`.
///
/// Internally, such a formula is stored using a single word
/// `FinNeg({1,8,9})`.
///
/// Note that `FinNeg` formulas are not supported by most methods
/// of this class, and not supported by algorithms in Spot.
/// This is mostly used in the parser for HOA files: if the
/// input file uses `Fin(!0)` as acceptance condition, the
/// condition will eventually be rewritten as `Fin(0)` by toggling
/// the membership to set 0 of each transition.
/// @{
static acc_code fin_neg(mark_t m)
{
acc_code res;
......@@ -533,7 +645,16 @@ namespace spot
{
return fin_neg(mark_t(vals));
}
/// @}
/// \brief Construct a generalized Büchi acceptance
///
/// For the input `m={1,8,9}`, this constructs
/// `Inf(1)&Inf(8)&Inf(9)`.
///
/// Internally, such a formula is stored using a single word
/// `Inf({1,8,9})`.
/// @{
static acc_code inf(mark_t m)
{
acc_code res;
......@@ -548,7 +669,24 @@ namespace spot
{
return inf(mark_t(vals));
}
/// @}
/// \brief Construct a generalized Büchi acceptance for
/// complemented sets.
///
/// For the input `m={1,8,9}`, this constructs
/// `Inf(!1)&Inf(!8)&Inf(!9)`.
///
/// Internally, such a formula is stored using a single word
/// `InfNeg({1,8,9})`.
///
/// Note that `InfNeg` formulas are not supported by most methods
/// of this class, and not supported by algorithms in Spot.
/// This is mostly used in the parser for HOA files: if the
/// input file uses `Inf(!0)` as acceptance condition, the
/// condition will eventually be rewritten as `Inf(0)` by toggling
/// the membership to set 0 of each transition.
/// @{
static acc_code inf_neg(mark_t m)
{
acc_code res;
......@@ -563,17 +701,29 @@ namespace spot
{
return inf_neg(mark_t(vals));
}
/// @}
/// \brief Build a Büchi acceptance condition.
///
/// This builds the formula `Inf(0)`.
static acc_code buchi()
{
return inf({0});
}
/// \brief Build a co-Büchi acceptance condition.
///
/// This builds the formula `Fin(0)`.
static acc_code cobuchi()
{
return fin({0});
}
/// \brief Build a generalized-Büchi acceptance condition with n sets
///
/// This builds the formula `Inf(0)&Inf(1)&...&Inf(n-1)`.
///
/// When n is zero, the acceptance condition reduces to true.
static acc_code generalized_buchi(unsigned n)
{
if (n == 0)
......@@ -583,6 +733,11 @@ namespace spot
return inf(m);
}
/// \brief Build a generalized-co-Büchi acceptance condition with n sets
///
/// This builds the formula `Fin(0)|Fin(1)|...|Fin(n-1)`.
///
/// When n is zero, the acceptance condition reduces to false.
static acc_code generalized_co_buchi(unsigned n)
{
if (n == 0)
......@@ -592,7 +747,10 @@ namespace spot
return fin(m);
}
// n is a number of pairs.
/// \brief Build a Rabin condition with n pairs.
///
/// This builds the formula
/// `(Fin(0)&Inf(1))|(Fin(2)&Inf(3))|...|(Fin(2n-2)&Inf(2n-1))`
static acc_code rabin(unsigned n)
{
acc_cond::acc_code res = f();
......@@ -604,7 +762,10 @@ namespace spot
return res;
}
// n is a number of pairs.
/// \brief Build a Streett condition with n pairs.
///
/// This builds the formula
/// `(Fin(0)|Inf(1))&(Fin(2)|Inf(3))&...&(Fin(2n-2)|Inf(2n-1))`
static acc_code streett(unsigned n)
{
acc_cond::acc_code res = t();
......@@ -616,6 +777,18 @@ namespace spot
return res;
}
/// \brief Build a generalized Rabin condition.
///
/// The two iterators should point to a range of integers, each
/// integer being the number of Inf term in a generalized Rabin pair.
///
/// For instance if the input is `[2,3,0]`, the output
/// will have three clauses (=generalized pairs), with 2 Inf terms in
/// the first clause, 3 in the second, and 0 in the last:
/// `(Fin(0)&Inf(1)&Inf(2))|Fin(3)&Inf(4)&Inf(5)&Inf(6)|Fin(7)`.
///
/// Since set numbers are not reused, the number of sets used is
/// the sum of all input integers plus their count.
template<class Iterator>
static acc_code generalized_rabin(Iterator begin, Iterator end)
{
......@@ -634,13 +807,33 @@ namespace spot
return res;
}
/// \brief Build a parity acceptance condition
///
/// In parity acceptance a word is accepting if the maximum (or
/// minimum) set number that is seen infinitely often is odd (or
/// even). This function will build a formula for that, as
/// specified in the HOA format.
static acc_code parity(bool max, bool odd, unsigned sets);
// Number of acceptance sets to use, and probability to reuse
// each set another time after it has been used in the
// acceptance formula.
/// \brief Build a random acceptance condition
///
/// If \a n is 0, this will always generate the true acceptance,
/// because working with false acceptance is somehow pointless.
///
/// For \a n>0, we randomly create a term Fin(i) or Inf(i) for
/// each set 0≤i<n. If \a reuse>0.0, it gives the probability
/// that a set i can generate more than one Fin(i)/Inf(i) term.
/// Set i will be reused as long as our [0,1) random number
/// generator gives a value ≤reuse. (Do not set reuse≥1.0 as
/// that will give an infinite loop.)
///
/// All these Fin/Inf terms are the leaves of the tree we are
/// building. That tree is then build by picking two random
/// subtrees, and joining them with & and | randomly, until we
/// are left with a single tree.
static acc_code random(unsigned n, double reuse = 0.0);
/// \brief Conjunct the current condition in place with \a r.
acc_code& operator&=(const acc_code& r)
{
if (is_t() || r.is_f())
......@@ -729,6 +922,7 @@ namespace spot
return *this;
}
/// \brief Conjunct the current condition with \a r.
acc_code operator&(const acc_code& r) const
{
acc_code res = *this;
......@@ -736,6 +930,7 @@ namespace spot
return res;
}
/// \brief Conjunct the current condition with \a r.
acc_code operator&(acc_code&& r) const
{
acc_code res = *this;
......@@ -743,6 +938,7 @@ namespace spot
return res;
}
/// \brief Disjunct the current condition in place with \a r.
acc_code& operator|=(const acc_code& r)
{
if (is_t() || r.is_f())
......@@ -829,6 +1025,7 @@ namespace spot
return *this;
}
/// \brief Disjunct the current condition with \a r.
acc_code operator|(acc_code&& r) const
{
acc_code res = *this;
......@@ -836,6 +1033,7 @@ namespace spot
return res;
}
/// \brief Disjunct the current condition with \a r.
acc_code operator|(const acc_code& r) const
{
acc_code res = *this;
......@@ -843,6 +1041,11 @@ namespace spot
return res;
}
/// \brief Apply a left shift to all mark_t that appear in the condition.
///
/// Shifting `Fin(0)&Inf(3)` by 2 will give `Fin(2)&Inf(5)`.
///
/// The result is modified in place.
acc_code& operator<<=(unsigned sets)
{
if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
......@@ -871,6 +1074,9 @@ namespace spot
return *this;
}
/// \brief Apply a left shift to all mark_t that appear in the condition.
///
/// Shifting `Fin(0)&Inf(3)` by 2 will give `Fin(2)&Inf(5)`.
acc_code operator<<(unsigned sets) const
{
acc_code res = *this;
......@@ -878,80 +1084,176 @@ namespace spot
return res;
}
/// \brief Whether the acceptance formula is in disjunctive normal form.
///
/// The formula is in DNF if it is either:
/// - one of `t`, `f`, `Fin(i)`, `Inf(i)`
/// - a conjunction of any of the above
/// - a disjunction of any of the above (including the conjunctions).
bool is_dnf() const;
/// \brief Whether the acceptance formula is in conjunctive normal form.
///
/// The formula is in DNF if it is either:
/// - one of `t`, `f`, `Fin(i)`, `Inf(i)`
/// - a disjunction of any of the above
/// - a conjunction of any of the above (including the disjunctions).
bool is_cnf() const;
/// \brief Convert the acceptance formula into disjunctive normal form
///
/// This works by distributing `&` over `|`, resulting in a formula that
/// can be exponentially larger than the input.
///
/// The implementation works by converting the formula into a
/// BDD where `Inf(i)` is encoded by vᵢ and `Fin(i)` is encoded
/// by !vᵢ, and then finding prime implicants to build an
/// irredundant sum-of-products. In practice, the results are
/// usually better than what we would expect by hand.
acc_code to_dnf() const;
/// \brief Convert the acceptance formula into disjunctive normal form
///
/// This works by distributing `|` over `&`, resulting in a formula that
/// can be exponentially larger than the input.
///
/// This implementation is the dual of `to_dnf()`.
acc_code to_cnf() const;
/// \brief Complement an acceptance formula.
///
/// Also known as "dualizing the acceptance condition" since
/// this replaces `Fin` ↔ `Inf`, and `&` ↔ `|`.
///
/// Not that dualizing the acceptance condition on a
/// deterministic automaton is enough to complement that
/// automaton. On a non-deterministic automaton, you should
/// also replace existential choices by universal choices,
/// as done by the dualize() function.
acc_code complement() const;
/// \brief Find a `Fin(i)` that is a unit clause.
///
/// This return a mark_t `{i}` such that `Fin(i)` appears as a
/// unit clause in the acceptance condition. I.e., either the
/// condition is exactly `Fin(i)`, or the condition has the form
/// `...&Fin(i)&...`. If there is no such `Fin(i)`, an empty
/// mark_t is returned.
///
/// If multiple unit-Fin appear as unit-clauses, the set of
/// those will be returned. For instance applied to
/// `Fin(0)&Fin(1)&(Inf(2)|Fin(3))``, this will return `{0,1}`.
mark_t fin_unit() const;
/// \brief Return one acceptance set i that appear as `Fin(i)`
/// in the condition.
///
/// Return -1 if no such set exist.
int fin_one() const;
// Return a list of acceptance marks needed to close a cycle
// that already visit INF infinitely often, so that the cycle is
// accepting (ACCEPTING=true) or rejecting (ACCEPTING=false).
// Positive values describe positive set.
// A negative value x means the set -x-1 must be absent.
/// \brief Help closing accepting or rejecting cycle.
///
/// Assuming you have a partial cycle visiting all acceptance
/// sets in \a inf, this returns the combination of set you
/// should see or avoid when closing the cycle to make it
/// accepting or rejecting (as specified with \a accepting).
///
/// The result is a vector of vectors of integers.
/// A positive integer x denote a set that should be seen,
/// a negative value x means the set -x-1 must be absent.
/// The different inter vectors correspond to different
/// solutions satisfying the \a accepting criterion.
std::vector<std::vector<int>>
missing(mark_t inf, bool accepting) const;
/// \brief Check whether visiting *exactly* all sets \a inf
/// infinitely often satisfies the acceptance condition.
bool accepting(mark_t inf) const;
/// \brief Assuming that we will visit at least all sets in \a
/// inf, is there any chance that we will satisfy the condition?
///
/// This return false only when it is sure that visiting more
/// set will never make the condition satisfiable.
bool inf_satisfiable(mark_t inf) const;
/// \brief Check potential acceptance of an SCC.
///
/// Assuming that an SCC intersects all sets in \a
/// infinitely_often (i.e., for each set in \a infinetely_often,
/// there exist one marked transition in the SCC), and is
/// included in all sets in \a always_present (i.e., all
/// transitions are marked with \a always_present), this returns
/// one tree possible results:
/// - trival::yes() the SCC is necessarily accepting,
/// - trival::no() the SCC is necessarily rejecting,
/// - trival::maybe() the SCC could contain an accepting cycle.
trival maybe_accepting(mark_t infinitely_often,
mark_t always_present) const;
// Return all symmetric marks of the condition.
// If two marks x and y are symmetric, it means that swapping them does
// not change (logically) the acc_code.
// In the returned vector, each mark points to the "root" of its symmetry
// class.
/// \brief compute the symmetry class of the acceptance sets.
///
/// Two sets x and y are symmetric if swapping them in the
/// acceptance condition produces an equivalent formula.
/// For instance 0 and 2 are symmetric in Inf(0)&Fin(1)&Inf(2).
///
/// The returned vector is indexed by set numbers, and each
/// entry points to the "root" (or representative element) of
/// its symmetry class. In the above example the result would
/// be [0,1,0], showing that 0 and 2 are in the same class.
std::vector<unsigned> symmetries() const;
// Remove all the acceptance sets in rem.
//
// If MISSING is set, the acceptance sets are assumed to be
// missing from the automaton, and the acceptance is updated to
// reflect this. For instance (Inf(1)&Inf(2))|Fin(3) will
// become Fin(3) if we remove 2 because it is missing from this
// automaton, because there is no way to fulfill Inf(1)&Inf(2)
// in this case. So essentially MISSING causes Inf(rem) to
// become f, and Fin(rem) to become t.
//
// If MISSING is unset, Inf(rem) become t while Fin(rem) become
// f. Removing 2 from (Inf(1)&Inf(2))|Fin(3) would then give
// Inf(1)|Fin(3).
/// \brief Remove all the acceptance sets in \a rem.
///
/// If \a missing is set, the acceptance sets are assumed to be
/// missing from the automaton, and the acceptance is updated to
/// reflect this. For instance `(Inf(1)&Inf(2))|Fin(3)` will
/// become `Fin(3)` if we remove `2` because it is missing from this
/// automaton. Indeed there is no way to fulfill `Inf(1)&Inf(2)`