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

* src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh,

Browse source 
src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: New files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them.
* src/tgbaalgos/dotty.hh (dotty_reachable): Take a dotty_decorator
as third parameter.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_state,
dotty_bfs::process_link): Use the decorator.
* src/tgbatest/ltl2tgba.cc: Graph the accepting run if the -g option
is given.
* src/tgbatest/emptchk.test: Exercize -g.
This commit is contained in:
Alexandre Duret-Lutz 2004-11-03 15:17:06 +00:00
parent a90b0648f8
commit 7688431451
10 changed files with 434 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

12
ChangeLog
View file

@ -1,5 +1,17 @@
2004-11-03 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh,
src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: New files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them.
* src/tgbaalgos/dotty.hh (dotty_reachable): Take a dotty_decorator
as third parameter.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_state,
dotty_bfs::process_link): Use the decorator.
* src/tgbatest/ltl2tgba.cc: Graph the accepting run if the -g option
is given.
* src/tgbatest/emptchk.test: Exercize -g.
* src/tgbaalgos/replayrun.cc (replay_tgba_run): Add missing std::endl.
* tgbaalgos/reachiter.hh, tgbaalgos/reachiter.cc

4
src/tgbaalgos/Makefile.am
View file

@ -28,6 +28,7 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos
tgbaalgos_HEADERS = \
dotty.hh \
dottydec.hh \
dupexp.hh \
emptiness.hh \
lbtt.hh \
@ -39,6 +40,7 @@ tgbaalgos_HEADERS = \
projrun.hh \
reachiter.hh \
replayrun.hh \
rundotdec.hh \
save.hh \
stats.hh \
reductgba_sim.hh
@ -46,6 +48,7 @@ tgbaalgos_HEADERS = \
noinst_LTLIBRARIES = libtgbaalgos.la
libtgbaalgos_la_SOURCES = \
dotty.cc \
dottydec.cc \
dupexp.cc \
emptiness.cc \
lbtt.cc \
@ -57,6 +60,7 @@ libtgbaalgos_la_SOURCES = \
projrun.cc \
reachiter.cc \
replayrun.cc \
rundotdec.cc \
save.cc \
stats.cc \
reductgba_sim.cc \

39
src/tgbaalgos/dotty.cc
View file

@ -33,8 +33,8 @@ namespace spot
class dotty_bfs : public tgba_reachable_iterator_breadth_first
{
public:
dotty_bfs(const tgba* a, std::ostream& os)
: tgba_reachable_iterator_breadth_first(a), os_(os)
dotty_bfs(std::ostream& os, const tgba* a, dotty_decorator* dd)
: tgba_reachable_iterator_breadth_first(a), os_(os), dd_(dd)
{
}
@ -53,34 +53,41 @@ namespace spot
}
void
process_state(const state* s, int n, tgba_succ_iterator*)
process_state(const state* s, int n, tgba_succ_iterator* si)
{
os_ << " " << n << " [label=\"";
escape_str(os_, automata_->format_state(s)) << "\"]" << std::endl;
os_ << " " << n << " "
<< dd_->state_decl(automata_, s, n, si,
escape_str(automata_->format_state(s)))
<< std::endl;
}
void
process_link(const state*, int in,
const state*, int out, const tgba_succ_iterator* si)
process_link(const state* in_s, int in,
const state* out_s, int out, const tgba_succ_iterator* si)
{
os_ << " " << in << " -> " << out << " [label=\"";
escape_str(os_, bdd_format_formula(automata_->get_dict(),
si->current_condition())) << "\\n";
escape_str(os_,
bdd_format_accset(automata_->get_dict(),
si->current_acceptance_conditions()))
<< "\"]" << std::endl;
std::string label =
bdd_format_formula(automata_->get_dict(),
si->current_condition())
+ "\n"
+ bdd_format_accset(automata_->get_dict(),
si->current_acceptance_conditions());
os_ << " " << in << " -> " << out << " "
<< dd_->link_decl(automata_, in_s, in, out_s, out, si,
escape_str(label))
<< std::endl;
}
private:
std::ostream& os_;
dotty_decorator* dd_;
};
}
std::ostream&
dotty_reachable(std::ostream& os, const tgba* g)
dotty_reachable(std::ostream& os, const tgba* g, dotty_decorator* dd)
{
dotty_bfs d(g, os);
dotty_bfs d(os, g, dd);
d.run();
return os;
}

9
src/tgbaalgos/dotty.hh
View file

@ -22,13 +22,18 @@
#ifndef SPOT_TGBAALGOS_DOTTY_HH
# define SPOT_TGBAALGOS_DOTTY_HH
#include "tgba/tgba.hh"
#include "dottydec.hh"
#include <iosfwd>
namespace spot
{
class tgba;
/// \brief Print reachable states in dot format.
std::ostream& dotty_reachable(std::ostream& os, const tgba* g);
std::ostream&
dotty_reachable(std::ostream& os,
const tgba* g,
dotty_decorator* dd = dotty_decorator::instance());
}
#endif // SPOT_TGBAALGOS_DOTTY_HH

56
src/tgbaalgos/dottydec.cc Normal file
View file

@ -0,0 +1,56 @@
// 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 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 "dottydec.hh"
#include "tgba/tgba.hh"
namespace spot
{
dotty_decorator::dotty_decorator()
{
}
dotty_decorator::~dotty_decorator()
{
}
std::string
dotty_decorator::state_decl(const tgba*, const state*, int,
tgba_succ_iterator*, const std::string& label)
{
return "[label=\"" + label + "\"]";
}
std::string
dotty_decorator::link_decl(const tgba*, 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;
}
}

87
src/tgbaalgos/dottydec.hh Normal file
View file

@ -0,0 +1,87 @@
// 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 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_TGBAALGOS_DOTTYDEC_HH
# define SPOT_TGBAALGOS_DOTTYDEC_HH
#include <string>
namespace spot
{
class state;
class tgba;
class tgba_succ_iterator;
/// Choose state and link styles for spot::dotty_reachable.
class 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
virtual std::string state_decl(const tgba* a, const state* s, int n,
tgba_succ_iterator* si,
const std::string& label);
/// \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 tgba* 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

143
src/tgbaalgos/rundotdec.cc Normal file
View file

@ -0,0 +1,143 @@
// 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 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 <sstream>
#include "rundotdec.hh"
#include "tgba/succiter.hh"
namespace spot
{
tgba_run_dotty_decorator::tgba_run_dotty_decorator(const tgba_run* 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.push_back(step_num(i, n));
for (tgba_run::steps::const_iterator i = run->cycle.begin();
i != run->cycle.end(); ++i, ++n)
map_[i->s].second.push_back(step_num(i, n));
}
tgba_run_dotty_decorator::~tgba_run_dotty_decorator()
{
}
std::string
tgba_run_dotty_decorator::state_decl(const tgba*, const state* s, int,
tgba_succ_iterator*,
const std::string& label)
{
step_map::const_iterator i = map_.find(s);
if (i == map_.end())
return "[label=\"" + label + "\"]";
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)
{
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)
{
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 + "]";
}
std::string
tgba_run_dotty_decorator::link_decl(const tgba*,
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 + "\"]";
}
}

60
src/tgbaalgos/rundotdec.hh Normal file
View file

@ -0,0 +1,60 @@
// 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 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_TGBAALGOS_RUNDOTDEC_HH
# define SPOT_TGBAALGOS_RUNDOTDEC_HH
#include <map>
#include <utility>
#include <list>
#include "dottydec.hh"
#include "emptiness.hh"
namespace spot
{
/// \brief Highlight a spot::tgba_run on a spot::tgba.
///
/// An instance of this class can be passed to spot::dotty_reachable.
class tgba_run_dotty_decorator: public dotty_decorator
{
public:
tgba_run_dotty_decorator(const tgba_run* run);
virtual ~tgba_run_dotty_decorator();
virtual std::string state_decl(const tgba* a, const state* s, int n,
tgba_succ_iterator* si,
const std::string& label);
virtual std::string link_decl(const tgba* 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* 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

26
src/tgbatest/emptchk.test
View file

@ -25,18 +25,24 @@
set -e
expect_ce_do()
{
run 0 ./ltl2tgba "$@"
run 0 ./ltl2tgba -g "$@"
}
expect_ce()
{
run 0 ./ltl2tgba -e "$1"
run 0 ./ltl2tgba -e -D "$1"
run 0 ./ltl2tgba -e -f "$1"
run 0 ./ltl2tgba -e -f -D "$1"
run 0 ./ltl2tgba -ecouvreur99_shy "$1"
run 0 ./ltl2tgba -ecouvreur99_shy -D "$1"
run 0 ./ltl2tgba -ecouvreur99_shy -f "$1"
run 0 ./ltl2tgba -ecouvreur99_shy -f -D "$1"
run 0 ./ltl2tgba -emagic_search "$1"
run 0 ./ltl2tgba -emagic_search -f "$1"
expect_ce_do -e "$1"
expect_ce_do -e -D "$1"
expect_ce_do -e -f "$1"
expect_ce_do -e -f -D "$1"
expect_ce_do -ecouvreur99_shy "$1"
expect_ce_do -ecouvreur99_shy -D "$1"
expect_ce_do -ecouvreur99_shy -f "$1"
expect_ce_do -ecouvreur99_shy -f -D "$1"
expect_ce_do -emagic_search "$1"
expect_ce_do -emagic_search -f "$1"
}
expect_no()

30
src/tgbatest/ltl2tgba.cc
View file

@ -43,6 +43,7 @@
#include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/reductgba_sim.hh"
#include "tgbaalgos/replayrun.hh"
#include "tgbaalgos/rundotdec.hh"
void
syntax(char* prog)
@ -65,6 +66,7 @@ syntax(char* prog)
<< " -f use Couvreur's FM algorithm for translation"
<< std::endl
<< " -F read the formula from the file" << std::endl
<< " -g graph the accepting run on the automaton (requires -e)"
<< " -L fair-loop approximation (implies -f)" << std::endl
<< " -N display the never clain for Spin "
<< "(implies -D)" << std::endl
@ -147,6 +149,7 @@ main(int argc, char** argv)
bool display_parity_game = false;
bool post_branching = false;
bool fair_loop_approx = false;
bool graph_run_opt = false;
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::atomic_prop_set* unobservables = 0;
@ -199,6 +202,10 @@ main(int argc, char** argv)
{
file_opt = true;
}
else if (!strcmp(argv[formula_index], "-g"))
{
graph_run_opt = true;
}
else if (!strcmp(argv[formula_index], "-L"))
{
fair_loop_approx = true;
@ -347,6 +354,12 @@ main(int argc, char** argv)
}
}
if (graph_run_opt && (echeck_algo == "" || !expect_counter_example))
{
std::cerr << argv[0] << ": error: -g requires -e." << std::endl;
exit(1);
}
std::string input;
if (file_opt)
@ -561,7 +574,8 @@ main(int argc, char** argv)
do
{
spot::emptiness_check_result* res = ec->check();
ec->print_stats(std::cout);
if (!graph_run_opt)
ec->print_stats(std::cout);
if (expect_counter_example != !!res)
exit_code = 1;
@ -580,9 +594,17 @@ main(int argc, char** argv)
}
else
{
spot::print_tgba_run(std::cout, ec_a, run);
if (!spot::replay_tgba_run(std::cout, ec_a, run))
exit_code = 1;
if (graph_run_opt)
{
spot::tgba_run_dotty_decorator deco(run);
spot::dotty_reachable(std::cout, ec_a, &deco);
}
else
{
spot::print_tgba_run(std::cout, ec_a, run);
if (!spot::replay_tgba_run(std::cout, ec_a, run))
exit_code = 1;
}
delete run;
}
}