From 176c9e2e171cb3f087835e4842d817f6cab78b2a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 18 Oct 2015 13:33:35 +0200 Subject: [PATCH] tl: rename ltl_simplifier to tl_simplifier * doc/org/tut01.org, doc/tl/tl.tex, src/bin/common_r.hh, src/bin/ltlfilt.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc, src/tests/randtgba.cc, src/tests/reduc.cc, src/tests/syntimpl.cc, src/tl/nenoform.cc, src/tl/randomltl.cc, src/tl/randomltl.hh, src/tl/simplify.cc, src/tl/simplify.hh, src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/stutter.cc, src/twaalgos/translate.cc, src/twaalgos/translate.hh, wrap/python/ajax/spotcgi.in, wrap/python/spot.py, wrap/python/tests/interdep.py: Rename ltl_simplifier to tl_simplifier. * NEWS: Mention it. --- NEWS | 6 ++- doc/org/tut01.org | 2 +- doc/tl/tl.tex | 34 +++++++-------- src/bin/common_r.hh | 2 +- src/bin/ltlfilt.cc | 8 ++-- src/tests/equalsf.cc | 14 +++--- src/tests/ikwiad.cc | 6 +-- src/tests/randtgba.cc | 6 +-- src/tests/reduc.cc | 6 +-- src/tests/syntimpl.cc | 2 +- src/tl/nenoform.cc | 2 +- src/tl/randomltl.cc | 4 +- src/tl/randomltl.hh | 2 +- src/tl/simplify.cc | 80 +++++++++++++++++------------------ src/tl/simplify.hh | 24 +++++------ src/twaalgos/ltl2tgba_fm.cc | 10 ++--- src/twaalgos/ltl2tgba_fm.hh | 4 +- src/twaalgos/stutter.cc | 2 +- src/twaalgos/translate.cc | 4 +- src/twaalgos/translate.hh | 6 +-- wrap/python/ajax/spotcgi.in | 4 +- wrap/python/spot.py | 6 +-- wrap/python/tests/interdep.py | 2 +- 23 files changed, 119 insertions(+), 117 deletions(-) diff --git a/NEWS b/NEWS index 912978ede..3315779f0 100644 --- a/NEWS +++ b/NEWS @@ -3,7 +3,7 @@ New in spot 1.99.4a (not yet released) Command-line tools: * autfilt has gained a --complement option. - It currently work only for deterministic automata. + It currently works only for deterministic automata. * By default, autfilt does not simplify automata (this has not changed), as if the --low --any options where used. But now, if @@ -18,7 +18,7 @@ New in spot 1.99.4a (not yet released) Library: - * Rename dtgba_complement() as dtwa_complement(), rename the header + * Rename dtgba_complement() to dtwa_complement(), rename the header as complement.hh, and restrict the purpose of this function to just complete the automaton and complement its acceptance condition. Any further acceptance condition transformation @@ -39,6 +39,8 @@ New in spot 1.99.4a (not yet released) * The HOA parser will diagnose any version that is not v1, unless it looks like a subversion of v1 and no parse error was detected. + * ltl_simplifier renamed to tl_simplifier. + Python: * Add bindings for complete() and dtwa_complement() diff --git a/doc/org/tut01.org b/doc/org/tut01.org index dd2174b75..5b19df569 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -309,7 +309,7 @@ prepared to reject the formula any way. In our example, we are lucky return 1; if (!f.is_ltl_formula()) { - spot::ltl_simplifier simp; + spot::tl_simplifier simp; f = simp.simplify(f); } if (!f.is_ltl_formula()) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index a2cc0e983..1e569512b 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1286,24 +1286,24 @@ you plan to abbreviate many formulas sharing identical subformulas. \section{LTL simplifier} The LTL rewritings described in the next three sections are all -implemented in the `\verb|ltl_simplifier|' class defined in +implemented in the `\verb|tl_simplifier|' class defined in \texttt{spot/tl/simplify.hh}. This class implements several caches in order to quickly rewrite formulas that have already been rewritten previously. For this reason, it is suggested that you reuse -your instance of `\verb|ltl_simplifier|' as much as possible. If you +your instance of `\verb|tl_simplifier|' as much as possible. If you write an algorithm that will simplify LTL formulas, we suggest you -accept an optional `\verb|ltl_simplifier|' argument, so that you can +accept an optional `\verb|tl_simplifier|' argument, so that you can benefit from an existing instance. -The `\verb|ltl_simplifier|' takes an optional -`\verb|ltl_simplifier_options|' argument, making it possible to tune +The `\verb|tl_simplifier|' takes an optional +`\verb|tl_simplifier_options|' argument, making it possible to tune the various rewritings that can be performed by this class. These options cannot be changed afterwards (because changing these options would invalidate the results stored in the caches). \section{Negative normal form}\label{sec:nnf} -This is implemented by the `\verb|ltl_simplifier::negative_normal_form|` +This is implemented by the `\verb|tl_simplifier::negative_normal_form|` method. A formula in negative normal form can only have negation @@ -1347,11 +1347,11 @@ Note that the above rules include the ``unabbreviation'' of operators rules \texttt{"ei\^"} of function `\verb=unabbreviate()= as described in Section~\ref{sec:unabbrev}. Therefore it is never necessary to apply these abbreviations before or after -`\verb|ltl_simplifier::negative_normal_form|`. +`\verb|tl_simplifier::negative_normal_form|`. If the option `\verb|nenoform_stop_on_boolean|' is set, the above recursive rewritings are not applied to Boolean subformulas. For -instance calling `\verb|ltl_simplifier::negative_normal_form|` on +instance calling `\verb|tl_simplifier::negative_normal_form|` on $\NOT\F\G(a \XOR b)$ will produce $\G\F(((\NOT a)\AND(\NOT b))\OR(a\AND b))$ if `\verb|nenoform_stop_on_boolean|' is unset, while it will produce $\G\F(\NOT(a \XOR b))$ if @@ -1359,8 +1359,8 @@ it will produce $\G\F(\NOT(a \XOR b))$ if \section{Simplifications} -The `\verb|ltl_simplifier::simplify|' method performs several kinds of -simplifications, depending on which `\verb|ltl_simplifier_options|' +The `\verb|tl_simplifier::simplify|' method performs several kinds of +simplifications, depending on which `\verb|tl_simplifier_options|' was set. The goals in most of these simplification are to: @@ -1381,7 +1381,7 @@ The goals in most of these simplification are to: \end{itemize} Rewritings defined with $\equivEU$ are applied only when -\verb|ltl_simplifier_options::favor_event_univ|' is \texttt{true}: +\verb|tl_simplifier_options::favor_event_univ|' is \texttt{true}: they try to lift subformulas that are both eventual and universal \emph{higher} in the syntax tree. Conversely, rules defined with $\equivNeu$ are applied only when \verb|favor_event_univ|' is \texttt{false}: they @@ -1390,10 +1390,10 @@ try to \textit{lower} subformulas that are both eventual and universal. \subsection{Basic Simplifications}\label{sec:basic-simp} These simplifications are enabled with -\verb|ltl_simplifier_options::reduce_basics|'. A couple of them may +\verb|tl_simplifier_options::reduce_basics|'. A couple of them may enlarge the size of the formula: they are denoted using $\equiV$ instead of $\equiv$, and they can be disabled by setting the -\verb|ltl_simplifier_options::reduce_size_strictly|' option to +\verb|tl_simplifier_options::reduce_size_strictly|' option to \texttt{true}. \subsubsection{Basic Simplifications for Temporal Operators} @@ -1596,7 +1596,7 @@ $\Esuffix$. They assume that $b$, denote a Boolean formula. As noted at the beginning for section~\ref{sec:basic-simp}, rewritings denoted with $\equiV$ can be disabled by setting the -\verb|ltl_simplifier_options::reduce_size_strictly|' option to +\verb|tl_simplifier_options::reduce_size_strictly|' option to \texttt{true}. \begin{align*} @@ -1707,19 +1707,19 @@ implication can be done in two ways: \begin{description} \item[Syntactic Implication Checks] were initially proposed by~\citet{somenzi.00.cav}. This detection is enabled by the - ``\verb|ltl_simplifier_options::synt_impl|'' option. This is a + ``\verb|tl_simplifier_options::synt_impl|'' option. This is a cheap way to detect implications, but it may miss some. The rules we implement are described in Appendix~\ref{ann:syntimpl}. \item[Language Containment Checks] were initially proposed by~\citet{tauriainen.03.a83}. This detection is enabled by the - ``\verb|ltl_simplifier_options::containment_checks|'' option. + ``\verb|tl_simplifier_options::containment_checks|'' option. \end{description} In the following rewritings rules, $f\simp g$ means that $g$ was proved to be implied by $f$ using either of the above two methods. Additionally, implications denoted by $f\Simp g$ are only checked if -the ``\verb|ltl_simplifier_options::containment_checks_stronger|'' +the ``\verb|tl_simplifier_options::containment_checks_stronger|'' option is set (otherwise the rewriting rule is not applied). \begin{equation*} diff --git a/src/bin/common_r.hh b/src/bin/common_r.hh index 9fb7d8950..95860e2bc 100644 --- a/src/bin/common_r.hh +++ b/src/bin/common_r.hh @@ -44,4 +44,4 @@ extern int simplification_level; void parse_r(const char* arg); -spot::ltl_simplifier_options simplifier_options(); +spot::tl_simplifier_options simplifier_options(); diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 81f3e8507..445c71025 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -445,11 +445,11 @@ namespace class ltl_processor: public job_processor { public: - spot::ltl_simplifier& simpl; + spot::tl_simplifier& simpl; fset_t unique_set; spot::relabeling_map relmap; - ltl_processor(spot::ltl_simplifier& simpl) + ltl_processor(spot::tl_simplifier& simpl) : simpl(simpl) { } @@ -641,9 +641,9 @@ main(int argc, char** argv) if (boolean_to_isop && simplification_level == 0) simplification_level = 1; - spot::ltl_simplifier_options opt(simplification_level); + spot::tl_simplifier_options opt(simplification_level); opt.boolean_to_isop = boolean_to_isop; - spot::ltl_simplifier simpl(opt); + spot::tl_simplifier simpl(opt); ltl_processor processor(simpl); if (processor.run()) diff --git a/src/tests/equalsf.cc b/src/tests/equalsf.cc index 31ece43d3..b73188aff 100644 --- a/src/tests/equalsf.cc +++ b/src/tests/equalsf.cc @@ -128,12 +128,12 @@ main(int argc, char** argv) f1.dump(std::cout) << std::endl; #endif #ifdef REDUC - spot::ltl_simplifier_options opt(true, true, true, + spot::tl_simplifier_options opt(true, true, true, false, false); # ifdef EVENT_UNIV opt.favor_event_univ = true; # endif - spot::ltl_simplifier simp(opt); + spot::tl_simplifier simp(opt); { spot::formula tmp; tmp = f1; @@ -150,9 +150,9 @@ main(int argc, char** argv) f1.dump(std::cout) << std::endl; #endif #ifdef REDUC_TAU - spot::ltl_simplifier_options opt(false, false, false, + spot::tl_simplifier_options opt(false, false, false, true, false); - spot::ltl_simplifier simp(opt); + spot::tl_simplifier simp(opt); { spot::formula tmp; tmp = f1; @@ -169,9 +169,9 @@ main(int argc, char** argv) f1.dump(std::cout) << std::endl; #endif #ifdef REDUC_TAUSTR - spot::ltl_simplifier_options opt(false, false, false, + spot::tl_simplifier_options opt(false, false, false, true, true); - spot::ltl_simplifier simp(opt); + spot::tl_simplifier simp(opt); { spot::formula tmp; tmp = f1; @@ -191,7 +191,7 @@ main(int argc, char** argv) exit_code |= f1 != f2; #if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR)) - spot::ltl_simplifier simp; + spot::tl_simplifier simp; #endif if (!simp.are_equivalent(f1, f2)) diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index bf73e6f8b..31185c534 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -326,7 +326,7 @@ checked_main(int argc, char** argv) bool nra2nba = false; bool scc_filter = false; bool simpltl = false; - spot::ltl_simplifier_options redopt(false, false, false, false, + spot::tl_simplifier_options redopt(false, false, false, false, false, false, false); bool simpcache_stats = false; bool scc_filter_all = false; @@ -944,9 +944,9 @@ checked_main(int argc, char** argv) } else { - spot::ltl_simplifier* simp = nullptr; + spot::tl_simplifier* simp = nullptr; if (simpltl) - simp = new spot::ltl_simplifier(redopt, dict); + simp = new spot::tl_simplifier(redopt, dict); if (simp) { diff --git a/src/tests/randtgba.cc b/src/tests/randtgba.cc index b1ebd5807..85aee7ae0 100644 --- a/src/tests/randtgba.cc +++ b/src/tests/randtgba.cc @@ -488,7 +488,7 @@ print_ar_stats(ar_stats_type& ar_stats, const std::string& s) static spot::formula generate_formula(const spot::random_ltl& rl, - spot::ltl_simplifier& simp, + spot::tl_simplifier& simp, int opt_f, int opt_s, int opt_l = 0, bool opt_u = false) { @@ -580,8 +580,8 @@ main(int argc, char** argv) spot::atomic_prop_set* ap = new spot::atomic_prop_set; auto dict = spot::make_bdd_dict(); - spot::ltl_simplifier_options simpopt(true, true, true, true, true); - spot::ltl_simplifier simp(simpopt); + spot::tl_simplifier_options simpopt(true, true, true, true, true); + spot::tl_simplifier simp(simpopt); if (argc <= 1) syntax(argv[0]); diff --git a/src/tests/reduc.cc b/src/tests/reduc.cc index 08659418c..60298c67c 100644 --- a/src/tests/reduc.cc +++ b/src/tests/reduc.cc @@ -45,7 +45,7 @@ main(int argc, char** argv) bool hidereduc = false; unsigned long sum_before = 0; unsigned long sum_after = 0; - spot::ltl_simplifier_options o(false, false, false, false, false); + spot::tl_simplifier_options o(false, false, false, false, false); if (argc < 3) syntax(argv[0]); @@ -147,9 +147,9 @@ main(int argc, char** argv) int exit_code = 0; { - spot::ltl_simplifier* simp = new spot::ltl_simplifier(o); + spot::tl_simplifier* simp = new spot::tl_simplifier(o); o.reduce_size_strictly = true; - spot::ltl_simplifier* simp_size = new spot::ltl_simplifier(o); + spot::tl_simplifier* simp_size = new spot::tl_simplifier(o); spot::formula f1 = nullptr; spot::formula f2 = nullptr; diff --git a/src/tests/syntimpl.cc b/src/tests/syntimpl.cc index e99aa44b9..3dcd786a0 100644 --- a/src/tests/syntimpl.cc +++ b/src/tests/syntimpl.cc @@ -63,7 +63,7 @@ main(int argc, char** argv) std::string f1s = spot::str_psl(f1); std::string f2s = spot::str_psl(f2); - spot::ltl_simplifier* c = new spot::ltl_simplifier; + spot::tl_simplifier* c = new spot::tl_simplifier; switch (opt) { diff --git a/src/tl/nenoform.cc b/src/tl/nenoform.cc index bd939b49a..7a7433fe0 100644 --- a/src/tl/nenoform.cc +++ b/src/tl/nenoform.cc @@ -31,7 +31,7 @@ namespace spot if (!negated && f.is_in_nenoform()) return f; - ltl_simplifier s; + tl_simplifier s; return s.negative_normal_form(f, negated); } } diff --git a/src/tl/randomltl.cc b/src/tl/randomltl.cc index 910f94bd0..c531e975c 100644 --- a/src/tl/randomltl.cc +++ b/src/tl/randomltl.cc @@ -470,8 +470,8 @@ namespace spot + std::string(tok_pB)); spot::srand(opt_seed_); - ltl_simplifier_options simpl_opts(opt_simpl_level_); - ltl_simplifier simpl_(simpl_opts); + tl_simplifier_options simpl_opts(opt_simpl_level_); + tl_simplifier simpl_(simpl_opts); } randltlgenerator::randltlgenerator(int aprops_n, diff --git a/src/tl/randomltl.hh b/src/tl/randomltl.hh index 8628d6040..86a490a9e 100644 --- a/src/tl/randomltl.hh +++ b/src/tl/randomltl.hh @@ -338,7 +338,7 @@ namespace spot bool opt_unique_; bool opt_wf_; int opt_simpl_level_; - ltl_simplifier simpl_; + tl_simplifier simpl_; int output_; diff --git a/src/tl/simplify.cc b/src/tl/simplify.cc index 8abea1d91..61754b9eb 100644 --- a/src/tl/simplify.cc +++ b/src/tl/simplify.cc @@ -39,7 +39,7 @@ namespace spot typedef std::vector vec; // The name of this class is public, but not its contents. - class ltl_simplifier_cache + class tl_simplifier_cache { typedef std::unordered_map f2f_map; typedef std::unordered_map f2b_map; @@ -47,21 +47,21 @@ namespace spot typedef std::map syntimpl_cache_t; public: bdd_dict_ptr dict; - ltl_simplifier_options options; + tl_simplifier_options options; language_containment_checker lcc; - ~ltl_simplifier_cache() + ~tl_simplifier_cache() { dict->unregister_all_my_variables(this); } - ltl_simplifier_cache(const bdd_dict_ptr& d) + tl_simplifier_cache(const bdd_dict_ptr& d) : dict(d), lcc(d, true, true, false, false) { } - ltl_simplifier_cache(const bdd_dict_ptr& d, - const ltl_simplifier_options& opt) + tl_simplifier_cache(const bdd_dict_ptr& d, + const tl_simplifier_options& opt) : dict(d), options(opt), lcc(d, true, true, false, false) { options.containment_checks |= options.containment_checks_stronger; @@ -319,10 +319,10 @@ namespace spot ////////////////////////////////////////////////////////////////////// formula - nenoform_rec(formula f, bool negated, ltl_simplifier_cache* c); + nenoform_rec(formula f, bool negated, tl_simplifier_cache* c); formula equiv_or_xor(bool equiv, formula f1, formula f2, - ltl_simplifier_cache* c) + tl_simplifier_cache* c) { auto rec = [c](formula f, bool negated) { @@ -354,7 +354,7 @@ namespace spot } formula - nenoform_rec(formula f, bool negated, ltl_simplifier_cache* c) + nenoform_rec(formula f, bool negated, tl_simplifier_cache* c) { if (f.is(op::Not)) { @@ -542,7 +542,7 @@ namespace spot // Forward declaration. formula - simplify_recursively(formula f, ltl_simplifier_cache* c); + simplify_recursively(formula f, tl_simplifier_cache* c); // X(a) R b or X(a) M b // This returns a. @@ -654,7 +654,7 @@ namespace spot }; private: - mospliter(unsigned split, ltl_simplifier_cache* cache) + mospliter(unsigned split, tl_simplifier_cache* cache) : split_(split), c_(cache), res_GF{(split_ & Split_GF) ? new vec : nullptr}, res_FG{(split_ & Split_FG) ? new vec : nullptr}, @@ -672,7 +672,7 @@ namespace spot } public: - mospliter(unsigned split, vec v, ltl_simplifier_cache* cache) + mospliter(unsigned split, vec v, tl_simplifier_cache* cache) : mospliter(split, cache) { for (auto f: v) @@ -683,7 +683,7 @@ namespace spot } mospliter(unsigned split, formula mo, - ltl_simplifier_cache* cache) + tl_simplifier_cache* cache) : mospliter(split, cache) { unsigned mos = mo.size(); @@ -788,7 +788,7 @@ namespace spot } unsigned split_; - ltl_simplifier_cache* c_; + tl_simplifier_cache* c_; std::unique_ptr res_GF; std::unique_ptr res_FG; std::unique_ptr res_F; @@ -807,7 +807,7 @@ namespace spot { public: - simplify_visitor(ltl_simplifier_cache* cache) + simplify_visitor(tl_simplifier_cache* cache) : c_(cache), opt_(cache->options) { } @@ -2973,14 +2973,14 @@ namespace spot } protected: - ltl_simplifier_cache* c_; - const ltl_simplifier_options& opt_; + tl_simplifier_cache* c_; + const tl_simplifier_options& opt_; }; formula simplify_recursively(formula f, - ltl_simplifier_cache* c) + tl_simplifier_cache* c) { #ifdef TRACE static int srec = 0; @@ -3029,7 +3029,7 @@ namespace spot } // anonymous namespace ////////////////////////////////////////////////////////////////////// - // ltl_simplifier_cache + // tl_simplifier_cache // This implements the recursive rules for syntactic implication. @@ -3037,7 +3037,7 @@ namespace spot // appendix in the documentation for temporal logic operators.) inline bool - ltl_simplifier_cache::syntactic_implication_aux(formula f, formula g) + tl_simplifier_cache::syntactic_implication_aux(formula f, formula g) { // We first process all lines from the table except the // first two, and then we process the first two as a fallback. @@ -3278,7 +3278,7 @@ namespace spot // Return true if f => g syntactically bool - ltl_simplifier_cache::syntactic_implication(formula f, + tl_simplifier_cache::syntactic_implication(formula f, formula g) { // We cannot run syntactic_implication on SERE formulae, @@ -3331,7 +3331,7 @@ namespace spot // If right==false, true if !f1 => f2, false otherwise. // If right==true, true if f1 => !f2, false otherwise. bool - ltl_simplifier_cache::syntactic_implication_neg(formula f1, + tl_simplifier_cache::syntactic_implication_neg(formula f1, formula f2, bool right) { @@ -3350,26 +3350,26 @@ namespace spot ///////////////////////////////////////////////////////////////////// - // ltl_simplifier + // tl_simplifier - ltl_simplifier::ltl_simplifier(const bdd_dict_ptr& d) + tl_simplifier::tl_simplifier(const bdd_dict_ptr& d) { - cache_ = new ltl_simplifier_cache(d); + cache_ = new tl_simplifier_cache(d); } - ltl_simplifier::ltl_simplifier(const ltl_simplifier_options& opt, + tl_simplifier::tl_simplifier(const tl_simplifier_options& opt, bdd_dict_ptr d) { - cache_ = new ltl_simplifier_cache(d, opt); + cache_ = new tl_simplifier_cache(d, opt); } - ltl_simplifier::~ltl_simplifier() + tl_simplifier::~tl_simplifier() { delete cache_; } formula - ltl_simplifier::simplify(formula f) + tl_simplifier::simplify(formula f) { if (!f.is_in_nenoform()) f = negative_normal_form(f, false); @@ -3377,68 +3377,68 @@ namespace spot } formula - ltl_simplifier::negative_normal_form(formula f, bool negated) + tl_simplifier::negative_normal_form(formula f, bool negated) { return nenoform_rec(f, negated, cache_); } bool - ltl_simplifier::syntactic_implication(formula f1, formula f2) + tl_simplifier::syntactic_implication(formula f1, formula f2) { return cache_->syntactic_implication(f1, f2); } bool - ltl_simplifier::syntactic_implication_neg(formula f1, + tl_simplifier::syntactic_implication_neg(formula f1, formula f2, bool right) { return cache_->syntactic_implication_neg(f1, f2, right); } bool - ltl_simplifier::are_equivalent(formula f, formula g) + tl_simplifier::are_equivalent(formula f, formula g) { return cache_->lcc.equal(f, g); } bool - ltl_simplifier::implication(formula f, formula g) + tl_simplifier::implication(formula f, formula g) { return cache_->lcc.contained(f, g); } bdd - ltl_simplifier::as_bdd(formula f) + tl_simplifier::as_bdd(formula f) { return cache_->as_bdd(f); } formula - ltl_simplifier::star_normal_form(formula f) + tl_simplifier::star_normal_form(formula f) { return cache_->star_normal_form(f); } formula - ltl_simplifier::boolean_to_isop(formula f) + tl_simplifier::boolean_to_isop(formula f) { return cache_->boolean_to_isop(f); } bdd_dict_ptr - ltl_simplifier::get_dict() const + tl_simplifier::get_dict() const { return cache_->dict; } void - ltl_simplifier::print_stats(std::ostream& os) const + tl_simplifier::print_stats(std::ostream& os) const { cache_->print_stats(os); } void - ltl_simplifier::clear_as_bdd_cache() + tl_simplifier::clear_as_bdd_cache() { cache_->clear_as_bdd_cache(); cache_->lcc.clear(); diff --git a/src/tl/simplify.hh b/src/tl/simplify.hh index 6680a945d..a3506fc9f 100644 --- a/src/tl/simplify.hh +++ b/src/tl/simplify.hh @@ -26,10 +26,10 @@ namespace spot { - class ltl_simplifier_options + class tl_simplifier_options { public: - ltl_simplifier_options(bool basics = true, + tl_simplifier_options(bool basics = true, bool synt_impl = true, bool event_univ = true, bool containment_checks = false, @@ -50,8 +50,8 @@ namespace spot { } - ltl_simplifier_options(int level) : - ltl_simplifier_options(false, false, false) + tl_simplifier_options(int level) : + tl_simplifier_options(false, false, false) { switch (level) { @@ -90,17 +90,17 @@ namespace spot }; // fwd declaration to hide technical details. - class ltl_simplifier_cache; + class tl_simplifier_cache; /// \ingroup tl_rewriting /// \brief Rewrite or simplify \a f in various ways. - class SPOT_API ltl_simplifier + class SPOT_API tl_simplifier { public: - ltl_simplifier(const bdd_dict_ptr& dict = make_bdd_dict()); - ltl_simplifier(const ltl_simplifier_options& opt, + tl_simplifier(const bdd_dict_ptr& dict = make_bdd_dict()); + tl_simplifier(const tl_simplifier_options& opt, bdd_dict_ptr dict = make_bdd_dict()); - ~ltl_simplifier(); + ~tl_simplifier(); /// Simplify the formula \a f (using options supplied to the /// constructor). @@ -193,9 +193,9 @@ namespace spot void print_stats(std::ostream& os) const; private: - ltl_simplifier_cache* cache_; + tl_simplifier_cache* cache_; // Copy disallowed. - ltl_simplifier(const ltl_simplifier&) = delete; - void operator=(const ltl_simplifier&) = delete; + tl_simplifier(const tl_simplifier&) = delete; + void operator=(const tl_simplifier&) = delete; }; } diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc index 9c1fa8e3e..6f8872238 100644 --- a/src/twaalgos/ltl2tgba_fm.cc +++ b/src/twaalgos/ltl2tgba_fm.cc @@ -133,7 +133,7 @@ namespace spot { public: - translate_dict(twa_graph_ptr& a, ltl_simplifier* ls, bool exprop, + translate_dict(twa_graph_ptr& a, tl_simplifier* ls, bool exprop, bool single_acc, bool unambiguous) : a_(a), dict(a->get_dict()), @@ -156,7 +156,7 @@ namespace spot twa_graph_ptr& a_; bdd_dict_ptr dict; - ltl_simplifier* ls; + tl_simplifier* ls; mark_tools mt; typedef bdd_dict::fv_map fv_map; @@ -1886,9 +1886,9 @@ namespace spot ltl_to_tgba_fm(formula f2, const bdd_dict_ptr& dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx, const atomic_prop_set* unobs, - ltl_simplifier* simplifier, bool unambiguous) + tl_simplifier* simplifier, bool unambiguous) { - ltl_simplifier* s = simplifier; + tl_simplifier* s = simplifier; // Simplify the formula, if requested. if (s) @@ -1903,7 +1903,7 @@ namespace spot // negations on the atomic propositions. We also suppress // logic abbreviations such as <=>, =>, or XOR, since they // would involve negations at the BDD level. - s = new ltl_simplifier(dict); + s = new tl_simplifier(dict); f2 = s->negative_normal_form(f2, false); } assert(f2.is_in_nenoform()); diff --git a/src/twaalgos/ltl2tgba_fm.hh b/src/twaalgos/ltl2tgba_fm.hh index c350516a2..35cf2e489 100644 --- a/src/twaalgos/ltl2tgba_fm.hh +++ b/src/twaalgos/ltl2tgba_fm.hh @@ -101,7 +101,7 @@ namespace spot /// representing each state of the automaton will be simplified /// before computing the successor. \a simpl should be configured /// for the type of reduction you want, see - /// spot::ltl_simplifier. This idea is taken from the + /// spot::tl_simplifier. This idea is taken from the /// following paper. /** \verbatim @InProceedings{ thirioux.02.fmics, @@ -145,6 +145,6 @@ namespace spot bool branching_postponement = false, bool fair_loop_approx = false, const atomic_prop_set* unobs = nullptr, - ltl_simplifier* simplifier = nullptr, + tl_simplifier* simplifier = nullptr, bool unambiguous = false); } diff --git a/src/twaalgos/stutter.cc b/src/twaalgos/stutter.cc index 6d1b20b3b..5631fd282 100644 --- a/src/twaalgos/stutter.cc +++ b/src/twaalgos/stutter.cc @@ -558,7 +558,7 @@ namespace spot bool res; if (algo == 0) // Equivalence check { - ltl_simplifier ls; + tl_simplifier ls; res = ls.are_equivalent(f, g); } else diff --git a/src/twaalgos/translate.cc b/src/twaalgos/translate.cc index 6cce712fb..d5bcc398b 100644 --- a/src/twaalgos/translate.cc +++ b/src/twaalgos/translate.cc @@ -43,7 +43,7 @@ namespace spot void translator::build_simplifier(const bdd_dict_ptr& dict) { - ltl_simplifier_options options(false, false, false); + tl_simplifier_options options(false, false, false); switch (level_) { case High: @@ -58,7 +58,7 @@ namespace spot options.event_univ = true; // fall through } - simpl_owned_ = simpl_ = new ltl_simplifier(options, dict); + simpl_owned_ = simpl_ = new tl_simplifier(options, dict); } twa_graph_ptr translator::run(formula* f) diff --git a/src/twaalgos/translate.hh b/src/twaalgos/translate.hh index c970d0193..2756cefb8 100644 --- a/src/twaalgos/translate.hh +++ b/src/twaalgos/translate.hh @@ -47,7 +47,7 @@ namespace spot class SPOT_API translator: protected postprocessor { public: - translator(ltl_simplifier* simpl, const option_map* opt = nullptr) + translator(tl_simplifier* simpl, const option_map* opt = nullptr) : postprocessor(opt), simpl_(simpl), simpl_owned_(nullptr) { assert(simpl); @@ -114,8 +114,8 @@ namespace spot void build_simplifier(const bdd_dict_ptr& dict); private: - ltl_simplifier* simpl_; - ltl_simplifier* simpl_owned_; + tl_simplifier* simpl_; + tl_simplifier* simpl_owned_; int comp_susp_; int early_susp_; int skel_wdba_; diff --git a/wrap/python/ajax/spotcgi.in b/wrap/python/ajax/spotcgi.in index ced25bad9..425075724 100755 --- a/wrap/python/ajax/spotcgi.in +++ b/wrap/python/ajax/spotcgi.in @@ -461,7 +461,7 @@ if not f: finish() # Formula simplifications -simpopt = spot.ltl_simplifier_options(False, False, False, +simpopt = spot.tl_simplifier_options(False, False, False, False, False, False, True) dored = False for r in form.getlist('r'): @@ -480,7 +480,7 @@ for r in form.getlist('r'): if dored: # Not keeping the ltl simplifier aive will also clear the as_bdd() # cache. - f = spot.ltl_simplifier(simpopt).simplify(f) + f = spot.tl_simplifier(simpopt).simplify(f) # Formula manipulation only. if output_type == 'f': diff --git a/wrap/python/spot.py b/wrap/python/spot.py index fcfc1e3cc..2641c6bf7 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -677,7 +677,7 @@ def randltl(ap, n=-1, **kwargs): def simplify(f, **kwargs): level = kwargs.get('level', None) if level is not None: - return ltl_simplifier(ltl_simplifier_options(level)).simplify(f) + return tl_simplifier(tl_simplifier_options(level)).simplify(f) basics = kwargs.get('basics', True) synt_impl = kwargs.get('synt_impl', True) @@ -689,7 +689,7 @@ def simplify(f, **kwargs): boolean_to_isop = kwargs.get('boolean_to_isop', False) favor_event_univ = kwargs.get('favor_event_univ', False) - simp_opts = ltl_simplifier_options(basics, + simp_opts = tl_simplifier_options(basics, synt_impl, event_univ, cont_checks, @@ -698,7 +698,7 @@ def simplify(f, **kwargs): reduce_size_strictly, boolean_to_isop, favor_event_univ) - return ltl_simplifier(simp_opts).simplify(f) + return tl_simplifier(simp_opts).simplify(f) for fun in dir(formula): diff --git a/wrap/python/tests/interdep.py b/wrap/python/tests/interdep.py index 853ff5d19..03a8e3465 100755 --- a/wrap/python/tests/interdep.py +++ b/wrap/python/tests/interdep.py @@ -26,7 +26,7 @@ import buddy import spot import sys -simp = spot.ltl_simplifier() +simp = spot.tl_simplifier() e = spot.default_environment.instance() p = spot.empty_parse_error_list()