/*
* 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 STUTTEREDNBA2DA_H
#define STUTTEREDNBA2DA_H
/** @file
* Provides class StutteredNBA2DA.
*/
#include "common/HashFunction.hpp"
#include "StutterSensitivenessInformation.hpp"
// debug:
// #define STUTTERED_VERBOSE 1
/**
* A class representing a tree (state in the original automaton) augmented with an AcceptanceSignature.
* Tree should be a shared_ptr type.
*/
template <typename Tree, typename AcceptanceSignature>
class TreeWithAcceptance {
public:
/** Constructor. The acceptance signature is initialized from the tree.
* @param tree the Tree
*/
TreeWithAcceptance(Tree tree) :
_tree(tree), _signature(*tree) {
}
/** Get the tree.
* @return the Tree.
*/
const Tree& getTree() const {return _tree;}
/** Get the AcceptanceSignature.
* @return the AcceptanceSignature */
const AcceptanceSignature& getSignature() const {return _signature;}
/** Get the AcceptanceSignature.
* @return the AcceptanceSignature */
AcceptanceSignature& getSignature() {return _signature;}
/** A shared_ptr to a TreeWithAcceptance */
typedef boost::shared_ptr<TreeWithAcceptance<Tree,AcceptanceSignature> > ptr;
/** Check if this TreeWithAcceptance is equal to another.
* @param other the other TreeWithAcceptance.
* @return true iff the two are equal
*/
bool operator==(const TreeWithAcceptance& other) const {
return (*_tree == *other.getTree()) && (_signature == other.getSignature());
}
/** Check if this TreeWithAcceptance is 'smaller' than another.
* @param other the other TreeWithAcceptance.
* @return true iff this is smaller than other
*/
bool operator<(const TreeWithAcceptance& other) const {
if (*_tree < *other.getTree()) {
return true;
}
if (*_tree == *other.getTree()) {
return _signature < other.getSignature();
}
return false;
}
/** Generate short description of this TreeWithAcceptance
* @return the description */
std::string toString() {
return _tree->toString()+_signature.toString();
}
/**
* Calculate a hash value using HashFunction
* @param hashfunction the HashFunction functor
*/
template <class HashFunction>
void hashCode(HashFunction& hashfunction) {
_tree->hashCode(hashfunction);
_signature.hashCode(hashfunction);
}
/**
* Generate the appropriate acceptance signature for Rabin Acceptance for this object
* @param acceptance the AcceptanceForState accessor to which the signature is copied
*/
void generateAcceptance(RabinAcceptance::AcceptanceForState acceptance) {
acceptance.setSignature(_signature);
}
/**
* Generate the appropriate acceptance signature for Rabin Acceptance for this object
* @param acceptance the acceptance signature to which the signature for this state is copied
*/
void generateAcceptance(RabinAcceptance::RabinSignature& acceptance) {
acceptance=_signature;
}
/**
* Set the description for this state.
* @param description the description
*/
void setDescription(const std::string& description) {
_description=description;
}
/**
* Get the description for this state.
* @return description the description
*/
const std::string& getDescription() const {
return _description;
}
/**
* Get the description for this state.
* @return description the description
*/
std::string toHTML() {
if (_description=="") {
return _tree->toHTML();
} else {
return _description;
}
}
private:
/** The tree */
const Tree _tree;
/** The acceptance signature */
AcceptanceSignature _signature;
/** The description */
std::string _description;
};
/** Calculate stuttered DA_t given Algorithm_t */
template <typename Algorithm_t,
typename DA_t>
class StutteredNBA2DA {
private:
/** Generate detailed descriptions for the states? */
bool _detailed_states;
/** Information which symbols may be stuttered */
StutterSensitivenessInformation::ptr _stutter_information;
public:
typedef typename DA_t::acceptance_condition_type Acceptance;
/** Constructor.
* detailed_states Generate detailed descriptions for the states?
* stutter_information Information which symbols may be stuttered
*/
StutteredNBA2DA(bool detailed_states,
StutterSensitivenessInformation::ptr stutter_information) :
_detailed_states(detailed_states),
_stutter_information(stutter_information) {
assert(_stutter_information);
}
~StutteredNBA2DA() {};
/**
* Perform the stuttered conversion.
* Throws LimitReachedException if a limit is set (>0) and
* there are more states in the generated DRA than the limit.
* @param algo the underlying algorithm to be used
* @param da_result the DRA where the result is stored
* (has to have same APSet as the nba)
* @param limit a limit for the number of states (0 disables the limit).
*/
void convert(Algorithm_t& algo,
DA_t& da_result,
unsigned int limit=0) {
StutteredConvertor conv(algo, da_result, limit, _detailed_states, _stutter_information);
conv.convert();
}
/**
* Converting an NBA using Algorithm_t into a DA
*/
class StutteredConvertor {
public:
/** Constructor.
* @param algo The Algorithm_t to use
* @param da_result The result automaton
* @param limit Limit the number of states in the result automaton?
* @param detailed_states Generate detailed descriptions?
* @param stutter_information Information about which symbols may be stuttered
*/
StutteredConvertor(Algorithm_t& algo,
DA_t& da_result,
unsigned int limit,
bool detailed_states,
StutterSensitivenessInformation::ptr stutter_information) :
_da_result(da_result),
_limit(limit),
_algo(algo),
_detailed_states(detailed_states),
_stutter_information(stutter_information) {
}
typedef typename DA_t::state_type da_state_t;
typedef typename Algorithm_t::state_t algo_state_t;
typedef typename Algorithm_t::result_t algo_result_t;
typedef TreeWithAcceptance<algo_state_t, typename Acceptance::signature_type> stuttered_state_t;
typedef typename stuttered_state_t::ptr stuttered_state_ptr_t;
typedef std::pair<stuttered_state_ptr_t, da_state_t*> unprocessed_value_t;
typedef std::stack<unprocessed_value_t> unprocessed_stack_t;
/** Convert the NBA to the DA */
void convert() {
const APSet& ap_set=_da_result.getAPSet();
if (_algo.checkEmpty()) {
_da_result.constructEmpty();
return;
}
_algo.prepareAcceptance(_da_result.acceptance());
stuttered_state_ptr_t s_start( new stuttered_state_t( _algo.getStartState() ));
da_state_t* start_state=_da_result.newState();
s_start->generateAcceptance(start_state->acceptance());
if (_detailed_states) {
start_state->setDescription(s_start->toHTML());
}
_state_mapper.add(s_start, start_state);
_da_result.setStartState(start_state);
unprocessed_stack_t unprocessed;
_unprocessed.push(unprocessed_value_t(s_start, start_state));
bool all_insensitive=_stutter_information->isCompletelyInsensitive();
const BitSet& partial_insensitive=
_stutter_information->getPartiallyInsensitiveSymbols();
while (!_unprocessed.empty()) {
unprocessed_value_t top=_unprocessed.top();
_unprocessed.pop();
stuttered_state_ptr_t from=top.first;
da_state_t *da_from=top.second;
for (APSet::element_iterator it_elem=ap_set.all_elements_begin();
it_elem!=ap_set.all_elements_end();
++it_elem) {
APElement elem=*it_elem;
if (!da_from->edges().get(elem)) {
// the edge was not yet calculated...
if (!all_insensitive &&
!partial_insensitive.get(elem)) {
// can't stutter for this symbol, do normal step
algo_state_t next_tree=_algo.delta(from->getTree(), elem)->getState();
stuttered_state_ptr_t next_state=stuttered_state_ptr_t(new stuttered_state_t(next_tree));
add_transition(da_from, next_state, elem);
continue;
}
// normal stuttering...
calc_delta(from, da_from, elem);
if (_limit!=0 && _da_result.size()>_limit) {
THROW_EXCEPTION(LimitReachedException, "");
}
}
}
}
}
private:
// ---- members ----
/** The result DA */
DA_t& _da_result;
/** Limit for the number of states */
unsigned int _limit;
/** The algorithm to use */
Algorithm_t& _algo;
/** Generate detailed descriptions? */
bool _detailed_states;
/** A state mapper for the already generated states */
StateMapper<int, stuttered_state_ptr_t, typename DA_t::state_type> _state_mapper;
/** Information about which symbols are safe to stutter */
StutterSensitivenessInformation::ptr _stutter_information;
/** A stack for the unprocessed states */
unprocessed_stack_t _unprocessed;
// --- private functions ----
/** Add a transition from DA states da_from to stuttered_state to for edge elem.
* If the state does not yet exist in the DA, create it.
* @param da_from the from state in the DA
* @param to the target state
* @param elem the edge label
*/
da_state_t* add_transition(da_state_t* da_from, stuttered_state_ptr_t to, APElement elem) {
da_state_t* da_to=_state_mapper.find(to);
if (!da_to) {
da_to=_da_result.newState();
to->generateAcceptance(da_to->acceptance());
if (_detailed_states) {
da_to->setDescription(to->toHTML());
}
_state_mapper.add(to, da_to);
_unprocessed.push(unprocessed_value_t(to, da_to));
}
#ifdef STUTTERED_VERBOSE
std::cerr << da_from->getName() << " -> " << da_to->getName() << std::endl;
#endif
da_from->edges().set(elem, da_to);
return da_to;
}
typedef std::vector<algo_state_t> intermediate_state_vector_t;
/**
* Calculate Acceptance for RabinAcceptance conditon
*/
bool calculate_acceptance(intermediate_state_vector_t& state_vector,
unsigned int cycle_point,
RabinAcceptance::RabinSignature* prefix_signature,
RabinAcceptance::RabinSignature* cycle_signature) {
unsigned int states=state_vector.size();
state_vector[cycle_point]->generateAcceptance(*cycle_signature); // start
for (unsigned int i=cycle_point+1;i<states;i++) {
cycle_signature->maxMerge(state_vector[i]->generateAcceptance());
}
if (prefix_signature) {
*prefix_signature=*cycle_signature;
for (unsigned int i=1;i<cycle_point;i++) {
prefix_signature->maxMerge(state_vector[i]->generateAcceptance());
}
}
if (prefix_signature) {
// check if prefix can be ommited
RabinAcceptance::RabinSignature p0_signature(prefix_signature->getSize());
state_vector[0]->generateAcceptance(p0_signature);
for (unsigned int j=0;j<prefix_signature->getSize();j++) {
if (prefix_signature->getColor(j) <= cycle_signature->getColor(j) ||
prefix_signature->getColor(j) <= p0_signature.getColor(j)) {
// acceptance pair j is ok
;
} else {
return false;
}
}
// all acceptance pairs are ok, return true
return true;
}
return false;
}
/** Store a prefix and a cycle state */
struct prefix_and_cycle_state_t {
prefix_and_cycle_state_t(stuttered_state_ptr_t prefix_,
stuttered_state_ptr_t cycle_) :
prefix_state(prefix_), cycle_state(cycle_) {}
stuttered_state_ptr_t prefix_state;
stuttered_state_ptr_t cycle_state;
};
/** Calculate the prefix and the cycle state */
prefix_and_cycle_state_t
calculate_prefix_and_cycle_state(intermediate_state_vector_t& state_vector,
unsigned int cycle_point) {
stuttered_state_ptr_t prefix_state, cycle_state;
unsigned states=state_vector.size();
unsigned int smallest=cycle_point;
for (unsigned int i=cycle_point+1;i<states;i++) {
if (*state_vector[i] < *state_vector[smallest]) {
smallest=i;
}
}
#ifdef STUTTERED_VERBOSE
std::cerr << "Smallest: " << smallest << std::endl;
#endif
cycle_state=stuttered_state_ptr_t(new stuttered_state_t(state_vector[smallest]));
if (! (cycle_point==0 || cycle_point==1)) {
prefix_state=
stuttered_state_ptr_t(new stuttered_state_t(state_vector[smallest]));
}
typename Acceptance::signature_type* signature_prefix=(typename Acceptance::signature_type*)NULL;
if (prefix_state) {
signature_prefix=&( prefix_state->getSignature() );
}
typename Acceptance::signature_type* signature_cycle=&( cycle_state->getSignature() );
bool omit_prefix=calculate_acceptance(state_vector,
cycle_point,
signature_prefix,
signature_cycle);
if (omit_prefix) {
prefix_state.reset();
}
if (_detailed_states) {
std::ostringstream prefix_description;
std::ostringstream cycle_description;
if (prefix_state) {
prefix_description << "<TABLE><TR><TD>Prefix</TD><TD>Cycle (" << (smallest-cycle_point) <<")</TD></TR>"
<< "<TR><TD>";
prefix_description << "<TABLE><TR>";
for (unsigned int i=1;i<cycle_point;i++) {
prefix_description << "<TD>" << state_vector[i]->toHTML() << "</TD>";
}
prefix_description << "</TR></TABLE></TD>";
}
cycle_description << "<TD><TABLE><TR>";
for (unsigned int i=cycle_point; i<state_vector.size();i++) {
cycle_description << "<TD>";
cycle_description << state_vector[i]->toHTML();
cycle_description << "</TD>";
}
cycle_description << "</TR></TABLE></TD>";
if (prefix_state) {
prefix_description << cycle_description.str();
prefix_description << "</TR></TABLE>";
prefix_state->setDescription(prefix_description.str());
}
cycle_description << "</TR></TABLE>";
cycle_state->setDescription("<TABLE><TR><TD>Cycle ("+
boost::lexical_cast<std::string>(smallest-cycle_point) +
")</TD></TR><TR>" + cycle_description.str());
}
return prefix_and_cycle_state_t(prefix_state, cycle_state);
}
/** Calculate and add transitions to the successor state.
* @param from the source stuttered_state
* @param da_from the source DA state
* @param elem the edge label
*/
void calc_delta(stuttered_state_ptr_t from, da_state_t* da_from, APElement elem) {
typedef myHashMap<algo_state_t,
unsigned int,
ptr_hash<algo_state_t>,
PtrComparator<algo_state_t> > intermediate_state_map_t;
intermediate_state_map_t state_map;
intermediate_state_vector_t state_vector;
algo_state_t start_tree=from->getTree();
state_map[start_tree]=0;
state_vector.push_back(start_tree);
#ifdef STUTTERED_VERBOSE
std::cerr << "Calculate from state [" << da_from->getName() << "], "<< (unsigned int) elem << ":" << std::endl;
std::cerr << start_tree->toString() << std::endl;
#endif
algo_state_t cur_tree=start_tree;
while (true) {
algo_state_t next_tree=_algo.delta(cur_tree, elem)->getState();
typename intermediate_state_map_t::iterator it;
it=state_map.find(next_tree);
if (it==state_map.end()) {
// tree doesn't yet exist...
// add tree
state_map[next_tree]=state_vector.size();
state_vector.push_back(next_tree);
cur_tree=next_tree;
continue;
} else {
// found the cycle!
unsigned int cycle_point=(*it).second;
#ifdef STUTTERED_VERBOSE
std::cerr << "-----------------------\n";
for (unsigned int i=0;i<state_vector.size();i++) {
std::cerr << "[" << i << "] ";
if (cycle_point==i) {
std::cerr << "* ";
}
std::cerr << "\n" << state_vector[i]->toString() << std::endl;
}
std::cerr << "-----------------------\n";
#endif
prefix_and_cycle_state_t pac=
calculate_prefix_and_cycle_state(state_vector, cycle_point);
da_state_t* da_prefix;
da_state_t* da_cycle;
if (pac.prefix_state &&
!(*pac.prefix_state==*pac.cycle_state)) {
da_prefix=add_transition(da_from, pac.prefix_state, elem);
da_cycle=add_transition(da_prefix, pac.cycle_state, elem);
} else {
da_cycle=add_transition(da_from, pac.cycle_state, elem);
}
da_cycle->edges().set(elem, da_cycle);
return;
}
}
}
};
};
#endif