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

Add a has_lbt_atomic_props() method to LTL formulas.

* src/ltlast/formula.hh (has_lbt_atomic_props): New method.
* src/ltlast/formula.cc (printprops): Display it.
* src/ltlast/atomic_prop.cc: Update it.
* src/bin/ltlcheck.cc, src/bin/genltl.cc: Use it.
* doc/tl/tl.tex: Menton has_lbt_atomic_props().
parent f40925f6
......@@ -40,6 +40,10 @@
\newcommand{\uni}[1]{\texttt{\small U+#1}}
% For tables.
\newcommand{\newfootnotemark}[1]{\addtocounter{footnote}{#1}\footnotemark[\value{footnote}]}
\newcommand{\newfootnotetext}[2]{\addtocounter{footnote}{#1}\footnotetext[\value{footnote}]{#2}}
%% ---------------------- %%
%% Mathematical symbols. %%
......@@ -991,16 +995,22 @@ instance using the following methods:
\\\texttt{is\_syntactic\_persistence()}& Whether the formula is a syntactic
persistence property.
\\\texttt{is\_marked()}& Whether the formula contains a special
``marked'' version of the $\Esuffix$ or $\nsere{r}$ operators.\footnotemark
``marked'' version of the $\Esuffix$ or $\nsere{r}$ operators.\newfootnotemark{1}
\\\texttt{accepts\_eword()}& Whether the formula accepts
$\eword$. (This can only be true for a SERE formula.)
\\\texttt{has\_lbt\_atomic\_props()}& Whether the atomic
propositions of the formula are all of the form ``\texttt{p}$nn$''
where $nn$ is a string of digits. This is required when converting
formula into LBT's format.\newfootnotemark{1}
\end{tabulary}
\footnotetext{These ``marked'' operators are used when
\newfootnotetext{-1}{These ``marked'' operators are used when
translating recurring $\Esuffix$ or $\nsere{r}$ operators. They are
rendered as $\EsuffixMarked$ and $\nsereMarked{r}$ and obey the
same simplification rules and properties as their unmarked
counterpart (except for the \texttt{is\_marked()} property).}
rendered as $\EsuffixMarked$ and $\nsereMarked{r}$ and obey the same
simplification rules and properties as their unmarked counterpart
(except for the \texttt{is\_marked()} property).}
\newfootnotetext{1}{\url{http://www.tcs.hut.fi/Software/maria/tools/lbt/}}
\section{Pure Eventualities and Purely Universal Formul\ae{}}
\label{sec:eventuniv}
......
......@@ -802,7 +802,7 @@ output_pattern(int pattern, int n)
// Make sure we use only "p42"-style of atomic propositions
// in lbt's output.
if (output_format == lbt_output)
if (output_format == lbt_output && !f->has_lbt_atomic_props())
{
const spot::ltl::formula* r = spot::ltl::relabel(f, spot::ltl::Pnn);
f->destroy();
......
......@@ -41,6 +41,7 @@
#include "ltlvisit/tostring.hh"
#include "ltlvisit/apcollect.hh"
#include "ltlvisit/lbt.hh"
#include "ltlvisit/relabel.hh"
#include "tgbaalgos/lbtt.hh"
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/gtec/gtec.hh"
......@@ -414,6 +415,8 @@ namespace
// Run-specific variables
printable_result_filename output;
public:
using spot::formater::has;
translator_runner()
{
declare('f', &string_ltl_spot);
......@@ -704,6 +707,16 @@ namespace
pstats->resize(m);
nstats->resize(m);
// If we need LBT atomic proposition in any of the input or
// output, relabel the formula.
if (!f->has_lbt_atomic_props() &&
(runner.has('l') || runner.has('L') || runner.has('T')))
{
const spot::ltl::formula* g = spot::ltl::relabel(f, spot::ltl::Pnn);
f->destroy();
f = g;
}
// ---------- Positive Formula ----------
runner.round_formula(f, round);
......
......@@ -52,6 +52,15 @@ namespace spot
is.syntactic_persistence = true;
is.not_marked = true;
is.accepting_eword = false;
// is.lbt_atomic_props should be true if the name has the form
// pNN where NN is any number of digit.
std::string::const_iterator pos = name.begin();
is.lbt_atomic_props = (pos != name.end() && *pos++ == 'p');
while (is.lbt_atomic_props && pos != name.end())
{
char l = *pos++;
is.lbt_atomic_props = (l >= '0' && l <= '9');
}
}
atomic_prop::~atomic_prop()
......
......@@ -81,7 +81,8 @@ namespace spot
proprint(is_syntactic_persistence, "p", "syntactic persistence"); \
proprint(is_syntactic_recurrence, "r", "syntactic recurrence"); \
proprint(is_marked, "+", "marked"); \
proprint(accepts_eword, "0", "accepts the empty word");
proprint(accepts_eword, "0", "accepts the empty word"); \
proprint(has_lbt_atomic_props, "l", "as LBT-style atomic props");
std::list<std::string>
......
......@@ -275,6 +275,11 @@ namespace spot
return is.accepting_eword;
}
bool has_lbt_atomic_props() const
{
return is.lbt_atomic_props;
}
/// The properties as a field of bits. For internal use.
unsigned get_props() const
{
......@@ -333,6 +338,7 @@ namespace spot
bool syntactic_persistence:1; // Syntactic Persistence Property.
bool not_marked:1; // No occurrence of EConcatMarked.
bool accepting_eword:1; // Accepts the empty word.
bool lbt_atomic_props:1; // Use only atomic propositions like p42.
};
union
{
......
Supports Markdown
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