Commit e2e138f6 authored by Felix Abecassis's avatar Felix Abecassis Committed by Alexandre Duret-Lutz
Browse files

Modify the powerset algorithm to keep track of accepting states

from the initial automaton.

* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
Added class tgba_explicit_number, a tgba_explicit where states are
labelled by integers.
* src/tgbaalgos/powerset.hh, src/tgbaalgos/powerset.cc:
When building the deterministic automaton, keep track of which states
were created from an accepting state in the initial automaton.
The states are added to the new optional parameter (if not 0),
acc_list.
Use tgba_explicit_number instead of tgba_explicit_string to build
the result.
* src/tgbaalgos/scc.cc (spot): Small fix.
Print everything on std::cout.
parent bd742ef6
2010-03-20 Felix Abecassis <abecassis@lrde.epita.fr>
Modify the powerset algorithm to keep track of accepting states
from the initial automaton.
* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
Added tgba_explicit_number, a tgba_explicit where states are labelled
by integers.
* src/tgbaalgos/powerset.hh, src/tgbaalgos/powerset.cc:
When building the deterministic automaton, keep track of which states
were created from an accepting state in the initial automaton.
The states are added to the new optional parameter (if not 0),
acc_list.
Now use tgba_explicit_number instead of tgba_explicit_string to build
the result.
* src/tgbaalgos/scc.cc (spot): Small fix.
Print everything on std::cout.
2011-01-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix computation of support_conditions for bdd-based TGBA.
......
......@@ -21,6 +21,7 @@
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include <sstream>
#include "ltlast/atomic_prop.hh"
#include "ltlast/constant.hh"
#include "tgbaexplicit.hh"
......@@ -349,4 +350,34 @@ namespace spot
return ltl::to_string(i->second);
}
tgba_explicit_number::~tgba_explicit_number()
{
ns_map::iterator i = name_state_map_.begin();
while (i != name_state_map_.end())
{
tgba_explicit::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
delete *i2;
// Advance the iterator before deleting the formula.
delete i->second;
++i;
}
}
tgba_explicit::state* tgba_explicit_number::add_default_init()
{
return add_state(0);
}
std::string
tgba_explicit_number::format_state(const spot::state* s) const
{
const state_explicit* se = dynamic_cast<const state_explicit*>(s);
assert(se);
sn_map::const_iterator i = state_name_map_.find(se->get_state());
assert(i != state_name_map_.end());
std::stringstream ss;
ss << i->second;
return ss.str();
}
}
......@@ -345,6 +345,18 @@ namespace spot
virtual state* add_default_init();
virtual std::string format_state(const spot::state* s) const;
};
class tgba_explicit_number:
public tgba_explicit_labelled<int, std::tr1::hash<int> >
{
public:
tgba_explicit_number(bdd_dict* dict):
tgba_explicit_labelled<int, std::tr1::hash<int> >(dict)
{};
virtual ~tgba_explicit_number();
virtual state* add_default_init();
virtual std::string format_state(const spot::state* s) const;
};
}
#endif // SPOT_TGBA_TGBAEXPLICIT_HH
......@@ -24,25 +24,28 @@
#include <set>
#include <map>
#include <deque>
#include <sstream>
#include "powerset.hh"
#include "misc/hash.hh"
#include "tgbaalgos/powerset.hh"
#include "tgbaalgos/scc.hh"
#include "bdd.h"
namespace spot
{
tgba_explicit*
tgba_powerset(const tgba* aut)
tgba_powerset(const tgba* aut,
std::list<const state*>* acc_list)
{
typedef Sgi::hash_set<const state*, state_ptr_hash,
state_ptr_equal> state_set;
typedef std::set<const state*, state_ptr_less_than> power_state;
typedef std::map<power_state, std::string> power_set;
typedef std::map<power_state, int> power_set;
typedef std::deque<power_state> todo_list;
power_set seen;
todo_list todo;
tgba_explicit_string* res = new tgba_explicit_string(aut->get_dict());
scc_map m(aut);
tgba_explicit_number* res = new tgba_explicit_number(aut->get_dict());
state_set states;
......@@ -52,7 +55,8 @@ namespace spot
states.insert(s);
ps.insert(s);
todo.push_back(ps);
seen[ps] = "1";
seen[ps] = 1;
m.build_map();
}
unsigned state_num = 1;
......@@ -77,6 +81,7 @@ namespace spot
// Construct the set of all states reachable via COND.
power_state dest;
bool accepting = false;
for (i = src.begin(); i != src.end(); ++i)
{
tgba_succ_iterator *si = aut->succ_iter(*i);
......@@ -94,30 +99,36 @@ namespace spot
{
states.insert(s);
}
unsigned scc_num = m.scc_of_state(s);
if (m.accepting(scc_num))
accepting = true;
dest.insert(s);
}
delete si;
}
if (dest.empty())
continue;
// Add that transition.
power_set::const_iterator i = seen.find(dest);
std::string dest_name;
int dest_num;
tgba_explicit::transition* t;
if (i != seen.end())
{
dest_name = i->second;
dest_num = i->second;
t = res->create_transition(seen[src], dest_num);
}
else
{
std::ostringstream str;
str << ++state_num;
dest_name = str.str();
seen[dest] = dest_name;
dest_num = ++state_num;
seen[dest] = dest_num;
todo.push_back(dest);
t = res->create_transition(seen[src], dest_num);
if (acc_list && accepting)
{
const state* dst = new state_explicit(t->dest);
acc_list->push_front(dst);
}
}
tgba_explicit::transition* t =
res->create_transition(seen[src], dest_name);
res->add_conditions(t, cond);
}
}
......
......@@ -22,6 +22,7 @@
#ifndef SPOT_TGBAALGOS_POWERSET_HH
# define SPOT_TGBAALGOS_POWERSET_HH
# include <list>
# include "tgba/tgbaexplicit.hh"
namespace spot
......@@ -32,7 +33,11 @@ namespace spot
/// This create a deterministic automaton that recognize the
/// same language as \a aut would if its acceptance conditions
/// were ignored. This is the classical powerset algorithm.
tgba_explicit* tgba_powerset(const tgba* aut);
/// If acc_list is not 0. Whenever a power state is created from one
/// accepting state (a state belonging to an accepting SCC), then this power
/// state is added to acc_list.
tgba_explicit* tgba_powerset(const tgba* aut,
std::list<const state*>* acc_list = 0);
}
#endif // SPOT_TGBAALGOS_POWERSET_HH
......@@ -505,9 +505,9 @@ namespace spot
m.useful_acc_of(state))) << "]";
}
std::cout << " " << state << " [shape=box,"
<< (m.accepting(state) ? "style=bold," : "")
<< "label=\"" << ostr.str() << "\"]" << std::endl;
out << " " << state << " [shape=box,"
<< (m.accepting(state) ? "style=bold," : "")
<< "label=\"" << ostr.str() << "\"]" << std::endl;
const scc_map::succ_type& succ = m.succ(state);
......
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