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

dotty: get rid of the decorated version

Browse source 
* src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh,
src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: Delete.
* src/tgbaalgos/Makefile.am, wrap/python/spot.i: Adjust.
* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: Remove the
decorated version, and the related arguments.
* src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/complementation.cc,
src/tgbatest/emptchk.cc: Adjust calls.
* wrap/python/ajax/spot.in: Draw the accepting run as an
automaton instead of painting it.
* wrap/python/ajax/ltl2tgba.html: Update help text.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-24 11:54:39 +01:00
parent 947ab17b12
commit 49701ca3bc
15 changed files with 26 additions and 583 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/bin/common_aoutput.cc
View file

@ -236,10 +236,7 @@ automaton_printer::print(const spot::tgba_digraph_ptr& aut,
// Do not output anything. // Do not output anything.
break; break;
case Dot: case Dot:
spot::dotty_reachable(std::cout, aut, spot::dotty_reachable(std::cout, aut, opt_dot);
(type == spot::postprocessor::BA)
|| (type == spot::postprocessor::Monitor),
opt_dot);
break; break;
case Lbtt: case Lbtt:
spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA); spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA);

5
src/bin/dstar2tgba.cc
View file

@ -353,10 +353,7 @@ namespace
switch (format) switch (format)
{ {
case Dot: case Dot:
spot::dotty_reachable(std::cout, aut, spot::dotty_reachable(std::cout, aut, opt_dot);
(type == spot::postprocessor::BA)
|| (type == spot::postprocessor::Monitor),
opt_dot);
break; break;
case Lbtt: case Lbtt:
spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA); spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA);

4
src/tgbaalgos/Makefile.am
View file

@ -36,7 +36,6 @@ tgbaalgos_HEADERS = \
cycles.hh \ cycles.hh \
dtgbacomp.hh \ dtgbacomp.hh \
degen.hh \ degen.hh \
dottydec.hh \
dotty.hh \ dotty.hh \
dtbasat.hh \ dtbasat.hh \
dtgbasat.hh \ dtgbasat.hh \
@ -62,7 +61,6 @@ tgbaalgos_HEADERS = \
reachiter.hh \ reachiter.hh \
reducerun.hh \ reducerun.hh \
replayrun.hh \ replayrun.hh \
rundotdec.hh \
safety.hh \ safety.hh \
save.hh \ save.hh \
sccfilter.hh \ sccfilter.hh \
@ -89,7 +87,6 @@ libtgbaalgos_la_SOURCES = \
dtgbacomp.cc \ dtgbacomp.cc \
degen.cc \ degen.cc \
dotty.cc \ dotty.cc \
dottydec.cc \
dtbasat.cc \ dtbasat.cc \
dtgbasat.cc \ dtgbasat.cc \
dupexp.cc \ dupexp.cc \
@ -114,7 +111,6 @@ libtgbaalgos_la_SOURCES = \
reachiter.cc \ reachiter.cc \
reducerun.cc \ reducerun.cc \
replayrun.cc \ replayrun.cc \
rundotdec.cc \
safety.cc \ safety.cc \
save.cc \ save.cc \
scc.cc \ scc.cc \

140
src/tgbaalgos/dotty.cc
View file

@ -24,7 +24,6 @@
#include <stdexcept> #include <stdexcept>
#include "tgba/tgbagraph.hh" #include "tgba/tgbagraph.hh"
#include "dotty.hh" #include "dotty.hh"
#include "dottydec.hh"
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
#include "reachiter.hh" #include "reachiter.hh"
#include "misc/escape.hh" #include "misc/escape.hh"
@ -168,147 +167,12 @@ namespace spot
end(); end();
} }
}; };
} // anonymous namespace
class dotty_bfs : public tgba_reachable_iterator_breadth_first
{
public:
dotty_bfs(std::ostream& os, const_tgba_ptr a, bool mark_accepting_states,
const char* options, dotty_decorator* dd)
: tgba_reachable_iterator_breadth_first(a), os_(os),
mark_accepting_states_(mark_accepting_states), dd_(dd),
sba_(std::dynamic_pointer_cast<const tgba_digraph>(a))
{
if (options)
while (char c = *options++)
switch (c)
{
case 'c':
opt_circles = true;
break;
case 'h':
opt_horizontal = true;
break;
case 'n':
opt_name = true;
break;
case 'N':
opt_name = false;
break;
case 'v':
opt_horizontal = false;
break;
case 't':
mark_accepting_states_ = false;
break;
default:
throw std::runtime_error
(std::string("unknown option for dotty(): ") + c);
}
}
void
start()
{
os_ << "digraph G {\n";
if (opt_horizontal)
os_ << " rankdir=LR\n";
if (opt_name)
if (auto n = aut_->get_named_prop<std::string>("automaton-name"))
escape_str(os_ << " label=\"", *n) << "\"\n labelloc=\"t\"\n";
if (opt_circles)
os_ << " node [shape=\"circle\"]\n";
os_ << " 0 [label=\"\", style=invis, ";
os_ << (opt_horizontal ? "width" : "height");
os_ << "=0]\n 0 -> 1\n";
}
void
end()
{
os_ << '}' << std::endl;
}
void
process_state(const state* s, int n, tgba_succ_iterator* si)
{
bool accepting;
if (mark_accepting_states_)
{
if (sba_)
{
accepting = sba_->state_is_accepting(s);
}
else
{
si->first();
auto a = si->current_acceptance_conditions();
accepting = !si->done() && aut_->acc().accepting(a);
}
}
else
{
accepting = false;
}
os_ << " " << n << ' '
<< dd_->state_decl(aut_, s, n, si,
escape_str(aut_->format_state(s)),
accepting)
<< '\n';
}
void
process_link(const state* in_s, int in,
const state* out_s, int out, const tgba_succ_iterator* si)
{
std::string label =
bdd_format_formula(aut_->get_dict(),
si->current_condition());
if (!mark_accepting_states_)
if (auto a = si->current_acceptance_conditions())
{
label += "\n";
label += aut_->acc().format(a);
}
std::string s = aut_->transition_annotation(si);
if (!s.empty())
{
if (*label.rbegin() != '\n')
label += '\n';
label += s;
}
os_ << " " << in << " -> " << out << ' '
<< dd_->link_decl(aut_, in_s, in, out_s, out, si,
escape_str(label))
<< '\n';
}
private:
std::ostream& os_;
bool mark_accepting_states_;
dotty_decorator* dd_;
const_tgba_digraph_ptr sba_;
bool opt_horizontal = true;
bool opt_name = true;
bool opt_circles = false;
};
}
std::ostream& std::ostream&
dotty_reachable(std::ostream& os, const const_tgba_ptr& g, dotty_reachable(std::ostream& os, const const_tgba_ptr& g,
bool assume_sba, const char* options, const char* options)
dotty_decorator* dd)
{ {
if (dd)
{
dotty_bfs d(os, g, assume_sba || g->has_state_based_acc(), options, dd);
d.run();
return os;
}
dotty_output d(os, options); dotty_output d(os, options);
auto aut = std::dynamic_pointer_cast<const tgba_digraph>(g); auto aut = std::dynamic_pointer_cast<const tgba_digraph>(g);
if (!aut) if (!aut)

15
src/tgbaalgos/dotty.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et // Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
// Developpement de l'Epita (LRDE). // et Developpement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
@ -29,19 +29,12 @@
namespace spot namespace spot
{ {
class dotty_decorator;
/// \ingroup tgba_io /// \ingroup tgba_io
/// \brief Print reachable states in dot format. /// \brief Print reachable states in dot format.
/// ///
/// If \a assume_sba is set, this assumes that the automaton /// If \a assume_sba is set, this assumes that the automaton
/// is an SBA and use double elipse to mark accepting states. /// is an SBA and use double elipse to mark accepting states.
/// ///
/// The \a dd argument allows to customize the output in various
/// ways. See \ref tgba_dotty "this page" for a list of available
/// decorators. If no decorator is specified, the dotty_decorator
/// is used.
///
/// \param options an optional string of letters, each indicating a /// \param options an optional string of letters, each indicating a
/// different option. Presently the following options are /// different option. Presently the following options are
/// supported: 'v' for vertical output, 'h' for horizontal output, /// supported: 'v' for vertical output, 'h' for horizontal output,
@ -50,9 +43,7 @@ namespace spot
SPOT_API std::ostream& SPOT_API std::ostream&
dotty_reachable(std::ostream& os, dotty_reachable(std::ostream& os,
const const_tgba_ptr& g, const const_tgba_ptr& g,
bool assume_sba = false, const char* options = nullptr);
const char* options = nullptr,
dotty_decorator* dd = nullptr);
} }
#endif // SPOT_TGBAALGOS_DOTTY_HH #endif // SPOT_TGBAALGOS_DOTTY_HH

62
src/tgbaalgos/dottydec.cc
View file

@ -1,62 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement 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
// et Marie Curie.
//
// 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 "dottydec.hh"
#include "tgba/tgba.hh"
namespace spot
{
dotty_decorator::dotty_decorator()
{
}
dotty_decorator::~dotty_decorator()
{
}
std::string
dotty_decorator::state_decl(const const_tgba_ptr&, const state*, int,
tgba_succ_iterator*, const std::string& label,
bool accepting)
{
if (accepting)
return "[label=\"" + label + "\", peripheries=2]";
else
return "[label=\"" + label + "\"]";
}
std::string
dotty_decorator::link_decl(const const_tgba_ptr&, const state*, int,
const state*, int,
const tgba_succ_iterator*,
const std::string& label)
{
return "[label=\"" + label + "\"]";
}
dotty_decorator*
dotty_decorator::instance()
{
static dotty_decorator d;
return &d;
}
}

98
src/tgbaalgos/dottydec.hh
View file

@ -1,98 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
// Developpement 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
// et Marie Curie.
//
// 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_DOTTYDEC_HH
# define SPOT_TGBAALGOS_DOTTYDEC_HH
# include "misc/common.hh"
# include <string>
# include <tgba/fwd.hh>
namespace spot
{
class state;
class tgba_succ_iterator;
/// \addtogroup tgba_dotty Decorating the dot output
/// \ingroup tgba_io
/// \ingroup tgba_dotty
/// \brief Choose state and link styles for spot::dotty_reachable.
class SPOT_API dotty_decorator
{
public:
virtual ~dotty_decorator();
/// \brief Compute the style of a state.
///
/// This function should output a string of the form
/// <code>[label="foo", style=bar, ...]</code>. The
/// default implementation will simply output <code>[label="LABEL"]</code>
/// with <code>LABEL</code> replaced by the value of \a label.
///
/// \param a the automaton being drawn
/// \param s the state being drawn (owned by the caller)
/// \param n a unique number for this state
/// \param si an iterator over the successors of this state (owned by the
/// caller, but can be freely iterated)
/// \param label the computed name of this state
/// \param accepting whether the state is accepting (it makes sense only
/// for state-acceptance automata)
virtual std::string state_decl(const const_tgba_ptr& a,
const state* s, int n,
tgba_succ_iterator* si,
const std::string& label,
bool accepting);
/// \brief Compute the style of a link.
///
/// This function should output a string of the form
/// <code>[label="foo", style=bar, ...]</code>. The
/// default implementation will simply output <code>[label="LABEL"]</code>
/// with <code>LABEL</code> replaced by the value of \a label.
///
/// \param a the automaton being drawn
/// \param in_s the source state of the transition being drawn
/// (owned by the caller)
/// \param in the unique number associated to \a in_s
/// \param out_s the destination state of the transition being drawn
/// (owned by the caller)
/// \param out the unique number associated to \a out_s
/// \param si an iterator over the successors of \a in_s, pointing to
/// the current transition (owned by the caller and cannot
/// be iterated)
/// \param label the computed name of this state
virtual std::string link_decl(const const_tgba_ptr& a,
const state* in_s, int in,
const state* out_s, int out,
const tgba_succ_iterator* si,
const std::string& label);
/// Get the unique instance of the default dotty_decorator.
static dotty_decorator* instance();
protected:
dotty_decorator();
};
}
#endif // SPOT_TGBAALGOS_DOTTYDEC_HH

146
src/tgbaalgos/rundotdec.cc
View file

@ -1,146 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2011 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 <sstream>
#include "rundotdec.hh"
namespace spot
{
tgba_run_dotty_decorator::tgba_run_dotty_decorator(const
const_tgba_run_ptr& run)
: run_(run)
{
int n = 1;
for (tgba_run::steps::const_iterator i = run->prefix.begin();
i != run->prefix.end(); ++i, ++n)
map_[i->s].first.emplace_back(i, n);
for (tgba_run::steps::const_iterator i = run->cycle.begin();
i != run->cycle.end(); ++i, ++n)
map_[i->s].second.emplace_back(i, n);
}
tgba_run_dotty_decorator::~tgba_run_dotty_decorator()
{
}
std::string
tgba_run_dotty_decorator::state_decl(const const_tgba_ptr&,
const state* s, int,
tgba_succ_iterator*,
const std::string& label,
bool accepting)
{
step_map::const_iterator i = map_.find(s);
std::string acc = accepting ? ", peripheries=2" : "";
if (i == map_.end())
return "[label=\"" + label + acc + "\"]";
std::ostringstream os;
std::string sep = "(";
bool in_prefix = false;
bool in_cycle = false;
for (auto j: i->second.first)
{
os << sep << j.second;
sep = ", ";
in_prefix = true;
}
if (sep == ", ")
sep = "; ";
for (auto j: i->second.second)
{
os << sep << j.second;
sep = ", ";
in_cycle = true;
}
assert(in_cycle || in_prefix);
os << ")\\n" << label;
std::string color = in_prefix ? (in_cycle ? "violet" : "blue") : "red";
return "[label=\"" + os.str() + "\", style=bold, color="
+ color + acc + "]";
}
std::string
tgba_run_dotty_decorator::link_decl(const const_tgba_ptr&,
const state* in_s, int,
const state* out_s, int,
const tgba_succ_iterator* si,
const std::string& label)
{
step_map::const_iterator i = map_.find(in_s);
if (i != map_.end())
{
std::ostringstream os;
std::string sep = "(";
bool in_prefix = false;
bool in_cycle = false;
for (step_set::const_iterator j = i->second.first.begin();
j != i->second.first.end(); ++j)
if (j->first->label == si->current_condition()
&& j->first->acc == si->current_acceptance_conditions())
{
tgba_run::steps::const_iterator j2 = j->first;
++j2;
if (j2 == run_->prefix.end())
j2 = run_->cycle.begin();
if (out_s->compare(j2->s))
continue;
os << sep << j->second;
sep = ", ";
in_prefix = true;
}
if (sep == ", ")
sep = "; ";
for (step_set::const_iterator j = i->second.second.begin();
j != i->second.second.end(); ++j)
if (j->first->label == si->current_condition()
&& j->first->acc == si->current_acceptance_conditions())
{
tgba_run::steps::const_iterator j2 = j->first;
++j2;
if (j2 == run_->cycle.end())
j2 = run_->cycle.begin();
if (out_s->compare(j2->s))
continue;
os << sep << j->second;
sep = ", ";
in_cycle = true;
}
os << ")\\n";
if (in_prefix || in_cycle)
{
std::string
color = in_prefix ? (in_cycle ? "violet" : "blue") : "red";
return ("[label=\"" + os.str() + label
+ "\", style=bold, color=" + color + "]");
}
}
return "[label=\"" + label + "\"]";
}
}

64
src/tgbaalgos/rundotdec.hh
View file

@ -1,64 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Developpement
// 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
// et Marie Curie.
//
// 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_RUNDOTDEC_HH
# define SPOT_TGBAALGOS_RUNDOTDEC_HH
#include <map>
#include <utility>
#include <list>
#include "dottydec.hh"
#include "emptiness.hh"
namespace spot
{
/// \ingroup tgba_dotty
/// \brief Highlight a spot::tgba_run on a spot::tgba.
///
/// An instance of this class can be passed to spot::dotty_reachable.
class SPOT_API tgba_run_dotty_decorator: public dotty_decorator
{
public:
tgba_run_dotty_decorator(const const_tgba_run_ptr& run);
virtual ~tgba_run_dotty_decorator();
virtual std::string state_decl(const const_tgba_ptr& a,
const state* s, int n,
tgba_succ_iterator* si,
const std::string& label,
bool accepting);
virtual std::string link_decl(const const_tgba_ptr& a,
const state* in_s, int in,
const state* out_s, int out,
const tgba_succ_iterator* si,
const std::string& label);
private:
const_tgba_run_ptr run_;
typedef std::pair<tgba_run::steps::const_iterator, int> step_num;
typedef std::list<step_num> step_set;
typedef std::map<const state*, std::pair<step_set, step_set>,
spot::state_ptr_less_than> step_map;
step_map map_;
};
}
#endif // SPOT_TGBAALGOS_RUNDOTDEC_HH

2
src/tgbatest/complementation.cc
View file

@ -251,7 +251,7 @@ int main(int argc, char* argv[])
return_value = 1; return_value = 1;
if (auto run = res->accepting_run()) if (auto run = res->accepting_run())
{ {
spot::dotty_reachable(std::cout, ec->automaton(), false); spot::dotty_reachable(std::cout, ec->automaton());
spot::print_tgba_run(std::cout, ec->automaton(), run); spot::print_tgba_run(std::cout, ec->automaton(), run);
} }
} }

4
src/tgbatest/emptchk.cc
View file

@ -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.
@ -163,7 +163,7 @@ main(int argc, char** argv)
if (auto run = res->accepting_run()) if (auto run = res->accepting_run())
{ {
auto ar = spot::tgba_run_to_tgba(a, run); auto ar = spot::tgba_run_to_tgba(a, run);
spot::dotty_reachable(std::cout, ar, false); spot::dotty_reachable(std::cout, ar);
} }
std::cout << '\n'; std::cout << '\n';
if (runs == 0) if (runs == 0)

28
src/tgbatest/ltl2tgba.cc
View file

@ -48,7 +48,6 @@
#include "taalgos/minimize.hh" #include "taalgos/minimize.hh"
#include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/replayrun.hh" #include "tgbaalgos/replayrun.hh"
#include "tgbaalgos/rundotdec.hh"
#include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/safety.hh" #include "tgbaalgos/safety.hh"
#include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/gtec/gtec.hh"
@ -248,8 +247,6 @@ syntax(char* prog)
<< std::endl << std::endl
<< " -CR compute and replay an accepting run (implies -C)" << " -CR compute and replay an accepting run (implies -C)"
<< std::endl << std::endl
<< " -g graph the accepting run on the automaton (requires -e)"
<< std::endl
<< " -G graph the accepting run seen as an automaton " << " -G graph the accepting run seen as an automaton "
<< " (requires -e)" << std::endl << " (requires -e)" << std::endl
<< " -m try to reduce accepting runs, in a second pass" << " -m try to reduce accepting runs, in a second pass"
@ -364,7 +361,6 @@ checked_main(int argc, char** argv)
bool display_reduced_form = false; bool display_reduced_form = false;
bool post_branching = false; bool post_branching = false;
bool fair_loop_approx = false; bool fair_loop_approx = false;
bool graph_run_opt = false;
bool graph_run_tgba_opt = false; bool graph_run_tgba_opt = false;
bool opt_reduce = false; bool opt_reduce = false;
bool opt_minimize = false; bool opt_minimize = false;
@ -531,11 +527,6 @@ checked_main(int argc, char** argv)
{ {
file_opt = true; file_opt = true;
} }
else if (!strcmp(argv[formula_index], "-g"))
{
accepting_run = true;
graph_run_opt = true;
}
else if (!strcmp(argv[formula_index], "-G")) else if (!strcmp(argv[formula_index], "-G"))
{ {
accepting_run = true; accepting_run = true;
@ -927,10 +918,10 @@ checked_main(int argc, char** argv)
} }
} }
if ((graph_run_opt || graph_run_tgba_opt) if ((graph_run_tgba_opt)
&& (!echeck_inst || !expect_counter_example)) && (!echeck_inst || !expect_counter_example))
{ {
std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl; std::cerr << argv[0] << ": error: -G requires -e." << std::endl;
exit(1); exit(1);
} }
@ -1531,7 +1522,7 @@ checked_main(int argc, char** argv)
switch (output) switch (output)
{ {
case 0: case 0:
spot::dotty_reachable(std::cout, a, assume_sba); spot::dotty_reachable(std::cout, a);
break; break;
case 5: case 5:
a->get_dict()->dump(std::cout); a->get_dict()->dump(std::cout);
@ -1702,7 +1693,7 @@ checked_main(int argc, char** argv)
} }
else else
{ {
if (!graph_run_opt && !graph_run_tgba_opt) if (!graph_run_tgba_opt)
ec->print_stats(std::cout); ec->print_stats(std::cout);
if (expect_counter_example != !!res && if (expect_counter_example != !!res &&
(!expect_counter_example || ec->safe())) (!expect_counter_example || ec->safe()))
@ -1753,17 +1744,10 @@ checked_main(int argc, char** argv)
else else
{ {
tm.start("printing accepting run"); tm.start("printing accepting run");
if (graph_run_opt) if (graph_run_tgba_opt)
{
spot::tgba_run_dotty_decorator deco(run);
spot::dotty_reachable(std::cout, a,
assume_sba, nullptr,
&deco);
}
else if (graph_run_tgba_opt)
{ {
auto ar = spot::tgba_run_to_tgba(a, run); auto ar = spot::tgba_run_to_tgba(a, run);
spot::dotty_reachable(std::cout, ar, false); spot::dotty_reachable(std::cout, ar);
} }
else else
{ {

2
wrap/python/ajax/ltl2tgba.html
View file

@ -551,7 +551,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
</label><br> </label><br>
<label class="rtip" title="Use color to show an accepting run in the automaton."> <label class="rtip" title="Use color to show an accepting run in the automaton.">
<INPUT type="radio" name="rf" value="d" checked> <INPUT type="radio" name="rf" value="d" checked>
draw an accepting run on top of the automaton draw an accepting run as a lasso-shaped automaton
</label><br> </label><br>
</div> </div>
<div id="tabs-ot"> <div id="tabs-ot">

30
wrap/python/ajax/spot.in
View file

@ -285,14 +285,14 @@ However you may download the <a href="''' + cgi.escape(autprefix)
else: else:
render_dot(autprefix) render_dot(autprefix)
def render_automaton(automaton, dont_run_dot, issba, deco = None): def render_automaton(automaton, dont_run_dot):
dotsrc = spot.ostringstream() dotsrc = spot.ostringstream()
if isinstance(automaton, spot.ta): # TA/GTA if isinstance(automaton, spot.ta): # TA/GTA
spot.dotty_reachable(dotsrc, automaton) spot.dotty_reachable(dotsrc, automaton)
elif hasattr(automaton, 'get_ta'): # TGTA elif hasattr(automaton, 'get_ta'): # TGTA
spot.dotty_reachable(dotsrc, automaton.get_ta()) spot.dotty_reachable(dotsrc, automaton.get_ta())
else: # TGBA else: # TGBA
spot.dotty_reachable(dotsrc, automaton, issba, "N", deco) spot.dotty_reachable(dotsrc, automaton, "N")
render_dot_maybe(dotsrc.str(), dont_run_dot) render_dot_maybe(dotsrc.str(), dont_run_dot)
def render_formula(f): def render_formula(f):
@ -510,7 +510,7 @@ cannot be translated using this algorithm. Please use Couveur/FM.'''
dict = spot.make_bdd_dict() dict = spot.make_bdd_dict()
if output_type == 't' and not (f.is_ltl_formula() and f.is_X_free()): if output_type == 't' and not f.is_syntactic_stutter_invariant():
unbufprint('<b>Warning:</b> The following result assumes the input formula is stuttering insensitive.</br>') unbufprint('<b>Warning:</b> The following result assumes the input formula is stuttering insensitive.</br>')
# Should the automaton be displayed as a SBA? # Should the automaton be displayed as a SBA?
@ -627,7 +627,7 @@ if output_type == 'm':
unbufprint('<div class="automata-stats">') unbufprint('<div class="automata-stats">')
dont_run_dot = print_stats(automaton) dont_run_dot = print_stats(automaton)
unbufprint('</div>') unbufprint('</div>')
render_automaton(automaton, dont_run_dot, issba) render_automaton(automaton, dont_run_dot)
automaton = 0 automaton = 0
finish() finish()
@ -685,7 +685,6 @@ if prune_scc:
or direct_simul or direct_simul
or reverse_simul or reverse_simul
or iterated_simul)) or iterated_simul))
issba = False
if wdba_minimize: if wdba_minimize:
minimized = spot.minimize_obligation(automaton, f) minimized = spot.minimize_obligation(automaton, f)
@ -693,20 +692,16 @@ if wdba_minimize:
automaton = minimized automaton = minimized
minimized = 0 minimized = 0
degen = False # No need to degeneralize anymore degen = False # No need to degeneralize anymore
issba = True
direct_simul = False # No need to simulate anymore direct_simul = False # No need to simulate anymore
reverse_simul = False reverse_simul = False
iterated_simul = False iterated_simul = False
if direct_simul and not iterated_simul: if direct_simul and not iterated_simul:
automaton = spot.simulation(automaton) automaton = spot.simulation(automaton)
issba = False
if reverse_simul and not iterated_simul: if reverse_simul and not iterated_simul:
automaton = spot.cosimulation(automaton) automaton = spot.cosimulation(automaton)
issba = False
if iterated_simul: if iterated_simul:
automaton = spot.iterated_simulations(automaton) automaton = spot.iterated_simulations(automaton)
issba = False
if prune_scc and (direct_simul or reverse_simul): if prune_scc and (direct_simul or reverse_simul):
# Make a second pass after the simulation, since these might leave # Make a second pass after the simulation, since these might leave
@ -715,7 +710,6 @@ if prune_scc and (direct_simul or reverse_simul):
if degen or neverclaim: if degen or neverclaim:
degen = spot.degeneralize(automaton) degen = spot.degeneralize(automaton)
issba = True
else: else:
degen = automaton degen = automaton
@ -728,7 +722,7 @@ if output_type == 'a':
del s del s
else: # 't' or 's' else: # 't' or 's'
dont_run_dot = print_stats(degen, True) dont_run_dot = print_stats(degen, True)
render_automaton(degen, dont_run_dot, issba) render_automaton(degen, dont_run_dot)
degen = 0 degen = 0
automaton = 0 automaton = 0
finish() finish()
@ -750,14 +744,13 @@ if output_type == 't':
tautomaton = spot.tgba_to_tgta(degen, propset) tautomaton = spot.tgba_to_tgta(degen, propset)
if bisimulation: if bisimulation:
tautomaton = spot.minimize_tgta(tautomaton) tautomaton = spot.minimize_tgta(tautomaton)
issba = False
else: else:
tautomaton = spot.tgba_to_ta(degen, propset, tautomaton = spot.tgba_to_ta(degen, propset,
issba, True, singlepass, livelock) True, True, singlepass, livelock)
if bisimulation: if bisimulation:
tautomaton = spot.minimize_ta(tautomaton) tautomaton = spot.minimize_ta(tautomaton)
dont_run_dot = print_stats(tautomaton, ta = True) dont_run_dot = print_stats(tautomaton, ta = True)
render_automaton(tautomaton, dont_run_dot, issba) render_automaton(tautomaton, dont_run_dot)
tautomaton = 0 tautomaton = 0
degen = 0 degen = 0
automaton = 0 automaton = 0
@ -767,14 +760,13 @@ if output_type == 't':
if output_type == 'r': if output_type == 'r':
print_acc_run = False print_acc_run = False
draw_acc_run = False
s = form.getfirst('rf', 'd') s = form.getfirst('rf', 'd')
draw_acc_run = False
if s == 'p': if s == 'p':
print_acc_run = True print_acc_run = True
elif s == 'd': elif s == 'd':
draw_acc_run = True draw_acc_run = True
err = "" err = ""
opt = (form.getfirst('ec', 'Cou99') + "(" + opt = (form.getfirst('ec', 'Cou99') + "(" +
form.getfirst('eo', '') + ")") form.getfirst('eo', '') + ")")
@ -823,12 +815,8 @@ if output_type == 'r':
unbufprint('<div class="accrun">%s</div>' % unbufprint('<div class="accrun">%s</div>' %
cgi.escape(s.str())) cgi.escape(s.str()))
del s del s
if draw_acc_run: if draw_acc_run:
deco = spot.tgba_run_dotty_decorator(ec_run) render_automaton(spot.tgba_run_to_tgba(ec_a, ec_run), False)
dont_run_dot = print_stats(ec_a)
render_automaton(ec_a, dont_run_dot, issba, deco)
del deco
del ec_run del ec_run
del ec_res del ec_res
unbufprint('</div>') unbufprint('</div>')

4
wrap/python/spot.i
View file

@ -110,7 +110,6 @@ namespace std {
#include "tgba/taatgba.hh" #include "tgba/taatgba.hh"
#include "tgba/tgbaproduct.hh" #include "tgba/tgbaproduct.hh"
#include "tgbaalgos/dottydec.hh"
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "tgbaalgos/degen.hh" #include "tgbaalgos/degen.hh"
#include "tgbaalgos/dupexp.hh" #include "tgbaalgos/dupexp.hh"
@ -123,7 +122,6 @@ namespace std {
#include "tgbaalgos/magic.hh" #include "tgbaalgos/magic.hh"
#include "tgbaalgos/minimize.hh" #include "tgbaalgos/minimize.hh"
#include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/rundotdec.hh"
#include "tgbaalgos/save.hh" #include "tgbaalgos/save.hh"
#include "tgbaalgos/safety.hh" #include "tgbaalgos/safety.hh"
#include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/sccfilter.hh"
@ -244,7 +242,6 @@ namespace spot {
%include "ltlvisit/apcollect.hh" %include "ltlvisit/apcollect.hh"
%include "tgbaalgos/degen.hh" %include "tgbaalgos/degen.hh"
%include "tgbaalgos/dottydec.hh"
%include "tgbaalgos/dotty.hh" %include "tgbaalgos/dotty.hh"
%include "tgbaalgos/dupexp.hh" %include "tgbaalgos/dupexp.hh"
%include "tgbaalgos/emptiness.hh" %include "tgbaalgos/emptiness.hh"
@ -256,7 +253,6 @@ namespace spot {
%include "tgbaalgos/magic.hh" %include "tgbaalgos/magic.hh"
%include "tgbaalgos/minimize.hh" %include "tgbaalgos/minimize.hh"
%include "tgbaalgos/neverclaim.hh" %include "tgbaalgos/neverclaim.hh"
%include "tgbaalgos/rundotdec.hh"
%include "tgbaalgos/save.hh" %include "tgbaalgos/save.hh"
%include "tgbaalgos/safety.hh" %include "tgbaalgos/safety.hh"
%include "tgbaalgos/sccfilter.hh" %include "tgbaalgos/sccfilter.hh"