Browse Source

Some minor changes, still doesn't compile.

Former-commit-id: cfc613fd8e
main
dehnert 11 years ago
parent
commit
94902388c7
  1. 2
      CMakeLists.txt
  2. 49
      src/storage/Block.cpp
  3. 57
      src/storage/StateBlock.cpp
  4. 13
      src/storage/StateBlock.h
  5. 15
      src/storage/StronglyConnectedComponent.h
  6. 4
      src/storage/StronglyConnectedComponentDecomposition.cpp
  7. 3
      src/storage/StronglyConnectedComponentDecomposition.h
  8. 13
      src/storage/sparse/StateType.h

2
CMakeLists.txt

@ -254,6 +254,7 @@ file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SO
file(GLOB_RECURSE STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp)
file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp)
# Test Sources
# Note that the tests also need the source files, except for the main file
@ -287,6 +288,7 @@ source_group(storage FILES ${STORM_STORAGE_FILES})
source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES})
source_group(storage\\expressions FILES ${STORM_STORAGE_EXPRESSIONS_FILES})
source_group(storage\\prism FILES ${STORM_STORAGE_PRISM_FILES})
source_group(storage\\sparse FILES ${STORM_STORAGE_SPARSE_FILES})
source_group(utility FILES ${STORM_UTILITY_FILES})
source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES})
source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES})

49
src/storage/Block.cpp

@ -1,49 +0,0 @@
#include "src/storage/Block.h"
namespace storm {
namespace storage {
Block::iterator Block::begin() {
return states.begin();
}
Block::const_iterator Block::begin() const {
return states.begin();
}
StronglyConnectedComponent::iterator Block::end() {
return states.end();
}
StronglyConnectedComponent::const_iterator Block::end() const {
return states.end();
}
std::size_t Block::size() const {
return states.size();
}
void Block::insert(value_type const& state) {
states.insert(state);
}
void Block::erase(value_type const& state) {
states.erase(state);
}
bool Block::containsState(value_type const& state) const {
return this->states.find(state) != this->states.end();
}
std::ostream& operator<<(std::ostream& out, StateBlock const& block) {
out << "{";
for (auto const& element : block) {
out << element << ", ";
}
out << "}";
return out;
}
// Explicitly instantiate template.
template Block<>;
}
}

57
src/storage/StateBlock.cpp

@ -0,0 +1,57 @@
#include "src/storage/StateBlock.h"
namespace storm {
namespace storage {
template <typename ContainerType>
typename StateBlock<ContainerType>::iterator StateBlock<ContainerType>::begin() {
return states.begin();
}
template <typename ContainerType>
typename StateBlock<ContainerType>::const_iterator StateBlock<ContainerType>::begin() const {
return states.begin();
}
template <typename ContainerType>
typename StateBlock<ContainerType>::iterator StateBlock<ContainerType>::end() {
return states.end();
}
template <typename ContainerType>
typename StateBlock<ContainerType>::const_iterator StateBlock<ContainerType>::end() const {
return states.end();
}
template <typename ContainerType>
std::size_t StateBlock<ContainerType>::size() const {
return states.size();
}
template <typename ContainerType>
void StateBlock<ContainerType>::insert(value_type const& state) {
states.insert(state);
}
template <typename ContainerType>
void StateBlock<ContainerType>::erase(value_type const& state) {
states.erase(state);
}
template <typename ContainerType>
bool StateBlock<ContainerType>::containsState(value_type const& state) const {
return this->states.find(state) != this->states.end();
}
std::ostream& operator<<(std::ostream& out, FlatSetStateContainer const& block) {
out << "{";
for (auto const& element : block) {
out << element << ", ";
}
out << "}";
return out;
}
// Explicitly instantiate template.
template Block<FlatSetStateContainer>;
}
}

13
src/storage/Block.h → src/storage/StateBlock.h

@ -3,10 +3,13 @@
#include <boost/container/flat_set.hpp>
#include "src/storage/sparse/StateType.h"
namespace storm {
namespace storage {
typedef boost::container::flat_set<uint_fast64_t> FlatSetStateContainer;
// Typedef the most common state container
typedef boost::container::flat_set<sparse::state_type> FlatSetStateContainer;
/*!
* Writes a string representation of the state block to the given output stream.
@ -17,10 +20,12 @@ namespace storm {
*/
std::ostream& operator<<(std::ostream& out, FlatSetStateContainer const& block);
class Block {
template <typename ContainerType = FlatSetStateContainer>
class StateBlock {
public:
typedef ContainerType container_type;
typedef typename container_type::value_type value_type;
static_assert(std::is_same<value_type, sparse::state_type>::value, "Illegal value type of container.");
typedef typename container_type::iterator iterator;
typedef typename container_type::const_iterator const_iterator;
@ -86,6 +91,10 @@ namespace storm {
* @return True iff the SCC is empty.
*/
bool empty() const;
private:
// The container that holds the states.
ContainerType states;
};
}
}

15
src/storage/StronglyConnectedComponent.h

@ -1,25 +1,17 @@
#ifndef STORM_STORAGE_STRONGLYCONNECTEDCOMPONENT_H_
#define STORM_STORAGE_STRONGLYCONNECTEDCOMPONENT_H_
#include "src/storage/Block.h"
#include "src/storage/StateBlock.h"
#include "src/storage/Decomposition.h"
namespace storm {
namespace storage {
typedef FlatSetStateContainer SccBlock;
/*!
* This class represents a strongly connected component, i.e., a set of states such that every state can reach
* every other state.
*/
class StronglyConnectedComponent : public Block<SccBlock> {
public:
typedef SccBlock block_type;
typedef block_type::value_type value_type;
typedef block_type::iterator iterator;
typedef block_type::const_iterator const_iterator;
class StronglyConnectedComponent : public StateBlock<FlatSetStateContainer> {
/*!
* Creates an empty strongly connected component.
*/
@ -42,9 +34,6 @@ namespace storm {
private:
// Stores whether this SCC is trivial.
bool isTrivialScc;
// The states in this SCC.
block_type states;
};
}

4
src/storage/StronglyConnectedComponentDecomposition.cpp

@ -14,7 +14,8 @@ namespace storm {
}
template <typename ValueType>
StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) {
template <typename ContainerType>
StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock<ContainerType> const& block, bool dropNaiveSccs, bool onlyBottomSccs) {
storm::storage::BitVector subsystem(model.getNumberOfStates(), block.begin(), block.end());
performSccDecomposition(model.getTransitionMatrix(), subsystem, dropNaiveSccs, onlyBottomSccs);
}
@ -203,5 +204,6 @@ namespace storm {
// Explicitly instantiate the SCC decomposition.
template class StronglyConnectedComponentDecomposition<double>;
template StronglyConnectedComponentDecomposition<double>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<double> const& model, StateBlock<FlatSetStateContainer> const& block, bool dropNaiveSccs, bool onlyBottomSccs);
} // namespace storage
} // namespace storm

3
src/storage/StronglyConnectedComponentDecomposition.h

@ -46,7 +46,8 @@ namespace storm {
* @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of
* leaving the SCC), are kept.
*/
StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, Block const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
template<typename ContainerType>
StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock<ContainerType> const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
/*
* Creates an SCC decomposition of the given subsystem in the given model.

13
src/storage/sparse/StateType.h

@ -0,0 +1,13 @@
#ifndef STORM_STORAGE_SPARSE_STATETYPE_H_
#define STORM_STORAGE_SPARSE_STATETYPE_H_
namespace storm {
namespace storage {
namespace sparse {
typedef uint_fast64_t state_type;
}
}
}
#endif /* STORM_STORAGE_SPARSE_STATETYPE_H_ */
Loading…
Cancel
Save