Commit 6a3cf753 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

bin/ltl2tgba: New user binary.

* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: New class to
capture the postprocessing logic.
* src/tgbaalgos/Makefile.am: Add them.
* src/bin/ltl2tgba.cc, src/bin/man/ltl2tgba.x: New files.
* src/bin/Makefile.am, src/bin/man/Makefile.am: Add them.
* src/tgbatest/spotlbtt.test: Prune the list of configurations slightly.
* src/tgbatest/spotlbtt2.test: New file.
* src/tgbatest/Makefile.am: Add it.
* bench/ltl2tgba/algorithms, bench/ltl2tgba/defs.in: Adjust to
use the new binary.
* NEWS: Update.
parent 26deb56a
...@@ -54,6 +54,10 @@ New in spot 0.9.2a: ...@@ -54,6 +54,10 @@ New in spot 0.9.2a:
files of formulas between different syntaxes, apply files of formulas between different syntaxes, apply
some simplifications, check whether to formulas are some simplifications, check whether to formulas are
equivalent, ... equivalent, ...
- ltl2tgba translate LTL/PSL formulas into Büchi automata. A
fondamental change to the interface is that you may
now specify the goal of the translation: do you
you favor deterministic or smaller automata?
New in spot 0.9.2 (2012-07-02): New in spot 0.9.2 (2012-07-02):
......
...@@ -77,100 +77,21 @@ Algorithm ...@@ -77,100 +77,21 @@ Algorithm
Path = "$LTL2NBA" Path = "$LTL2NBA"
Enabled = $HAVE_LTL2NBA Enabled = $HAVE_LTL2NBA
} }
EOF
Algorithm
{
Name = "Spot FM (degen)"
Path = "$LBTT_TRANSLATE"
Parameters = "--spin '$LTL2TGBA -f -N -R3 -r7 -F'"
Enabled = yes
}
Algorithm
{
Name = "Spot FM det. (degen)"
Path = "$LBTT_TRANSLATE"
Parameters = "--spin '$LTL2TGBA -f -N -R3 -r7 -x -F'"
Enabled = yes
}
Algorithm
{
Name = "Spot FM Sim (degen)"
Path = "$LBTT_TRANSLATE"
Parameters = "--spin '$LTL2TGBA -f -N -R3 -r7 -x -RIS -F'"
Enabled = yes
}
Algorithm
{
Name = "Spot FM WDBA (degen)"
Path = "$LBTT_TRANSLATE"
Parameters = "--spin '$LTL2TGBA -f -N -R3 -r7 -x -Rm -F'"
Enabled = yes
}
Algorithm
{
Name = "Spot FM WDBA+Sim (degen)"
Path = "$LBTT_TRANSLATE"
Parameters = "--spin '$LTL2TGBA -f -N -R3 -r7 -x -Rm -RIS -F'"
Enabled = yes
}
Algorithm
{
Name = "Spot FM (TGBA)"
Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -f -t -R3f -r7 -F'"
Enabled = yes
}
Algorithm
{
Name = "Spot FM det. (TGBA)"
Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -f -t -R3f -r7 -x -F'"
Enabled = yes
}
Algorithm
{
Name = "Spot FM Sim (TGBA)"
Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -f -t -R3 -r7 -x -RIS -F'"
Enabled = yes
}
Algorithm
{
Name = "Spot FM WDBA (TGBA)"
Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -f -t -R3f -r7 -x -Rm -F'"
Enabled = yes
}
Algorithm
{
Name = "Spot FM WDBA* (TGBA)"
Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -f -t -R3f -r7 -x -RM -F'"
Enabled = yes
}
Algorithm
{
Name = "Spot FM WDBA+ISim (TGBA)"
Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -f -t -R3 -r7 -x -Rm -RIS -F'"
Enabled = yes
}
for type in tgba ba; do
for pref in any deterministic small; do
for level in high; do
cat >>$conffile <<EOF
Algorithm Algorithm
{ {
Name = "Spot FM WDBA*+ISim (TGBA)" Name = "Spot ($type $pref $level)"
Path = "$LBTT_TRANSLATE" Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '$LTL2TGBA -f -t -R3 -r7 -x -RM -RIS -F'" Parameters = "--spot '$LTL2TGBA --$type --$pref --$level --lbtt -F'"
Enabled = yes Enabled = yes
} }
EOF EOF
done
done
done
...@@ -43,8 +43,7 @@ LBTT_TRANSLATE="@LBTT_TRANSLATE@" ...@@ -43,8 +43,7 @@ LBTT_TRANSLATE="@LBTT_TRANSLATE@"
LTL2BA="@LTL2BA@" LTL2BA="@LTL2BA@"
LTL3BA="@LTL3BA@" LTL3BA="@LTL3BA@"
LTL2NBA="@LTL2NBA@" LTL2NBA="@LTL2NBA@"
LTL2TGBA="@top_builddir@/src/tgbatest/ltl2tgba@EXEEXT@" LTL2TGBA="@top_builddir@/src/bin/ltl2tgba@EXEEXT@"
ELTL2TGBA="@top_builddir@/src/tgbatest/eltl2tgba@EXEEXT@"
MODELLA="@MODELLA@" MODELLA="@MODELLA@"
SPIN="@SPIN@" SPIN="@SPIN@"
WRING2LBTT="@WRING2LBTT@" WRING2LBTT="@WRING2LBTT@"
......
ltlfilt ltlfilt
ltl2tgba
randltl
genltl
*.a
*.1
...@@ -36,7 +36,8 @@ libcommon_a_SOURCES = \ ...@@ -36,7 +36,8 @@ libcommon_a_SOURCES = \
common_r.hh \ common_r.hh \
common_sys.hh common_sys.hh
bin_PROGRAMS = ltlfilt genltl randltl bin_PROGRAMS = ltlfilt genltl randltl ltl2tgba
ltlfilt_SOURCES = ltlfilt.cc ltlfilt_SOURCES = ltlfilt.cc
genltl_SOURCES = genltl.cc genltl_SOURCES = genltl.cc
randltl_SOURCES = randltl.cc randltl_SOURCES = randltl.cc
ltl2tgba_SOURCES = ltl2tgba.cc
// -*- 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_sys.hh"
#include <vector>
#include <string>
#include <iostream>
#include <fstream>
#include <argp.h>
#include "progname.h"
#include "error.h"
#include "common_r.hh"
#include "misc/_config.h"
#include "ltlparse/public.hh"
#include "ltlvisit/simplify.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/postproc.hh"
#include "tgbaalgos/save.hh"
const char* argp_program_version = "\
ltl2tgba (" 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[] ="\
Translate linear formulas (LTL/PSL) into Büchi automata.\n\n\
The default is to take the time to apply all available optimization \
to output the smallest Transition-based Generalized Büchi Automata, \
in GraphViz's format.\n\
If multiple formulas are supplied, several automata will be output.";
#define OPT_TGBA 1
#define OPT_SMALL 2
#define OPT_LOW 3
#define OPT_MEDIUM 4
#define OPT_HIGH 5
#define OPT_DOT 6
#define OPT_LBTT 7
#define OPT_SPOT 8
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 },
{ "ba", 'B', 0, 0, "Büchi Automaton", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Output format:", 3 },
{ "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 },
{ "lbtt", OPT_LBTT, 0, 0, "LBTT's format", 0 },
{ "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
{ "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Translation intent:", 4 },
{ "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 0 },
{ "deterministic", 'D', 0, 0, "prefer deterministic automata", 0 },
{ "any", 'a', 0, 0, "no preference", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Optimization level:", 5 },
{ "low", OPT_LOW, 0, 0, "minimal optimizations (fast)", 0 },
{ "medium", OPT_MEDIUM, 0, 0, "moderate optimizations", 0 },
{ "high", OPT_HIGH, 0, 0,
"all available optimizations (slow, default)", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
{ 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)
{
}
};
typedef std::vector<job> jobs_t;
static jobs_t jobs;
spot::postprocessor::output_type type = spot::postprocessor::TGBA;
spot::postprocessor::output_pref pref = spot::postprocessor::Small;
spot::postprocessor::optimization_level level = spot::postprocessor::High;
enum output_format { Dot, Lbtt, Spin, Spot } format = Dot;
static int
parse_opt(int key, char* arg, struct argp_state*)
{
// This switch is alphabetically-ordered.
switch (key)
{
case 'a':
pref = spot::postprocessor::Any;
break;
case 'B':
type = spot::postprocessor::BA;
break;
case 'D':
pref = spot::postprocessor::Deterministic;
break;
case 'f':
jobs.push_back(job(arg, false));
break;
case 'F':
jobs.push_back(job(arg, true));
break;
case 's':
format = Spin;
type = spot::postprocessor::BA;
break;
case OPT_HIGH:
level = spot::postprocessor::High;
simplification_level = 3;
break;
case OPT_DOT:
format = Dot;
break;
case OPT_LBTT:
format = Lbtt;
break;
case OPT_LOW:
level = spot::postprocessor::Low;
simplification_level = 1;
break;
case OPT_MEDIUM:
level = spot::postprocessor::Medium;
simplification_level = 2;
break;
case OPT_SMALL:
pref = spot::postprocessor::Small;
break;
case OPT_SPOT:
format = Spot;
break;
case OPT_TGBA:
if (format == Spin)
error(2, 0, "--spin and --tgba are incompatible");
type = spot::postprocessor::TGBA;
break;
case ARGP_KEY_ARG:
// FIXME: use stat() to distinguish filename from string?
jobs.push_back(job(arg, false));
break;
default:
return ARGP_ERR_UNKNOWN;
}
return 0;
}
namespace
{
class trans_processor
{
public:
spot::ltl::ltl_simplifier& simpl;
spot::postprocessor& post;
trans_processor(spot::ltl::ltl_simplifier& simpl,
spot::postprocessor& post)
: simpl(simpl), post(post)
{
}
int
process_formula(const std::string& input,
const char* filename = 0, int linenum = 0)
{
spot::ltl::parse_error_list pel;
const spot::ltl::formula* f = spot::ltl::parse(input, pel);
if (!f || pel.size() > 0)
{
if (filename)
error_at_line(0, 0, filename, linenum, "parse error:");
spot::ltl::format_parse_errors(std::cerr, input, pel);
if (f)
f->destroy();
return 1;
}
const spot::ltl::formula* res = simpl.simplify(f);
f->destroy();
f = res;
// This helps ltl_to_tgba_fm() to order BDD variables in a more
// natural way (improving the degeneralization).
simpl.clear_as_bdd_cache();
bool exprop = level == spot::postprocessor::High;
const spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict(), exprop);
aut = post.run(aut, f);
switch (format)
{
case Dot:
spot::dotty_reachable(std::cout, aut);
break;
case Lbtt:
spot::lbtt_reachable(std::cout, aut);
break;
case Spot:
spot::tgba_save_reachable(std::cout, aut);
break;
case Spin:
spot::never_claim_reachable(std::cout, aut, f);
break;
}
delete aut;
return 0;
}
int
process_stream(std::istream& is, const char* filename)
{
int error = 0;
int linenum = 0;
std::string line;
while (std::getline(is, line))
error |= process_formula(line, filename, ++linenum);
return error;
}
int
process_file(const char* filename)
{
// Special case for stdin.
if (filename[0] == '-' && filename[1] == 0)
return process_stream(std::cin, filename);
errno = 0;
std::ifstream input(filename);
if (!input)
error(2, errno, "cannot open '%s'", filename);
return process_stream(input, filename);
}
};
}
static int
run_jobs()
{
spot::ltl::ltl_simplifier simpl(simplifier_options());
spot::postprocessor postproc;
postproc.set_pref(pref);
postproc.set_type(type);
postproc.set_level(level);
trans_processor processor(simpl, postproc);
int error = 0;
jobs_t::const_iterator i;
for (i = jobs.begin(); i != jobs.end(); ++i)
{
if (!i->file_p)
error |= processor.process_formula(i->str);
else
error |= processor.process_file(i->str);
}
if (error)
return 2;
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, "[FORMULA...]",
argp_program_doc, 0, 0, 0 };
if (int err = argp_parse(&ap, argc, argv, 0, 0, 0))
exit(err);
if (jobs.empty())
error(2, 0, "No formula to translate? Run '%s --help' for usage.",
program_name);
return run_jobs();
}
...@@ -22,12 +22,15 @@ ...@@ -22,12 +22,15 @@
common_dep = $(top_builddir)/configure.ac common_dep = $(top_builddir)/configure.ac
x_to_1 = $(top_builddir)/tools/x-to-1 x_to_1 = $(top_builddir)/tools/x-to-1
convman = ARGP_HELP_FMT=header-col=0 $(SHELL) "$(x_to_1)" \ convman = ARGP_HELP_FMT=header-col=0 $(SHELL) "$(x_to_1)" \
"$(PERL)" "$(top_srcdir)/tools/help2man -N" "$(PERL)" "$(top_srcdir)/tools/help2man -N -L 'en_US.UTF-8'"
dist_man1_MANS = ltlfilt.1 genltl.1 randltl.1 dist_man1_MANS = ltlfilt.1 genltl.1 randltl.1 ltl2tgba.1
MAINTAINERCLEANFILES = $(dist_man1_MANS) MAINTAINERCLEANFILES = $(dist_man1_MANS)
EXTRA_DIST = $(dist_man1_MANS:.1=.x) EXTRA_DIST = $(dist_man1_MANS:.1=.x)
ltl2tgba.1: $(common_dep) $(srcdir)/ltl2tgba.x $(srcdir)/../ltl2tgba.cc
$(convman) ../ltl2tgba$(EXEEXT) $(srcdir)/ltl2tgba.x $@
ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc
$(convman) ../ltlfilt$(EXEEXT) $(srcdir)/ltlfilt.x $@ $(convman) ../ltlfilt$(EXEEXT) $(srcdir)/ltlfilt.x $@
...@@ -36,5 +39,3 @@ genltl.1: $(common_dep) $(srcdir)/genltl.x $(srcdir)/../genltl.cc ...@@ -36,5 +39,3 @@ genltl.1: $(common_dep) $(srcdir)/genltl.x $(srcdir)/../genltl.cc
randltl.1: $(common_dep) $(srcdir)/randltl.x $(srcdir)/../randltl.cc randltl.1: $(common_dep) $(srcdir)/randltl.x $(srcdir)/../randltl.cc
$(convman) ../randltl$(EXEEXT) $(srcdir)/randltl.x $@ $(convman) ../randltl$(EXEEXT) $(srcdir)/randltl.x $@
[NAME]
ltl2tgba \- translate LTL/PSL formulas into Büchi automata
[DESCRIPTION]
.\" Add any additional description here
...@@ -48,6 +48,7 @@ tgbaalgos_HEADERS = \ ...@@ -48,6 +48,7 @@ tgbaalgos_HEADERS = \
magic.hh \ magic.hh \
minimize.hh \ minimize.hh \
neverclaim.hh \ neverclaim.hh \
postproc.hh \
powerset.hh \ powerset.hh \
projrun.hh \ projrun.hh \
randomgraph.hh \ randomgraph.hh \
...@@ -87,6 +88,7 @@ libtgbaalgos_la_SOURCES = \ ...@@ -87,6 +88,7 @@ libtgbaalgos_la_SOURCES = \
minimize.cc \ minimize.cc \
ndfs_result.hxx \ ndfs_result.hxx \
neverclaim.cc \ neverclaim.cc \
postproc.cc \
powerset.cc \ powerset.cc \
projrun.cc \ projrun.cc \
randomgraph.cc \ randomgraph.cc \
......
// -*- 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 "postproc.hh"
#include "minimize.hh"
#include "simulation.hh"
#include "sccfilter.hh"
#include "degen.hh"
#include "stats.hh"
namespace spot
{
unsigned count_states(const tgba* a)
{
// FIXME: the number of states can be found more
// efficiently in explicit automata.
tgba_statistics st = stats_reachable(a);
return st.states;
}
const tgba* postprocessor::run(const tgba* a, const ltl::formula* f)
{
if (type_ == TGBA && pref_ == Any && level_ == Low)
return a;
// Remove useless SCCs.
{
const tgba* s = scc_filter(a, false);
delete a;
a = s;
}
if (pref_ == Any)
{
if (type_ == BA)
{
const tgba* d = degeneralize(a);
delete a;
a = d;
}
return a;
}
const tgba* wdba = 0;
const tgba* sim = 0;
// (Small,Low) is the only configuration where we do not run
// WDBA-minimization.
if (pref_ != Small || level_ != Low)
{