From 3c0aecf4e6b493565938038a74ab5921e20f2190 Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Thu, 20 Apr 2017 18:25:49 +0200 Subject: [PATCH] Add a genaut binary. Similarly to genltl that generates LTL formulas for various classes that appear in the literature, genaut generates automata. * NEWS: Mention the modification. * bin/Makefile.am: Build the new binary. * bin/genaut.cc: The new binary itself. --- NEWS | 5 ++ bin/Makefile.am | 5 +- bin/genaut.cc | 199 ++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 208 insertions(+), 1 deletion(-) create mode 100644 bin/genaut.cc diff --git a/NEWS b/NEWS index 9c9c56fd1..699775ede 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,11 @@ New in spot 2.3.3.dev (not yet released) - In autfilt, the option --dualize is now available to obtain the dual of any automaton. + - Add a new binary: genaut. Similarly to genltl that produces LTL + formulas from the literature, this tool produces automata from + the literature. It currently features only one class of + automata. + Library: - Add a new library libspotgen. It is intended to be place to gather diff --git a/bin/Makefile.am b/bin/Makefile.am index 85e5ca059..761474db2 100644 --- a/bin/Makefile.am +++ b/bin/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +## Copyright (C) 2012, 2013, 2014, 2015, 2016-2017 Laboratoire de Recherche ## et Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -58,6 +58,7 @@ libcommon_a_SOURCES = \ bin_PROGRAMS = \ autfilt \ dstar2tgba \ + genaut \ genltl \ ltl2tgba \ ltl2tgta \ @@ -75,6 +76,8 @@ noinst_PROGRAMS = spot-x spot autfilt_SOURCES = autfilt.cc ltlfilt_SOURCES = ltlfilt.cc +genaut_SOURCES = genaut.cc +genaut_LDADD = $(top_builddir)/spot/gen/libspotgen.la $(LDADD) genltl_SOURCES = genltl.cc randaut_SOURCES = randaut.cc randltl_SOURCES = randltl.cc diff --git a/bin/genaut.cc b/bin/genaut.cc new file mode 100644 index 000000000..0e0526566 --- /dev/null +++ b/bin/genaut.cc @@ -0,0 +1,199 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 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 3 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 this program. If not, see . + +#include "common_sys.hh" + +#include +#include +#include +#include +#include "error.h" +#include + +#include "common_setup.hh" +#include "common_aoutput.hh" +#include "common_range.hh" +#include "common_cout.hh" + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +using namespace spot; + +const char argp_program_doc[] ="\ +Generate omega automata from predefined patterns."; + +enum { + FIRST_CLASS = 256, + OPT_KS_COBUCHI = FIRST_CLASS, + LAST_CLASS, +}; +/* +const char* const class_name[LAST_CLASS - FIRST_CLASS] = + { + "ks-cobuchi", + }; +*/ + +#define OPT_ALIAS(o) { #o, 0, nullptr, OPTION_ALIAS, nullptr, 0 } + +static const argp_option options[] = + { + /**************************************************/ + // Keep this alphabetically sorted (expect for aliases). + { nullptr, 0, nullptr, 0, "Pattern selection:", 1}, + { "ks-cobuchi", OPT_KS_COBUCHI, "N", 0, + "A co-Bûchi automaton with 2N+1 states for which any equivalent " + "deterministic co-Büchi automaton has at least 2^N/(2N+1) states.", 0}, + /**************************************************/ + { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, + { nullptr, 0, nullptr, 0, nullptr, 0 } + }; + +struct job +{ + int pattern; + struct range range; +}; + +typedef std::vector jobs_t; +static jobs_t jobs; + +const struct argp_child children[] = + { + { &aoutput_argp, 0, nullptr, -20 }, + { &misc_argp, 0, nullptr, -1 }, + { nullptr, 0, nullptr, 0 } + }; + +static void +enqueue_job(int pattern, const char* range_str) +{ + job j; + j.pattern = pattern; + j.range = parse_range(range_str); + jobs.push_back(j); +} +/* +static void +enqueue_job(int pattern, int min, int max) +{ + job j; + j.pattern = pattern; + j.range = {min, max}; + jobs.push_back(j); +} +*/ +static int +parse_opt(int key, char* arg, struct argp_state*) +{ + // This switch is alphabetically-ordered. + switch (key) + { + case OPT_KS_COBUCHI: + enqueue_job(key, arg); + break; + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} +/* +static void +bad_number(const char* pattern, int n, int max = 0) +{ + std::ostringstream err; + err << "no pattern " << n << " for " << pattern + << ", supported range is 1.."; + if (max) + err << max; + throw std::runtime_error(err.str()); +} +*/ +static void +output_pattern(int pattern, int n) +{ + twa_graph_ptr aut = nullptr; + switch (pattern) + { + // Keep this alphabetically-ordered! + case OPT_KS_COBUCHI: + aut = spot::gen::ks_cobuchi(n); + break; + default: + error(100, 0, "internal error: pattern not implemented"); + } + + process_timer timer; + automaton_printer printer; + printer.print(aut, timer); +} + +static void +run_jobs() +{ + for (auto& j: jobs) + { + int inc = (j.range.max < j.range.min) ? -1 : 1; + int n = j.range.min; + for (;;) + { + output_pattern(j.pattern, n); + if (n == j.range.max) + break; + n += inc; + } + } +} + + +int +main(int argc, char** argv) +{ + setup(argv); + + const argp ap = { options, parse_opt, nullptr, argp_program_doc, + children, nullptr, nullptr }; + + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) + exit(err); + + if (jobs.empty()) + error(1, 0, "Nothing to do. Try '%s --help' for more information.", + program_name); + + try + { + run_jobs(); + } + catch (const std::runtime_error& e) + { + error(2, 0, "%s", e.what()); + } + + flush_cout(); + return 0; +}