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

postproc: add the possibility to output a monitor

* src/tgbaalgos/stripacc.cc, src/tgbaalgos/stripacc.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add a Monitor
output option.
* src/bin/ltl2tgba.cc: Add a --monitor/-M option.
* NEWS: Mention monitors.
* src/tgba/tgbaexplicit.hh (is_accepting_state): Fix for the
case where the automaton has no acceptance set.
parent 5f6c262a
...@@ -25,17 +25,19 @@ New in spot 0.9.2a: ...@@ -25,17 +25,19 @@ New in spot 0.9.2a:
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 - ltl2tgba: Translate LTL/PSL formulas into Büchi automata (TGBA,
fondamental change to the interface is that you may BA, or Monitor). A fondamental change to the
now specify the goal of the translation: do you interface is that you may now specify the goal of the
you favor deterministic or smaller automata? translation: do you you favor deterministic or smaller
automata?
- ltl2tgta: Translate LTL/PSL formulas into Testing Automata. - ltl2tgta: Translate LTL/PSL formulas into Testing Automata.
- ltlcheck: A tool to find bugs in translators from LTL/PSL to - ltlcheck: Compare the output of translators from LTL/PSL to
Büchi automata. This is essentially a Spot-based Büchi automata, to find bug or for benchmarking. This
reimplementation of LBTT that supports PSL in addition is essentially a Spot-based reimplementation of LBTT
to LTL, and that can output more statistics. that supports PSL in addition to LTL, and that can
output more statistics.
These binaries are built in the src/bin/ directory. The former These binaries are built in the src/bin/ directory. The former
test versions of genltl and randltl have been removed from the test versions of genltl and randltl have been removed from the
...@@ -113,7 +115,7 @@ New in spot 0.9.2a: ...@@ -113,7 +115,7 @@ New in spot 0.9.2a:
automata generated with the web interface.) automata generated with the web interface.)
- A new class, "postprocessor", makes it easier to apply - A new class, "postprocessor", makes it easier to apply
all availlable simplification algorithms on a TGBA. all availlable simplification algorithms on a TGBA/BA/Monitors.
* Minor changes: * Minor changes:
......
...@@ -56,10 +56,12 @@ If multiple formulas are supplied, several automata will be output."; ...@@ -56,10 +56,12 @@ If multiple formulas are supplied, several automata will be output.";
static const argp_option options[] = static const argp_option options[] =
{ {
/**************************************************/ /**************************************************/
{ 0, 0, 0, 0, "Automaton type:", 2 }, { 0, 0, 0, 0, "Output automaton type:", 2 },
{ "tgba", OPT_TGBA, 0, 0, { "tgba", OPT_TGBA, 0, 0,
"Transition-based Generalized Büchi Automaton (default)", 0 }, "Transition-based Generalized Büchi Automaton (default)", 0 },
{ "ba", 'B', 0, 0, "Büchi Automaton", 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 }, { 0, 0, 0, 0, "Output format:", 3 },
{ "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 },
...@@ -116,9 +118,13 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -116,9 +118,13 @@ parse_opt(int key, char* arg, struct argp_state*)
case 'B': case 'B':
type = spot::postprocessor::BA; type = spot::postprocessor::BA;
break; break;
case 'M':
type = spot::postprocessor::Monitor;
break;
case 's': case 's':
format = Spin; format = Spin;
type = spot::postprocessor::BA; if (type != spot::postprocessor::Monitor)
type = spot::postprocessor::BA;
break; break;
case OPT_DOT: case OPT_DOT:
format = Dot; format = Dot;
...@@ -209,7 +215,8 @@ namespace ...@@ -209,7 +215,8 @@ namespace
{ {
case Dot: case Dot:
spot::dotty_reachable(std::cout, aut, spot::dotty_reachable(std::cout, aut,
type == spot::postprocessor::BA); (type == spot::postprocessor::BA)
|| (type == spot::postprocessor::Monitor));
break; break;
case Lbtt: case Lbtt:
spot::lbtt_reachable(std::cout, aut); spot::lbtt_reachable(std::cout, aut);
......
...@@ -710,7 +710,8 @@ namespace spot ...@@ -710,7 +710,8 @@ namespace spot
// So we need only to check one to decide // So we need only to check one to decide
if (st->successors.empty()) if (st->successors.empty())
return false; return false;
return st->successors.front().acceptance_conditions != bddfalse; return (st->successors.front().acceptance_conditions
== this->all_acceptance_conditions_);
} }
private: private:
......
...@@ -63,6 +63,7 @@ tgbaalgos_HEADERS = \ ...@@ -63,6 +63,7 @@ tgbaalgos_HEADERS = \
se05.hh \ se05.hh \
simulation.hh \ simulation.hh \
stats.hh \ stats.hh \
stripacc.hh \
tau03.hh \ tau03.hh \
tau03opt.hh \ tau03opt.hh \
reductgba_sim.hh \ reductgba_sim.hh \
...@@ -105,6 +106,7 @@ libtgbaalgos_la_SOURCES = \ ...@@ -105,6 +106,7 @@ libtgbaalgos_la_SOURCES = \
se05.cc \ se05.cc \
simulation.cc \ simulation.cc \
stats.cc \ stats.cc \
stripacc.cc \
tau03.cc \ tau03.cc \
tau03opt.cc \ tau03opt.cc \
reductgba_sim.cc \ reductgba_sim.cc \
......
...@@ -23,6 +23,7 @@ ...@@ -23,6 +23,7 @@
#include "sccfilter.hh" #include "sccfilter.hh"
#include "degen.hh" #include "degen.hh"
#include "stats.hh" #include "stats.hh"
#include "stripacc.hh"
namespace spot namespace spot
{ {
...@@ -46,6 +47,49 @@ namespace spot ...@@ -46,6 +47,49 @@ namespace spot
a = s; a = s;
} }
if (type_ == Monitor)
{
if (pref_ == Deterministic)
{
const tgba* m = minimize_monitor(a);
delete a;
return m;
}
else
{
const tgba* m = strip_acceptance(a);
delete a;
a = m;
}
if (pref_ == Any)
return a;
const tgba* sim;
if (level_ == Low)
sim = simulation(a);
else
sim = iterated_simulations(a);
if (level_ != High)
{
delete a;
return sim;
}
// For Small,High we return the smallest between the output of
// the simulation, and that of the deterministic minimization.
const tgba* m = minimize_monitor(a);
delete a;
if (count_states(m) > count_states(sim))
{
delete m;
return sim;
}
else
{
delete sim;
return m;
}
}
if (pref_ == Any) if (pref_ == Any)
{ {
if (type_ == BA) if (type_ == BA)
......
...@@ -27,7 +27,8 @@ namespace spot ...@@ -27,7 +27,8 @@ namespace spot
/// \addtogroup tgba_reduction /// \addtogroup tgba_reduction
/// @{ /// @{
/// \brief Wrap TGBA/BA post-processing algorithms in an easy interface. /// \brief Wrap TGBA/BA/Monitor post-processing algorithms in an
/// easy interface.
/// ///
/// This class is a shell around scc_filter(), /// This class is a shell around scc_filter(),
/// minimize_obligation(), simulation(), iterated_simulations(), and /// minimize_obligation(), simulation(), iterated_simulations(), and
...@@ -61,7 +62,7 @@ namespace spot ...@@ -61,7 +62,7 @@ namespace spot
{ {
} }
enum output_type { TGBA, BA }; enum output_type { TGBA, BA, Monitor };
void void
set_type(output_type type) set_type(output_type type)
{ {
......
// -*- 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 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 "stripacc.hh"
#include "reachiter.hh"
namespace spot
{
namespace
{
class strip_iter: public tgba_reachable_iterator_depth_first
{
public:
strip_iter(const tgba* a)
: tgba_reachable_iterator_depth_first(a),
out_(new sba_explicit_number(a->get_dict()))
{
}
sba_explicit_number*
result()
{
return out_;
}
void
process_link(const state*, int in,
const state*, int out,
const tgba_succ_iterator* si)
{
state_explicit_number::transition* t = out_->create_transition(in, out);
out_->add_conditions(t, si->current_condition());
}
private:
sba_explicit_number* out_;
};
}
sba_explicit_number*
strip_acceptance(const tgba* a)
{
strip_iter si(a);
si.run();
return si.result();
}
}
// -*- 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 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_TGBAALGOS_STRIPACC_HH
# define SPOT_TGBAALGOS_STRIPACC_HH
# include "tgba/tgbaexplicit.hh"
namespace spot
{
/// \brief Duplicate automaton \a a, removing all acceptance sets.
///
/// This is equivalent to marking all states/transitions as accepting.
/// \ingroup tgba_misc
sba_explicit_number* strip_acceptance(const tgba* a);
}
#endif // SPOT_TGBAALGOS_STRIPACC_HH
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment