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

dstar2tgba: new command.

* src/bin/dstar2tgba.cc, src/bin/man/dstar2tgba.x: New files.
* src/bin/Makefile.am, src/bin/man/Makefile.am: Add them.
* NEWS: Mention it.
* src/bin/ltl2tgba.cc, src/tgbaalgos/stats.cc, doc/org/ltl2tgba.org:
Rename the %S sequence as %c, for consistency with dstar2tgba.
* src/tgbatest/ltl2dstar.test: Add more tests.
* src/tgbatest/ltl2dstar2.test: New file.
* src/tgbatest/Makefile.am: Add it.
parent 9a7590a6
New in spot 1.1.4a (not relased)
* All the parsers implemented in Spot now use the same type
to store locations.
* Changes to command-line tools:
* ltlcross has a new option --color to color its output. It is enabled
by default when the output is a terminal.
- ltlcross has a new option --color to color its output. It is
enabled by default when the output is a terminal.
* ltlcross will give an example of infinite word accepted by the
two automata when the product between a positive automaton and
a negative automaton is non-empty.
- ltlcross will give an example of infinite word accepted by the
two automata when the product between a positive automaton and a
negative automaton is non-empty.
* ltlcross can now read the Rabin and Streett automata output by
- ltlcross can now read the Rabin and Streett automata output by
ltl2dstar. This type of output should be specified using '%D':
ltlcross 'ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-s %L %D'
......@@ -21,9 +20,25 @@ New in spot 1.1.4a (not relased)
search for bugs in translators to Rabin or Streett automata, but
the statistics might not be very relevant.
* Environment variables SPOT_TMPDIR and SPOT_TMPKEEP control where
- To help with debugging problems detected by ltlcross, the
environment variables SPOT_TMPDIR and SPOT_TMPKEEP control where
temporary files are created and if they should be erased. Read
the man page of ltlcross for detail.
the man page of ltlcross for details.
- There is a new command, named dstar2tgba, that converts a
deterministic Rabin or Streett automaton as output by
ltl2dstar into a TGBA, BA or Monitor. When a deterministic
Rabin automaton is realizable by a deterministic Büchi automaton,
the conversion preserve determinism. (This is not implemented
for Streett.)
- The %S escape sequence used by ltl2tgba --stats to display the
number of SCCs in the output automaton has been renamed to %c.
This makes it more homogeneous with the --stats option of the
new dstar2tgba command.
* All the parsers implemented in Spot now use the same type
to store locations.
* Degeneralization was not indempotant on automata with an accepting
initial state that was on a cycle, but without self-loop.
......
......@@ -546,12 +546,12 @@ ltl2tgba --help | sed -n '/^ *%/p'
#+RESULTS:
: %% a single %
: %a number of acceptance sets
: %c number of SCCs
: %d 1 if the automaton is deterministic, 0 otherwise
: %e number of edges
: %f the formula, in Spot's syntax
: %n number of nondeterministic states
: %s number of states
: %S number of SCCs
: %t number of transitions
For instance we can study the size of the automata generated for the
......
......@@ -42,7 +42,8 @@ libcommon_a_SOURCES = \
common_setup.hh \
common_sys.hh
bin_PROGRAMS = ltlfilt genltl randltl ltl2tgba ltl2tgta ltlcross
bin_PROGRAMS = ltlfilt genltl randltl ltl2tgba ltl2tgta ltlcross \
dstar2tgba
# Dummy program used just to generate man/spot-x.7 in a way that is
# consistent with the other man pages (e.g., with a version number that
......@@ -55,5 +56,6 @@ randltl_SOURCES = randltl.cc
ltl2tgba_SOURCES = ltl2tgba.cc
ltl2tgta_SOURCES = ltl2tgta.cc
ltlcross_SOURCES = ltlcross.cc
dstar2tgba_SOURCES = dstar2tgba.cc
spot_x_SOURCES = spot-x.cc
ltlcross_LDADD = $(LDADD) $(LIB_GETHRXTIME)
// -*- coding: utf-8 -*-
// Copyright (C) 2013 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_sys.hh"
#include <string>
#include <iostream>
#include <argp.h>
#include "error.h"
#include "common_setup.hh"
#include "common_finput.hh"
#include "common_cout.hh"
#include "common_post.hh"
#include "ltlast/formula.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh"
#include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/save.hh"
#include "tgbaalgos/stats.hh"
#include "tgba/bddprint.hh"
#include "misc/optionmap.hh"
#include "dstarparse/public.hh"
#include "tgbaalgos/scc.hh"
const char argp_program_doc[] ="\
Convert Rabin and Streett automata into Büchi automata.\n\n\
This reads the output format of ltl2dstar and will output a \n\
Transition-based Generalized Büchi Automata in GraphViz's format by default.\n\
If multiple files are supplied (one automaton per file), several automata\n\
will be output.";
#define OPT_TGBA 1
#define OPT_DOT 2
#define OPT_LBTT 3
#define OPT_SPOT 4
#define OPT_STATS 5
static const argp_option options[] =
{
/**************************************************/
{ 0, 0, 0, 0, "Input:", 1 },
{ "file", 'F', "FILENAME", 0,
"process the automaton in FILENAME", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Output automaton type:", 2 },
{ "tgba", OPT_TGBA, 0, 0,
"Transition-based Generalized Büchi Automaton (default)", 0 },
{ "ba", 'B', 0, 0, "Büchi Automaton", 0 },
{ "monitor", 'M', 0, 0, "Monitor (accepts all finite prefixes "
"of the given formula)", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Output format:", 3 },
{ "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 },
{ "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
"LBTT's format (add =t to force transition-based acceptance even"
" on Büchi automata)", 0 },
{ "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
{ "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
{ "utf8", '8', 0, 0, "enable UTF-8 characters in output "
"(ignored with --lbtt or --spin)", 0 },
{ "stats", OPT_STATS, "FORMAT", 0,
"output statistics about the automaton", 0 },
/**************************************************/
{ 0, 0, 0, 0, "The FORMAT string passed to --stats may use "\
"the following interpreted sequences (capitals for input,"
" minuscules for output):", 4 },
{ "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"name of the input file", 0 },
{ "%S, %s", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"number of states", 0 },
{ "%E, %e", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"number of edges", 0 },
{ "%T, %t", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"number of transitions", 0 },
{ "%A, %a", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"number of acceptance pairs or sets", 0 },
{ "%C, %c", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"number of SCCs", 0 },
{ "%n", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"number of nondeterministic states in output", 0 },
{ "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"1 if the output is deterministic, 0 otherwise", 0 },
{ "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"a single %", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
{ "extra-options", 'x', "OPTS", 0,
"fine-tuning options (see spot-x (7))", 0 },
{ 0, 0, 0, 0, 0, 0 }
};
const struct argp_child children[] =
{
{ &post_argp, 0, 0, 20 },
{ &misc_argp, 0, 0, -1 },
{ 0, 0, 0, 0 }
};
enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats } format = Dot;
bool utf8 = false;
const char* stats = "";
spot::option_map extra_options;
static int
parse_opt(int key, char* arg, struct argp_state*)
{
// This switch is alphabetically-ordered.
switch (key)
{
case '8':
spot::enable_utf8();
break;
case 'B':
type = spot::postprocessor::BA;
break;
case 'F':
jobs.push_back(job(arg, true));
break;
case 'M':
type = spot::postprocessor::Monitor;
break;
case 's':
format = Spin;
if (type != spot::postprocessor::Monitor)
type = spot::postprocessor::BA;
break;
case 'x':
{
const char* opt = extra_options.parse_options(arg);
if (opt)
error(2, 0, "failed to parse --options near '%s'", opt);
}
break;
case OPT_DOT:
format = Dot;
break;
case OPT_LBTT:
if (arg)
{
if (arg[0] == 't' && arg[1] == 0)
format = Lbtt_t;
else
error(2, 0, "unknown argument for --lbtt: '%s'", arg);
}
else
{
format = Lbtt;
}
break;
case OPT_SPOT:
format = Spot;
break;
case OPT_STATS:
if (!*arg)
error(2, 0, "empty format string for --stats");
stats = arg;
format = Stats;
break;
case OPT_TGBA:
if (format == Spin)
error(2, 0, "--spin and --tgba are incompatible");
type = spot::postprocessor::TGBA;
break;
case ARGP_KEY_ARG:
jobs.push_back(job(arg, true));
break;
default:
return ARGP_ERR_UNKNOWN;
}
return 0;
}
namespace
{
/// \brief prints various statistics about a TGBA
///
/// This object can be configured to display various statistics
/// about a TGBA. Some %-sequence of characters are interpreted in
/// the format string, and replaced by the corresponding statistics.
class dstar_stat_printer: protected spot::stat_printer
{
public:
dstar_stat_printer(std::ostream& os, const char* format)
: spot::stat_printer(os, format)
{
declare('A', &daut_acc_);
declare('C', &daut_scc_);
declare('E', &daut_edges_);
declare('F', &filename_);
declare('f', &filename_); // Override the formula printer.
declare('S', &daut_states_);
declare('T', &daut_trans_);
}
/// \brief print the configured statistics.
///
/// The \a f argument is not needed if the Formula does not need
/// to be output.
std::ostream&
print(const spot::dstar_aut* daut, const spot::tgba* aut,
const char* filename)
{
filename_ = filename;
if (has('T'))
{
spot::tgba_sub_statistics s = sub_stats_reachable(daut->aut);
daut_states_ = s.states;
daut_edges_ = s.transitions;
daut_trans_ = s.sub_transitions;
}
else if (has('E'))
{
spot::tgba_sub_statistics s = sub_stats_reachable(daut->aut);
daut_states_ = s.states;
daut_edges_ = s.transitions;
}
else if (has('S'))
{
daut_states_ = daut->aut->num_states();
}
if (has('A'))
daut_acc_ = daut->accpair_count;
if (has('C'))
{
spot::scc_map m(daut->aut);
m.build_map();
daut_scc_ = m.scc_count();
}
return this->spot::stat_printer::print(aut);
}
private:
spot::printable_value<const char*> filename_;
spot::printable_value<unsigned> daut_states_;
spot::printable_value<unsigned> daut_edges_;
spot::printable_value<unsigned> daut_trans_;
spot::printable_value<unsigned> daut_acc_;
spot::printable_value<unsigned> daut_scc_;
};
class dstar_processor: public job_processor
{
public:
spot::postprocessor& post;
dstar_stat_printer statistics;
dstar_processor(spot::postprocessor& post)
: post(post), statistics(std::cout, stats)
{
}
int
process_formula(const spot::ltl::formula*, const char*, int)
{
assert(!"should not happen");
return 0;
}
int
process_file(const char* filename)
{
spot::dstar_parse_error_list pel;
spot::dstar_aut* daut;
spot::bdd_dict dict;
daut = spot::dstar_parse(filename, pel, &dict);
if (spot::format_dstar_parse_errors(std::cerr, filename, pel))
{
delete daut;
return 2;
}
if (!daut)
{
error(2, 0, "failed to read automaton from %s", filename);
}
spot::tgba* nba = spot::dstar_to_tgba(daut);
const spot::tgba* aut = post.run(nba, 0);
if (utf8)
{
spot::tgba* a = const_cast<spot::tgba*>(aut);
if (spot::tgba_explicit_formula* tef =
dynamic_cast<spot::tgba_explicit_formula*>(a))
tef->enable_utf8();
else if (spot::sba_explicit_formula* sef =
dynamic_cast<spot::sba_explicit_formula*>(a))
sef->enable_utf8();
}
switch (format)
{
case Dot:
spot::dotty_reachable(std::cout, aut,
(type == spot::postprocessor::BA)
|| (type == spot::postprocessor::Monitor));
break;
case Lbtt:
spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA);
break;
case Lbtt_t:
spot::lbtt_reachable(std::cout, aut, false);
break;
case Spot:
spot::tgba_save_reachable(std::cout, aut);
break;
case Spin:
spot::never_claim_reachable(std::cout, aut);
break;
case Stats:
// FIXME: filename
statistics.print(daut, aut, filename) << "\n";
break;
}
delete aut;
delete daut;
flush_cout();
return 0;
}
};
}
int
main(int argc, char** argv)
{
setup(argv);
const argp ap = { options, parse_opt, "[FILENAMES...]",
argp_program_doc, children, 0, 0 };
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
exit(err);
if (jobs.empty())
jobs.push_back(job("-", true));
spot::postprocessor post(&extra_options);
post.set_pref(pref);
post.set_type(type);
post.set_level(level);
dstar_processor processor(post);
if (processor.run())
return 2;
return 0;
}
......@@ -86,7 +86,7 @@ static const argp_option options[] =
{ "%t", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of transitions", 0 },
{ "%a", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"number of acceptance sets", 0 },
{ "%S", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of SCCs", 0 },
{ "%c", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of SCCs", 0 },
{ "%n", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"number of nondeterministic states", 0 },
{ "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
......
......@@ -23,6 +23,7 @@ convman = ARGP_HELP_FMT=header-col=0 $(SHELL) "$(x_to_1)" \
"$(PERL)" "$(top_srcdir)/tools/help2man -N -L 'en_US.UTF-8'"
dist_man1_MANS = \
dstar2tgba.1 \
genltl.1 \
ltl2tgba.1 \
ltl2tgta.1 \
......@@ -35,6 +36,9 @@ dist_man7_MANS = \
MAINTAINERCLEANFILES = $(dist_man1_MANS) $(dist_man7_MANS)
EXTRA_DIST = $(dist_man1_MANS:.1=.x) $(dist_man7_MANS:.7=.x)
dstar2tgba.1: $(common_dep) $(srcdir)/dstar2tgba.x $(srcdir)/../dstar2tgba.cc
$(convman) ../dstar2tgba$(EXEEXT) $(srcdir)/dstar2tgba.x $@
ltl2tgba.1: $(common_dep) $(srcdir)/ltl2tgba.x $(srcdir)/../ltl2tgba.cc
$(convman) ../ltl2tgba$(EXEEXT) $(srcdir)/ltl2tgba.x $@
......
[NAME]
dstar2tgba \- convert Rabin or Streett automata into Büchi automata
[BIBLIOGRAPHY]
.TP
1.
<http://www.ltl2dstar.de/docs/ltl2dstar.html>
Documents the output format of ltl2dstar.
.TP
2.
Chistof Löding: Mehods for the Transformation of ω-Automata:
Complexity and Connection to Second Order Logic. Diploma Thesis.
University of Kiel. 1998.
Describes various tranformations from non-deterministic Rabin and
Streett automata to Büchi automata. Slightly optimized variants of
these transformations are used by dstar2tgba for the general cases.
.TP
3.
Sriram C. Krishnan, Anuj Puri, and Robert K. Brayton: Deterministic
ω-automata vis-a-vis Deterministic Büchi Automata. ISAAC'94.
Explains how to preserve the determinism of Rabin and Streett automata
when the property can be repreted by a Deterministic automaton.
dstar2tgba implements this for the Rabin case only. In other words,
translating a deterministic Rabin automaton with dstar2tgba will
produce a deterministic TGBA or BA if such a automaton exists.
[SEE ALSO]
.BR spot-x (7)
// Copyright (C) 2008, 2011, 2012 Laboratoire de Recherche et Développement
// Copyright (C) 2008, 2011, 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
......@@ -142,12 +142,13 @@ namespace spot
: format_(format)
{
declare('a', &acc_);
declare('c', &scc_);
declare('d', &deterministic_);
declare('e', &edges_);
declare('f', &form_);
declare('n', &nondetstates_);
declare('s', &states_);
declare('S', &scc_);
declare('S', &scc_); // Historical. Deprecated. Use %c instead.
declare('t', &trans_);
set_output(os);
prime(format);
......@@ -176,7 +177,7 @@ namespace spot
if (has('a'))
acc_ = aut->number_of_acceptance_conditions();
if (has('S'))
if (has('c') || has('S'))
{
scc_map m(aut);
m.build_map();
......
......@@ -111,6 +111,7 @@ TESTS = \
wdba2.test \
babiak.test \
ltl2dstar.test \
ltl2dstar2.test \
randtgba.test \
emptchk.test \
emptchke.test \
......
......@@ -33,6 +33,7 @@ ltl2tgba=../../bin/ltl2tgba
ltlcross=../../bin/ltlcross
randltl=../../bin/randltl
ltlfilt=../../bin/ltlfilt
dstar2tgba=../../bin/dstar2tgba
$ltlfilt -f 'a U b' -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-s - - |
......@@ -62,11 +63,16 @@ EOF
diff expected out
RAB=--automata=rabin
STR=--automata=streett
$randltl -n 15 a b | $ltlfilt --nnf --remove-wm |
$ltlcross -F - -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \
--timeout=10 \
--timeout=30 \
"$ltl2tgba -s %f >%N" \
"ltl2dstar --automata=rabin --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \
"ltl2dstar --automata=rabin --ltl2nba=spin:$ltl2tgba@-s %L %D" \
"ltl2dstar --automata=streett --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \
"ltl2dstar --automata=streett --ltl2nba=spin:$ltl2tgba@-s %L %D"
"ltl2dstar $RAB --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \
"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \
"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L - | $dstar2tgba --low -s >%N" \
"ltl2dstar $STR --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" \
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L - | $dstar2tgba --low -s >%N"
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013 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/>.
# Do some quick translations to make sure the neverclaims produced by
# spot actually look correct! We do that by parsing them via ltlcross.
# ltl2neverclaim-lbtt.test does the same with LBTT if it is installed.
. ./defs
set -e
# Skip this test if ltl2dstar is not installed.
(ltl2dstar --version) || exit 77
ltlfilt=../../bin/ltlfilt
ltl2tgba=../../bin/ltl2tgba
dstar2tgba=../../bin/dstar2tgba
randltl=../../bin/randltl
# Make sure all recurrence formulas are translated into deterministic
# Büchi automata by the DRA->TGBA converster.
$randltl -n -1 a b --tree-size=5..15 |