diff --git a/ChangeLog b/ChangeLog index 606871c68..1fc464767 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2010-12-04 Alexandre Duret-Lutz + + Preliminary implementation of a tool to generate some interesting + families of LTL formulae. + + * src/ltltest/genltl.cc: New file. Based on five classes of + formulae defined in a paper by Cichón, Czubak, and JasiÅ„ski. + * src/ltltest/Makefile.am (noinst_PROGRAMS): Build genltl. + 2010-12-03 Alexandre Duret-Lutz Add full_parent support to to_spin_string(). @@ -587,7 +596,7 @@ Optimize tgba_tba_proxy and tgba_sba_proxy for states that share an acceptance condition on all outgoing transitions. - This was motivated by experiments from Rüdiger Ehlers, showing + This was motivated by experiments from Rüdiger Ehlers, showing that "ltl2ba -f 'a U (b U c)'" outperformed "ltl2tgba -f -N -R3 'a U (b U c)'". With this change and the previous one, it is no longer the case. @@ -610,7 +619,7 @@ * src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the degeneralization, because it might remove useless acceptance conditions. I realized this while looking at experiments from - Rüdiger Ehlers. + Rüdiger Ehlers. 2010-02-24 Alexandre Duret-Lutz @@ -620,7 +629,7 @@ Work around a spurious style.test error. - * src/saba/sabacomplementtgba.hh (spot): Rewrite Büchi as B\"uchi + * src/saba/sabacomplementtgba.hh (spot): Rewrite Büchi as B\"uchi is the BibTex entry used as comment, because some version of sed will choke on non-ascii character and cause sanity/style.test to fail. @@ -1242,12 +1251,12 @@ 2009-11-30 Guillaume Sadegh - Add a new type of automata: State-labeled Alternating Büchi + Add a new type of automata: State-labeled Alternating Büchi Automata (SABA). * src/saba/saba.hh, src/saba/saba.cc, src/saba/sabastate.hh, src/saba/sabasucciter.hh: New. Interface for - SABA (State-labeled Alternating Büchi Automata). + SABA (State-labeled Alternating Büchi Automata). * src/saba/explicitstateconjunction.cc, src/saba/explicitstateconjunction.hh: New. Default implementation for a conjunction of states. @@ -1843,7 +1852,7 @@ 2009-10-07 Alexandre Duret-Lutz - * AUTHORS: Add Damien Lefortier, Guillaume Sadegh, and Félix + * AUTHORS: Add Damien Lefortier, Guillaume Sadegh, and Félix Abecassis. 2009-10-01 Guillaume Sadegh @@ -2043,7 +2052,7 @@ * src/tgba/tgbacomplement.cc: Stay on 80 columns. -2009-07-08 Félix Abecassis +2009-07-08 Félix Abecassis Add 2 benchmarks directories. Add an algorithm to split an automaton in several automata. @@ -2095,7 +2104,7 @@ automaton into a TGBA instead of a TBA. * src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: - Adjust the transformation from Streett to Büchi to support + Adjust the transformation from Streett to Büchi to support generalized acceptance conditions. * src/tgbatest/complementation.cc: Improve output messages. * src/tgbatest/complementation.test: New tests. @@ -2125,7 +2134,7 @@ 2009-06-05 Guillaume Sadegh - Add an algorithm to complement Büchi automata. + Add an algorithm to complement Büchi automata. * src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: New files. The complementation algorithm. @@ -4944,10 +4953,10 @@ * src/tgbaalgos/gtec/ce.cc (counter_example::counter_example): Do not parenthesize the type after the new operator (g++ 3.4 complains). * src/tgbaalgos/dupexp.cc (dupexp_iter::process_state, - dupexp_iter::declare_state): Use this->automata_ instead of + dupexp_iter::declare_state): Use this->automata_ instead of automata_. Local protected member automata_ inherited from template base class must be prefixed or g++ 3.4 will not look it - up (conforming to §14.6.2.3). + up (conforming to §14.6.2.3). 2004-07-07 Alexandre Duret-Lutz @@ -8208,7 +8217,7 @@ not a bdd. * src/tgba/tgbabddconcrete.cc: Likewise. - Initial code for TGBA (Transition Generalized Büchi Automata). + Initial code for TGBA (Transition Generalized Büchi Automata). Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba, a LTL-to-TGBA translator using Couvreur's algorithm. diff --git a/src/ltltest/.gitignore b/src/ltltest/.gitignore index 286fb15c1..2b95bf96c 100644 --- a/src/ltltest/.gitignore +++ b/src/ltltest/.gitignore @@ -21,3 +21,4 @@ randltl *.dot reductau reductaustr +genltl diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index a9d9bb6d9..1ab89725e 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2009 Laboratoire de Recherche et Développement +## Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -43,6 +43,7 @@ check_PROGRAMS = \ tunenoform noinst_PROGRAMS = \ + genltl \ randltl equals_SOURCES = equals.cc diff --git a/src/ltltest/genltl.cc b/src/ltltest/genltl.cc new file mode 100644 index 000000000..c3a60fce2 --- /dev/null +++ b/src/ltltest/genltl.cc @@ -0,0 +1,261 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include +#include +#include +#include +#include +#include +#include "ltlast/allnodes.hh" +#include "ltlvisit/tostring.hh" +#include "ltlenv/defaultenv.hh" + +using namespace spot; +using namespace spot::ltl; + +environment& env(default_environment::instance()); + + + +// The five first classes defined here come from the following paper: +// +// @InProceedings{cichon.09.depcos, +// author = {Jacek Cicho{\'n} and Adam Czubak and Andrzej Jasi{\'n}ski}, +// title = {Minimal {B\"uchi} Automata for Certain Classes of {LTL} Formulas}, +// booktitle = {Proceedings of the Fourth International Conference on +// Dependability of Computer Systems}, +// pages = {17--24}, +// year = 2009, +// publisher = {IEEE Computer Society}, +// } + +void +syntax(char* prog) +{ + std::cerr << "Usage: "<< prog << " [-s] F N" << std::endl + << std::endl + << "-s output using Spin's syntax" << std::endl + << "F specifies the familly of LTL formula to build" << std::endl + << "N is the size parameter of the familly" << std::endl + << std::endl + << "Classes available (F):" << std::endl + << " 1: F(p1&F(p2&F(p3&...F(pn)))) & F(q1&F(q2&F(q3&...F(qn))))" + << std::endl + << " 2: p&X(p&X(p&...X(p)))) & X(q&F(q&F(q&...F(q))))" + << std::endl + << " 3: p&(Xp)&(XXp)&...(X...X(p)) & p&(Xq)&(XXq)&...(X...X(q))" + << std::endl + << " 4: GF(p1)&GF(p2)&...&GF(pn)" + << std::endl + << " 5: FG(p1)|GF(p2)|...|GF(pn)" + << std::endl; + exit(2); +} + +int +to_int(const char* s) +{ + char* endptr; + int res = strtol(s, &endptr, 10); + if (*endptr) + { + std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl; + exit(1); + } + return res; +} + + +// F(p_1 & F(p_2 & F(p_3 & ... F(p_n)))) +formula* E_n(std::string name, int n) +{ + if (n <= 0) + return constant::true_instance(); + + formula* result = 0; + + for (; n > 0; --n) + { + std::ostringstream p; + p << name << n; + formula* f = env.require(p.str()); + if (result) + result = multop::instance(multop::And, f, result); + else + result = f; + result = unop::instance(unop::F, result); + } + return result; +} + +// p & X(p & X(p & ... X(p))) +formula* phi_n(std::string name, int n) +{ + if (n <= 0) + return constant::true_instance(); + + formula* result = 0; + formula* p = env.require(name); + for (; n > 0; --n) + { + if (result) + result = + multop::instance(multop::And, p->clone(), + unop::instance(unop::X, result)); + else + result = p; + } + return result; +} + +formula* N_n(std::string name, int n) +{ + return unop::instance(unop::F, phi_n(name, n)); +} + +// p & X(p) & XX(p) & XXX(p) & ... X^n(p) +formula* phi_prime_n(std::string name, int n) +{ + if (n <= 0) + return constant::true_instance(); + + formula* result = 0; + formula* p = env.require(name); + for (; n > 0; --n) + { + if (result) + { + p = unop::instance(unop::X, p->clone()); + result = multop::instance(multop::And, result, p); + } + else + { + result = p; + } + } + return result; +} + +formula* N_prime_n(std::string name, int n) +{ + return unop::instance(unop::F, phi_prime_n(name, n)); +} + + +// GF(p_1) | GF(p_2) | ... | GF(p_n) +formula* FG_n(std::string name, int n) +{ + if (n <= 0) + return constant::true_instance(); + + formula* result = 0; + + for (int i = 1; i <= n; ++i) + { + std::ostringstream p; + p << name << i; + formula* f = unop::instance(unop::G, + unop::instance(unop::F, + env.require(p.str()))); + + if (result) + result = multop::instance(multop::And, f, result); + else + result = f; + } + return result; +} + +// FG(p_1) | FG(p_2) | ... | FG(p_n) +formula* GF_n(std::string name, int n) +{ + if (n <= 0) + return constant::false_instance(); + + formula* result = 0; + + for (int i = 1; i <= n; ++i) + { + std::ostringstream p; + p << name << i; + formula* f = unop::instance(unop::F, + unop::instance(unop::G, + env.require(p.str()))); + + if (result) + result = multop::instance(multop::Or, f, result); + else + result = f; + } + return result; +} + +int +main(int argc, char** argv) +{ + bool spin_syntax = false; + if (argc >= 2 && !strcmp(argv[1], "-s")) + { + spin_syntax = true; + --argc; + ++argv; + } + + if (argc != 3) + syntax(argv[0]); + + int f = to_int(argv[1]); + int n = to_int(argv[2]); + + formula* res = 0; + + switch (f) + { + case 1: + res = multop::instance(multop::And, E_n("p", n), E_n("q", n)); + break; + case 2: + res = multop::instance(multop::And, N_n("p", n), N_n("q", n)); + break; + case 3: + res = multop::instance(multop::And, N_prime_n("p", n), N_prime_n("q", n)); + break; + case 4: + res = FG_n("p", n); + break; + case 5: + res = GF_n("p", n); + break; + default: + std::cerr << "Unknown familly " << f << std::endl; + break; + } + + if (spin_syntax) + to_spin_string(res, std::cout, true) << std::endl; + else + to_string(res, std::cout, true) << std::endl; + + res->destroy(); + + return 0; +}