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

Rename the class taa as taa_tgba.

Browse source 
* src/tgba/taa.cc, src/tgba/taa.hh: Rename as ...
* src/tgba/taatgba.cc, src/tgba/taatgba.hh: ... these, and
rename the class taa as taa_tgba.
* src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh,
src/tgbaalgos/Makefile.am: Adjust.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/taa.test: Rename as ...
* src/tgbatest/taatgba.test ... this.
* src/tgbatest/taa.cc: Rename as ...
* src/tgbatest/taatgba.cc ... this, and adjust.
This commit is contained in:
Guillaume Sadegh 2009-11-27 23:17:38 +01:00
parent d362e752d1
commit f00aa49dc3
9 changed files with 117 additions and 101 deletions
Download patch file Download diff file Expand all files Collapse all files

496
src/tgba/taatgba.cc Normal file
View file

@ -0,0 +1,496 @@
// Copyright (C) 2009 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 <map>
#include <algorithm>
#include <iterator>
#include <iostream>
#include "tgba/formula2bdd.hh"
#include "misc/bddop.hh"
#include "taatgba.hh"
namespace spot
{
/*--------.
| taa_tgba |
`--------*/
taa_tgba::taa_tgba(bdd_dict* dict)
: name_state_map_(), state_name_map_(), dict_(dict),
all_acceptance_conditions_(bddfalse),
all_acceptance_conditions_computed_(false),
neg_acceptance_conditions_(bddtrue),
init_(0), state_set_vec_()
{
}
taa_tgba::~taa_tgba()
{
ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
taa_tgba::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
delete *i2;
delete i->second;
}
ss_vec::iterator j;
for (j = state_set_vec_.begin(); j != state_set_vec_.end(); ++j)
delete *j;
dict_->unregister_all_my_variables(this);
}
void
taa_tgba::set_init_state(const std::string& s)
{
std::vector<std::string> v(1);
v[0] = s;
set_init_state(v);
}
void
taa_tgba::set_init_state(const std::vector<std::string>& s)
{
init_ = add_state_set(s);
}
taa_tgba::transition*
taa_tgba::create_transition(const std::string& s,
const std::vector<std::string>& d)
{
state* src = add_state(s);
state_set* dst = add_state_set(d);
transition* t = new transition;
t->dst = dst;
t->condition = bddtrue;
t->acceptance_conditions = bddfalse;
src->push_back(t);
return t;
}
taa_tgba::transition*
taa_tgba::create_transition(const std::string& s, const std::string& d)
{
std::vector<std::string> vec;
vec.push_back(d);
return create_transition(s, vec);
}
void
taa_tgba::add_condition(transition* t, const ltl::formula* f)
{
t->condition &= formula_to_bdd(f, dict_, this);
f->destroy();
}
void
taa_tgba::add_acceptance_condition(transition* t, const ltl::formula* f)
{
if (dict_->acc_map.find(f) == dict_->acc_map.end())
{
int v = dict_->register_acceptance_variable(f, this);
bdd neg = bdd_nithvar(v);
neg_acceptance_conditions_ &= neg;
// Append neg to all acceptance conditions.
ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
taa_tgba::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
(*i2)->acceptance_conditions &= neg;
}
all_acceptance_conditions_computed_ = false;
}
bdd_dict::fv_map::iterator i = dict_->acc_map.find(f);
assert(i != dict_->acc_map.end());
f->destroy();
bdd v = bdd_ithvar(i->second);
t->acceptance_conditions |= v & bdd_exist(neg_acceptance_conditions_, v);
}
void
taa_tgba::output(std::ostream& os) const
{
ns_map::const_iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
taa_tgba::state::const_iterator i2;
os << "State: " << i->first << std::endl;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
{
os << " " << format_state_set((*i2)->dst)
<< ", C:" << (*i2)->condition
<< ", A:" << (*i2)->acceptance_conditions << std::endl;
}
}
}
state*
taa_tgba::get_init_state() const
{
assert(init_);
return new spot::state_set(init_);
}
tgba_succ_iterator*
taa_tgba::succ_iter(const spot::state* state,
const spot::state* global_state,
const tgba* global_automaton) const
{
const spot::state_set* s = dynamic_cast<const spot::state_set*>(state);
assert(s);
(void) global_state;
(void) global_automaton;
return new taa_succ_iterator(s->get_state(), all_acceptance_conditions());
}
bdd_dict*
taa_tgba::get_dict() const
{
return dict_;
}
std::string
taa_tgba::format_state(const spot::state* s) const
{
const spot::state_set* se = dynamic_cast<const spot::state_set*>(s);
assert(se);
const state_set* ss = se->get_state();
return format_state_set(ss);
}
bdd
taa_tgba::all_acceptance_conditions() const
{
if (!all_acceptance_conditions_computed_)
{
all_acceptance_conditions_ =
compute_all_acceptance_conditions(neg_acceptance_conditions_);
all_acceptance_conditions_computed_ = true;
}
return all_acceptance_conditions_;
}
bdd
taa_tgba::neg_acceptance_conditions() const
{
return neg_acceptance_conditions_;
}
bdd
taa_tgba::compute_support_conditions(const spot::state* s) const
{
const spot::state_set* se = dynamic_cast<const spot::state_set*>(s);
assert(se);
const state_set* ss = se->get_state();
bdd res = bddtrue;
taa_tgba::state_set::const_iterator i;
taa_tgba::state::const_iterator j;
for (i = ss->begin(); i != ss->end(); ++i)
for (j = (*i)->begin(); j != (*i)->end(); ++j)
res |= (*j)->condition;
return res;
}
bdd
taa_tgba::compute_support_variables(const spot::state* s) const
{
const spot::state_set* se = dynamic_cast<const spot::state_set*>(s);
assert(se);
const state_set* ss = se->get_state();
bdd res = bddtrue;
taa_tgba::state_set::const_iterator i;
taa_tgba::state::const_iterator j;
for (i = ss->begin(); i != ss->end(); ++i)
for (j = (*i)->begin(); j != (*i)->end(); ++j)
res &= bdd_support((*j)->condition);
return res;
}
taa_tgba::state*
taa_tgba::add_state(const std::string& name)
{
ns_map::iterator i = name_state_map_.find(name);
if (i == name_state_map_.end())
{
taa_tgba::state* s = new taa_tgba::state;
name_state_map_[name] = s;
state_name_map_[s] = name;
return s;
}
return i->second;
}
taa_tgba::state_set*
taa_tgba::add_state_set(const std::vector<std::string>& names)
{
state_set* ss = new state_set;
for (unsigned i = 0; i < names.size(); ++i)
ss->insert(add_state(names[i]));
state_set_vec_.push_back(ss);
return ss;
}
std::string
taa_tgba::format_state_set(const taa_tgba::state_set* ss) const
{
state_set::const_iterator i1 = ss->begin();
sn_map::const_iterator i2;
if (ss->empty())
return std::string("{}");
if (ss->size() == 1)
{
i2 = state_name_map_.find(*i1);
assert(i2 != state_name_map_.end());
return "{" + i2->second + "}";
}
else
{
std::string res("{");
while (i1 != ss->end())
{
i2 = state_name_map_.find(*i1++);
assert(i2 != state_name_map_.end());
res += i2->second;
res += ",";
}
res[res.size() - 1] = '}';
return res;
}
}
/*----------.
| state_set |
`----------*/
const taa_tgba::state_set*
state_set::get_state() const
{
return s_;
}
int
state_set::compare(const spot::state* other) const
{
const state_set* o = dynamic_cast<const state_set*>(other);
assert(o);
const taa_tgba::state_set* s1 = get_state();
const taa_tgba::state_set* s2 = o->get_state();
if (s1->size() != s2->size())
return s1->size() - s2->size();
taa_tgba::state_set::const_iterator it1 = s1->begin();
taa_tgba::state_set::const_iterator it2 = s2->begin();
while (it2 != s2->end())
{
int i = *it1++ - *it2++;
if (i != 0)
return i;
}
return 0;
}
size_t
state_set::hash() const
{
size_t res = 0;
taa_tgba::state_set::const_iterator it = s_->begin();
while (it != s_->end())
{
res ^= reinterpret_cast<const char*>(*it++) - static_cast<char*>(0);
res = wang32_hash(res);
}
return res;
}
state_set*
state_set::clone() const
{
if (delete_me_ && s_)
return new spot::state_set(new taa_tgba::state_set(*s_), true);
else
return new spot::state_set(s_, false);
}
/*--------------.
| taa_succ_iter |
`--------------*/
taa_succ_iterator::taa_succ_iterator(const taa_tgba::state_set* s,
bdd all_acc)
: all_acceptance_conditions_(all_acc), seen_()
{
if (s->empty())
{
taa_tgba::transition* t = new taa_tgba::transition;
t->condition = bddtrue;
t->acceptance_conditions = bddfalse;
t->dst = new taa_tgba::state_set;
succ_.push_back(t);
return;
}
bounds_t bounds;
for (taa_tgba::state_set::const_iterator i = s->begin(); i != s->end(); ++i)
bounds.push_back(std::make_pair((*i)->begin(), (*i)->end()));
/// Sorting might make the cartesian product faster by not
/// exploring all possibilities.
std::sort(bounds.begin(), bounds.end(), distance_sort());
std::vector<iterator> pos;
pos.reserve(bounds.size());
for (bounds_t::const_iterator i = bounds.begin(); i != bounds.end(); ++i)
pos.push_back(i->first);
while (pos[0] != bounds[0].second)
{
taa_tgba::transition* t = new taa_tgba::transition;
t->condition = bddtrue;
t->acceptance_conditions = bddfalse;
taa_tgba::state_set* ss = new taa_tgba::state_set;
unsigned p;
for (p = 0; p < pos.size() && t->condition != bddfalse; ++p)
{
taa_tgba::state_set::const_iterator j;
for (j = (*pos[p])->dst->begin(); j != (*pos[p])->dst->end(); ++j)
if ((*j)->size() > 0) // Remove sink states.
ss->insert(*j);
// Fill the new transition.
t->condition &= (*pos[p])->condition;
t->acceptance_conditions |= (*pos[p])->acceptance_conditions;
} // If p != pos.size() we have found a contradiction
assert(p > 0);
t->dst = ss;
// Boxing to be able to insert ss in the map directly.
spot::state_set* b = new spot::state_set(ss);
// If no contradiction, then look for another transition to
// merge with the new one.
seen_map::iterator i;
if (t->condition != bddfalse)
{
for (i = seen_.find(b); i != seen_.end(); ++i)
{
if (*i->second->dst == *t->dst
&& i->second->condition == t->condition)
{
i->second->acceptance_conditions &= t->acceptance_conditions;
break;
}
if (*i->second->dst == *t->dst
&& i->second->acceptance_conditions == t->acceptance_conditions)
{
i->second->condition |= t->condition;
break;
}
}
}
// Mark the new transition as seen and keep it if we have not
// found any contraction and no other transition to merge with,
// or delete it otherwise.
if (t->condition != bddfalse && i == seen_.end())
{
seen_.insert(std::make_pair(b, t));
succ_.push_back(t);
}
else
{
delete t->dst;
delete t;
delete b;
}
for (int i = pos.size() - 1; i >= 0; --i)
{
if ((i < int(p))
&& (std::distance(pos[i], bounds[i].second) > 1
|| (i == 0 && std::distance(pos[i], bounds[i].second) == 1)))
{
++pos[i];
break;
}
else
pos[i] = bounds[i].first;
}
}
}
taa_succ_iterator::~taa_succ_iterator()
{
for (unsigned i = 0; i < succ_.size(); ++i)
{
delete succ_[i]->dst;
delete succ_[i];
}
for (seen_map::iterator i = seen_.begin(); i != seen_.end(); ++i)
delete i->first;
}
void
taa_succ_iterator::first()
{
i_ = succ_.begin();
}
void
taa_succ_iterator::next()
{
++i_;
}
bool
taa_succ_iterator::done() const
{
return i_ == succ_.end();
}
spot::state_set*
taa_succ_iterator::current_state() const
{
assert(!done());
return new spot::state_set(new taa_tgba::state_set(*(*i_)->dst), true);
}
bdd
taa_succ_iterator::current_condition() const
{
assert(!done());
return (*i_)->condition;
}
bdd
taa_succ_iterator::current_acceptance_conditions() const
{
assert(!done());
return all_acceptance_conditions_ -
((*i_)->acceptance_conditions & all_acceptance_conditions_);
}
}