formula: accept additional arguments for map and traverse
Fixes #306. * spot/tl/formula.hh, python/spot/__init__.py: Implement this in C++ and Python. * doc/org/tut03.org: Document (and indirectly test) it. * NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz
parent
7dd791fe59
commit
7b2517a518
4 changed files with 167 additions and 22 deletions
4
NEWS
4
NEWS
|
|
@ -190,6 +190,10 @@ New in spot 2.4.2.dev (not yet released)
|
|||
- The new spot::formula::is_leaf() method can be used to detect
|
||||
formulas without children (atomic propositions, or constants).
|
||||
|
||||
- spot::formula::map(fun) and spot::formula::traverse(fun) will
|
||||
accept additionnal arguments and pass them to fun(). See
|
||||
https://spot.lrde.epita.fr/tut03.html for some examples.
|
||||
|
||||
- The new function spot::print_aiger() encodes an automaton as an
|
||||
AIGER circuit and prints it. This is only possible for automata
|
||||
whose acceptance condition is trivial. It relies on a new named
|
||||
|
|
|
|||
|
|
@ -198,7 +198,7 @@ sugar (the =is_sugar_free_ltl()= method is a constant-time operation
|
|||
that tells whether a formula contains a =F= or =G= operator) to save
|
||||
time time by not exploring further.
|
||||
|
||||
|
||||
#+NAME: gcount_cpp
|
||||
#+BEGIN_SRC C++ :results verbatim :exports both
|
||||
#include <iostream>
|
||||
#include <spot/tl/formula.hh>
|
||||
|
|
@ -222,7 +222,7 @@ time time by not exploring further.
|
|||
}
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+RESULTS: gcount_cpp
|
||||
#+begin_example
|
||||
FGa -> (GFb & GF(b & c & d))
|
||||
FGa
|
||||
|
|
@ -238,7 +238,6 @@ b & c & d
|
|||
=== 3 G seen ===
|
||||
#+end_example
|
||||
|
||||
|
||||
The other useful operation is =map=. This also takes a functional
|
||||
argument, but that function should input a formula and output a
|
||||
replacement formula. =f.map(fun)= applies =fun= to all children of
|
||||
|
|
@ -247,6 +246,7 @@ replacement formula. =f.map(fun)= applies =fun= to all children of
|
|||
Here is a demonstration of how to exchange all =F= and =G= operators
|
||||
in a formula:
|
||||
|
||||
#+NAME: xchg_fg_cpp
|
||||
#+BEGIN_SRC C++ :results verbatim :exports both
|
||||
#include <iostream>
|
||||
#include <spot/tl/formula.hh>
|
||||
|
|
@ -280,6 +280,136 @@ in a formula:
|
|||
: after: GFa -> (FGb & FG(b & c & d))
|
||||
|
||||
|
||||
*** Additional tricks about =map= and =traverse= in C++
|
||||
|
||||
As seen above, the first argument of =map()= and =traverse()= is a
|
||||
function =fun()= (or actually any object that as an =operator()=) that
|
||||
will be applied to subformulas. If additional arguments are passed to
|
||||
=map()= or =traverse()=, those will be passed on to =fun()= after the
|
||||
formula.
|
||||
|
||||
For instance instead of having a lambda capturing the [[gcount_cpp][=gcount=
|
||||
variable in the first example]], we could pass a reference to this
|
||||
variable:
|
||||
|
||||
#+BEGIN_SRC C++ :results verbatim :exports both
|
||||
#include <iostream>
|
||||
#include <spot/tl/formula.hh>
|
||||
#include <spot/tl/print.hh>
|
||||
#include <spot/tl/parse.hh>
|
||||
|
||||
int main()
|
||||
{
|
||||
spot::formula f = spot::parse_formula("FGa -> (GFb & GF(c & b & d))");
|
||||
|
||||
int gcount = 0;
|
||||
f.traverse([](spot::formula f, int& count)
|
||||
{
|
||||
if (f.is(spot::op::G))
|
||||
++count;
|
||||
return f.is_sugar_free_ltl();
|
||||
}, gcount);
|
||||
std::cout << "=== " << gcount << " G seen ===\n";
|
||||
return 0;
|
||||
}
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
: === 3 G seen ===
|
||||
|
||||
(Here we have removed the print statement inside the lambda to focus
|
||||
more on how =gcount= get passed as the =&count= reference. Here there
|
||||
is no real advantage to passing such reference by argument instead of
|
||||
capturing them in the lambda.
|
||||
|
||||
The possibility to pass additional arguments is however more useful in
|
||||
the case of =map=. Let's write a variant of our [[xchg_fg_cpp][=xchg_fg()= example]]
|
||||
that counts the number of exchanges performed. First, we do it
|
||||
without lambda:
|
||||
|
||||
#+BEGIN_SRC C++ :results verbatim :exports both
|
||||
#include <iostream>
|
||||
#include <spot/tl/formula.hh>
|
||||
#include <spot/tl/print.hh>
|
||||
#include <spot/tl/parse.hh>
|
||||
|
||||
spot::formula xchg_fg(spot::formula in, int& count)
|
||||
{
|
||||
if (in.is(spot::op::F, spot::op::G))
|
||||
++count;
|
||||
if (in.is(spot::op::F))
|
||||
return spot::formula::G(xchg_fg(in[0], count));
|
||||
if (in.is(spot::op::G))
|
||||
return spot::formula::F(xchg_fg(in[0], count));
|
||||
// No need to transform subformulas without F or G
|
||||
if (in.is_sugar_free_ltl())
|
||||
return in;
|
||||
// Apply xchg_fg recursively on any other operator's children
|
||||
return in.map(xchg_fg, count);
|
||||
}
|
||||
|
||||
int main()
|
||||
{
|
||||
spot::formula f = spot::parse_formula("FGa -> (GFb & GF(c & b & d))");
|
||||
std::cout << "before: " << f << '\n';
|
||||
int count = 0;
|
||||
std::cout << "after: " << xchg_fg(f, count) << '\n';
|
||||
std::cout << "exchanges: " << count << '\n';
|
||||
return 0;
|
||||
}
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
: before: FGa -> (GFb & GF(b & c & d))
|
||||
: after: GFa -> (FGb & FG(b & c & d))
|
||||
: exchanges: 6
|
||||
|
||||
Now let's pretend that we want to define =xchg_fg= as a lambda, and
|
||||
=count= to by captured by reference. In order to call pass the lambda
|
||||
recursively to =map=, the lambda needs to know its address.
|
||||
Unfortunately, if the lambda is stored with type =auto=, it cannot
|
||||
capture itself. A solution is to use =std::function= but that has a
|
||||
large penalty cost. We can work around that by assuming that that
|
||||
address will be passed as an argument (=self=) to the lambda:
|
||||
|
||||
#+BEGIN_SRC C++ :results verbatim :exports both
|
||||
#include <iostream>
|
||||
#include <spot/tl/formula.hh>
|
||||
#include <spot/tl/print.hh>
|
||||
#include <spot/tl/parse.hh>
|
||||
|
||||
int main()
|
||||
{
|
||||
spot::formula f = spot::parse_formula("FGa -> (GFb & GF(c & b & d))");
|
||||
std::cout << "before: " << f << '\n';
|
||||
|
||||
int count = 0;
|
||||
auto xchg_fg = [&count](spot::formula in, auto&& self) -> spot::formula
|
||||
{
|
||||
if (in.is(spot::op::F, spot::op::G))
|
||||
++count;
|
||||
if (in.is(spot::op::F))
|
||||
return spot::formula::G(self(in[0], self));
|
||||
if (in.is(spot::op::G))
|
||||
return spot::formula::F(self(in[0], self));
|
||||
// No need to transform subformulas without F or G
|
||||
if (in.is_sugar_free_ltl())
|
||||
return in;
|
||||
// Apply xchg_fg recursively on any other operator's children
|
||||
return in.map(self, self);
|
||||
};
|
||||
std::cout << "after: " << xchg_fg(f, xchg_fg) << '\n';
|
||||
std::cout << "exchanges: " << count << '\n';
|
||||
return 0;
|
||||
}
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
: before: FGa -> (GFb & GF(b & c & d))
|
||||
: after: GFa -> (FGb & FG(b & c & d))
|
||||
: exchanges: 6
|
||||
|
||||
|
||||
** Python
|
||||
|
||||
The Python version of the above two examples uses a very similar
|
||||
|
|
@ -342,3 +472,6 @@ Here is the =F= and =G= exchange:
|
|||
#+RESULTS:
|
||||
: before: FGa -> (GFb & GF(b & c & d))
|
||||
: after: GFa -> (FGb & FG(b & c & d))
|
||||
|
||||
Like in C++, extra arguments to =map= and =traverse= are passed as
|
||||
additional to the function given in the first argument.
|
||||
|
|
|
|||
|
|
@ -282,27 +282,28 @@ class formula:
|
|||
|
||||
return s.__format__(spec)
|
||||
|
||||
def traverse(self, func):
|
||||
if func(self):
|
||||
def traverse(self, func, *args):
|
||||
if func(self, *args):
|
||||
return
|
||||
for f in self:
|
||||
f.traverse(func)
|
||||
f.traverse(func, *args)
|
||||
|
||||
def map(self, func):
|
||||
def map(self, func, *args):
|
||||
k = self.kind()
|
||||
if k in (op_ff, op_tt, op_eword, op_ap):
|
||||
return self
|
||||
if k in (op_Not, op_X, op_F, op_G, op_Closure,
|
||||
op_NegClosure, op_NegClosureMarked):
|
||||
return formula.unop(k, func(self[0]))
|
||||
return formula.unop(k, func(self[0], *args))
|
||||
if k in (op_Xor, op_Implies, op_Equiv, op_U, op_R, op_W,
|
||||
op_M, op_EConcat, op_EConcatMarked, op_UConcat):
|
||||
return formula.binop(k, func(self[0]), func(self[1]))
|
||||
return formula.binop(k, func(self[0], *args), func(self[1], *args))
|
||||
if k in (op_Or, op_OrRat, op_And, op_AndRat, op_AndNLM,
|
||||
op_Concat, op_Fusion):
|
||||
return formula.multop(k, [func(x) for x in self])
|
||||
return formula.multop(k, [func(x, *args) for x in self])
|
||||
if k in (op_Star, op_FStar):
|
||||
return formula.bunop(k, func(self[0]), self.min(), self.max())
|
||||
return formula.bunop(k, func(self[0], *args),
|
||||
self.min(), self.max())
|
||||
raise ValueError("unknown type of formula")
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -1602,8 +1602,10 @@ namespace spot
|
|||
#undef SPOT_DEF_PROP
|
||||
|
||||
/// \brief Clone this node after applying \a trans to its children.
|
||||
template<typename Trans>
|
||||
formula map(Trans trans)
|
||||
///
|
||||
/// Any additional argument is passed to trans.
|
||||
template<typename Trans, typename... Args>
|
||||
formula map(Trans trans, Args&&... args)
|
||||
{
|
||||
switch (op o = kind())
|
||||
{
|
||||
|
|
@ -1619,7 +1621,7 @@ namespace spot
|
|||
case op::Closure:
|
||||
case op::NegClosure:
|
||||
case op::NegClosureMarked:
|
||||
return unop(o, trans((*this)[0]));
|
||||
return unop(o, trans((*this)[0], std::forward<Args>(args)...));
|
||||
case op::Xor:
|
||||
case op::Implies:
|
||||
case op::Equiv:
|
||||
|
|
@ -1631,8 +1633,9 @@ namespace spot
|
|||
case op::EConcatMarked:
|
||||
case op::UConcat:
|
||||
{
|
||||
formula tmp = trans((*this)[0]);
|
||||
return binop(o, tmp, trans((*this)[1]));
|
||||
formula tmp = trans((*this)[0], std::forward<Args>(args)...);
|
||||
return binop(o, tmp,
|
||||
trans((*this)[1], std::forward<Args>(args)...));
|
||||
}
|
||||
case op::Or:
|
||||
case op::OrRat:
|
||||
|
|
@ -1645,12 +1648,13 @@ namespace spot
|
|||
std::vector<formula> tmp;
|
||||
tmp.reserve(size());
|
||||
for (auto f: *this)
|
||||
tmp.emplace_back(trans(f));
|
||||
tmp.emplace_back(trans(f, std::forward<Args>(args)...));
|
||||
return multop(o, std::move(tmp));
|
||||
}
|
||||
case op::Star:
|
||||
case op::FStar:
|
||||
return bunop(o, trans((*this)[0]), min(), max());
|
||||
return bunop(o, trans((*this)[0], std::forward<Args>(args)...),
|
||||
min(), max());
|
||||
}
|
||||
SPOT_UNREACHABLE();
|
||||
}
|
||||
|
|
@ -1660,13 +1664,16 @@ namespace spot
|
|||
/// This does a simple DFS without checking for duplicate
|
||||
/// subformulas. If \a func returns true, the children of the
|
||||
/// current node are skipped.
|
||||
template<typename Func>
|
||||
void traverse(Func func)
|
||||
///
|
||||
/// Any additional argument is passed to \a func when it is
|
||||
/// invoked.
|
||||
template<typename Func, typename... Args>
|
||||
void traverse(Func func, Args&&... args)
|
||||
{
|
||||
if (func(*this))
|
||||
if (func(*this, std::forward<Args>(args)...))
|
||||
return;
|
||||
for (auto f: *this)
|
||||
f.traverse(func);
|
||||
f.traverse(func, std::forward<Args>(args)...);
|
||||
}
|
||||
|
||||
private:
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue