diff --git a/NEWS b/NEWS index 05af3081f..cbcfe8b28 100644 --- a/NEWS +++ b/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 diff --git a/doc/org/tut03.org b/doc/org/tut03.org index 0ea13b88a..945c4ad0d 100644 --- a/doc/org/tut03.org +++ b/doc/org/tut03.org @@ -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 #include @@ -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 #include @@ -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 + #include + #include + #include + + 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 + #include + #include + #include + + 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 + #include + #include + #include + + 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. diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 5c07028c8..acaad47c0 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -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") diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index e596dec96..59cdf4883 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -1602,8 +1602,10 @@ namespace spot #undef SPOT_DEF_PROP /// \brief Clone this node after applying \a trans to its children. - template - formula map(Trans trans) + /// + /// Any additional argument is passed to trans. + template + 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)...)); 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)...); + return binop(o, tmp, + trans((*this)[1], std::forward(args)...)); } case op::Or: case op::OrRat: @@ -1645,12 +1648,13 @@ namespace spot std::vector tmp; tmp.reserve(size()); for (auto f: *this) - tmp.emplace_back(trans(f)); + tmp.emplace_back(trans(f, std::forward(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)...), + 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 - void traverse(Func func) + /// + /// Any additional argument is passed to \a func when it is + /// invoked. + template + void traverse(Func func, Args&&... args) { - if (func(*this)) + if (func(*this, std::forward(args)...)) return; for (auto f: *this) - f.traverse(func); + f.traverse(func, std::forward(args)...); } private: