From a0e1a144ad6ab4bc4e9f98fac46c654860d662c4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 31 Aug 2012 13:41:22 +0200 Subject: [PATCH] ltlfilt: initial implementation. * src/bin/ltlfilt.cc, src/bin/Makefile.am: New files. * src/Makefile.am (SUBDIRS): Add bin. * configure.ac: Add src/bin/Makefile.am. * README: Document src/bin/. --- README | 1 + configure.ac | 1 + src/Makefile.am | 2 +- src/bin/.gitignore | 1 + src/bin/Makefile.am | 27 +++ src/bin/ltlfilt.cc | 562 ++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 593 insertions(+), 1 deletion(-) create mode 100644 src/bin/.gitignore create mode 100644 src/bin/Makefile.am create mode 100644 src/bin/ltlfilt.cc diff --git a/README b/README index 13804f257..2363061f2 100644 --- a/README +++ b/README @@ -143,6 +143,7 @@ src/ Sources for libspot. sabaalgos/ Algorithms on SABA. sabatest/ Tests for saba/, sabaalgos/. neverparse/ Parser for SPIN never claims. + bin/ User tools built using the Spot library. sanity/ Sanity tests for the whole project. doc/ Documentation for libspot. tl/ Documentation of the Temporal Logic operators. diff --git a/configure.ac b/configure.ac index bf61e9db7..1c37ccd46 100644 --- a/configure.ac +++ b/configure.ac @@ -125,6 +125,7 @@ AC_CONFIG_FILES([ iface/gspn/defs iface/gspn/Makefile iface/Makefile + src/bin/Makefile src/eltlparse/Makefile src/eltltest/defs src/eltltest/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index 824ec2fbd..50c0207d7 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -30,7 +30,7 @@ AUTOMAKE_OPTIONS = subdir-objects SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse tgba \ tgbaalgos tgbaparse ta taalgos evtgba evtgbaalgos \ evtgbaparse kripke saba sabaalgos neverparse kripkeparse \ - . ltltest eltltest tgbatest evtgbatest sabatest sanity \ + . bin ltltest eltltest tgbatest evtgbatest sabatest sanity \ kripketest lib_LTLIBRARIES = libspot.la diff --git a/src/bin/.gitignore b/src/bin/.gitignore new file mode 100644 index 000000000..8cd80703b --- /dev/null +++ b/src/bin/.gitignore @@ -0,0 +1 @@ +ltlfilt diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am new file mode 100644 index 000000000..56c0ff5ef --- /dev/null +++ b/src/bin/Makefile.am @@ -0,0 +1,27 @@ +## -*- coding: utf-8 -*- +## Copyright (C) 2012 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. + +AM_CPPFLAGS = -I$(top_srcdir)/src $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) +LDADD = $(top_builddir)/src/libspot.la + +bin_PROGRAMS = ltlfilt +ltlfilt_SOURCES = ltlfilt.cc diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc new file mode 100644 index 000000000..e417e6f09 --- /dev/null +++ b/src/bin/ltlfilt.cc @@ -0,0 +1,562 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 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. + +#ifdef HAVE_CONFIG_H +# include "config.h" +#endif + +#include +#include +#include +#include +#include +#include +#include "misc/_config.h" +#include "misc/hash.hh" +#include "ltlparse/public.hh" +#include "ltlvisit/tostring.hh" +#include "ltlvisit/simplify.hh" +#include "ltlvisit/length.hh" +#include "ltlast/unop.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" +#include "tgbaalgos/minimize.hh" +#include "tgbaalgos/safety.hh" + +const char* argp_program_version = "\ +ltlfilter (" SPOT_PACKAGE_STRING ")\n\ +\n\ +Copyright (C) 2012 Laboratoire de Recherche et Développement de l'Epita.\n\ +This is free software; see the source for copying conditions. There is NO\n\ +warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE,\n\ +to the extent permitted by law."; + +const char* argp_program_bug_address = "<" SPOT_PACKAGE_BUGREPORT ">"; + +const char argp_program_doc[] ="\ +Read a list of formulas and output them back after some optional processing."; + +#define OPT_SPOT 1 +#define OPT_SKIP_ERRORS 3 +#define OPT_DROP_ERRORS 4 +#define OPT_NNF 5 +#define OPT_LTL 10 +#define OPT_PSL 11 +#define OPT_NOX 12 +#define OPT_BOOLEAN 13 +#define OPT_EVENTUAL 14 +#define OPT_UNIVERSAL 15 +#define OPT_SYNTACTIC_SAFETY 16 +#define OPT_SYNTACTIC_GUARANTEE 17 +#define OPT_SYNTACTIC_OBLIGATION 18 +#define OPT_SYNTACTIC_RECURRENCE 19 +#define OPT_SYNTACTIC_PERSISTENCE 20 +#define OPT_SAFETY 21 +#define OPT_GUARANTEE 22 +#define OPT_OBLIGATION 23 +#define OPT_SIZE_MIN 24 +#define OPT_SIZE_MAX 25 +#define OPT_BSIZE_MIN 26 +#define OPT_BSIZE_MAX 27 + +static const argp_option options[] = + { + /**************************************************/ + { 0, 0, 0, 0, "Input options:", 1 }, + { "formula", 'f', "STRING", 0, "process the formula STRING", 0 }, + { "file", 'F', "FILENAME", 0, + "process each line of FILENAME as a formula", 0 }, + { 0, 0, 0, 0, "Error handling:", 2 }, + { "skip-errors", OPT_SKIP_ERRORS, 0, 0, + "output erroneous lines as-is without processing", 0 }, + { "drop-errors", OPT_DROP_ERRORS, 0, 0, + "discard erroneous lines (default)", 0 }, + { "quiet", 'q', 0, 0, "do not report syntax errors", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Transformation options:", 3 }, + { "negate", 'n', 0, 0, "negate each formula", 0 }, + { "nnf", OPT_NNF, 0, 0, "rewrite formulas in negative normal form", 0 }, + { "simplify", 'r', "LEVEL", OPTION_ARG_OPTIONAL, + "simplify formulas according to LEVEL (see below)", 0 }, + { 0, 0, 0, 0, " The simplification LEVEL might be one of:", 4 }, + { " 0", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "No rewriting", 0 }, + { " 1", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "basic rewritings and eventual/universal rules", 0 }, + { " 2", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "additional syntactic implication rules", 0 }, + { " 3", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "better implications using containment (default)", 0 }, + /**************************************************/ + { 0, 0, 0, 0, + "Filtering options (matching is done after transformation):", 5 }, + { "ltl", OPT_LTL, 0, 0, "match LTL formulas", 0 }, + { "psl", OPT_PSL, 0, 0, "match PSL formulas", 0 }, + { "nox", OPT_NOX, 0, 0, "match X-free formulas", 0 }, + { "boolean", OPT_BOOLEAN, 0, 0, "match Boolean formulas", 0 }, + { "eventual", OPT_EVENTUAL, 0, 0, "match pure eventualities", 0 }, + { "universal", OPT_UNIVERSAL, 0, 0, "match purely universal formulas", 0 }, + { "syntactic-safety", OPT_SYNTACTIC_SAFETY, 0, 0, + "match syntactic-safety formulas", 0 }, + { "syntactic-guarantee", OPT_SYNTACTIC_GUARANTEE, 0, 0, + "match syntactic-guarantee formulas", 0 }, + { "syntactic-obligation", OPT_SYNTACTIC_OBLIGATION, 0, 0, + "match syntactic-obligation formulas", 0 }, + { "syntactic-recurrence", OPT_SYNTACTIC_RECURRENCE, 0, 0, + "match syntactic-recurrence formulas", 0 }, + { "syntactic-persistence", OPT_SYNTACTIC_PERSISTENCE, 0, 0, + "match syntactic-persistence formulas", 0 }, + { "safety", OPT_SAFETY, 0, 0, + "match safety formulas (even pathological)", 0 }, + { "guarantee", OPT_GUARANTEE, 0, 0, + "match guarantee formulas (even pathological)", 0 }, + { "obligation", OPT_OBLIGATION, 0, 0, + "match obligation formulas (even pathological)", 0 }, + { "size-max", OPT_SIZE_MAX, "INT", 0, + "match formulas with size <= INT", 0 }, + { "size-min", OPT_SIZE_MIN, "INT", 0, + "match formulas with size >= INT", 0 }, + { "bsize-max", OPT_BSIZE_MAX, "INT", 0, + "match formulas with Boolean size <= INT", 0 }, + { "bsize-min", OPT_BSIZE_MIN, "INT", 0, + "match formulas with Boolean size >= INT", 0 }, + { "invert-match", 'v', 0, 0, "Select non-matching formulas", 0}, + /**************************************************/ + { 0, 0, 0, 0, "Output options:", 6 }, + { "full-parentheses", 'p', 0, 0, + "output fully-parenthesized formulas", 0 }, + { "spin", 's', 0, 0, "output in Spin's syntax", 0 }, + { "spot", OPT_SPOT, 0, 0, "output in Spot's syntax (default)", 0 }, + { "utf8", '8', 0, 0, "output using UTF-8 characters", 0 }, + { "unique", 'u', 0, 0, "drop formulas that have already been outpout", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Miscellaneous options:", -1 }, + { 0, 0, 0, 0, 0, 0 } + }; + +struct job +{ + const char* str; + bool file_p; // true if str is a filename, false if it is a formula + + job(const char* str, bool file_p) + : str(str), file_p(file_p) + { + } +}; + +typedef std::vector jobs_t; +static jobs_t jobs; + +enum error_style_t { drop_errors, skip_errors }; +static error_style_t error_style = drop_errors; +static bool quiet = false; +enum output_format_t { spot_output, spin_output, utf8_output }; +static output_format_t output_format = spot_output; +static bool full_parenth = false; +static bool nnf = false; +static bool negate = false; +static int level = 0; +static bool unique = false; +static bool psl = false; +static bool ltl = false; +static bool nox = false; +static bool invert = false; +static bool boolean = false; +static bool universal = false; +static bool eventual = false; +static bool syntactic_safety = false; +static bool syntactic_guarantee = false; +static bool syntactic_obligation = false; +static bool syntactic_recurrence = false; +static bool syntactic_persistence = false; +static bool safety = false; +static bool guarantee = false; +static bool obligation = false; +static int size_min = -1; +static int size_max = -1; +static int bsize_min = -1; +static int bsize_max = -1; + +static 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; +} + +static int +parse_opt(int key, char* arg, struct argp_state* state) +{ + (void) state; + // This switch is alphabetically-ordered. + switch (key) + { + case '8': + output_format = utf8_output; + break; + case 'f': + jobs.push_back(job(arg, false)); + break; + case 'F': + jobs.push_back(job(arg, true)); + break; + case 'n': + negate = true; + break; + case 'p': + full_parenth = true; + break; + case 'q': + quiet = true; + break; + case 'r': + if (!arg) + { + level = 3; + break; + } + else + { + if (arg[1] == 0) + switch (arg[0]) + { + case '0': + case '1': + case '2': + case '3': + level = arg[0] = '0'; + return 0; + } + std::cerr << "Invalid simplification LEVEL: " << arg << "\n"; + return 1; + } + break; + case 's': + output_format = spin_output; + break; + case 'u': + unique = true; + break; + case 'v': + invert = true; + break; + case ARGP_KEY_ARG: + // FIXME: use stat() to distinguish filename from string? + jobs.push_back(job(arg, true)); + break; + case OPT_BOOLEAN: + boolean = true; + break; + case OPT_BSIZE_MIN: + bsize_min = to_int(arg); + break; + case OPT_BSIZE_MAX: + bsize_max = to_int(arg); + break; + case OPT_DROP_ERRORS: + error_style = drop_errors; + break; + case OPT_GUARANTEE: + guarantee = obligation = true; + break; + case OPT_LTL: + ltl = true; + break; + case OPT_NNF: + nnf = true; + break; + case OPT_NOX: + nox = true; + break; + case OPT_OBLIGATION: + obligation = true; + break; + case OPT_PSL: + psl = true; + break; + case OPT_SAFETY: + safety = obligation = true; + break; + case OPT_SIZE_MIN: + size_min = to_int(arg); + break; + case OPT_SIZE_MAX: + size_max = to_int(arg); + break; + case OPT_SKIP_ERRORS: + error_style = skip_errors; + break; + case OPT_SPOT: + output_format = spot_output; + break; + case OPT_SYNTACTIC_SAFETY: + syntactic_safety = true; + break; + case OPT_SYNTACTIC_GUARANTEE: + syntactic_guarantee = true; + break; + case OPT_SYNTACTIC_OBLIGATION: + syntactic_obligation = true; + break; + case OPT_SYNTACTIC_RECURRENCE: + syntactic_recurrence = true; + break; + case OPT_SYNTACTIC_PERSISTENCE: + syntactic_persistence = true; + break; + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + +typedef Sgi::hash_set > fset_t; + +namespace +{ + class ltl_processor + { + public: + spot::ltl::ltl_simplifier& simpl; + fset_t unique_set; + + ltl_processor(spot::ltl::ltl_simplifier& simpl) + : simpl(simpl) + { + } + + int + process_formula(const std::string& input, + const char* filename = 0, int linenum = 0) + { + spot::ltl::parse_error_list pel; + const spot::ltl::formula* f = spot::ltl::parse(input, pel); + + if (!f || pel.size() > 0) + { + if (!quiet) + { + if (filename) + std::cerr << "at " << filename << ":" << linenum << ":\n"; + spot::ltl::format_parse_errors(std::cerr, input, pel); + } + + if (f) + f->destroy(); + + if (error_style == drop_errors) + return 1; + if (error_style == skip_errors) + { + std::cout << input << std::endl; + return 1; + } + assert(!"unreachable"); + } + + + if (negate) + { + f = spot::ltl::unop::instance(spot::ltl::unop::Not, f); + } + + if (level) + { + const spot::ltl::formula* res = simpl.simplify(f); + f->destroy(); + f = res; + } + + if (nnf) + { + const spot::ltl::formula* res = simpl.negative_normal_form(f); + f->destroy(); + f = res; + } + + bool matched = true; + + matched &= !ltl || f->is_ltl_formula(); + matched &= !psl || f->is_psl_formula(); + matched &= !nox || f->is_X_free(); + matched &= !boolean || f->is_boolean(); + matched &= !universal || f->is_universal(); + matched &= !eventual || f->is_eventual(); + matched &= !syntactic_safety || f->is_syntactic_safety(); + matched &= !syntactic_guarantee || f->is_syntactic_guarantee(); + matched &= !syntactic_obligation || f->is_syntactic_obligation(); + matched &= !syntactic_recurrence || f->is_syntactic_recurrence(); + matched &= !syntactic_persistence || f->is_syntactic_persistence(); + + if (matched && (size_min > 0 || size_max >= 0)) + { + int l = spot::ltl::length(f); + matched &= (size_min <= 0) || (l >= size_min); + matched &= (size_max < 0) || (l <= size_max); + } + + if (matched && (bsize_min > 0 || bsize_max >= 0)) + { + int l = spot::ltl::length_boolone(f); + matched &= (bsize_min <= 0) || (l >= bsize_min); + matched &= (bsize_max < 0) || (l <= bsize_max); + } + + // Match obligations and subclasses using WDBA minimization. + // Because this is costly, we compute it later, so that we don't + // have to compute it on formulas that have been discarded for + // other reasons. + if (matched && obligation) + { + spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict()); + spot::tgba* min = minimize_obligation(aut, f); + assert(min); + if (aut == min) + { + // Not an obligation + matched = false; + } + else + { + matched &= !guarantee || is_guarantee_automaton(min); + matched &= !safety || is_safety_mwdba(min); + delete min; + } + delete aut; + } + + matched ^= invert; + + if (unique) + { + if (unique_set.insert(f).second) + f->clone(); + else + matched = false; + } + + if (matched) + { + switch (output_format) + { + case spot_output: + spot::ltl::to_string(f, std::cout, full_parenth); + break; + case spin_output: + spot::ltl::to_spin_string(f, std::cout, full_parenth); + break; + case utf8_output: + spot::ltl::to_utf8_string(f, std::cout, full_parenth); + break; + } + std::cout << "\n"; + } + + f->destroy(); + return 0; + } + + int + process_file(const char* filename) + { + int error = 0; + int linenum = 0; + std::string line; + // Special case for stdin. + if (filename[0] == '-' && filename[1] == 0) + { + while (std::getline(std::cin, line)) + error |= process_formula(line, "stdin", ++linenum); + return error; + } + + std::ifstream input(filename); + if (!input) + { + std::cerr << "cannot open " << filename << std::endl; + return 1; + } + while (std::getline(input, line)) + error |= process_formula(line, filename, ++linenum); + return error; + } + + }; +} + +static int +run_jobs() +{ + spot::ltl::ltl_simplifier_options options; + + switch (level) + { + case 3: + options.containment_checks = true; + options.containment_checks_stronger = true; + // fall through + case 2: + options.synt_impl = true; + // fall through + case 1: + options.reduce_basics = true; + options.event_univ = true; + // fall through + default: + break; + } + + spot::ltl::ltl_simplifier simpl(options); + ltl_processor processor(simpl); + + int error = 0; + jobs_t::const_iterator i; + for (i = jobs.begin(); i != jobs.end(); ++i) + { + if (!i->file_p) + error |= processor.process_formula(i->str); + else + error |= processor.process_file(i->str); + } + return error; +} + +int +main(int argc, char** argv) +{ + const argp ap = { options, parse_opt, "[FILENAME...]", + argp_program_doc, 0, 0, 0 }; + + if (int err = argp_parse(&ap, argc, argv, 0, 0, 0)) + exit(err); + + if (jobs.empty()) + jobs.push_back(job("-", 1)); + + return run_jobs(); +}