Add option --lbt-input to ltl2tgba. Factor it with ltlfilt.
* src/bin/ltlfilt.cc: Extra input options into... * src/bin/common_finput.cc, src/bin/common_finput.hh: ... these new files... * src/bin/ltl2tgba.cc: ... and use them here. * src/bin/Makefile.am: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
f02156ebff
commit
f4381d59ce
5 changed files with 142 additions and 59 deletions
|
|
@ -30,6 +30,8 @@ noinst_LIBRARIES = libcommon.a
|
|||
libcommon_a_SOURCES = \
|
||||
common_cout.hh \
|
||||
common_cout.cc \
|
||||
common_finput.cc \
|
||||
common_finput.hh \
|
||||
common_output.cc \
|
||||
common_output.hh \
|
||||
common_range.cc \
|
||||
|
|
|
|||
71
src/bin/common_finput.cc
Normal file
71
src/bin/common_finput.cc
Normal file
|
|
@ -0,0 +1,71 @@
|
|||
// -*- 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_finput.hh"
|
||||
#include "error.h"
|
||||
|
||||
#define OPT_LBT 1
|
||||
|
||||
jobs_t jobs;
|
||||
bool lbt_input = false;
|
||||
|
||||
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 },
|
||||
{ "lbt-input", OPT_LBT, 0, 0,
|
||||
"read all formulas using LBT's prefix syntax", 0 },
|
||||
{ 0, 0, 0, 0, 0, 0 }
|
||||
};
|
||||
|
||||
const struct argp finput_argp = { options, parse_opt_finput, 0, 0, 0, 0, 0 };
|
||||
|
||||
int
|
||||
parse_opt_finput(int key, char* arg, struct argp_state*)
|
||||
{
|
||||
// This switch is alphabetically-ordered.
|
||||
switch (key)
|
||||
{
|
||||
case 'f':
|
||||
jobs.push_back(job(arg, false));
|
||||
break;
|
||||
case 'F':
|
||||
jobs.push_back(job(arg, true));
|
||||
break;
|
||||
case OPT_LBT:
|
||||
lbt_input = true;
|
||||
break;
|
||||
default:
|
||||
return ARGP_ERR_UNKNOWN;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
const spot::ltl::formula*
|
||||
parse_formula(const std::string& s, spot::ltl::parse_error_list& pel)
|
||||
{
|
||||
if (lbt_input)
|
||||
return spot::ltl::parse_lbt(s, pel);
|
||||
else
|
||||
return spot::ltl::parse(s, pel);
|
||||
}
|
||||
54
src/bin/common_finput.hh
Normal file
54
src/bin/common_finput.hh
Normal file
|
|
@ -0,0 +1,54 @@
|
|||
// -*- 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_FINPUT_HH
|
||||
#define SPOT_BIN_COMMON_FINPUT_HH
|
||||
|
||||
#include "common_sys.hh"
|
||||
|
||||
#include <argp.h>
|
||||
#include <vector>
|
||||
#include "ltlparse/public.hh"
|
||||
|
||||
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<job> jobs_t;
|
||||
extern jobs_t jobs;
|
||||
extern bool lbt_input;
|
||||
|
||||
extern const struct argp finput_argp;
|
||||
|
||||
int parse_opt_finput(int key, char* arg, struct argp_state* state);
|
||||
|
||||
const spot::ltl::formula*
|
||||
parse_formula(const std::string& s, spot::ltl::parse_error_list& error_list);
|
||||
|
||||
|
||||
#endif // SPOT_BIN_COMMON_FINPUT_HH
|
||||
|
|
@ -32,6 +32,7 @@
|
|||
|
||||
#include "common_r.hh"
|
||||
#include "common_cout.hh"
|
||||
#include "common_finput.hh"
|
||||
|
||||
#include "misc/_config.h"
|
||||
#include "ltlparse/public.hh"
|
||||
|
|
@ -73,11 +74,6 @@ If multiple formulas are supplied, several automata will be output.";
|
|||
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, "Automaton type:", 2 },
|
||||
{ "tgba", OPT_TGBA, 0, 0,
|
||||
"Transition-based Generalized Büchi Automaton (default)", 0 },
|
||||
|
|
@ -106,19 +102,11 @@ static const argp_option options[] =
|
|||
{ 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)
|
||||
const struct argp_child children[] =
|
||||
{
|
||||
}
|
||||
};
|
||||
|
||||
typedef std::vector<job> jobs_t;
|
||||
static jobs_t jobs;
|
||||
{ &finput_argp, 0, 0, 1 },
|
||||
{ 0, 0, 0, 0 }
|
||||
};
|
||||
|
||||
spot::postprocessor::output_type type = spot::postprocessor::TGBA;
|
||||
spot::postprocessor::output_pref pref = spot::postprocessor::Small;
|
||||
|
|
@ -214,7 +202,7 @@ namespace
|
|||
const char* filename = 0, int linenum = 0)
|
||||
{
|
||||
spot::ltl::parse_error_list pel;
|
||||
const spot::ltl::formula* f = spot::ltl::parse(input, pel);
|
||||
const spot::ltl::formula* f = parse_formula(input, pel);
|
||||
|
||||
if (!f || pel.size() > 0)
|
||||
{
|
||||
|
|
@ -252,7 +240,8 @@ namespace
|
|||
switch (format)
|
||||
{
|
||||
case Dot:
|
||||
spot::dotty_reachable(std::cout, aut, type == spot::postprocessor::BA);
|
||||
spot::dotty_reachable(std::cout, aut,
|
||||
type == spot::postprocessor::BA);
|
||||
break;
|
||||
case Lbtt:
|
||||
spot::lbtt_reachable(std::cout, aut);
|
||||
|
|
@ -331,7 +320,7 @@ main(int argc, char** argv)
|
|||
argv[0] = const_cast<char*>(program_name);
|
||||
|
||||
const argp ap = { options, parse_opt, "[FORMULA...]",
|
||||
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);
|
||||
|
|
|
|||
|
|
@ -31,13 +31,13 @@
|
|||
#include "progname.h"
|
||||
#include "error.h"
|
||||
|
||||
#include "common_finput.hh"
|
||||
#include "common_output.hh"
|
||||
#include "common_cout.hh"
|
||||
#include "common_r.hh"
|
||||
|
||||
#include "misc/_config.h"
|
||||
#include "misc/hash.hh"
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlvisit/simplify.hh"
|
||||
#include "ltlvisit/length.hh"
|
||||
#include "ltlvisit/relabel.hh"
|
||||
|
|
@ -89,19 +89,12 @@ Exit status:\n\
|
|||
#define OPT_IMPLIED_BY 23
|
||||
#define OPT_IMPLY 24
|
||||
#define OPT_EQUIVALENT_TO 25
|
||||
#define OPT_LBT 26
|
||||
#define OPT_RELABEL 27
|
||||
#define OPT_REMOVE_WM 28
|
||||
#define OPT_RELABEL 26
|
||||
#define OPT_REMOVE_WM 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 },
|
||||
{ "lbt-input", OPT_LBT, 0, 0,
|
||||
"read all formulas using LBT's prefix syntax", 0 },
|
||||
{ 0, 0, 0, 0, "Error handling:", 2 },
|
||||
{ "skip-errors", OPT_SKIP_ERRORS, 0, 0,
|
||||
"output erroneous lines as-is without processing", 0 },
|
||||
|
|
@ -169,29 +162,15 @@ static const argp_option options[] =
|
|||
|
||||
const struct argp_child children[] =
|
||||
{
|
||||
{ &finput_argp, 0, 0, 1 },
|
||||
{ &output_argp, 0, 0, -20 },
|
||||
{ 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<job> jobs_t;
|
||||
static jobs_t jobs;
|
||||
|
||||
static bool one_match = false;
|
||||
|
||||
enum error_style_t { drop_errors, skip_errors };
|
||||
static error_style_t error_style = drop_errors;
|
||||
static bool lbt = false;
|
||||
static bool quiet = false;
|
||||
static bool nnf = false;
|
||||
static bool negate = false;
|
||||
|
|
@ -238,7 +217,7 @@ static const spot::ltl::formula*
|
|||
parse_formula_arg(const std::string& input)
|
||||
{
|
||||
spot::ltl::parse_error_list pel;
|
||||
const spot::ltl::formula* f = spot::ltl::parse(input, pel);
|
||||
const spot::ltl::formula* f = parse_formula(input, pel);
|
||||
if (spot::ltl::format_parse_errors(std::cerr, input, pel))
|
||||
error(2, 0, "parse error when parsing an argument");
|
||||
return f;
|
||||
|
|
@ -252,12 +231,6 @@ parse_opt(int key, char* arg, struct argp_state*)
|
|||
// This switch is alphabetically-ordered.
|
||||
switch (key)
|
||||
{
|
||||
case 'f':
|
||||
jobs.push_back(job(arg, false));
|
||||
break;
|
||||
case 'F':
|
||||
jobs.push_back(job(arg, true));
|
||||
break;
|
||||
case 'n':
|
||||
negate = true;
|
||||
break;
|
||||
|
|
@ -315,8 +288,6 @@ parse_opt(int key, char* arg, struct argp_state*)
|
|||
spot::ltl::multop::instance(spot::ltl::multop::And, imply, i);
|
||||
break;
|
||||
}
|
||||
case OPT_LBT:
|
||||
lbt = true;
|
||||
case OPT_LTL:
|
||||
ltl = true;
|
||||
break;
|
||||
|
|
@ -398,11 +369,7 @@ namespace
|
|||
const char* filename = 0, int linenum = 0)
|
||||
{
|
||||
spot::ltl::parse_error_list pel;
|
||||
const spot::ltl::formula* f;
|
||||
if (lbt)
|
||||
f = spot::ltl::parse_lbt(input, pel);
|
||||
else
|
||||
f = spot::ltl::parse(input, pel);
|
||||
const spot::ltl::formula* f = parse_formula(input, pel);
|
||||
|
||||
if (!f || pel.size() > 0)
|
||||
{
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue