sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge master into parametricSystems. 

Former-commit-id: 7097b5a846
main
dehnert 10 years ago
parent
582b4a5862 d3fc2d8fbf
commit
79c9f2c662
7 changed files with 174 additions and 147 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 17
      CMakeLists.txt
  2. 228
      src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
  3. 31
      src/storage/DeterministicModelStrongBisimulationDecomposition.h
  4. 4
      src/storage/StronglyConnectedComponent.cpp
  5. 2
      src/storage/StronglyConnectedComponent.h
  6. 18
      src/utility/ConstantsComparator.cpp
  7. 21
      src/utility/macros.h

17
CMakeLists.txt
View File

@ -103,11 +103,9 @@ if(CMAKE_COMPILER_IS_GNUCC)
set(STORM_COMPILED_BY "GCC")
# Set standard flags for GCC
set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic -DBOOST_RESULT_OF_USE_TR1")
# -Werror is atm removed as this gave some problems with existing code
# May be re-set later
# (Thomas Heinemann, 2012-12-21)
add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic")
# Turn on popcnt instruction if desired (yes by default)
if (STORM_USE_POPCNT)
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt")
@ -125,6 +123,8 @@ elseif(MSVC)
add_definitions(/D_VARIADIC_MAX=10)
# Windows.h breaks GMM in gmm_except.h because of its macro definition for min and max
add_definitions(/DNOMINMAX)
# required for using boost's transform iterator
add_definitions(/DBOOST_RESULT_OF_USE_DECLTYPE)
# since nobody cares at the moment
add_definitions(/wd4250)
@ -153,10 +153,9 @@ else(CLANG)
set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LIBRARY "libc++")
endif()
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE -ftemplate-depth=1024")
set (CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -g")
add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE)
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-unused-variable -ftemplate-depth=1024")
# Turn on popcnt instruction if desired (yes by default)
if (STORM_USE_POPCNT)
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt")

228
src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
View File

@ -4,6 +4,7 @@
#include <unordered_map>
#include <chrono>
#include <iomanip>
#include <boost/iterator/transform_iterator.hpp>
#include "src/utility/graph.h"
#include "src/exceptions/IllegalFunctionCallException.h"
@ -11,6 +12,11 @@
namespace storm {
namespace storage {
namespace {
static std::chrono::high_resolution_clock::duration probabilityRefineTime;
static std::chrono::high_resolution_clock::duration qualitativeRefineTime;
}
template<typename ValueType>
std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::blockId = 0;
@ -30,15 +36,15 @@ namespace storm {
std::cout << "begin: " << this->begin << " and end: " << this->end << " (number of states: " << this->getNumberOfStates() << ")" << std::endl;
std::cout << "states:" << std::endl;
for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) {
std::cout << partition.states[index] << " ";
std::cout << partition.statesAndValues[index].first << " ";
}
std::cout << std::endl << "original: " << std::endl;
for (storm::storage::sparse::state_type index = this->getOriginalBegin(); index < this->end; ++index) {
std::cout << partition.states[index] << " ";
std::cout << partition.statesAndValues[index].first << " ";
}
std::cout << std::endl << "values:" << std::endl;
for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) {
std::cout << std::setprecision(3) << partition.values[index] << " ";
std::cout << std::setprecision(3) << partition.statesAndValues[index].second << " ";
}
std::cout << std::endl;
}
@ -245,28 +251,28 @@ namespace storm {
}
template<typename ValueType>
DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates) {
// Create the block and give it an iterator to itself.
typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr);
it->setIterator(it);
// Set up the different parts of the internal structure.
for (storm::storage::sparse::state_type state = 0; state < numberOfStates; ++state) {
states[state] = state;
statesAndValues[state] = std::make_pair(state, storm::utility::zero<ValueType>());
positions[state] = state;
stateToBlockMapping[state] = &blocks.back();
}
}
template<typename ValueType>
DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates) {
typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr);
Block& firstBlock = *firstIt;
firstBlock.setIterator(firstIt);
storm::storage::sparse::state_type position = 0;
for (auto state : prob0States) {
states[position] = state;
statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
positions[state] = position;
stateToBlockMapping[state] = &firstBlock;
++position;
@ -278,7 +284,7 @@ namespace storm {
secondBlock.setIterator(secondIt);
for (auto state : prob1States) {
states[position] = state;
statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
positions[state] = position;
stateToBlockMapping[state] = &secondBlock;
++position;
@ -291,7 +297,7 @@ namespace storm {
storm::storage::BitVector otherStates = ~(prob0States | prob1States);
for (auto state : otherStates) {
states[position] = state;
statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
positions[state] = position;
stateToBlockMapping[state] = &thirdBlock;
++position;
@ -300,18 +306,16 @@ namespace storm {
template<typename ValueType>
void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
std::swap(this->states[this->positions[state1]], this->states[this->positions[state2]]);
std::swap(this->values[this->positions[state1]], this->values[this->positions[state2]]);
std::swap(this->statesAndValues[this->positions[state1]], this->statesAndValues[this->positions[state2]]);
std::swap(this->positions[state1], this->positions[state2]);
}
template<typename ValueType>
void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
storm::storage::sparse::state_type state1 = this->states[position1];
storm::storage::sparse::state_type state2 = this->states[position2];
storm::storage::sparse::state_type state1 = this->statesAndValues[position1].first;
storm::storage::sparse::state_type state2 = this->statesAndValues[position2].first;
std::swap(this->states[position1], this->states[position2]);
std::swap(this->values[position1], this->values[position2]);
std::swap(this->statesAndValues[position1], this->statesAndValues[position2]);
this->positions[state1] = position2;
this->positions[state2] = position1;
@ -329,38 +333,33 @@ namespace storm {
template<typename ValueType>
storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getState(storm::storage::sparse::state_type position) const {
return this->states[position];
return this->statesAndValues[position].first;
}
template<typename ValueType>
ValueType const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getValue(storm::storage::sparse::state_type state) const {
return this->values[this->positions[state]];
return this->statesAndValues[this->positions[state]].second;
}
template<typename ValueType>
ValueType const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const {
return this->values[position];
return this->statesAndValues[position].second;
}
template<typename ValueType>
void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) {
this->values[this->positions[state]] = value;
}
template<typename ValueType>
std::vector<ValueType>& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getValues() {
return this->values;
this->statesAndValues[this->positions[state]].second = value;
}
template<typename ValueType>
void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
this->values[this->positions[state]] += value;
this->statesAndValues[this->positions[state]].second += value;
}
template<typename ValueType>
void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::updateBlockMapping(Block& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator last) {
void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::updateBlockMapping(Block& block, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
for (; first != last; ++first) {
this->stateToBlockMapping[*first] = &block;
this->stateToBlockMapping[first->first] = &block;
}
}
@ -380,56 +379,61 @@ namespace storm {
}
template<typename ValueType>
std::vector<storm::storage::sparse::state_type>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBeginOfStates(Block const& block) {
return this->states.begin() + block.getBegin();
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) {
return this->statesAndValues.begin() + block.getBegin();
}
template<typename ValueType>
std::vector<storm::storage::sparse::state_type>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEndOfStates(Block const& block) {
return this->states.begin() + block.getEnd();
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEnd(Block const& block) {
return this->statesAndValues.begin() + block.getEnd();
}
template<typename ValueType>
std::vector<storm::storage::sparse::state_type>::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBeginOfStates(Block const& block) const {
return this->states.begin() + block.getBegin();
}
template<typename ValueType>
std::vector<storm::storage::sparse::state_type>::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEndOfStates(Block const& block) const {
return this->states.begin() + block.getEnd();
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) const {
return this->statesAndValues.begin() + block.getBegin();
}
template<typename ValueType>
typename std::vector<ValueType>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBeginOfValues(Block const& block) {
return this->values.begin() + block.getBegin();
}
template<typename ValueType>
typename std::vector<ValueType>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEndOfValues(Block const& block) {
return this->values.begin() + block.getEnd();
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEnd(Block const& block) const {
return this->statesAndValues.begin() + block.getEnd();
}
template<typename ValueType>
typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
// FIXME: this could be improved by splitting off the smaller of the two resulting blocks.
// In case one of the resulting blocks would be empty, we simply return the current block and do not create
// a new one.
if (position == block.getBegin() || position == block.getEnd()) {
return block;
}
// We only split off the smaller of the two resulting blocks so we don't have to update large parts of the
// block mapping.
bool insertAfterCurrent = false;
if ((block.getBegin() + position) > ((block.getEnd() - block.getBegin()) / 2)) {
// If the splitting position is far in the back, we create the new block after the one we are splitting.
insertAfterCurrent = true;
}
// Actually create the new block and insert it at the correct position.
typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr());
typename std::list<Block>::iterator selfIt;
if (insertAfterCurrent) {
selfIt = this->blocks.emplace(block.hasNextBlock() ? block.getNextIterator() : this->blocks.end(), position, block.getEnd(), &block, block.getNextBlockPointer(), block.getLabelPtr());
} else {
selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr());
}
selfIt->setIterator(selfIt);
Block& newBlock = *selfIt;
// Make the current block end at the given position.
block.setBegin(position);
// Resize the current block appropriately.
if (insertAfterCurrent) {
block.setEnd(position);
} else {
block.setBegin(position);
}
// Update the mapping of the states in the newly created block.
for (auto it = this->getBeginOfStates(newBlock), ite = this->getEndOfStates(newBlock); it != ite; ++it) {
stateToBlockMapping[*it] = &newBlock;
for (auto it = this->getBegin(newBlock), ite = this->getEnd(newBlock); it != ite; ++it) {
stateToBlockMapping[it->first] = &newBlock;
}
return newBlock;
@ -451,8 +455,8 @@ namespace storm {
newBlock.setIterator(it);
// Update the mapping of the states in the newly created block.
for (auto it = this->getBeginOfStates(newBlock), ite = this->getEndOfStates(newBlock); it != ite; ++it) {
stateToBlockMapping[*it] = &newBlock;
for (auto it = this->getBegin(newBlock), ite = this->getEnd(newBlock); it != ite; ++it) {
stateToBlockMapping[it->first] = &newBlock;
}
return *it;
@ -464,20 +468,20 @@ namespace storm {
Block& block = *blockIterator;
// Sort the range of the block such that all states that have the label are moved to the front.
std::sort(this->getBeginOfStates(block), this->getEndOfStates(block), [&statesWithLabel] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statesWithLabel.get(a) && !statesWithLabel.get(b); } );
std::sort(this->getBegin(block), this->getEnd(block), [&statesWithLabel] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return statesWithLabel.get(a.first) && !statesWithLabel.get(b.first); } );
// Update the positions vector.
storm::storage::sparse::state_type position = block.getBegin();
for (auto stateIt = this->getBeginOfStates(block), stateIte = this->getEndOfStates(block); stateIt != stateIte; ++stateIt, ++position) {
this->positions[*stateIt] = position;
for (auto stateIt = this->getBegin(block), stateIte = this->getEnd(block); stateIt != stateIte; ++stateIt, ++position) {
this->positions[stateIt->first] = position;
}
// Now we can find the first position in the block that does not have the label and create new blocks.
std::vector<storm::storage::sparse::state_type>::iterator it = std::find_if(this->getBeginOfStates(block), this->getEndOfStates(block), [&] (storm::storage::sparse::state_type const& a) { return !statesWithLabel.get(a); });
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator it = std::find_if(this->getBegin(block), this->getEnd(block), [&] (std::pair<storm::storage::sparse::state_type, ValueType> const& a) { return !statesWithLabel.get(a.first); });
// If not all the states agreed on the validity of the label, we need to split the block.
if (it != this->getBeginOfStates(block) && it != this->getEndOfStates(block)) {
auto cutPoint = std::distance(this->states.begin(), it);
if (it != this->getBegin(block) && it != this->getEnd(block)) {
auto cutPoint = std::distance(this->statesAndValues.begin(), it);
this->splitBlock(block, cutPoint);
} else {
// Otherwise, we simply proceed to the next block.
@ -492,8 +496,8 @@ namespace storm {
}
template<typename ValueType>
std::vector<storm::storage::sparse::state_type>& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getStates() {
return this->states;
std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getStatesAndValues() {
return this->statesAndValues;
}
template<typename ValueType>
@ -504,14 +508,14 @@ namespace storm {
template<typename ValueType>
bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::check() const {
for (uint_fast64_t state = 0; state < this->positions.size(); ++state) {
if (this->states[this->positions[state]] != state) {
if (this->statesAndValues[this->positions[state]].first != state) {
assert(false);
}
}
for (auto const& block : this->blocks) {
assert(block.check());
for (auto stateIt = this->getBeginOfStates(block), stateIte = this->getEndOfStates(block); stateIt != stateIte; ++stateIt) {
if (this->stateToBlockMapping[*stateIt] != &block) {
for (auto stateIt = this->getBegin(block), stateIte = this->getEnd(block); stateIt != stateIte; ++stateIt) {
if (this->stateToBlockMapping[stateIt->first] != &block) {
assert(false);
}
}
@ -525,8 +529,8 @@ namespace storm {
block.print(*this);
}
std::cout << "states in partition" << std::endl;
for (auto const& state : states) {
std::cout << state << " ";
for (auto const& stateValue : statesAndValues) {
std::cout << stateValue.first << " ";
}
std::cout << std::endl << "positions: " << std::endl;
for (auto const& index : positions) {
@ -695,75 +699,94 @@ namespace storm {
template<typename ModelType>
void DeterministicModelStrongBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, bool buildQuotient) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// Initially, all blocks are potential splitter, so we insert them in the splitterQueue.
std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now();
std::deque<Block*> splitterQueue;
std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); });
// Then perform the actual splitting until there are no more splitters.
while (!splitterQueue.empty()) {
std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
refinePartition(backwardTransitions, *splitterQueue.front(), partition, splitterQueue);
splitterQueue.pop_front();
}
std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart;
// Now move the states from the internal partition into their final place in the decomposition. We do so in
// a way that maintains the block IDs as indices.
std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now();
this->blocks.resize(partition.size());
for (auto const& block : partition.getBlocks()) {
// We need to sort the states to allow for rapid construction of the blocks.
std::sort(partition.getBeginOfStates(block), partition.getEndOfStates(block));
this->blocks[block.getId()] = block_type(partition.getBeginOfStates(block), partition.getEndOfStates(block), true);
std::sort(partition.getBegin(block), partition.getEnd(block), [] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return a.first < b.first; });
// Convert the state-value-pairs to states only.
auto lambda = [] (std::pair<storm::storage::sparse::state_type, ValueType> const& a) -> storm::storage::sparse::state_type { return a.first; };
this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), lambda), boost::make_transform_iterator(partition.getEnd(block), lambda), true);
}
// If we are required to build the quotient model, do so now.
if (buildQuotient) {
this->buildQuotient(model, partition);
}
std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart;
std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
if (storm::settings::generalSettings().isShowStatisticsSet()) {
std::cout << "Computed bisimulation quotient in " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms." << std::endl;
std::cout << std::endl;
std::cout << "Time breakdown:" << std::endl;
std::cout << " * time for partitioning: " << std::chrono::duration_cast<std::chrono::milliseconds>(refinementTime).count() << "ms" << std::endl;
std::cout << " * time for qualitative refinement: " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeRefineTime).count() << "ms" << std::endl;
std::cout << " * time for probability refinement: " << std::chrono::duration_cast<std::chrono::milliseconds>(probabilityRefineTime).count() << "ms" << std::endl;
std::cout << " * time for extraction: " << std::chrono::duration_cast<std::chrono::milliseconds>(extractionTime).count() << "ms" << std::endl;
std::cout << "------------------------------------------" << std::endl;
std::cout << " * total time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms" << std::endl;
std::cout << std::endl;
}
}
template<typename ValueType>
void DeterministicModelStrongBisimulationDecomposition<ValueType>::refineBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue) {
std::chrono::high_resolution_clock::time_point probabilityRefineStart = std::chrono::high_resolution_clock::now();
// First, we simplify all the values. For most types this does not change anything, but for rational
// functions, this achieves a canonicity that is used for sorting the rational functions later.
for (auto probabilityIt = partition.getBeginOfValues(block), probabilityIte = partition.getEndOfValues(block); probabilityIt != probabilityIte; ++probabilityIt) {
storm::utility::simplify(*probabilityIt);
for (auto probabilityIt = partition.getBegin(block), probabilityIte = partition.getEnd(block); probabilityIt != probabilityIte; ++probabilityIt) {
storm::utility::simplify(probabilityIt->second);
}
// Sort the states in the block based on their probabilities.
std::sort(partition.getBeginOfStates(block), partition.getEndOfStates(block), [&partition] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return partition.getValue(a) < partition.getValue(b); } );
// FIXME: This can probably be done more efficiently.
std::sort(partition.getBeginOfValues(block), partition.getEndOfValues(block));
std::sort(partition.getBegin(block), partition.getEnd(block), [] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return a.second < b.second; } );
// Update the positions vector.
storm::storage::sparse::state_type position = block.getBegin();
for (auto stateIt = partition.getBeginOfStates(block), stateIte = partition.getEndOfStates(block); stateIt != stateIte; ++stateIt, ++position) {
partition.setPosition(*stateIt, position);
for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) {
partition.setPosition(stateIt->first, position);
}
// Finally, we need to scan the ranges of states that agree on the probability.
storm::storage::sparse::state_type beginIndex = block.getBegin();
storm::storage::sparse::state_type currentIndex = beginIndex;
storm::storage::sparse::state_type endIndex = block.getEnd();
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block);
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1;
storm::storage::sparse::state_type currentIndex = block.getBegin();
// Perform a sanity check that the smallest probability is still not zero.
STORM_LOG_ASSERT(!comparator.isZero(begin->second), "Probability to go to splitter must not be zero.");
// Now we can check whether the block needs to be split, which is the case iff the probabilities for the
// first and the last state are different.
while (!comparator.isEqual(partition.getValueAtPosition(beginIndex), partition.getValueAtPosition(endIndex - 1))) {
while (!comparator.isEqual(begin->second, end->second)) {
// Now we scan for the first state in the block that disagrees on the probability value.
// Note that we do not have to check currentIndex for staying within bounds, because we know the matching
// state is within bounds.
ValueType const& currentValue = partition.getValueAtPosition(beginIndex);
ValueType const& currentValue = begin->second;
typename std::vector<ValueType>::const_iterator valueIterator = partition.getValues().begin() + beginIndex + 1;
++begin;
++currentIndex;
while (currentIndex < endIndex && comparator.isEqual(*valueIterator, currentValue)) {
++valueIterator;
while (begin != end && comparator.isEqual(begin->second, currentValue)) {
++begin;
++currentIndex;
}
@ -773,12 +796,14 @@ namespace storm {
splitterQueue.push_back(&newBlock);
newBlock.markAsSplitter();
}
beginIndex = currentIndex;
}
for (auto index = currentIndex; index < endIndex - 1; ++index) {
STORM_LOG_ASSERT(comparator.isEqual(partition.getValueAtPosition(index + 1), partition.getValueAtPosition(index + 1)), "Expected equal probabilities after sorting block, but got '" << partition.getValueAtPosition(index) << "' and '" << partition.getValueAtPosition(index + 1) << "'.");
for (auto it = partition.getBegin(newBlock), ite = partition.getEnd(newBlock) - 1; it != ite; ++it) {
STORM_LOG_ASSERT(comparator.isEqual(partition.getValueAtPosition(it->first), partition.getValueAtPosition((it + 1)->first)), "Expected equal probabilities after sorting block, but got '" << partition.getValueAtPosition(it->first) << "' and '" << partition.getValueAtPosition((it + 1)->first) << "'.");
}
}
probabilityRefineTime += std::chrono::high_resolution_clock::now() - probabilityRefineStart;
}
template<typename ValueType>
@ -786,9 +811,10 @@ namespace storm {
std::list<Block*> predecessorBlocks;
// Iterate over all states of the splitter and check its predecessors.
std::chrono::high_resolution_clock::time_point qualitativeRefineStart = std::chrono::high_resolution_clock::now();
storm::storage::sparse::state_type currentPosition = splitter.getBegin();
for (auto stateIterator = partition.getBeginOfStates(splitter), stateIte = partition.getEndOfStates(splitter); stateIterator != stateIte; ++stateIterator, ++currentPosition) {
storm::storage::sparse::state_type currentState = *stateIterator;
for (auto stateIterator = partition.getBegin(splitter), stateIte = partition.getEnd(splitter); stateIterator != stateIte; ++stateIterator, ++currentPosition) {
storm::storage::sparse::state_type currentState = stateIterator->first;
uint_fast64_t elementsToSkip = 0;
for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
@ -852,8 +878,8 @@ namespace storm {
}
// Now we can traverse the list of states of the splitter whose predecessors we have not yet explored.
for (auto stateIterator = partition.getStates().begin() + splitter.getOriginalBegin(), stateIte = partition.getStates().begin() + splitter.getMarkedPosition(); stateIterator != stateIte; ++stateIterator) {
storm::storage::sparse::state_type currentState = *stateIterator;
for (auto stateIterator = partition.getStatesAndValues().begin() + splitter.getOriginalBegin(), stateIte = partition.getStatesAndValues().begin() + splitter.getMarkedPosition(); stateIterator != stateIte; ++stateIterator) {
storm::storage::sparse::state_type currentState = stateIterator->first;
for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
@ -905,6 +931,8 @@ namespace storm {
}
}
qualitativeRefineTime += std::chrono::high_resolution_clock::now() - qualitativeRefineStart;
// Finally, we walk through the blocks that have a transition to the splitter and split them using
// probabilistic information.
for (auto blockPtr : blocksToSplit) {

31
src/storage/DeterministicModelStrongBisimulationDecomposition.h
View File

@ -76,6 +76,7 @@ namespace storm {
typedef typename std::list<Block>::iterator iterator;
typedef typename std::list<Block>::const_iterator const_iterator;
// Creates a new block with the given begin and end.
Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr<std::string> const& label = nullptr);
// Prints the block.
@ -284,30 +285,21 @@ namespace storm {
// Retrieves the blocks of the partition.
std::list<Block>& getBlocks();
// Retrieves the vector of all the states.
std::vector<storm::storage::sparse::state_type>& getStates();
// Checks the partition for internal consistency.
bool check() const;
// Returns an iterator to the beginning of the states of the given block.
std::vector<storm::storage::sparse::state_type>::iterator getBeginOfStates(Block const& block);
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator getBegin(Block const& block);
// Returns an iterator to the beginning of the states of the given block.
std::vector<storm::storage::sparse::state_type>::iterator getEndOfStates(Block const& block);
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator getEnd(Block const& block);
// Returns an iterator to the beginning of the states of the given block.
std::vector<storm::storage::sparse::state_type>::const_iterator getBeginOfStates(Block const& block) const;
// Returns an iterator to the beginning of the states of the given block.
std::vector<storm::storage::sparse::state_type>::const_iterator getEndOfStates(Block const& block) const;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator getBegin(Block const& block) const;
// Returns an iterator to the beginning of the states of the given block.
typename std::vector<ValueType>::iterator getBeginOfValues(Block const& block);
// Returns an iterator to the beginning of the states of the given block.
typename std::vector<ValueType>::iterator getEndOfValues(Block const& block);
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator getEnd(Block const& block) const;
// Swaps the positions of the two given states.
void swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2);
@ -340,13 +332,13 @@ namespace storm {
void setValue(storm::storage::sparse::state_type state, ValueType value);
// Retrieves the vector with the probabilities going into the current splitter.
std::vector<ValueType>& getValues();
std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>& getStatesAndValues();
// Increases the value for the given state by the specified amount.
void increaseValue(storm::storage::sparse::state_type state, ValueType value);
// Updates the block mapping for the given range of states to the specified block.
void updateBlockMapping(Block& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator end);
void updateBlockMapping(Block& block, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator end);
// Retrieves the first block of the partition.
Block& getFirstBlock();
@ -357,15 +349,12 @@ namespace storm {
// A mapping of states to their blocks.
std::vector<Block*> stateToBlockMapping;
// A vector containing all the states. It is ordered in a special way such that the blocks only need to
// define their start/end indices.
std::vector<storm::storage::sparse::state_type> states;
// A vector containing all the states and their values. It is ordered in a special way such that the
// blocks only need to define their start/end indices.
std::vector<std::pair<storm::storage::sparse::state_type, ValueType>> statesAndValues;
// This vector keeps track of the position of each state in the state vector.
std::vector<storm::storage::sparse::state_type> positions;
// This vector stores the probabilities of going to the current splitter.
std::vector<ValueType> values;
};
/*!

4
src/storage/StronglyConnectedComponent.cpp
View File

@ -2,6 +2,10 @@
namespace storm {
namespace storage {
StronglyConnectedComponent::StronglyConnectedComponent() : isTrivialScc(false) {
// Intentionally left empty.
}
void StronglyConnectedComponent::setIsTrivial(bool trivial) {
this->isTrivialScc = trivial;
}

2
src/storage/StronglyConnectedComponent.h
View File

@ -14,7 +14,7 @@ namespace storm {
*/
class StronglyConnectedComponent : public StateBlock {
public:
StronglyConnectedComponent() = default;
StronglyConnectedComponent();
StronglyConnectedComponent(StronglyConnectedComponent const& other) = default;
#ifndef WINDOWS
StronglyConnectedComponent(StronglyConnectedComponent&& other) = default;

18
src/utility/ConstantsComparator.cpp
View File

@ -118,7 +118,6 @@ namespace storm {
}
#endif
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) {
simplify(matrixEntry.getValue());
@ -126,26 +125,29 @@ namespace storm {
}
template class ConstantsComparator<double>;
template class ConstantsComparator<RationalFunction>;
template class ConstantsComparator<Polynomial>;
template double one();
template double zero();
template double infinity();
template double simplify(double value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
#ifdef PARAMETRIC_SYSTEMS
template class ConstantsComparator<RationalFunction>;
template class ConstantsComparator<Polynomial>;
template RationalFunction one();
template RationalFunction zero();
template Polynomial one();
template Polynomial zero();
template double simplify(double value);
template RationalFunction simplify(RationalFunction value);
template RationalFunction& simplify(RationalFunction& value);
template RationalFunction&& simplify(RationalFunction&& value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);
#endif
}
}

21
src/utility/macros.h
View File

@ -9,15 +9,8 @@
extern log4cplus::Logger logger;
/*!
* Define the macros STORM_LOG_ASSERT, STORM_LOG_DEBUG and STORM_LOG_TRACE.
* Define the macros STORM_LOG_DEBUG and STORM_LOG_TRACE.
*/
#define STORM_LOG_ASSERT(cond, message) \
{ \
if (!(cond)) { \
LOG4CPLUS_ERROR(logger, message); \
assert(cond); \
} \
} while (false)
#define STORM_LOG_DEBUG(message) \
{ \
LOG4CPLUS_DEBUG(logger, message); \
@ -27,6 +20,18 @@ extern log4cplus::Logger logger;
LOG4CPLUS_TRACE(logger, message); \
} while (false)
// Define STORM_LOG_ASSERT which is only checked when NDEBUG is not set.
#ifndef NDEBUG
#define STORM_LOG_ASSERT(cond, message) \
{ \
if (!(cond)) { \
LOG4CPLUS_ERROR(logger, message); \
assert(cond); \
} \
} while (false)
#else
#define STORM_LOG_ASSERT(cond, message)
#endif
// Define STORM_LOG_THROW to always throw the exception with the given message if the condition fails to hold.
#define STORM_LOG_THROW(cond, exception, message) \
{ \

Write Preview
Loading…
Cancel
Save