bin: factor common conversion functions
* src/bin/common_conv.cc, src/bin/common_conv.hh: New files. * src/bin/Makefile.am: Add them. * src/bin/autfilt.cc, src/bin/ltlcross.cc, src/bin/ltlfilt.cc, src/bin/ltlgrind.cc, src/bin/randaut.cc, src/bin/randltl.cc: Use them.
This commit is contained in:
parent
06d1c1ea96
commit
d9045d131c
9 changed files with 136 additions and 148 deletions
|
|
@ -1,5 +1,5 @@
|
||||||
## -*- coding: utf-8 -*-
|
## -*- coding: utf-8 -*-
|
||||||
## Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
|
## Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||||
## Développement de l'Epita (LRDE).
|
## Développement de l'Epita (LRDE).
|
||||||
##
|
##
|
||||||
## This file is part of Spot, a model checking library.
|
## This file is part of Spot, a model checking library.
|
||||||
|
|
@ -28,6 +28,8 @@ noinst_LIBRARIES = libcommon.a
|
||||||
libcommon_a_SOURCES = \
|
libcommon_a_SOURCES = \
|
||||||
common_aoutput.cc \
|
common_aoutput.cc \
|
||||||
common_aoutput.hh \
|
common_aoutput.hh \
|
||||||
|
common_conv.hh \
|
||||||
|
common_conv.cc \
|
||||||
common_cout.hh \
|
common_cout.hh \
|
||||||
common_cout.cc \
|
common_cout.cc \
|
||||||
common_finput.cc \
|
common_finput.cc \
|
||||||
|
|
|
||||||
|
|
@ -34,6 +34,7 @@
|
||||||
#include "common_aoutput.hh"
|
#include "common_aoutput.hh"
|
||||||
#include "common_range.hh"
|
#include "common_range.hh"
|
||||||
#include "common_post.hh"
|
#include "common_post.hh"
|
||||||
|
#include "common_conv.hh"
|
||||||
|
|
||||||
#include "tgbaalgos/product.hh"
|
#include "tgbaalgos/product.hh"
|
||||||
#include "tgbaalgos/isdet.hh"
|
#include "tgbaalgos/isdet.hh"
|
||||||
|
|
@ -169,36 +170,6 @@ static char opt_instut = 0;
|
||||||
static bool opt_is_empty = false;
|
static bool opt_is_empty = false;
|
||||||
static std::unique_ptr<unique_aut_t> opt_uniq = nullptr;
|
static std::unique_ptr<unique_aut_t> opt_uniq = nullptr;
|
||||||
|
|
||||||
static int
|
|
||||||
to_int(const char* s)
|
|
||||||
{
|
|
||||||
char* endptr;
|
|
||||||
int res = strtol(s, &endptr, 10);
|
|
||||||
if (*endptr)
|
|
||||||
error(2, 0, "failed to parse '%s' as an integer.", s);
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
static int
|
|
||||||
to_pos_int(const char* s)
|
|
||||||
{
|
|
||||||
int res = to_int(s);
|
|
||||||
if (res < 0)
|
|
||||||
error(2, 0, "%d is not positive", res);
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
static spot::tgba_digraph_ptr
|
|
||||||
read_automaton(const char* filename)
|
|
||||||
{
|
|
||||||
spot::hoa_parse_error_list pel;
|
|
||||||
auto p = hoa_parse(filename, pel, dict);
|
|
||||||
if (spot::format_hoa_parse_errors(std::cerr, filename, pel)
|
|
||||||
|| !p || p->aborted)
|
|
||||||
error(2, 0, "failed to read automaton from %s", filename);
|
|
||||||
return std::move(p->aut);
|
|
||||||
}
|
|
||||||
|
|
||||||
static int
|
static int
|
||||||
parse_opt(int key, char* arg, struct argp_state*)
|
parse_opt(int key, char* arg, struct argp_state*)
|
||||||
{
|
{
|
||||||
|
|
@ -238,7 +209,7 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
|
opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
|
||||||
break;
|
break;
|
||||||
case OPT_ARE_ISOMORPHIC:
|
case OPT_ARE_ISOMORPHIC:
|
||||||
opt_are_isomorphic = read_automaton(arg);
|
opt_are_isomorphic = read_automaton(arg, dict);
|
||||||
break;
|
break;
|
||||||
case OPT_EDGES:
|
case OPT_EDGES:
|
||||||
opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
|
opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
|
||||||
|
|
@ -252,7 +223,7 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
error(2, 0, "unknown argument for --instut: %s", arg);
|
error(2, 0, "unknown argument for --instut: %s", arg);
|
||||||
break;
|
break;
|
||||||
case OPT_INTERSECT:
|
case OPT_INTERSECT:
|
||||||
opt_intersect = read_automaton(arg);
|
opt_intersect = read_automaton(arg, dict);
|
||||||
break;
|
break;
|
||||||
case OPT_DESTUT:
|
case OPT_DESTUT:
|
||||||
opt_destut = true;
|
opt_destut = true;
|
||||||
|
|
@ -271,7 +242,7 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
break;
|
break;
|
||||||
case OPT_PRODUCT:
|
case OPT_PRODUCT:
|
||||||
{
|
{
|
||||||
auto a = read_automaton(arg);
|
auto a = read_automaton(arg, dict);
|
||||||
if (!opt_product)
|
if (!opt_product)
|
||||||
opt_product = std::move(a);
|
opt_product = std::move(a);
|
||||||
else
|
else
|
||||||
|
|
|
||||||
82
src/bin/common_conv.cc
Normal file
82
src/bin/common_conv.cc
Normal file
|
|
@ -0,0 +1,82 @@
|
||||||
|
// -*- coding: utf-8 -*-
|
||||||
|
// Copyright (C) 2015 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 <http://www.gnu.org/licenses/>.
|
||||||
|
|
||||||
|
#include "common_conv.hh"
|
||||||
|
#include <cstdlib>
|
||||||
|
#include "error.h"
|
||||||
|
#include "hoaparse/public.hh"
|
||||||
|
|
||||||
|
int
|
||||||
|
to_int(const char* s)
|
||||||
|
{
|
||||||
|
char* endptr;
|
||||||
|
int res = strtol(s, &endptr, 10);
|
||||||
|
if (*endptr)
|
||||||
|
error(2, 0, "failed to parse '%s' as an integer.", s);
|
||||||
|
return res;
|
||||||
|
}
|
||||||
|
|
||||||
|
int
|
||||||
|
to_pos_int(const char* s)
|
||||||
|
{
|
||||||
|
int res = to_int(s);
|
||||||
|
if (res < 0)
|
||||||
|
error(2, 0, "%d is not positive", res);
|
||||||
|
return res;
|
||||||
|
}
|
||||||
|
|
||||||
|
unsigned
|
||||||
|
to_unsigned (const char *s)
|
||||||
|
{
|
||||||
|
char* endptr;
|
||||||
|
unsigned res = strtoul(s, &endptr, 10);
|
||||||
|
if (*endptr)
|
||||||
|
error(2, 0, "failed to parse '%s' as an unsigned integer.", s);
|
||||||
|
return res;
|
||||||
|
}
|
||||||
|
|
||||||
|
float
|
||||||
|
to_float(const char* s)
|
||||||
|
{
|
||||||
|
char* endptr;
|
||||||
|
float res = strtof(s, &endptr);
|
||||||
|
if (*endptr)
|
||||||
|
error(2, 0, "failed to parse '%s' as a float.", s);
|
||||||
|
return res;
|
||||||
|
}
|
||||||
|
|
||||||
|
float
|
||||||
|
to_probability(const char* s)
|
||||||
|
{
|
||||||
|
float res = to_float(s);
|
||||||
|
if (res < 0.0 || res > 1.0)
|
||||||
|
error(2, 0, "%f is not between 0 and 1.", res);
|
||||||
|
return res;
|
||||||
|
}
|
||||||
|
|
||||||
|
spot::tgba_digraph_ptr
|
||||||
|
read_automaton(const char* filename, spot::bdd_dict_ptr& dict)
|
||||||
|
{
|
||||||
|
spot::hoa_parse_error_list pel;
|
||||||
|
auto p = spot::hoa_parse(filename, pel, dict);
|
||||||
|
if (spot::format_hoa_parse_errors(std::cerr, filename, pel)
|
||||||
|
|| !p || p->aborted)
|
||||||
|
error(2, 0, "failed to read automaton from %s", filename);
|
||||||
|
return std::move(p->aut);
|
||||||
|
}
|
||||||
36
src/bin/common_conv.hh
Normal file
36
src/bin/common_conv.hh
Normal file
|
|
@ -0,0 +1,36 @@
|
||||||
|
// -*- coding: utf-8 -*-
|
||||||
|
// Copyright (C) 2015 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 <http://www.gnu.org/licenses/>.
|
||||||
|
|
||||||
|
#ifndef SPOT_BIN_COMMON_CONV_HH
|
||||||
|
#define SPOT_BIN_COMMON_CONV_HH
|
||||||
|
|
||||||
|
#include "common_sys.hh"
|
||||||
|
#include "tgba/tgbagraph.hh"
|
||||||
|
|
||||||
|
int to_int(const char* s);
|
||||||
|
int to_pos_int(const char* s);
|
||||||
|
unsigned to_unsigned (const char *s);
|
||||||
|
float to_float(const char* s);
|
||||||
|
float to_probability(const char* s);
|
||||||
|
|
||||||
|
spot::tgba_digraph_ptr
|
||||||
|
read_automaton(const char* filename, spot::bdd_dict_ptr& dict);
|
||||||
|
|
||||||
|
|
||||||
|
#endif // SPOT_BIN_COMMON_CONV_HH
|
||||||
|
|
@ -35,6 +35,7 @@
|
||||||
|
|
||||||
#include "common_setup.hh"
|
#include "common_setup.hh"
|
||||||
#include "common_cout.hh"
|
#include "common_cout.hh"
|
||||||
|
#include "common_conv.hh"
|
||||||
#include "common_finput.hh"
|
#include "common_finput.hh"
|
||||||
#include "dstarparse/public.hh"
|
#include "dstarparse/public.hh"
|
||||||
#include "hoaparse/public.hh"
|
#include "hoaparse/public.hh"
|
||||||
|
|
@ -466,46 +467,6 @@ typedef std::vector<statistics_formula> statistics_vector;
|
||||||
statistics_vector vstats;
|
statistics_vector vstats;
|
||||||
std::vector<std::string> formulas;
|
std::vector<std::string> formulas;
|
||||||
|
|
||||||
static int
|
|
||||||
to_int(const char* s)
|
|
||||||
{
|
|
||||||
char* endptr;
|
|
||||||
int res = strtol(s, &endptr, 10);
|
|
||||||
if (*endptr)
|
|
||||||
error(2, 0, "failed to parse '%s' as an integer.", s);
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
static int
|
|
||||||
to_pos_int(const char* s)
|
|
||||||
{
|
|
||||||
int res = to_int(s);
|
|
||||||
if (res < 0)
|
|
||||||
error(2, 0, "%d is not positive", res);
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
static float
|
|
||||||
to_float(const char* s)
|
|
||||||
{
|
|
||||||
char* endptr;
|
|
||||||
// Do not use strtof(), it does not exist on Solaris 9.
|
|
||||||
float res = strtod(s, &endptr);
|
|
||||||
if (*endptr)
|
|
||||||
error(2, 0, "failed to parse '%s' as a float.", s);
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
static float
|
|
||||||
to_probability(const char* s)
|
|
||||||
{
|
|
||||||
float res = to_float(s);
|
|
||||||
if (res < 0.0 || res > 1.0)
|
|
||||||
error(2, 0, "%f is not between 0 and 1.", res);
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
static int
|
static int
|
||||||
parse_opt(int key, char* arg, struct argp_state*)
|
parse_opt(int key, char* arg, struct argp_state*)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -31,6 +31,7 @@
|
||||||
#include "common_finput.hh"
|
#include "common_finput.hh"
|
||||||
#include "common_output.hh"
|
#include "common_output.hh"
|
||||||
#include "common_cout.hh"
|
#include "common_cout.hh"
|
||||||
|
#include "common_conv.hh"
|
||||||
#include "common_r.hh"
|
#include "common_r.hh"
|
||||||
|
|
||||||
#include "misc/hash.hh"
|
#include "misc/hash.hh"
|
||||||
|
|
@ -239,25 +240,6 @@ static const spot::ltl::formula* implied_by = 0;
|
||||||
static const spot::ltl::formula* imply = 0;
|
static const spot::ltl::formula* imply = 0;
|
||||||
static const spot::ltl::formula* equivalent_to = 0;
|
static const spot::ltl::formula* equivalent_to = 0;
|
||||||
|
|
||||||
static int
|
|
||||||
to_int(const char* s)
|
|
||||||
{
|
|
||||||
char* endptr;
|
|
||||||
int res = strtol(s, &endptr, 10);
|
|
||||||
if (*endptr)
|
|
||||||
error(2, 0, "failed to parse '%s' as an integer.", s);
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
static int
|
|
||||||
to_pos_int(const char* s)
|
|
||||||
{
|
|
||||||
int res = to_int(s);
|
|
||||||
if (res < 0)
|
|
||||||
error(2, 0, "%d is not positive", res);
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
static const spot::ltl::formula*
|
static const spot::ltl::formula*
|
||||||
parse_formula_arg(const std::string& input)
|
parse_formula_arg(const std::string& input)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de
|
||||||
// l'Epita (LRDE).
|
// l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -20,10 +20,13 @@
|
||||||
|
|
||||||
#include "common_sys.hh"
|
#include "common_sys.hh"
|
||||||
#include <argp.h>
|
#include <argp.h>
|
||||||
|
#include "error.h"
|
||||||
|
|
||||||
#include "common_setup.hh"
|
#include "common_setup.hh"
|
||||||
#include "common_finput.hh"
|
#include "common_finput.hh"
|
||||||
#include "common_output.hh"
|
#include "common_output.hh"
|
||||||
#include "error.h"
|
#include "common_conv.hh"
|
||||||
|
|
||||||
#include "ltlast/allnodes.hh"
|
#include "ltlast/allnodes.hh"
|
||||||
#include "ltlvisit/clone.hh"
|
#include "ltlvisit/clone.hh"
|
||||||
#include "ltlvisit/apcollect.hh"
|
#include "ltlvisit/apcollect.hh"
|
||||||
|
|
@ -89,30 +92,9 @@ static const argp_child children[] = {
|
||||||
{0, 0, 0, 0}
|
{0, 0, 0, 0}
|
||||||
};
|
};
|
||||||
|
|
||||||
static int
|
|
||||||
to_int(const char *s)
|
|
||||||
{
|
|
||||||
char* endptr;
|
|
||||||
unsigned res = strtol(s, &endptr, 10);
|
|
||||||
if (*endptr)
|
|
||||||
error(2, 0, "failed to parse '%s' as an unsigned integer.", s);
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
static unsigned
|
|
||||||
to_unsigned (const char *s)
|
|
||||||
{
|
|
||||||
char* endptr;
|
|
||||||
unsigned res = strtoul(s, &endptr, 10);
|
|
||||||
if (*endptr)
|
|
||||||
error(2, 0, "failed to parse '%s' as an unsigned integer.", s);
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
namespace
|
namespace
|
||||||
{
|
{
|
||||||
class mutate_processor:
|
class mutate_processor: public job_processor
|
||||||
public job_processor
|
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
int
|
int
|
||||||
|
|
|
||||||
|
|
@ -31,6 +31,7 @@
|
||||||
#include "common_range.hh"
|
#include "common_range.hh"
|
||||||
#include "common_cout.hh"
|
#include "common_cout.hh"
|
||||||
#include "common_aoutput.hh"
|
#include "common_aoutput.hh"
|
||||||
|
#include "common_conv.hh"
|
||||||
|
|
||||||
#include "ltlenv/defaultenv.hh"
|
#include "ltlenv/defaultenv.hh"
|
||||||
#include "misc/timer.hh"
|
#include "misc/timer.hh"
|
||||||
|
|
@ -115,26 +116,6 @@ static bool opt_state_acc = false;
|
||||||
static bool ba_wanted = false;
|
static bool ba_wanted = false;
|
||||||
static std::unique_ptr<unique_aut_t> opt_uniq = nullptr;
|
static std::unique_ptr<unique_aut_t> opt_uniq = nullptr;
|
||||||
|
|
||||||
static int
|
|
||||||
to_int(const char* s)
|
|
||||||
{
|
|
||||||
char* endptr;
|
|
||||||
int res = strtol(s, &endptr, 10);
|
|
||||||
if (*endptr)
|
|
||||||
error(2, 0, "failed to parse '%s' as an integer.", s);
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
static float
|
|
||||||
to_float(const char* s)
|
|
||||||
{
|
|
||||||
char* endptr;
|
|
||||||
float res = strtof(s, &endptr);
|
|
||||||
if (*endptr)
|
|
||||||
error(2, 0, "failed to parse '%s' as a float.", s);
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
static void
|
static void
|
||||||
ba_options()
|
ba_options()
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
|
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||||
// Développement de l'Epita (LRDE).
|
// Développement de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -30,6 +30,7 @@
|
||||||
#include "common_output.hh"
|
#include "common_output.hh"
|
||||||
#include "common_range.hh"
|
#include "common_range.hh"
|
||||||
#include "common_r.hh"
|
#include "common_r.hh"
|
||||||
|
#include "common_conv.hh"
|
||||||
|
|
||||||
#include <sstream>
|
#include <sstream>
|
||||||
#include "ltlast/multop.hh"
|
#include "ltlast/multop.hh"
|
||||||
|
|
@ -179,16 +180,6 @@ GF_n(spot::ltl::atomic_prop_set& ap)
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
static int
|
|
||||||
to_int(const char* s)
|
|
||||||
{
|
|
||||||
char* endptr;
|
|
||||||
int res = strtol(s, &endptr, 10);
|
|
||||||
if (*endptr)
|
|
||||||
error(2, 0, "failed to parse '%s' as an integer.", s);
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
static int
|
static int
|
||||||
parse_opt(int key, char* arg, struct argp_state* as)
|
parse_opt(int key, char* arg, struct argp_state* as)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue