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

tgba_union: Remove this unused class.

* src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh: Delete.
* src/tgba/Makefile.am: Adjust.
parent dc5ad78b
......@@ -42,7 +42,6 @@ tgba_HEADERS = \
tgbaproduct.hh \
tgbasgba.hh \
tgbasafracomplement.hh \
tgbaunion.hh \
wdbacomp.hh
noinst_LTLIBRARIES = libtgba.la
......@@ -61,5 +60,4 @@ libtgba_la_SOURCES = \
tgbasafracomplement.cc \
tgbascc.cc \
tgbasgba.cc \
tgbaunion.cc \
wdbacomp.cc
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// 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 "tgbaunion.hh"
#include <string>
#include <cassert>
#include "misc/hashfunc.hh"
namespace spot
{
////////////////////////////////////////////////////////////
// state_union
state_union::state_union(const state_union& o)
: state(),
left_(o.left()->clone()),
right_(o.right()->clone())
{
}
state_union::~state_union()
{
left_->destroy();
right_->destroy();
}
int
state_union::compare(const state* other) const
{
const state_union* o = down_cast<const state_union*>(other);
assert(o);
// Initial state
if (!o->left() && !o->right())
return left_ || right_;
// States from different automata.
if (left_ && !o->left())
return -1;
// States from different automata.
if (right_ && !o->right())
return 1;
// States from left automata.
if (left_)
return left_->compare(o->left());
// States from right automata.
if (right_)
return right_->compare(o->right());
// 0 should never be returned.
return 0;
}
size_t
state_union::hash() const
{
// We assume that size_t is 32-bit wide.
if (left_)
return wang32_hash(left_->hash());
if (right_)
return wang32_hash(right_->hash());
return 0;
}
state_union*
state_union::clone() const
{
return new state_union(*this);
}
////////////////////////////////////////////////////////////
// tgba_succ_iterator_union
tgba_succ_iterator_union::tgba_succ_iterator_union
(tgba_succ_iterator* left, tgba_succ_iterator* right,
bdd left_missing, bdd right_missing, bdd left_neg, bdd right_neg)
: left_(left), right_(right),
left_missing_(left_missing),
right_missing_(right_missing),
left_neg_(left_neg), right_neg_(right_neg)
{
}
void
tgba_succ_iterator_union::recycle(const tgba* l, tgba_succ_iterator* left,
const tgba* r, tgba_succ_iterator* right)
{
l->release_iter(left_);
left_ = left;
r->release_iter(right_);
right_ = right;
}
tgba_succ_iterator_union::~tgba_succ_iterator_union()
{
delete left_;
delete right_;
}
bool
tgba_succ_iterator_union::next()
{
// Is it the initial state ?
if (left_ && right_)
{
// Yes, first iterate on the successors of the initial state of the
// left automaton.
if (!left_->done())
{
if (left_->next())
{
current_cond_ = left_->current_condition();
return true;
}
else if (!right_->done())
{
current_cond_ = right_->current_condition();
return true;
}
else
{
return false;
}
}
// Now iterate with the successors of the initial state of the right
// automaton.
else
{
if (right_->next())
{
current_cond_ = right_->current_condition();
return true;
}
else
{
return false;
}
}
}
else
{
// No, iterate either on the left or the right automaton.
if (left_)
{
if (left_->next())
{
current_cond_ = left_->current_condition();
return true;
}
else
{
return false;
}
}
else
{
if (right_->next())
{
current_cond_ = right_->current_condition();
return true;
}
else
{
return false;
}
}
}
}
bool
tgba_succ_iterator_union::first()
{
bool r = false;
if (right_)
{
r = right_->first();
if (r)
current_cond_ = right_->current_condition();
}
bool l = false;
if (left_)
{
l = left_->first();
if (l)
current_cond_ = left_->current_condition();
}
return r || l;
}
bool
tgba_succ_iterator_union::done() const
{
if (right_)
return right_->done();
else
return left_->done();
}
state_union*
tgba_succ_iterator_union::current_state() const
{
if (left_ && !left_->done())
return new state_union(left_->current_state(), 0);
else
return new state_union(0, right_->current_state());
}
bdd
tgba_succ_iterator_union::current_condition() const
{
return current_cond_;
}
bdd tgba_succ_iterator_union::current_acceptance_conditions() const
{
if (left_ && right_)
{
if (left_->done())
return right_->current_acceptance_conditions();
else
return left_->current_acceptance_conditions();
}
// If we are either on the left or the right automaton, we need to modify
// the acceptance conditions of the transition.
if (left_)
{
bdd cur = (left_->current_acceptance_conditions() & left_neg_)
| left_missing_;
return cur;
}
else
{
bdd cur = (right_->current_acceptance_conditions() & right_neg_)
| right_missing_;
return cur;
}
}
////////////////////////////////////////////////////////////
// tgba_union
tgba_union::tgba_union(const tgba* left, const tgba* right)
: dict_(left->get_dict()), left_(left), right_(right)
{
assert(dict_ == right->get_dict());
// Conjunction of negated acceptance conditions, e.g. !a & !b & !c
bdd lna = left_->neg_acceptance_conditions();
bdd rna = right_->neg_acceptance_conditions();
left_acc_complement_ = lna;
right_acc_complement_ = rna;
// Disjunctive Normal Form for all acceptance conditions
// e.g. (a & !b & !c) | (b & !a & !c) | (c & !a & !b)
bdd lac = left_->all_acceptance_conditions();
bdd rac = right_->all_acceptance_conditions();
// Remove all occurences in rna of the variables in the set lna.
// The result is a set with the missing variables in the left automaton,
// i.e. the variables that are in the right automaton but not in the left
// one.
bdd lmac = bdd_exist(rna, lna);
left_var_missing_ = lmac;
// Remove all occurences in lna of the variables in the set rna.
// The result is a set with the missing variables in the right automaton,
// i.e. the variables that are in the left automaton but not in the right
// one.
bdd rmac = bdd_exist(lna, rna);
right_var_missing_ = rmac;
// The new Disjunctive Normal Form for our union.
all_acceptance_conditions_ = ((lac & lmac) | (rac & rmac));
// Simply the conjunction of left and right negated acceptance conditions.
neg_acceptance_conditions_ = lna & rna;
// "-" is a NAND between the two sets.
// The result is the list of acceptance conditions to add to each
// transition.
// For example if a transition on the left automaton has (a & !b)
// and the right automaton has a new acceptance condition c, the resulting
// acceptance condition will be (a & !b & !c) | (c & !a & !b)
left_acc_missing_ = all_acceptance_conditions_ - (lac & lmac);
right_acc_missing_ = all_acceptance_conditions_ - (rac & rmac);
dict_->register_all_variables_of(&left_, this);
dict_->register_all_variables_of(&right_, this);
}
tgba_union::~tgba_union()
{
dict_->unregister_all_my_variables(this);
}
state*
tgba_union::get_init_state() const
{
return new state_union(0, 0);
}
tgba_succ_iterator_union*
tgba_union::succ_iter(const state* st) const
{
const state_union* s = down_cast<const state_union*>(st);
assert(s);
// Is it the initial state ?
tgba_succ_iterator* li;
tgba_succ_iterator* ri;
if (!s->left() && !s->right())
{
// Yes, create an iterator with both initial states.
state* left_init = left_->get_init_state();
state* right_init = right_->get_init_state();
li = left_->succ_iter(left_init);
ri = right_->succ_iter(right_init);
left_init->destroy();
right_init->destroy();
}
// No, create an iterator based on the corresponding state
// in the left or in the right automaton.
else if (s->left())
{
li = left_->succ_iter(s->left());
ri = nullptr;
}
else
{
li = nullptr;
ri = right_->succ_iter(s->right());
}
if (iter_cache_)
{
tgba_succ_iterator_union* res =
down_cast<tgba_succ_iterator_union*>(iter_cache_);
res->recycle(left_, li, right_, ri);
iter_cache_ = nullptr;
return res;
}
return new tgba_succ_iterator_union(li, ri,
left_acc_missing_,
right_acc_missing_,
left_var_missing_,
right_var_missing_);
}
bdd
tgba_union::compute_support_conditions(const state* in) const
{
const state_union* s = down_cast<const state_union*>(in);
assert(s);
if (!s->left() && !s->right())
return (left_->support_conditions(left_->get_init_state())
& right_->support_conditions(right_->get_init_state()));
if (s->left())
return left_->support_conditions(s->left());
else
return right_->support_conditions(s->right());
}
bdd_dict_ptr
tgba_union::get_dict() const
{
return dict_;
}
std::string
tgba_union::format_state(const state* target_state) const
{
const state_union* s = down_cast<const state_union*>(target_state);
assert(s);
if (!s->left() && !s->right())
{
return "initial";
}
else
{
if (s->left())
return (left_->format_state(s->left()));
else
return (right_->format_state(s->right()));
}
}
state*
tgba_union::project_state(const state* s, const tgba* t) const
{
const state_union* s2 = down_cast<const state_union*>(s);
assert(s2);
// We can't project the initial state of our union.
if (!s2->left() && !s2->right())
return 0;
if (t == this)
return s2->clone();
if (s2->left())
return left_->project_state(s2->left(), t);
else
return right_->project_state(s2->right(), t);
}
bdd
tgba_union::all_acceptance_conditions() const
{
return all_acceptance_conditions_;
}
bdd
tgba_union::neg_acceptance_conditions() const
{
return neg_acceptance_conditions_;
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// 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_TGBA_TGBAUNION_HH
# define SPOT_TGBA_TGBAUNION_HH
#include "tgba.hh"
namespace spot
{
/// \ingroup tgba_on_the_fly_algorithms
/// \brief A state for spot::tgba_union.
///
/// This state is in fact a pair.
/// If the first member equals 0 and the second is different from 0,
/// the state belongs to the left automaton.
/// If the first member is different from 0 and the second is 0,
/// the state belongs to the right automaton.
/// If both members are 0, the state is the initial state.
class SPOT_API state_union : public state
{
public:
/// \brief Constructor
/// \param left The state from the left automaton.
/// \param right The state from the right automaton.
/// These states are acquired by spot::state_union, and will
/// be destroyed on destruction.
state_union(state* left, state* right)
: left_(left),
right_(right)
{
}
/// Copy constructor
state_union(const state_union& o);
virtual ~state_union();
state*
left() const
{
return left_;
}
state*
right() const
{
return right_;
}
virtual int compare(const state* other) const;
virtual size_t hash() const;
virtual state_union* clone() const;
private:
state* left_; ///< Does the state belongs
/// to the left automaton ?
state* right_; ///< Does the state belongs
/// to the right automaton ?
};
/// \brief Iterate over the successors of an union computed on the fly.
class SPOT_API tgba_succ_iterator_union: public tgba_succ_iterator
{
public:
tgba_succ_iterator_union(tgba_succ_iterator* left,
tgba_succ_iterator* right,
bdd left_missing,
bdd right_missing, bdd left_var, bdd right_var);
void recycle(const tgba* l, tgba_succ_iterator* left,
const tgba* r, tgba_succ_iterator* right);
virtual ~tgba_succ_iterator_union();
// iteration
bool first();
bool next();
bool done() const;
// inspection
state_union* current_state() const;
bdd current_condition() const;
bdd current_acceptance_conditions() const;
protected:
tgba_succ_iterator* left_;
tgba_succ_iterator* right_;
bdd current_cond_;
bdd left_missing_;
bdd right_missing_;
bdd left_neg_;
bdd right_neg_;
friend class tgba_union;
};
/// \brief A lazy union. (States are computed on the fly.)
class SPOT_API tgba_union: public tgba
{
public:
/// \brief Constructor.
/// \param left The left automata in the union.
/// \param right The right automata in the union.
tgba_union(const tgba* left, const tgba* right);
virtual ~tgba_union();
virtual state* get_init_state() const;
virtual tgba_succ_iterator_union*
succ_iter(const state* state) const;
virtual bdd_dict_ptr get_dict() const;
virtual std::string format_state(const state* state) const;
virtual state* project_state(const state* s, const tgba* t) const;
virtual bdd all_acceptance_conditions() const;
virtual bdd neg_acceptance_conditions() const;
protected:
virtual bdd compute_support_conditions(const state* state) const;
private:
bdd_dict_ptr dict_;
const tgba* left_;
const tgba* right_;
bdd left_acc_missing_;
bdd right_acc_missing_;
bdd left_acc_complement_;
bdd right_acc_complement_;
bdd left_var_missing_;
bdd right_var_missing_;
bdd all_acceptance_conditions_;
bdd neg_acceptance_conditions_;
// Disallow copy.
tgba_union(const tgba_union&) SPOT_DELETED;
tgba_union& operator=(const tgba_union&) SPOT_DELETED;
};
}
#endif // SPOT_TGBA_TGBAUNION_HH
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