alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/ltlvisit/reducform.hh: Update Doxygen comments for

Browse source 
previous change.
This commit is contained in:
Alexandre Duret-Lutz 2004-05-25 12:55:48 +00:00
parent 8f82f1d5f3
commit 20bdf49a70
2 changed files with 14 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

3
ChangeLog
View file

@ -1,5 +1,8 @@
2004-05-25 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/ltlvisit/reducform.hh: Update Doxygen comments for
previous change.
* src/ltlvisit/reducform.hh (option): Rename as ...
(reduce_options): ... this, and use it as a bit field so
option can be combined easily.

20
src/ltlvisit/reducform.hh
View file

@ -30,25 +30,27 @@ namespace spot
namespace ltl
{
/// Options for spot::ltl::reduce.
enum reduce_options
{
/// No reduction.
Reduce_None = 0,
/// Basic reductions.
Reduce_Basics = 1,
/// Somenzi & Bloem syntactic implication.
Reduce_Syntactic_Implications = 2,
/// Etessami & Holzmann eventuality and universality reductions.
Reduce_Eventuality_And_Universality = 4,
/// All reductions.
Reduce_All = -1U
};
/// \brief Reduce a formula \a f using Basic rewriting, implies
/// relation, and class of eventuality and univerality formula.
/// \brief Reduce a formula \a f.
///
/// Put the formula in negative normal form with
/// spot::ltl::negative_normal_form and then reduce it according
/// to options:
/// Base for spot::ltl::Basic_reduce_form,
/// Inf for spot::ltl::reduce_inf_form,
/// EventualUniversal for spot::ltl::reduce_eventuality_universality_form,
/// BRI for spot::ltl::reduce_form.
/// \param f the formula to reduce
/// \param opt a conjonction of spot::ltl::reduce_options specifying
// which optimizations to apply.
/// \return the reduced formula
formula* reduce(const formula* f, int opt = Reduce_All);
/// Implement basic rewriting.