alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlfilt, genltl: factor the common output options.

Browse source 
* src/bin/common_output.cc, src/bin/common_output.hh: New file
with the common output code.
* src/bin/Makefile.am: Add them.
* src/bin/genltl.cc, src/bin/ltlfilt.cc: Simplify, using
argp's children parser, and calling output_formula().
This commit is contained in:
Alexandre Duret-Lutz 2012-09-03 19:31:29 +02:00
parent 267183bda7
commit e0873cc7d6
5 changed files with 155 additions and 86 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/bin/Makefile.am
View file

@ -25,5 +25,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
LDADD = $(top_builddir)/src/libspot.la $(top_builddir)/lib/libgnu.a
bin_PROGRAMS = ltlfilt genltl
ltlfilt_SOURCES = ltlfilt.cc
genltl_SOURCES = genltl.cc
ltlfilt_SOURCES = ltlfilt.cc common_output.cc
genltl_SOURCES = genltl.cc common_output.cc
noinst_HEADERS = common_output.hh

82
src/bin/common_output.cc Normal file
View file

@ -0,0 +1,82 @@
// -*- 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.
#include "common_output.hh"
#include <iostream>
#define OPT_SPOT 1
output_format_t output_format = spot_output;
bool full_parenth = false;
static const argp_option options[] =
{
{ "full-parentheses", 'p', 0, 0,
"output fully-parenthesized formulas", -20 },
{ "spin", 's', 0, 0, "output in Spin's syntax", -20 },
{ "spot", OPT_SPOT, 0, 0, "output in Spot's syntax (default)", -20 },
{ "utf8", '8', 0, 0, "output using UTF-8 characters", -20 },
{ 0, 0, 0, 0, 0, 0 }
};
const struct argp output_argp = { options, parse_opt_output, 0, 0, 0, 0, 0 };
int
parse_opt_output(int key, char*, struct argp_state*)
{
// This switch is alphabetically-ordered.
switch (key)
{
case '8':
output_format = utf8_output;
break;
case 'p':
full_parenth = true;
break;
case 's':
output_format = spin_output;
break;
case OPT_SPOT:
output_format = spot_output;
break;
default:
return ARGP_ERR_UNKNOWN;
}
return 0;
}
void
output_formula(const spot::ltl::formula* f)
{
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";
}

41
src/bin/common_output.hh Normal file
View file

@ -0,0 +1,41 @@
// -*- 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.
#ifndef SPOT_BIN_COMMON_OUTPUT_HH
#define SPOT_BIN_COMMON_OUTPUT_HH
#ifdef HAVE_CONFIG_H
# include "config.h"
#endif
#include <argp.h>
#include "ltlvisit/tostring.hh"
enum output_format_t { spot_output, spin_output, utf8_output };
extern output_format_t output_format;
extern bool full_parenth;
extern const struct argp output_argp;
int parse_opt_output(int key, char* arg, struct argp_state* state);
void output_formula(const spot::ltl::formula* f);
#endif // SPOT_BIN_COMMON_OUTPUT_HH

55
src/bin/genltl.cc
View file

@ -80,8 +80,9 @@
#include "error.h"
#include <vector>
#include "misc/_config.h"
#include "common_output.hh"
#include "misc/_config.h"
#include <cassert>
#include <iostream>
#include <sstream>
@ -90,7 +91,6 @@
#include <cstdlib>
#include <cstring>
#include "ltlast/allnodes.hh"
#include "ltlvisit/tostring.hh"
#include "ltlenv/defaultenv.hh"
using namespace spot;
@ -121,8 +121,6 @@ Translation. LNCS 2102\n\
[rv] K. Rozier and M. Vardi (Spin'07): LTL Satisfiability Checking. \
LNCS 4595.\n";
#define OPT_SPOT 1
#define OPT_AND_F 2
#define OPT_AND_FG 3
#define OPT_AND_GF 4
@ -192,14 +190,8 @@ static const argp_option options[] =
{ "u-right", OPT_U_RIGHT, "RANGE", 0, "(p1 U (p2 U (... U pn)))", 0 },
OPT_ALIAS(gh-u2),
OPT_ALIAS(go-phi),
/**************************************************/
{ 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 },
/**************************************************/
{ 0, 0, 0, 0, "Output options:", -20 },
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
{ 0, 0, 0, 0, 0, 0 }
};
@ -214,9 +206,12 @@ struct job
typedef std::vector<job> jobs_t;
static jobs_t jobs;
enum output_format_t { spot_output, spin_output, utf8_output };
static output_format_t output_format = spot_output;
static bool full_parenth = false;
const struct argp_child children[] =
{
{ &output_argp, 0, 0, -20 },
{ 0, 0, 0, 0 }
};
// static int
// to_int(const char* s)
@ -275,21 +270,11 @@ enqueue_job(int pattern, const char* range)
}
static int
parse_opt(int key, char* arg, struct argp_state* state)
parse_opt(int key, char* arg, struct argp_state*)
{
(void) state;
// This switch is alphabetically-ordered.
switch (key)
{
case '8':
output_format = utf8_output;
break;
case 'p':
full_parenth = true;
break;
case 's':
output_format = spin_output;
break;
case OPT_AND_F:
case OPT_AND_FG:
case OPT_AND_GF:
@ -310,9 +295,6 @@ parse_opt(int key, char* arg, struct argp_state* state)
case OPT_RV_COUNTER_LINEAR:
enqueue_job(key, arg);
break;
case OPT_SPOT:
output_format = spot_output;
break;
default:
return ARGP_ERR_UNKNOWN;
}
@ -888,19 +870,7 @@ output_pattern(int pattern, int n)
error(100, 0, "internal error: pattern not implemented");
}
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";
output_formula(f);
f->destroy();
}
@ -931,7 +901,8 @@ main(int argc, char** argv)
// and display help text.
argv[0] = const_cast<char*>(program_name);
const argp ap = { options, parse_opt, 0, argp_program_doc, 0, 0, 0 };
const argp ap = { options, parse_opt, 0, argp_program_doc,
children, 0, 0 };
if (int err = argp_parse(&ap, argc, argv, 0, 0, 0))
exit(err);

57
src/bin/ltlfilt.cc
View file

@ -32,10 +32,11 @@
#include "progname.h"
#include "error.h"
#include "common_output.hh"
#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"
@ -61,7 +62,6 @@ Exit status:\n\
1 if no formula were output (no match)\n\
2 if any error has been reported";
#define OPT_SPOT 1
#define OPT_SKIP_ERRORS 2
#define OPT_DROP_ERRORS 3
#define OPT_NNF 4
@ -154,20 +154,21 @@ static const argp_option options[] =
"match formulas implying FORMULA", 0 },
{ "equivalent-to", OPT_EQUIVALENT_TO, "FORMULA", 0,
"match formulas equivalent to FORMULA", 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 },
{ "invert-match", 'v', 0, 0, "select non-matching formulas", 0},
{ "unique", 'u', 0, 0,
"drop formulas that have already been output (not affected by -v)", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Output options:", -20 },
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
{ 0, 0, 0, 0, 0, 0 }
};
const struct argp_child children[] =
{
{ &output_argp, 0, 0, -20 },
{ 0, 0, 0, 0 }
};
struct job
{
const char* str;
@ -187,9 +188,6 @@ static bool one_match = false;
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;
@ -242,15 +240,11 @@ parse_formula_arg(const std::string& input)
static int
parse_opt(int key, char* arg, struct argp_state* state)
parse_opt(int key, char* arg, struct argp_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;
@ -260,9 +254,6 @@ parse_opt(int key, char* arg, struct argp_state* state)
case 'n':
negate = true;
break;
case 'p':
full_parenth = true;
break;
case 'q':
quiet = true;
break;
@ -287,9 +278,6 @@ parse_opt(int key, char* arg, struct argp_state* state)
error(2, 0, "invalid simplification level '%s'", arg);
}
break;
case 's':
output_format = spin_output;
break;
case 'u':
unique = true;
break;
@ -342,9 +330,6 @@ parse_opt(int key, char* arg, struct argp_state* state)
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;
@ -516,19 +501,7 @@ namespace
if (matched)
{
one_match = true;
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";
output_formula(f);
}
f->destroy();
@ -610,7 +583,7 @@ main(int argc, char** argv)
argv[0] = const_cast<char*>(program_name);
const argp ap = { options, parse_opt, "[FILENAME...]",
argp_program_doc, 0, 0, 0 };
argp_program_doc, children, 0, 0 };
if (int err = argp_parse(&ap, argc, argv, 0, 0, 0))
exit(err);