Commit e0819268 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

* spot/twaalgos/word.hh: Add documentation.

parent 8bc10dea
......@@ -26,6 +26,13 @@ namespace spot
class bdd_dict;
/// \brief An infinite word stored as a lasso.
///
/// This is not exactly a word in the traditional sense because we
/// use boolean formulas instead of letters. So technically a
/// twa_word can represent a set of words.
///
/// This class only represent lasso-shaped words using two list of
/// BDDs: one list of the prefix, one list for the cycle.
struct SPOT_API twa_word final
{
twa_word(const bdd_dict_ptr& dict);
......@@ -35,6 +42,26 @@ namespace spot
dict_->unregister_all_my_variables(this);
}
/// \brief Simplify a lasso-shapped word.
///
/// The simplified twa_word may represent a subset of the actual
/// words represented by the original twa_word. The typical
/// use-case is that a counterexample generated by an
/// emptiness-check was converted into a twa_word (maybe accepting
/// several words) and we want to present a simpler word as a
/// counterexample to the user. ltlcross does that, for instance.
///
/// This method performs three reductions:
///
/// - If all the formulas on the cycle are compatible, the cycle
/// will be reduced to a loop with the intersection of all
/// formulas.
///
/// - If the end of the prefix can be folded into the cycle,
/// remove those letters, and rotate the cycle accordingly.
///
/// - If any formula contains a disjunction, replace it by a
/// single operand.
void simplify();
typedef std::list<bdd> seq_t;
......@@ -46,8 +73,21 @@ namespace spot
return dict_;
}
/// \brief Convert the twa_word as an automaton.
///
/// This is useful to evaluate a word on an automaton.
twa_graph_ptr as_automaton() const;
/// \brief Print a twa_word
///
/// Words are printed as
/// \code
/// BF;BF;...;BF;cycle{BF;BF;...;BF}
/// \endcode
///
/// where BF denote Boolean Formulas. The prefix part (before
/// cycle{...}) can be empty. The cycle part (inside cycle{...})
/// may not be empty.
SPOT_API
friend std::ostream& operator<<(std::ostream& os, const twa_word& w);
private:
......@@ -56,16 +96,33 @@ namespace spot
typedef std::shared_ptr<twa_word> twa_word_ptr;
/// \brief Create an empty twa_word
///
/// Note that empty twa_word are invalid and cannot be printed.
/// After creating an empty twa_word, you should at least populate
/// the cycle.
inline twa_word_ptr make_twa_word(const bdd_dict_ptr& dict)
{
return std::make_shared<twa_word>(dict);
}
/// Create a twa_word from a twa_run
inline twa_word_ptr make_twa_word(const twa_run_ptr& run)
{
return std::make_shared<twa_word>(run);
}
/// \brief Parse a twa_word.
///
/// The input should have the form
/// \code
/// BF;BF;...;BF;cycle{BF;BF;...;BF}
/// \endcode
/// where BF can be any Boolean formula, and the prefix
/// sequence (before cycle{...}) may be empty.
///
/// \param word the string to parse
/// \param dict the bdd_dict where atomic propositions should be registered
SPOT_API
twa_word_ptr parse_word(const std::string& word, const bdd_dict_ptr& dict);
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment