You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
568 lines
17 KiB
568 lines
17 KiB
/*
|
|
* 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 std::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
|