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

randltl: first stage of the reimplementation

Browse source 
* src/bin/common_range.cc, src/bin/common_range.hh: New files,
extracted from...
* src/bin/genltl.cc: ... here.
* src/bin/randltl.cc, src/bin/man/randltl.x: New files.
* src/bin/Makefile.am, src/bin/man/Makefile.am: Adjust.
* src/bin/man/genltl.x: Point to randltl(1).
This commit is contained in:
Alexandre Duret-Lutz 2012-09-05 12:03:24 +02:00
parent a3e54af924
commit 760d75cc44
8 changed files with 497 additions and 54 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/bin/Makefile.am
View file

@ -26,9 +26,10 @@ AM_CPPFLAGS = -I$(top_srcdir)/src -I$(top_builddir)/src $(BUDDY_CPPFLAGS) \
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
LDADD = $(top_builddir)/src/libspot.la $(top_builddir)/lib/libgnu.a
bin_PROGRAMS = ltlfilt genltl
bin_PROGRAMS = ltlfilt genltl randltl
noinst_HEADERS = common_output.hh
noinst_HEADERS = common_output.hh common_range.hh
ltlfilt_SOURCES = ltlfilt.cc common_output.cc
genltl_SOURCES = genltl.cc common_output.cc
genltl_SOURCES = genltl.cc common_output.cc common_range.cc
randltl_SOURCES = randltl.cc common_output.cc common_range.cc

75
src/bin/common_range.cc Normal file
View file

@ -0,0 +1,75 @@
// -*- 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 "error.h"
#include "common_range.hh"
#include <iostream>
#include <cstdlib>
range
parse_range(const char* str)
{
range res;
// The range should have the form INT..INT or INT:INT, with
// "42" standing for "42..42", and "..42" meaning "1..42".
char* end;
res.min = strtol(str, &end, 10);
if (end == str)
{
// No leading number. It's OK as long as the string is not
// empty.
if (!*end)
error(1, 0, "invalid empty range");
res.min = 1;
}
if (!*end)
{
// Only one number.
res.max = res.min;
}
else
{
// Skip : or ..
if (end[0] == ':')
++end;
else if (end[0] == '.' && end[1] == '.')
end += 2;
// Parse the next integer.
char* end2;
res.max = strtol(end, &end2, 10);
if (end == end2)
error(1, 0, "invalid range '%s' (missing end?)", str);
if (*end2)
error(1, 0, "invalid range '%s' (trailing garbage?)", str);
}
if (res.min < 0 || res.max < 0)
error(1, 0, "invalid range '%s': values must be positive", str);
return res;
}

39
src/bin/common_range.hh Normal file
View file

@ -0,0 +1,39 @@
// -*- 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_RANGE_HH
#define SPOT_BIN_COMMON_RANGE_HH
#define RANGE_DOC \
{ 0, 0, 0, 0, "RANGE may have one of the following forms: 'INT', " \
"'INT..INT', or '..INT'.\nIn the latter case, the missing number " \
"is assumed to be 1.", 0 }
struct range
{
int min;
int max;
};
range parse_range(const char* str);
#endif // SPOT_BIN_COMMON_RANGE_HH

58
src/bin/genltl.cc
View file

@ -81,6 +81,7 @@
#include <vector>
#include "common_output.hh"
#include "common_range.hh"
#include "misc/_config.h"
#include <cassert>
@ -178,10 +179,7 @@ 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, "RANGE may have one of the following forms: 'INT', "
"'INT..INT', or '..INT'.\nIn the latter case, the missing number "
"is assumed to be 1.", 0 },
RANGE_DOC,
/**************************************************/
{ 0, 0, 0, 0, "Output options:", -20 },
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
@ -191,8 +189,7 @@ static const argp_option options[] =
struct job
{
int pattern;
int range_min;
int range_max;
struct range range;
};
typedef std::vector<job> jobs_t;
@ -211,53 +208,16 @@ const struct argp_child children[] =
// char* endptr;
// int res = strtol(s, &endptr, 10);
// if (*endptr)
// error(1, 0, "failed to parse '%s' as an integer.", s);
// error(2, 0, "failed to parse '%s' as an integer.", s);
// return res;
// }
static void
enqueue_job(int pattern, const char* range)
enqueue_job(int pattern, const char* range_str)
{
job j;
j.pattern = pattern;
// Parse the range; it should have the form INT..INT or INT:INT
char* end;
j.range_min = strtol(range, &end, 10);
if (end == range)
{
// No leading number. It's OK as long as the string is not
// empty.
if (!*end)
error(1, 0, "invalid empty range");
j.range_min = 1;
}
if (!*end)
{
// Only one number.
j.range_max = j.range_min;
}
else
{
// Skip : or ..
if (end[0] == ':')
++end;
else if (end[0] == '.' && end[1] == '.')
end += 2;
// Parse the next integer.
char* end2;
j.range_max = strtol(end, &end2, 10);
if (end == end2)
error(1, 0, "invalid range '%s' (missing end?)", range);
if (*end2)
error(1, 0, "invalid range '%s' (trailing garbage?)", range);
}
if (j.range_min < 0 || j.range_max < 0)
error(1, 0, "invalid range '%s': values must be positive", range);
j.range = parse_range(range_str);
jobs.push_back(j);
}
@ -872,12 +832,12 @@ run_jobs()
jobs_t::const_iterator i;
for (i = jobs.begin(); i != jobs.end(); ++i)
{
int inc = (i->range_max < i->range_min) ? -1 : 1;
int n = i->range_min;
int inc = (i->range.max < i->range.min) ? -1 : 1;
int n = i->range.min;
for (;;)
{
output_pattern(i->pattern, n);
if (n == i->range_max)
if (n == i->range.max)
break;
n += inc;
}

7
src/bin/man/Makefile.am
View file

@ -24,9 +24,9 @@ x_to_1 = $(top_builddir)/tools/x-to-1
convman = ARGP_HELP_FMT=header-col=0 $(SHELL) "$(x_to_1)" \
"$(PERL)" "$(top_srcdir)/tools/help2man -N"
dist_man1_MANS = ltlfilt.1 genltl.1
dist_man1_MANS = ltlfilt.1 genltl.1 randltl.1
MAINTAINERCLEANFILES = $(dist_man1_MANS)
man_aux = $(dist_man1_MANS:.1=.x)
EXTRA_DIST = $(dist_man1_MANS:.1=.x)
ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc
$(convman) ../ltlfilt$(EXEEXT) $(srcdir)/ltlfilt.x $@
@ -34,4 +34,7 @@ ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc
genltl.1: $(common_dep) $(srcdir)/genltl.x $(srcdir)/../genltl.cc
$(convman) ../genltl$(EXEEXT) $(srcdir)/genltl.x $@
randltl.1: $(common_dep) $(srcdir)/randltl.x $(srcdir)/../randltl.cc
$(convman) ../randltl$(EXEEXT) $(srcdir)/randltl.x $@

2
src/bin/man/genltl.x
View file

@ -20,3 +20,5 @@ Proceedings of CAV'01. LNCS 2102
rv
K. Rozier and M. Vardi: LTL Satisfiability Checking.
Proceedings of Spin'07. LNCS 4595.
[SEE ALSO]
randltl(1)

6
src/bin/man/randltl.x Normal file
View file

@ -0,0 +1,6 @@
[NAME]
randltl \- generate random LTL/PSL formulas
[DESCRIPTION]
.\" Add any additional description here
[SEE ALSO]
genltl(1), ltlfilt(1)

357
src/bin/randltl.cc Normal file
View file

@ -0,0 +1,357 @@
// -*- 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 <iostream>
#include <fstream>
#include <argp.h>
#include <cstdlib>
#include "progname.h"
#include "error.h"
#include "common_output.hh"
#include "common_range.hh"
#include "misc/_config.h"
#include <sstream>
#include "ltlast/atomic_prop.hh"
#include "ltlvisit/randomltl.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/length.hh"
#include "ltlvisit/simplify.hh"
#include "ltlenv/defaultenv.hh"
#include "misc/random.hh"
#include "misc/hash.hh"
const char* argp_program_version = "\
randltl (" 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[] ="\
Generate random temporal logic formulas.\v\
Examples:\n\
\n\
The following generates 10 random LTL formulas over the propositions a, b,\n\
and c, with the default tree-size, and all available operators.\n\
% randltl -n10 a b c\n\
\n\
You can disable or favor certain operators by changing their priority.\n\
The following disables xor, implies, and equiv, and multiply the probability\n\
of X to occur by 10.\n\
% ./randltl --ltl-priorities='xor=0,implies=0,equiv=0,X=10' -n10 a b c\n\
";
#define OPT_DUMP_PRIORITIES 1
#define OPT_LTL_PRIORITIES 2
#define OPT_SERE_PRIORITIES 3
#define OPT_PSL_PRIORITIES 4
#define OPT_BOOLEAN_PRIORITIES 5
#define OPT_SEED 6
#define OPT_TREE_SIZE 7
static const argp_option options[] =
{
// Keep this alphabetically sorted (expect for aliases).
/**************************************************/
{ 0, 0, 0, 0, "Type of formula to generate:", 1 },
{ "boolean", 'B', 0, 0, "generate Boolean formulas", 0 },
{ "ltl", 'L', 0, 0, "generate LTL formulas (default)", 0 },
{ "sere", 'S', 0, 0, "generate SERE", 0 },
{ "psl", 'P', 0, 0, "generate PSL formulas", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Generation:", 2 },
{ "formulas", 'n', "INT", 0, "number of formulas to output (1)\n"\
"use a negative value for unbounded generation", 0 },
{ "seed", OPT_SEED, "INT", 0,
"seed for the random number generator (0)", 0 },
{ "tree-size", OPT_TREE_SIZE, "RANGE", 0,
"tree size of the formulas generated, before mandatory "\
"trivial simplifications (15)", 0 },
{ "unique", 'u', 0, 0, "do not generate duplicate formulas", 0 },
RANGE_DOC,
/**************************************************/
{ 0, 0, 0, 0, "Adjusting probabilities:", 3 },
{ "dump-priorities", OPT_DUMP_PRIORITIES, 0, 0,
"show current priorities, do not generate any formula", 0 },
{ "ltl-priorities", OPT_LTL_PRIORITIES, "STRING", 0,
"set priorities for LTL formulas", 0 },
{ "sere-priorities", OPT_SERE_PRIORITIES, "STRING", 0,
"set priorities for SERE formulas", 0 },
{ "boolean-priorities", OPT_BOOLEAN_PRIORITIES, "STRING", 0,
"set priorities for Boolean formulas", 0 },
{ 0, 0, 0, 0, "STRING should be a comma-separated list of "
"assignments, assigning integer priorities to the tokens "
"listed by --dump-priorities.", 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 }
};
static enum { OutputBool, OutputLTL, OutputSERE, OutputPSL }
output = OutputLTL;
spot::ltl::atomic_prop_set aprops;
static char* opt_pL = 0;
static char* opt_pS = 0;
static char* opt_pB = 0;
static bool opt_dump_priorities = false;
static int opt_formulas = 1;
static int opt_seed = 0;
static range opt_tree_size = { 15, 15 };
static bool opt_unique = false;
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
parse_opt(int key, char* arg, struct argp_state*)
{
// This switch is alphabetically-ordered.
switch (key)
{
case 'B':
output = OutputBool;
break;
case 'L':
output = OutputLTL;
break;
case 'n':
opt_formulas = to_int(arg);
break;
case 'P':
output = OutputPSL;
break;
case 'S':
output = OutputSERE;
break;
case 'u':
opt_unique = true;
break;
case OPT_BOOLEAN_PRIORITIES:
opt_pB = arg;
break;
case OPT_LTL_PRIORITIES:
opt_pL = arg;
break;
case OPT_DUMP_PRIORITIES:
opt_dump_priorities = true;
break;
// case OPT_PSL_PRIORITIES: break;
case OPT_SERE_PRIORITIES:
opt_pS = arg;
break;
case OPT_SEED:
opt_seed = to_int(arg);
break;
case OPT_TREE_SIZE:
opt_tree_size = parse_range(arg);
if (opt_tree_size.min > opt_tree_size.max)
std::swap(opt_tree_size.min, opt_tree_size.max);
break;
case ARGP_KEY_ARG:
aprops.insert(static_cast<const spot::ltl::atomic_prop*>
(spot::ltl::default_environment::instance().require(arg)));
break;
default:
return ARGP_ERR_UNKNOWN;
}
return 0;
}
int
main(int argc, char** argv)
{
set_program_name(argv[0]);
// Simplify the program name, because argp() uses it to report errors
// and display help text.
argv[0] = const_cast<char*>(program_name);
const argp ap = { options, parse_opt, "PROP...", argp_program_doc,
children, 0, 0 };
if (int err = argp_parse(&ap, argc, argv, 0, 0, 0))
exit(err);
spot::ltl::random_formula* rf = 0;
spot::ltl::random_psl* rp = 0;
spot::ltl::random_sere* rs = 0;
const char* tok_pL = 0;
const char* tok_pS = 0;
const char* tok_pB = 0;
switch (output)
{
case OutputLTL:
rf = new spot::ltl::random_ltl(&aprops);
tok_pL = rf->parse_options(opt_pL);
if (opt_pS)
error(2, 0, "option --sere-priorities unsupported for LTL output");
if (opt_pB)
error(2, 0, "option --boolean-priorities unsupported for LTL output");
break;
case OutputBool:
rf = new spot::ltl::random_boolean(&aprops);
tok_pB = rf->parse_options(opt_pB);
if (opt_pL)
error(2, 0, "option --ltl-priorities unsupported for Boolean output");
if (opt_pS)
error(2, 0, "option --sere-priorities unsupported for Boolean output");
break;
case OutputSERE:
rf = rs = new spot::ltl::random_sere(&aprops);
tok_pS = rf->parse_options(opt_pS);
if (opt_pL)
error(2, 0, "option --ltl-priorities unsupported for SERE output");
break;
case OutputPSL:
rf = rp = new spot::ltl::random_psl(&aprops);
rs = &rp->rs;
tok_pL = rp->parse_options(opt_pL);
tok_pS = rs->parse_options(opt_pS);
tok_pB = rs->rb.parse_options(opt_pB);
break;
}
if (tok_pL)
error(2, 0, "failed to parse LTL priorities near '%s'", tok_pL);
if (tok_pS)
error(2, 0, "failed to parse SERE priorities near '%s'", tok_pS);
if (tok_pB)
error(2, 0, "failed to parse Boolean priorities near '%s'", tok_pB);
if (opt_dump_priorities)
{
switch (output)
{
case OutputLTL:
std::cout
<< "Use --ltl-priorities to set the following LTL priorities:\n";
rf->dump_priorities(std::cout);
break;
case OutputBool:
std::cout
<< ("Use --boolean-priorities to set the following Boolean "
"formula priorities:\n");
rf->dump_priorities(std::cout);
break;
case OutputPSL:
std::cout
<< "Use --ltl-priorities to set the following LTL priorities:\n";
rp->dump_priorities(std::cout);
// Fall through.
case OutputSERE:
std::cout
<< "Use --sere-priorities to set the following SERE priorities:\n";
rs->dump_priorities(std::cout);
std::cout
<< ("Use --boolean-priorities to set the following Boolean "
"formula priorities:\n");
rs->rb.dump_priorities(std::cout);
break;
default:
error(2, 0, "internal error: unknown type of output");
}
exit(0);
}
if (aprops.empty())
error(2, 0, "No atomic proposition supplied? Run '%s --help' for usage.",
program_name);
typedef Sgi::hash_set<const spot::ltl::formula*,
const spot::ptr_hash<const spot::ltl::formula> > fset_t;
fset_t unique_set;
while (opt_formulas < 0 || opt_formulas--)
{
#define MAX_TRIALS 100000
unsigned trials = MAX_TRIALS;
bool ignore;
const spot::ltl::formula* f = 0;
spot::srand(opt_seed++);
do
{
ignore = false;
int size = opt_tree_size.min;
if (size != opt_tree_size.max)
size = spot::rrand(size, opt_tree_size.max);
f = rf->generate(size);
if (opt_unique)
{
if (unique_set.insert(f).second)
{
f->clone();
}
else
{
ignore = true;
f->destroy();
}
}
}
while (ignore && --trials);
if (trials == 0)
error(2, 0, "failed to generate a new unique formula after %d trials",
MAX_TRIALS);
output_formula(f);
f->destroy();
};
delete rf;
// Cleanup the unicity table.
{
fset_t::const_iterator i;
for (i = unique_set.begin(); i != unique_set.end(); ++i)
(*i)->destroy();
}
// Cleanup the atomic_prop set.
{
spot::ltl::atomic_prop_set::const_iterator i = aprops.begin();
while (i != aprops.end())
(*(i++))->destroy();
}
return 0;
}