Commit 176c9e2e authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 21be883c
......@@ -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()
......
......@@ -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())
......
......@@ -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*}
......
......@@ -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();
......@@ -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())
......
......@@ -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))
......
......@@ -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)
{
......
......@@ -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]);
......
......@@ -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;
......
......@@ -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)
{
......
......@@ -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);
}
}
......@@ -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,
......
......@@ -338,7 +338,7 @@ namespace spot
bool opt_unique_;
bool opt_wf_;
int opt_simpl_level_;
ltl_simplifier simpl_;
tl_simplifier simpl_;
int output_;
......
......@@ -39,7 +39,7 @@ namespace spot
typedef std::vector<formula> vec;
// The name of this class is public, but not its contents.
class ltl_simplifier_cache
class tl_simplifier_cache
{
typedef std::unordered_map<formula, formula> f2f_map;
typedef std::unordered_map<formula, bdd> f2b_map;
......@@ -47,21 +47,21 @@ namespace spot
typedef std::map<pairf, bool> 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<vec> res_GF;
std::unique_ptr<vec> res_FG;
std::unique_ptr<vec> 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();
......
......@@ -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