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

* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add reachiters.hh.

(libtgbaalgos_la_SOURCES): Add reachiters.cc.
* src/tgbaalgos/dotty.cc, src/tgbaalgos/save.cc: Rewrite using
spot::tgba_reachable_iterator_breadth_first.
* src/tgbatest/explicit.test, src/tgbatest/tgbaread.test,
src/tgbatest/tripprod.test: Adjust expected output.
parent 664e49e0
2003-07-25 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add reachiters.hh.
(libtgbaalgos_la_SOURCES): Add reachiters.cc.
* src/tgbaalgos/dotty.cc, src/tgbaalgos/save.cc: Rewrite using
spot::tgba_reachable_iterator_breadth_first.
* src/tgbatest/explicit.test, src/tgbatest/tgbaread.test,
src/tgbatest/tripprod.test: Adjust expected output.
2003-07-24 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* configure.ac: Output iface/gspn/defs.
* iface/gspn/Makefile.am (EXTRA_DIST): Add $(TESTS).
(TESTS, check_SCRIPTS, distclean-local): New.
* iface/gspn/dcswave.test, iface/gspn/simple.test,
* iface/gspn/dcswave.test, iface/gspn/simple.test,
iface/gspn/defs.in: New files.
* iface/gspn/dottygspn.cc (main): Take the list of properties
of interest in argument.
......
......@@ -4,6 +4,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
tgbaalgosdir = $(pkgincludedir)/tgbaalgos
tgbaalgos_HEADERS = \
reachiter.hh \
dotty.hh \
lbtt.hh \
ltl2tgba.hh \
......@@ -11,6 +12,7 @@ tgbaalgos_HEADERS = \
noinst_LTLIBRARIES = libtgbaalgos.la
libtgbaalgos_la_SOURCES = \
reachiter.cc \
dotty.cc \
lbtt.cc \
ltl2tgba.cc \
......
#include <map>
#include "tgba/tgba.hh"
#include "dotty.hh"
#include "tgba/bddprint.hh"
#include "reachiter.hh"
namespace spot
{
typedef std::map<state*, int, state_ptr_less_than> seen_map;
/// Output and record a state.
static bool
dotty_state(std::ostream& os,
const tgba* g, state* st, seen_map& m, int& node)
class dotty_bfs : public tgba_reachable_iterator_breadth_first
{
seen_map::iterator i = m.find(st);
// Already drawn?
if (i != m.end())
{
node = i->second;
return false;
}
node = m.size() + 1;
m[st] = node;
os << " " << node << " [label=\""
<< g->format_state(st) << "\"]" << std::endl;
return true;
}
/// Process successors.
static void
dotty_rec(std::ostream& os,
const tgba* g, state* st, seen_map& m, int father)
{
tgba_succ_iterator* si = g->succ_iter(st);
for (si->first(); !si->done(); si->next())
{
int node;
state* s = si->current_state();
bool recurse = dotty_state(os, g, s, m, node);
os << " " << father << " -> " << node << " [label=\"";
bdd_print_set(os, g->get_dict(), si->current_condition()) << "\\n";
bdd_print_set(os, g->get_dict(), si->current_accepting_conditions())
<< "\"]" << std::endl;
if (recurse)
{
dotty_rec(os, g, s, m, node);
// Do not delete S, it is used as key in M.
}
else
{
delete s;
}
}
delete si;
}
public:
dotty_bfs(const tgba* a, std::ostream& os)
: tgba_reachable_iterator_breadth_first(a), os_(os)
{
}
void
start()
{
os_ << "digraph G {" << std::endl;
os_ << " size=\"7.26,10.69\"" << std::endl;
os_ << " 0 [label=\"\", style=invis]" << std::endl;
os_ << " 0 -> 1" << std::endl;
}
void
end()
{
os_ << "}" << std::endl;
}
void
process_state(const state* s, int n, tgba_succ_iterator*)
{
os_ << " " << n << " [label=\""
<< automata_->format_state(s) << "\"]" << std::endl;
}
void
process_link(int in, int out, const tgba_succ_iterator* si)
{
os_ << " " << in << " -> " << out << " [label=\"";
bdd_print_set(os_, automata_->get_dict(),
si->current_condition()) << "\\n";
bdd_print_set(os_, automata_->get_dict(),
si->current_accepting_conditions()) << "\"]" << std::endl;
}
private:
std::ostream& os_;
};
std::ostream&
dotty_reachable(std::ostream& os, const tgba* g)
{
seen_map m;
state* state = g->get_init_state();
os << "digraph G {" << std::endl;
os << " size=\"7.26,10.69\"" << std::endl;
os << " 0 [label=\"\", style=invis]" << std::endl;
int init;
dotty_state(os, g, state, m, init);
os << " 0 -> " << init << std::endl;
dotty_rec(os, g, state, m, init);
os << "}" << std::endl;
// Finally delete all states used as keys in m:
for (seen_map::iterator i = m.begin(); i != m.end(); ++i)
delete i->first;
dotty_bfs d(g, os);
d.run();
return os;
}
......
#include "reachiter.hh"
namespace spot
{
// tgba_reachable_iterator
//////////////////////////////////////////////////////////////////////
tgba_reachable_iterator::tgba_reachable_iterator(const tgba* a)
: automata_(a)
{
}
tgba_reachable_iterator::~tgba_reachable_iterator()
{
for (seen_map::const_iterator s = seen.begin(); s != seen.end(); ++s)
delete s->first;
}
void
tgba_reachable_iterator::run()
{
int n = 0;
start();
state* i = automata_->get_init_state();
add_state(i);
seen[i] = ++n;
const state* t;
while ((t = next_state()))
{
assert(seen.find(t) != seen.end());
int tn = seen[t];
tgba_succ_iterator* si = automata_->succ_iter(t);
process_state(t, tn, si);
for (si->first(); ! si->done(); si->next())
{
const state* current = si->current_state();
seen_map::const_iterator s = seen.find(current);
if (s == seen.end())
{
seen[current] = ++n;
add_state(current);
process_link(tn, n, si);
}
else
{
process_link(tn, seen[current], si);
delete current;
}
}
delete si;
}
end();
}
void
tgba_reachable_iterator::start()
{
}
void
tgba_reachable_iterator::end()
{
}
void
tgba_reachable_iterator::process_state(const state*, int,
tgba_succ_iterator*)
{
}
void
tgba_reachable_iterator::process_link(int, int, const tgba_succ_iterator*)
{
}
// tgba_reachable_iterator_depth_first
//////////////////////////////////////////////////////////////////////
tgba_reachable_iterator_depth_first::
tgba_reachable_iterator_depth_first(const tgba* a)
: tgba_reachable_iterator(a)
{
}
void
tgba_reachable_iterator_depth_first::add_state(const state* s)
{
todo.push(s);
}
const state*
tgba_reachable_iterator_depth_first::next_state()
{
if (todo.empty())
return 0;
const state* s = todo.top();
todo.pop();
return s;
}
// tgba_reachable_iterator_breadth_first
//////////////////////////////////////////////////////////////////////
tgba_reachable_iterator_breadth_first::
tgba_reachable_iterator_breadth_first(const tgba* a)
: tgba_reachable_iterator(a)
{
}
void
tgba_reachable_iterator_breadth_first::add_state(const state* s)
{
todo.push_back(s);
}
const state*
tgba_reachable_iterator_breadth_first::next_state()
{
if (todo.empty())
return 0;
const state* s = todo.front();
todo.pop_front();
return s;
}
}
#ifndef SPOT_TGBAALGOS_REACHITER_HH
# define SPOT_TGBAALGOS_REACHITER_HH
#include "tgba/tgba.hh"
#include <stack>
#include <deque>
namespace spot
{
/// \brief Iterate over all reachable states of a spot::tgba.
class tgba_reachable_iterator
{
public:
tgba_reachable_iterator(const tgba* a);
virtual ~tgba_reachable_iterator();
/// \brief Iterate over all reachable states of a spot::tgba.
///
/// This is a template method that will call add_state(), next_state(),
/// start(), end(), process_state(), and process_link(), while it
/// iterate over state.
void run();
/// \name Todo list management.
///
/// spot::tgba_reachable_iterator_depth_first and
/// spot::tgba_reachable_iterator_breadth_first offer two precanned
/// implementations for these functions.
/// \{
/// \brief Called by run() to register newly discovered states.
virtual void add_state(const state* s) = 0;
/// \brief Called by run() to obtain the
virtual const state* next_state() = 0;
/// \}
/// Called by run() before starting its iteration.
virtual void start();
/// Called by run() once all states have been explored.
virtual void end();
/// Called by run() to process a state.
///
/// \param s The current state.
/// \param n An unique number assigned to \a s.
/// \param si The spot::tgba_succ_iterator for \a s.
virtual void process_state(const state* s, int n, tgba_succ_iterator* si);
/// Called by run() to process a transition.
///
/// \param in The source state number.
/// \param out The destination state number.
/// \param si The spot::tgba_succ_iterator positionned on the current
/// transition.
virtual void process_link(int in, int out, const tgba_succ_iterator* si);
protected:
const tgba* automata_; ///< The spot::tgba to explore.
typedef std::map<const state*, int, state_ptr_less_than> seen_map;
seen_map seen; ///< States already seen.
};
/// \brief An implementation of spot::tgba_reachable_iterator that browses
/// states depth first.
class tgba_reachable_iterator_depth_first : public tgba_reachable_iterator
{
public:
tgba_reachable_iterator_depth_first(const tgba* a);
virtual void add_state(const state* s);
virtual const state* next_state();
protected:
std::stack<const state*> todo; ///< A stack of state yet to explore.
};
/// \brief An implementation of spot::tgba_reachable_iterator that browses
/// states breadth first.
class tgba_reachable_iterator_breadth_first : public tgba_reachable_iterator
{
public:
tgba_reachable_iterator_breadth_first(const tgba* a);
virtual void add_state(const state* s);
virtual const state* next_state();
protected:
std::deque<const state*> todo; ///< A queue of state yet to explore.
};
}
#endif // SPOT_TGBAALGOS_REACHITER_HH
#include <set>
#include "tgba/tgba.hh"
#include "save.hh"
#include "tgba/bddprint.hh"
#include "ltlvisit/tostring.hh"
#include "reachiter.hh"
namespace spot
{
typedef std::set<state*, state_ptr_less_than> seen_set;
/// Process successors.
static void
save_rec(std::ostream& os, const tgba* g, state* st, seen_set& m)
class save_bfs : public tgba_reachable_iterator_breadth_first
{
m.insert(st);
std::string cur = g->format_state(st);
tgba_succ_iterator* si = g->succ_iter(st);
for (si->first(); !si->done(); si->next())
{
state* s = si->current_state();
os << "\"" << cur << "\", \"" << g->format_state(s) << "\", ";
public:
save_bfs(const tgba* a, std::ostream& os)
: tgba_reachable_iterator_breadth_first(a), os_(os)
{
}
bdd_print_sat(os, g->get_dict(), si->current_condition()) << ",";
bdd_print_acc(os, g->get_dict(), si->current_accepting_conditions())
<< ";" << std::endl;
void
start()
{
const bdd_dict* d = automata_->get_dict();
os_ << "acc =";
for (bdd_dict::fv_map::const_iterator ai = d->acc_map.begin();
ai != d->acc_map.end(); ++ai)
{
os_ << " \"";
ltl::to_string(ai->first, os_) << "\"";
}
os_ << ";" << std::endl;
}
void
process_state(const state* s, int, tgba_succ_iterator* si)
{
const bdd_dict* d = automata_->get_dict();
std::string cur = automata_->format_state(s);
for (si->first(); !si->done(); si->next())
{
state* dest = si->current_state();
os_ << "\"" << cur << "\", \""
<< automata_->format_state(dest) << "\", ";
bdd_print_sat(os_, d, si->current_condition()) << ",";
bdd_print_acc(os_, d, si->current_accepting_conditions());
os_ << ";" << std::endl;
}
}
private:
std::ostream& os_;
};
// Destination already explored?
seen_set::iterator i = m.find(s);
if (i != m.end())
{
delete s;
}
else
{
save_rec(os, g, s, m);
// Do not delete S, it is used as key in M.
}
}
delete si;
}
std::ostream&
tgba_save_reachable(std::ostream& os, const tgba* g)
{
const bdd_dict* d = g->get_dict();
os << "acc =";
for (bdd_dict::fv_map::const_iterator ai = d->acc_map.begin();
ai != d->acc_map.end(); ++ai)
{
os << " \"";
ltl::to_string(ai->first, os) << "\"";
}
os << ";" << std::endl;
seen_set m;
state* state = g->get_init_state();
save_rec(os, g, state, m);
// Finally delete all states used as keys in m:
for (seen_set::iterator i = m.begin(); i != m.end(); ++i)
delete *i;
save_bfs b(g, os);
b.run();
return os;
}
}
......@@ -10,12 +10,12 @@ cat >expected <<EOF
digraph G {
size="7.26,10.69"
0 [label="", style=invis]
1 [label="state 0"]
0 -> 1
2 [label="state 1"]
1 [label="state 0"]
1 -> 2 [label="T\n<Acc[p]:0, Acc[q]:1, Acc[r]:0><Acc[p]:1, Acc[q]:0, Acc[r]:0>"]
3 [label="state 2"]
2 [label="state 1"]
2 -> 3 [label="<a:1>\n<Acc[p]:0, Acc[q]:0, Acc[r]:1>"]
3 [label="state 2"]
3 -> 1 [label="<b:1, c:1>\nF"]
}
EOF
......
......@@ -17,12 +17,12 @@ cat >expected <<EOF
digraph G {
size="7.26,10.69"
0 [label="", style=invis]
1 [label="s1"]
0 -> 1
2 [label="s2"]
1 [label="s1"]
1 -> 2 [label="<a:1, b:0>\n<Acc[c]:0, Acc[d]:1><Acc[c]:1, Acc[d]:0>"]
3 [label="state 3"]
2 [label="s2"]
2 -> 3 [label="<a:1>\n<Acc[c]:1, Acc[d]:0>"]
3 [label="state 3"]
3 -> 1 [label="T\nF"]
}
EOF
......
......@@ -30,9 +30,9 @@ cat >expected <<EOF
acc = "p1" "p2" "p3" "p4";
"s1 * s1 * s1", "s3 * s2 * s2", a b, "p1" "p2";
"s1 * s1 * s1", "s2 * s2 * s2", a b, "p1" "p2";
"s2 * s2 * s2", "s3 * s1 * s3", a c, "p3" "p4";
"s1 * s1 * s1", "s3 * s2 * s3", a b, "p1" "p2";
"s1 * s1 * s1", "s2 * s2 * s3", b, "p1" "p2";
"s2 * s2 * s2", "s3 * s1 * s3", a c, "p3" "p4";
"s2 * s2 * s3", "s3 * s1 * s2", a c, "p3" "p4";
EOF
......
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