/*
* This file is part of the program ltl2dstar (http://www.ltl2dstar.de/).
* Copyright (C) 2005-2007 Joachim Klein <j.klein@ltl2dstar.de>
*
* This program is free software; you can redistribute it and/or modify
* it under the terms of the GNU General Public License version 2 as
* published by the Free Software Foundation.
*
* This program 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, write to the Free Software
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
*/
#ifndef NBA_H
#define NBA_H
/** @file
* Provides class NBA to store a nondeterministic B�chi automaton.
*/
#include "common/Exceptions.hpp"
#include "common/Index.hpp"
#include "common/BitSet.hpp"
#include <boost/iterator/iterator_facade.hpp>
#include <boost/shared_ptr.hpp>
#include <string>
#include <iostream>
#include <iterator>
#include <vector>
#include <map>
#include <utility>
#include "NBA_I.hpp"
#include "APSet.hpp"
#include "GraphAlgorithms.hpp"
// forward declaration of NBA_State
template <typename Label, template <typename N> class EdgeContainer > class NBA_State;
/**
* A nondeterministic B�chi automaton.
* See class DA for description of template parameters.
*/
template <typename Label, template <typename N> class EdgeContainer >
class NBA : public NBA_I {
public:
NBA(APSet_cp apset);
virtual ~NBA();
/** The type of the states of the NBA. */
typedef NBA_State<Label,EdgeContainer> state_type;
/** The type of the graph (ie the NBA class itself). */
typedef NBA<Label,EdgeContainer> graph_type;
/** The type of an iterator over the edges of a state. */
typedef typename EdgeContainer<BitSet>::iterator edge_iterator;
/**
* The type of an edge, consisting of the label and a pointer to a BitSet
* of the target states.
*/
typedef std::pair<Label, BitSet*> edge_type;
state_type* newState();
/** Get number of states. */
unsigned int size() {return _index.size();}
/** Type of an iterator over the states (by reference) */
typedef typename Index<state_type>::ref_iterator iterator;
/** An iterator over the states (by reference) pointing to the first state. */
iterator begin() {return _index.begin_ref();}
/** An iterator over the states (by reference) pointing to the first state. */
iterator end() {return _index.end_ref();}
/** Array index operator, get the state with index i. */
state_type* operator[](unsigned int i) {
return _index.get(i);
}
/** Get the size of the underlying APSet. */
unsigned int getAPSize() const {return _apset->size();};
/** Get a const reference to the underlying APSet. */
const APSet& getAPSet() const {return *_apset;};
/** Get a const pointer to the underlying APSet. */
APSet_cp getAPSet_cp() const {return _apset;};
/** Switch the APSet to another with the same number of APs. */
void switchAPSet(APSet_cp new_apset) {
if (new_apset->size()!=_apset->size()) {
THROW_EXCEPTION(IllegalArgumentException, "New APSet has to have the same size as the old APSet!");
}
_apset=new_apset;
}
/** Get the index for a state. */
unsigned int getIndexForState(const state_type *state) const {
return _index.get_index(state);
}
/** Set the start state. */
void setStartState(state_type *state) {_start_state=state;};
/**
* Get the start state.
* @return the start state, or NULL if it wasn't set.
*/
state_type* getStartState() {return _start_state;}
/** Get the set of final (accepting) states in the NBA */
BitSet& getFinalStates() {return _final_states;}
BitSet calculateFinalTrueLoops(SCCs& sccs);
void removeRedundantFinalStates(SCCs& sccs);
void print(std::ostream& out);
void print_lbtt(std::ostream& out);
void print_dot(std::ostream& out);
/** Return number of states. */
unsigned int getStateCount() {return _state_count;}
// -- NBA_I virtual functions -----------
/**
* Create a new state.
* @return the index of the new state
*/
virtual unsigned int nba_i_newState() {
return newState()->getName();
}
/**
* Add an edge from state <i>from</i> to state <i>to</i>
* for the edges covered by the APMonom.
* @param from the index of the 'from' state
* @param m the APMonom
* @param to the index of the 'to' state
*/
virtual void nba_i_addEdge(unsigned int from,
APMonom& m,
unsigned int to) {
(*this)[from]->addEdge(m, *((*this)[to]));
}
/**
* Get the underlying APSet
* @return a const pointer to the APSet
*/
virtual APSet_cp nba_i_getAPSet() {
return getAPSet_cp();
}
/**
* Set the final flag (accepting) for a state.
* @param state the state index
* @param final the flag
*/
virtual void nba_i_setFinal(unsigned int state, bool final) {
(*this)[state]->setFinal(final);
}
/**
* Set the state as the start state.
* @param state the state index
*/
virtual void nba_i_setStartState(unsigned int state) {
setStartState((*this)[state]);
}
/** Type of a boost::shared_ptr for this NBA */
typedef boost::shared_ptr< NBA<Label,EdgeContainer> > shared_ptr;
bool isDeterministic();
static
boost::shared_ptr<NBA<Label, EdgeContainer> >
product_automaton(NBA<Label, EdgeContainer>& nba_1, NBA<Label, EdgeContainer>& nba_2);
private:
/** Number of states */
int _state_count;
/** Storage for the states */
Index<state_type> _index;
/** The underlying APSet */
APSet_cp _apset;
/** The start states */
state_type *_start_state;
/** The states that are accepting (final) */
BitSet _final_states;
};
/**
* Constructor.
* @param apset The underlying APSet
*/
template <typename Label, template <typename N> class EdgeContainer >
NBA<Label, EdgeContainer>::NBA(APSet_cp apset)
: _state_count(0), _apset(apset), _start_state(0) {
}
/**
* Destructor.
*/
template <typename Label, template <typename N> class EdgeContainer >
NBA<Label, EdgeContainer>::~NBA() {
for (unsigned int i=0;i<_index.size();i++) {
if (_index[i]) {
delete _index[i];
}
}
}
/**
* Add a new state.
* @return a pointer to the newly generated state
*/
template <typename Label, template <typename N> class EdgeContainer >
typename NBA<Label, EdgeContainer>::state_type*
NBA<Label, EdgeContainer>::newState() {
_state_count++;
state_type *state=new state_type(*this);
_index.add(state);
return state;
}
/**
* Print the NBA on the output stream.
*/
template <typename Label, template <typename N> class EdgeContainer >
void
NBA<Label, EdgeContainer>::print(std::ostream& out) {
for (iterator state_it=begin();
state_it!=end();
++state_it) {
state_type& state=*state_it;
out << "State " << state.getName();
if (getStartState()==&state) {
out << " *";
}
if (state.isFinal()) {
out << " !";
}
out << std::endl;
for (edge_iterator edge_it=state.edges_begin();
edge_it!=state.edges_end();
++edge_it) {
edge_type edge=*edge_it;
APElement label=edge.first;
BitSet* to_states=edge.second;
out << " " << label.toString(getAPSet()) << " -> " << *to_states << std::endl;
}
}
}
/**
* Print the NBA on the output stream in LBTT format.
*/
template <typename Label, template <typename N> class EdgeContainer >
void
NBA<Label, EdgeContainer>::print_lbtt(std::ostream& out) {
out << size() << " " << "1" << std::endl; // states sp acc
for (iterator state_it=begin();
state_it!=end();
++state_it) {
state_type& state=*state_it;
out << state.getName();
if (getStartState()==&state) {
out << " 1";
} else {
out << " 0";
}
if (state.isFinal()) {
out << " 0";
}
out << " -1"<< std::endl;
for (edge_iterator edge_it=state.edges_begin();
edge_it!=state.edges_end();
++edge_it) {
edge_type edge=*edge_it;
APElement label=edge.first;
BitSet* to_states=edge.second;
for (int to_i=to_states->nextSetBit(0);
to_i!=-1;
to_i=to_states->nextSetBit(to_i+1)) {
out << to_i << " " << label.toStringLBTT(getAPSet()) << std::endl;
}
}
out << "-1" << std::endl;
}
}
/**
* Remove states from the set of accepting (final) states when this is redundant.
* @param sccs the SCCs of the NBA
*/
template <typename Label, template <typename N> class EdgeContainer >
void
NBA<Label, EdgeContainer>::removeRedundantFinalStates(SCCs& sccs) {
for (unsigned int scc=0;
scc<sccs.countSCCs();
++scc) {
if (sccs[scc].cardinality()==1) {
unsigned int state_id=sccs[scc].nextSetBit(0);
state_type *state=(*this)[state_id];
if (state->isFinal()) {
if (!sccs.stateIsReachable(state_id, state_id)) {
// The state is final and has no self-loop
// -> the final flag is redundant
state->setFinal(false);
// std::cerr << "Removing final flag for " << state_id << std::endl;
}
}
}
}
}
/**
* Checks if the NBA is deterministic (every edge has at most one target state).
*/
template <typename Label,
template <typename N> class EdgeContainer >
bool
NBA<Label, EdgeContainer>::isDeterministic() {
for (iterator state_it=begin();
state_it!=end();
++state_it) {
state_type& state=*state_it;
for (edge_iterator edge_it=state.edges_begin();
edge_it!=state.edges_end();
++edge_it) {
edge_type edge=*edge_it;
if (edge.second->cardinality()>1) {
return false;
}
}
}
return true;
}
/**
* Print the NBA in DOT format to the output stream.
* @param out the output stream
*/
template <typename Label,
template <typename N> class EdgeContainer >
void
NBA<Label, EdgeContainer>::print_dot(std::ostream& out) {
if (this->getStartState()==0) {
// No start state!
THROW_EXCEPTION(IllegalArgumentException, "No start state in NBA!");
}
#define DOT_STATE_FONT "Helvetica"
#define DOT_EDGE_FONT "Helvetica"
out << "digraph nba {\n";
#ifdef DOT_STATE_FONT
out << " node [fontname=" << DOT_STATE_FONT << "]\n";
#endif
#ifdef DOT_EDGE_FONT
out << " edge [constraints=false, fontname=" << DOT_EDGE_FONT << "]\n";
#endif
const APSet& ap_set=getAPSet();
for (iterator state_it=begin();
state_it!=end();
++state_it) {
state_type& state=*state_it;
unsigned int i_state=state.getName();
out << "\"" << i_state << "\" [";
out << "label= \"" << i_state << "\"";
if (state.isFinal()) {
out << ", shape=box";
} else {
out << ", shape=circle";
}
if (getStartState()==&state) {
out << ", style=filled, color=black, fillcolor=grey";
}
out << "]\n"; // close parameters for state
// transitions
for (edge_iterator edge_it=state.edges_begin();
edge_it!=state.edges_end();
++edge_it) {
edge_type edge=*edge_it;
APElement label=edge.first;
BitSet* to_states=edge.second;
for (int to_i=to_states->nextSetBit(0);
to_i!=-1;
to_i=to_states->nextSetBit(to_i+1)) {
out << "\"" << i_state << "\" -> \"" << to_i;
out << "\" [label=\" " << label.toString(ap_set, false) << "\"]\n";
}
}
}
out << "}" << std::endl;
}
template <typename Label,
template <typename N> class EdgeContainer >
boost::shared_ptr<NBA<Label, EdgeContainer> >
NBA<Label, EdgeContainer>::product_automaton(NBA<Label, EdgeContainer>& nba_1,
NBA<Label, EdgeContainer>& nba_2) {
assert(nba_1.getAPSet() == nba_2.getAPSet());
boost::shared_ptr<NBA<Label, EdgeContainer> > product_nba(new NBA<Label, EdgeContainer>(nba_1.getAPSet_cp()));
const APSet& apset=nba_1.getAPSet();
assert(apset == nba_2.getAPSet());
for (unsigned int s_1=0;s_1<nba_1.size();s_1++) {
for (unsigned int s_2=0;s_2<nba_2.size();s_2++) {
for (unsigned int copy=0; copy<2; copy++) {
unsigned int s_r=product_nba->nba_i_newState();
assert(s_r == (s_1*nba_2.size() + s_2)*2 + copy);
#ifdef VERBOSE
std::cerr << s_1 << ":" << s_2 << ":" << copy << " = " << s_r << std::endl;
#endif
unsigned int to_copy=copy;
if (copy==0 && nba_1[s_1]->isFinal()) {
to_copy=1;
}
if (copy==1 && nba_2[s_2]->isFinal()) {
(*product_nba)[s_r]->setFinal(true);
to_copy=0;
}
for (typename APSet::element_iterator it=apset.all_elements_begin();
it!=apset.all_elements_end();
++it) {
APElement label=*it;
BitSet *to_s1=nba_1[s_1]->getEdge(label);
BitSet *to_s2=nba_2[s_2]->getEdge(label);
BitSet to_set;
for (BitSetIterator it_e_1=BitSetIterator(*to_s1);
it_e_1!=BitSetIterator::end(*to_s1);
++it_e_1) {
for (BitSetIterator it_e_2=BitSetIterator(*to_s2);
it_e_2!=BitSetIterator::end(*to_s2);
++it_e_2) {
unsigned int to=((*it_e_1)*nba_2.size() + (*it_e_2))*2 + to_copy;
to_set.set(to);
}
}
*((*product_nba)[s_r]->getEdge(label))=to_set;
}
}
}
}
unsigned int start_1 = nba_1.getStartState()->getName();
unsigned int start_2 = nba_2.getStartState()->getName();
product_nba->setStartState( (*product_nba)[ start_1*nba_2.size() + start_2 ]);
return product_nba;
}
#endif