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

Made the OptimalSCC algorithm MUCH faster. 

Fixed error reporting in AtomicPropositionLabelingParser.cpp and SparseStateRewardParser.cpp.


Former-commit-id: 77ba352a29
tempestpy_adaptions
PBerger 10 years ago
parent
7e77fbb6bb
commit
422a317407
3 changed files with 60 additions and 36 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 23
      src/parser/AtomicPropositionLabelingParser.cpp
  2. 17
      src/parser/SparseStateRewardParser.cpp
  3. 38
      src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp

23
src/parser/AtomicPropositionLabelingParser.cpp
View File

@ -29,8 +29,8 @@ namespace storm {
// Open the given file. // Open the given file.
if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
throw storm::exceptions::FileIoException() << "The supplied Labeling input file \"" << filename << "\" does not exist or is not readable by this process.";
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process.");
throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process.";
} }
MappedFile file(filename.c_str()); MappedFile file(filename.c_str());
@ -68,10 +68,10 @@ namespace storm {
// If #DECLARATION or #END have not been found, the file format is wrong. // If #DECLARATION or #END have not been found, the file format is wrong.
if (!(foundDecl && foundEnd)) { if (!(foundDecl && foundEnd)) {
LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). File header is corrupted.");
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File header is corrupted (#DECLARATION or #END missing - case sensitive).");
if (!foundDecl) LOG4CPLUS_ERROR(logger, "\tDid not find #DECLARATION token."); if (!foundDecl) LOG4CPLUS_ERROR(logger, "\tDid not find #DECLARATION token.");
if (!foundEnd) LOG4CPLUS_ERROR(logger, "\tDid not find #END token."); if (!foundEnd) LOG4CPLUS_ERROR(logger, "\tDid not find #END token.");
throw storm::exceptions::WrongFormatException();
throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": File header is corrupted (#DECLARATION or #END missing - case sensitive).";
} }
@ -100,8 +100,8 @@ namespace storm {
if (cnt >= sizeof(proposition)) { if (cnt >= sizeof(proposition)) {
// if token is longer than our buffer, the following strncpy code might get risky... // if token is longer than our buffer, the following strncpy code might get risky...
LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). Atomic proposition with length > " << (sizeof(proposition)-1) << " was found.");
throw storm::exceptions::WrongFormatException();
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Atomic proposition with length > " << (sizeof(proposition) - 1) << " was found.");
throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": Atomic proposition with length > " << (sizeof(proposition) - 1) << " was found.";
} else if (cnt > 0) { } else if (cnt > 0) {
@ -127,6 +127,7 @@ namespace storm {
uint_fast64_t state = 0; uint_fast64_t state = 0;
uint_fast64_t lastState = (uint_fast64_t)-1; uint_fast64_t lastState = (uint_fast64_t)-1;
uint_fast64_t const startIndexComparison = lastState;
cnt = 0; cnt = 0;
// Now parse the assignments of labels to nodes. // Now parse the assignments of labels to nodes.
@ -137,9 +138,9 @@ namespace storm {
state = checked_strtol(buf, &buf); state = checked_strtol(buf, &buf);
// If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks). // If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks).
if(state <= lastState && lastState != (uint_fast64_t)-1) {
LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). State " << state << " was found but has already been read or skipped previously.");
throw storm::exceptions::WrongFormatException() << "State " << state << " was found but has already been read or skipped previously.";
if (state <= lastState && lastState != startIndexComparison) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously.");
throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously.";
} }
while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) { while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) {
@ -159,8 +160,8 @@ namespace storm {
// Has the label been declared in the header? // Has the label been declared in the header?
if(!labeling.containsAtomicProposition(proposition)) { if(!labeling.containsAtomicProposition(proposition)) {
LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). Atomic proposition" << proposition << " was found but not declared.");
throw storm::exceptions::WrongFormatException();
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Atomic proposition" << proposition << " was found but not declared.");
throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": Atomic proposition" << proposition << " was found but not declared.";
} }
labeling.addAtomicPropositionToState(proposition, state); labeling.addAtomicPropositionToState(proposition, state);
buf += cnt; buf += cnt;

17
src/parser/SparseStateRewardParser.cpp
View File

@ -4,7 +4,7 @@
* Created on: 23.12.2012 * Created on: 23.12.2012
* Author: Christian Dehnert * Author: Christian Dehnert
*/ */
#include <iostream>
#include "src/parser/SparseStateRewardParser.h" #include "src/parser/SparseStateRewardParser.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
@ -37,6 +37,7 @@ namespace storm {
// Now parse state reward assignments. // Now parse state reward assignments.
uint_fast64_t state = 0; uint_fast64_t state = 0;
uint_fast64_t lastState = (uint_fast64_t)-1; uint_fast64_t lastState = (uint_fast64_t)-1;
uint_fast64_t const startIndexComparison = lastState;
double reward; double reward;
// Iterate over states. // Iterate over states.
@ -47,21 +48,21 @@ namespace storm {
// If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks). // If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks).
// Note: The value -1 shows that lastState has not yet been set, i.e. this is the first run of the loop (state index (2^64)-1 is a really bad starting index). // Note: The value -1 shows that lastState has not yet been set, i.e. this is the first run of the loop (state index (2^64)-1 is a really bad starting index).
if(state <= lastState && lastState != (uint_fast64_t)-1) {
LOG4CPLUS_ERROR(logger, "State " << state << " was found but has already been read or skipped previously.");
throw storm::exceptions::WrongFormatException() << "State " << state << " was found but has already been read or skipped previously.";
if (state <= lastState && lastState != startIndexComparison) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously.");
throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously.";
} }
if(stateCount <= state) { if(stateCount <= state) {
LOG4CPLUS_ERROR(logger, "Found reward for a state of an invalid index \"" << state << "\". The model has only " << stateCount << " states.");
throw storm::exceptions::OutOfRangeException() << "Found reward for a state of an invalid index \"" << state << "\"";
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Found reward for a state of an invalid index \"" << state << "\". The model has only " << stateCount << " states.");
throw storm::exceptions::OutOfRangeException() << "Error while parsing " << filename << ": Found reward for a state of an invalid index \"" << state << "\"";
} }
reward = checked_strtod(buf, &buf); reward = checked_strtod(buf, &buf);
if (reward < 0.0) { if (reward < 0.0) {
LOG4CPLUS_ERROR(logger, "Expected positive reward value but got \"" << reward << "\".");
throw storm::exceptions::WrongFormatException() << "State reward file specifies illegal reward value.";
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Expected positive reward value but got \"" << reward << "\".");
throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": State reward file specifies illegal reward value.";
} }
stateRewards[state] = reward; stateRewards[state] = reward;

38
src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
View File

@ -97,7 +97,7 @@ namespace storm {
std::vector<uint_fast64_t> sccSubNondeterministicChoiceIndices(sccSubmatrix.getColumnCount() + 1); std::vector<uint_fast64_t> sccSubNondeterministicChoiceIndices(sccSubmatrix.getColumnCount() + 1);
sccSubNondeterministicChoiceIndices.at(0) = 0; sccSubNondeterministicChoiceIndices.at(0) = 0;
// Preprocess all dependent states
// Pre-process all dependent states
// Remove outgoing transitions and create the ChoiceIndices // Remove outgoing transitions and create the ChoiceIndices
uint_fast64_t innerIndex = 0; uint_fast64_t innerIndex = 0;
uint_fast64_t outerIndex = 0; uint_fast64_t outerIndex = 0;
@ -135,8 +135,7 @@ namespace storm {
localIterations = 0; localIterations = 0;
if (minimize) { if (minimize) {
result = basicValueIteration_mvReduce_uint64_double_minimize(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations); result = basicValueIteration_mvReduce_uint64_double_minimize(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations);
}
else {
} else {
result = basicValueIteration_mvReduce_uint64_double_maximize(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations); result = basicValueIteration_mvReduce_uint64_double_maximize(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations);
} }
LOG4CPLUS_INFO(logger, "Executed " << localIterations << " of max. " << maximalNumberOfIterations << " Iterations on GPU."); LOG4CPLUS_INFO(logger, "Executed " << localIterations << " of max. " << maximalNumberOfIterations << " Iterations on GPU.");
@ -276,13 +275,24 @@ namespace storm {
storm::storage::StateBlock const& scc_first = sccDecomposition[topologicalSort[startIndex]]; storm::storage::StateBlock const& scc_first = sccDecomposition[topologicalSort[startIndex]];
tempGroups.insert(tempGroups.cend(), scc_first.cbegin(), scc_first.cend()); tempGroups.insert(tempGroups.cend(), scc_first.cbegin(), scc_first.cend());
for (size_t j = startIndex + 1; j < i; ++j) {
if (((startIndex + 1) + 80) >= i) {
size_t lastSize = 0;
for (size_t j = startIndex + 1; j < topologicalSort.size(); ++j) {
storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]]; storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]];
std::vector<uint_fast64_t>::iterator const middleIterator = tempGroups.end();
lastSize = tempGroups.size();
tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend()); tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend());
std::vector<uint_fast64_t>::iterator middleIterator = tempGroups.begin();
std::advance(middleIterator, lastSize);
std::inplace_merge(tempGroups.begin(), middleIterator, tempGroups.end()); std::inplace_merge(tempGroups.begin(), middleIterator, tempGroups.end());
} }
} else {
// Use std::sort
for (size_t j = startIndex + 1; j < i; ++j) {
storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]];
tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend());
}
std::sort(tempGroups.begin(), tempGroups.end());
}
result.push_back(std::make_pair(true, storm::storage::StateBlock(boost::container::ordered_unique_range, tempGroups.cbegin(), tempGroups.cend()))); result.push_back(std::make_pair(true, storm::storage::StateBlock(boost::container::ordered_unique_range, tempGroups.cbegin(), tempGroups.cend())));
} else { } else {
// Only one group, copy construct. // Only one group, copy construct.
@ -318,13 +328,25 @@ namespace storm {
storm::storage::StateBlock const& scc_first = sccDecomposition[topologicalSort[startIndex]]; storm::storage::StateBlock const& scc_first = sccDecomposition[topologicalSort[startIndex]];
tempGroups.insert(tempGroups.cend(), scc_first.cbegin(), scc_first.cend()); tempGroups.insert(tempGroups.cend(), scc_first.cbegin(), scc_first.cend());
// For set counts <= 80, Inplace Merge is faster
if (((startIndex + 1) + 80) >= topologicalSortSize) {
size_t lastSize = 0;
for (size_t j = startIndex + 1; j < topologicalSort.size(); ++j) { for (size_t j = startIndex + 1; j < topologicalSort.size(); ++j) {
storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]]; storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]];
std::vector<uint_fast64_t>::iterator const middleIterator = tempGroups.end();
lastSize = tempGroups.size();
tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend()); tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend());
std::vector<uint_fast64_t>::iterator middleIterator = tempGroups.begin();
std::advance(middleIterator, lastSize);
std::inplace_merge(tempGroups.begin(), middleIterator, tempGroups.end()); std::inplace_merge(tempGroups.begin(), middleIterator, tempGroups.end());
} }
} else {
// Use std::sort
for (size_t j = startIndex + 1; j < topologicalSort.size(); ++j) {
storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]];
tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend());
}
std::sort(tempGroups.begin(), tempGroups.end());
}
result.push_back(std::make_pair(true, storm::storage::StateBlock(boost::container::ordered_unique_range, tempGroups.cbegin(), tempGroups.cend()))); result.push_back(std::make_pair(true, storm::storage::StateBlock(boost::container::ordered_unique_range, tempGroups.cbegin(), tempGroups.cend())));
} }
else { else {

Write Preview
Loading…
Cancel
Save