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

progress in monitoring with timeouts etc

tempestpy_adaptions
Sebastian Junges 4 years ago
parent
4760a12815
commit
e513a3fb62
8 changed files with 146 additions and 35 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. 2
      src/storm-pomdp/generator/BeliefSupportTracker.cpp
  2. 46
      src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp
  3. 15
      src/storm-pomdp/generator/NondeterministicBeliefTracker.h
  4. 67
      src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp
  5. 9
      src/storm-pomdp/transformer/ObservationTraceUnfolder.h
  6. 2
      src/storm/storage/expressions/ExpressionManager.cpp
  7. 27
      src/storm/storage/geometry/ReduceVertexCloud.cpp
  8. 13
      src/storm/storage/geometry/ReduceVertexCloud.h

2
src/storm-pomdp/generator/BeliefSupportTracker.cpp
View File

@ -30,6 +30,8 @@ namespace storm {
} }
template class BeliefSupportTracker<double>; template class BeliefSupportTracker<double>;
template class BeliefSupportTracker<storm::RationalNumber>;
} }
} }

46
src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp
View File

@ -4,6 +4,7 @@
#include "storm/storage/geometry/nativepolytopeconversion/QuickHull.h" #include "storm/storage/geometry/nativepolytopeconversion/QuickHull.h"
#include "storm/storage/geometry/ReduceVertexCloud.h" #include "storm/storage/geometry/ReduceVertexCloud.h"
#include "storm/utility/vector.h" #include "storm/utility/vector.h"
#include "storm/utility/Stopwatch.h"
namespace storm { namespace storm {
namespace generator { namespace generator {
@ -207,7 +208,9 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void SparseBeliefState<ValueType>::setSupport(storm::storage::BitVector& support) const { void SparseBeliefState<ValueType>::setSupport(storm::storage::BitVector& support) const {
assert(false);
for(auto const& entry : belief) {
support.set(entry.first, true);
}
} }
template<typename ValueType> template<typename ValueType>
@ -425,8 +428,8 @@ namespace storm {
template<typename ValueType, typename BeliefState> template<typename ValueType, typename BeliefState>
NondeterministicBeliefTracker<ValueType, BeliefState>::NondeterministicBeliefTracker(storm::models::sparse::Pomdp<ValueType> const& pomdp) :
pomdp(pomdp), manager(std::make_shared<BeliefStateManager<ValueType>>(pomdp)), beliefs() {
NondeterministicBeliefTracker<ValueType, BeliefState>::NondeterministicBeliefTracker(storm::models::sparse::Pomdp<ValueType> const& pomdp, typename NondeterministicBeliefTracker<ValueType, BeliefState>::Options options ) :
pomdp(pomdp), manager(std::make_shared<BeliefStateManager<ValueType>>(pomdp)), beliefs(), options(options) {
// //
} }
@ -448,8 +451,12 @@ namespace storm {
STORM_LOG_THROW(!beliefs.empty(), storm::exceptions::InvalidOperationException, "Cannot track without a belief (need to reset)."); STORM_LOG_THROW(!beliefs.empty(), storm::exceptions::InvalidOperationException, "Cannot track without a belief (need to reset).");
std::unordered_set<BeliefState> newBeliefs; std::unordered_set<BeliefState> newBeliefs;
//for (uint64_t action = 0; action < manager->getActionsForObservation(lastObservation); ++action) { //for (uint64_t action = 0; action < manager->getActionsForObservation(lastObservation); ++action) {
storm::utility::Stopwatch trackTimer(true);
for (auto const& belief : beliefs) { for (auto const& belief : beliefs) {
belief.update(newObservation, newBeliefs); belief.update(newObservation, newBeliefs);
if (options.trackTimeOut > 0 && trackTimer.getTimeInMilliseconds() > options.trackTimeOut) {
return false;
}
} }
//} //}
beliefs = newBeliefs; beliefs = newBeliefs;
@ -492,11 +499,28 @@ namespace storm {
return lastObservation; return lastObservation;
} }
template<typename ValueType, typename BeliefState>
uint64_t NondeterministicBeliefTracker<ValueType, BeliefState>::getNumberOfBeliefs() const {
return beliefs.size();
}
template<typename ValueType, typename BeliefState>
uint64_t NondeterministicBeliefTracker<ValueType, BeliefState>::getCurrentDimension() const {
storm::storage::BitVector support(beliefs.begin()->getSupportSize());
for(auto const& belief : beliefs) {
belief.setSupport(support);
}
return support.getNumberOfSetBits();
}
// //
template<typename ValueType, typename BeliefState> template<typename ValueType, typename BeliefState>
uint64_t NondeterministicBeliefTracker<ValueType, BeliefState>::reduce() { uint64_t NondeterministicBeliefTracker<ValueType, BeliefState>::reduce() {
reductionTimedOut = false;
std::shared_ptr<storm::utility::solver::SmtSolverFactory> solverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>(); std::shared_ptr<storm::utility::solver::SmtSolverFactory> solverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
storm::storage::geometry::ReduceVertexCloud<ValueType> rvc(solverFactory);
storm::storage::geometry::ReduceVertexCloud<ValueType> rvc(solverFactory, options.wiggle, options.timeOut);
std::vector<std::map<uint64_t, ValueType>> points; std::vector<std::map<uint64_t, ValueType>> points;
std::vector<typename std::unordered_set<BeliefState>::iterator> iterators; std::vector<typename std::unordered_set<BeliefState>::iterator> iterators;
for (auto it = beliefs.begin(); it != beliefs.end(); ++it) { for (auto it = beliefs.begin(); it != beliefs.end(); ++it) {
@ -504,7 +528,11 @@ namespace storm {
points.push_back(it->getBeliefMap()); points.push_back(it->getBeliefMap());
iterators.push_back(it); iterators.push_back(it);
} }
storm::storage::BitVector eliminate = ~rvc.eliminate(points, pomdp.getNumberOfStates());
auto res = rvc.eliminate(points, pomdp.getNumberOfStates());
storm::storage::BitVector eliminate = ~res.first;
if (res.second) {
reductionTimedOut = true;
}
auto selectedIterators = storm::utility::vector::filterVector(iterators, eliminate); auto selectedIterators = storm::utility::vector::filterVector(iterators, eliminate);
for (auto iter : selectedIterators) { for (auto iter : selectedIterators) {
@ -513,6 +541,11 @@ namespace storm {
return eliminate.getNumberOfSetBits(); return eliminate.getNumberOfSetBits();
} }
template<typename ValueType, typename BeliefState>
bool NondeterministicBeliefTracker<ValueType, BeliefState>::hasTimedOut() const {
return reductionTimedOut;
}
template class SparseBeliefState<double>; template class SparseBeliefState<double>;
template bool operator==(SparseBeliefState<double> const&, SparseBeliefState<double> const&); template bool operator==(SparseBeliefState<double> const&, SparseBeliefState<double> const&);
@ -521,6 +554,9 @@ namespace storm {
//template bool operator==(ObservationDenseBeliefState<double> const&, ObservationDenseBeliefState<double> const&); //template bool operator==(ObservationDenseBeliefState<double> const&, ObservationDenseBeliefState<double> const&);
//template class NondeterministicBeliefTracker<double, ObservationDenseBeliefState<double>>; //template class NondeterministicBeliefTracker<double, ObservationDenseBeliefState<double>>;
template class SparseBeliefState<storm::RationalNumber>;
template bool operator==(SparseBeliefState<storm::RationalNumber> const&, SparseBeliefState<storm::RationalNumber> const&);
template class NondeterministicBeliefTracker<storm::RationalNumber, SparseBeliefState<storm::RationalNumber>>;
} }
} }

15
src/storm-pomdp/generator/NondeterministicBeliefTracker.h
View File

@ -93,23 +93,34 @@ namespace storm {
uint64_t prevId; uint64_t prevId;
}; };
template<typename ValueType, typename BeliefState> template<typename ValueType, typename BeliefState>
class NondeterministicBeliefTracker { class NondeterministicBeliefTracker {
public: public:
NondeterministicBeliefTracker(storm::models::sparse::Pomdp<ValueType> const& pomdp);
struct Options {
uint64_t trackTimeOut = 0;
uint64_t timeOut = 0; // for reduction, in milliseconds, 0 is no timeout
ValueType wiggle; // tolerance, anything above 0 means that we are incomplete.
};
NondeterministicBeliefTracker(storm::models::sparse::Pomdp<ValueType> const& pomdp, typename NondeterministicBeliefTracker<ValueType, BeliefState>::Options options = Options());
bool reset(uint32_t observation); bool reset(uint32_t observation);
bool track(uint64_t newObservation); bool track(uint64_t newObservation);
std::unordered_set<BeliefState> const& getCurrentBeliefs() const; std::unordered_set<BeliefState> const& getCurrentBeliefs() const;
uint32_t getCurrentObservation() const; uint32_t getCurrentObservation() const;
uint64_t getNumberOfBeliefs() const;
ValueType getCurrentRisk(bool max=true); ValueType getCurrentRisk(bool max=true);
void setRisk(std::vector<ValueType> const& risk); void setRisk(std::vector<ValueType> const& risk);
uint64_t getCurrentDimension() const;
uint64_t reduce(); uint64_t reduce();
bool hasTimedOut() const;
private: private:
storm::models::sparse::Pomdp<ValueType> const& pomdp; storm::models::sparse::Pomdp<ValueType> const& pomdp;
std::shared_ptr<BeliefStateManager<ValueType>> manager; std::shared_ptr<BeliefStateManager<ValueType>> manager;
std::unordered_set<BeliefState> beliefs; std::unordered_set<BeliefState> beliefs;
bool reductionTimedOut = false;
Options options;
uint32_t lastObservation; uint32_t lastObservation;
}; };
} }

67
src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp
View File

@ -2,21 +2,23 @@
#include "storm-pomdp/transformer/ObservationTraceUnfolder.h" #include "storm-pomdp/transformer/ObservationTraceUnfolder.h"
#include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/ExpressionManager.h"
#undef _VERBOSE_OBSERVATION_UNFOLDING
namespace storm { namespace storm {
namespace pomdp { namespace pomdp {
template<typename ValueType> template<typename ValueType>
ObservationTraceUnfolder<ValueType>::ObservationTraceUnfolder(storm::models::sparse::Pomdp<ValueType> const& model,
std::shared_ptr<storm::expressions::ExpressionManager>& exprManager) : model(model), exprManager(exprManager) {
ObservationTraceUnfolder<ValueType>::ObservationTraceUnfolder(storm::models::sparse::Pomdp<ValueType> const& model, std::vector<ValueType> const& risk,
std::shared_ptr<storm::expressions::ExpressionManager>& exprManager) : model(model), risk(risk), exprManager(exprManager) {
statesPerObservation = std::vector<storm::storage::BitVector>(model.getNrObservations(), storm::storage::BitVector(model.getNumberOfStates())); statesPerObservation = std::vector<storm::storage::BitVector>(model.getNrObservations(), storm::storage::BitVector(model.getNumberOfStates()));
for (uint64_t state = 0; state < model.getNumberOfStates(); ++state) { for (uint64_t state = 0; state < model.getNumberOfStates(); ++state) {
statesPerObservation[model.getObservation(state)].set(state, true); statesPerObservation[model.getObservation(state)].set(state, true);
} }
svvar = exprManager->declareFreshIntegerVariable(false, "_s");
} }
template<typename ValueType> template<typename ValueType>
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<ValueType>::transform( std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<ValueType>::transform(
const std::vector<uint32_t> &observations, std::vector<ValueType> const& risk) {
const std::vector<uint32_t> &observations) {
std::vector<uint32_t> modifiedObservations = observations; std::vector<uint32_t> modifiedObservations = observations;
// First observation should be special. // First observation should be special.
// This just makes the algorithm simpler because we do not treat the first step as a special case later. // This just makes the algorithm simpler because we do not treat the first step as a special case later.
@ -34,14 +36,20 @@ namespace storm {
statesPerObservation.resize(model.getNrObservations() + 1); statesPerObservation.resize(model.getNrObservations() + 1);
statesPerObservation[model.getNrObservations()] = actualInitialStates; statesPerObservation[model.getNrObservations()] = actualInitialStates;
#ifdef _VERBOSE_OBSERVATION_UNFOLDING
std::cout << "build valution builder.." << std::endl;
#endif
storm::storage::sparse::StateValuationsBuilder svbuilder; storm::storage::sparse::StateValuationsBuilder svbuilder;
auto svvar = exprManager->declareFreshIntegerVariable(false, "_s");
svbuilder.addVariable(svvar); svbuilder.addVariable(svvar);
std::map<uint64_t,uint64_t> unfoldedToOld; std::map<uint64_t,uint64_t> unfoldedToOld;
std::map<uint64_t,uint64_t> unfoldedToOldNextStep; std::map<uint64_t,uint64_t> unfoldedToOldNextStep;
std::map<uint64_t,uint64_t> oldToUnfolded; std::map<uint64_t,uint64_t> oldToUnfolded;
#ifdef _VERBOSE_OBSERVATION_UNFOLDING
std::cout << "start buildiing matrix..." << std::endl;
#endif
// Add this initial state state: // Add this initial state state:
unfoldedToOldNextStep[0] = actualInitialStates.getNextSetIndex(0); unfoldedToOldNextStep[0] = actualInitialStates.getNextSetIndex(0);
@ -52,22 +60,25 @@ namespace storm {
// Notice that we are going to use a special last step // Notice that we are going to use a special last step
for (uint64_t step = 0; step < observations.size() - 1; ++step) { for (uint64_t step = 0; step < observations.size() - 1; ++step) {
std::cout << "step " << step << std::endl;
oldToUnfolded.clear(); oldToUnfolded.clear();
unfoldedToOld = unfoldedToOldNextStep; unfoldedToOld = unfoldedToOldNextStep;
unfoldedToOldNextStep.clear(); unfoldedToOldNextStep.clear();
for (auto const& unfoldedToOldEntry : unfoldedToOld) { for (auto const& unfoldedToOldEntry : unfoldedToOld) {
transitionMatrixBuilder.newRowGroup(newRowGroupStart); transitionMatrixBuilder.newRowGroup(newRowGroupStart);
//std::cout << "\tconsider new state " << unfoldedToOldEntry.first << std::endl;
#ifdef _VERBOSE_OBSERVATION_UNFOLDING
std::cout << "\tconsider new state " << unfoldedToOldEntry.first << std::endl;
#endif
assert(step == 0 || newRowCount == transitionMatrixBuilder.getLastRow() + 1); assert(step == 0 || newRowCount == transitionMatrixBuilder.getLastRow() + 1);
svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast<int64_t>(unfoldedToOldEntry.second)}); svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast<int64_t>(unfoldedToOldEntry.second)});
uint64_t oldRowIndexStart = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second]; uint64_t oldRowIndexStart = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second];
uint64_t oldRowIndexEnd = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second+1]; uint64_t oldRowIndexEnd = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second+1];
for (uint64_t oldRowIndex = oldRowIndexStart; oldRowIndex != oldRowIndexEnd; oldRowIndex++) { for (uint64_t oldRowIndex = oldRowIndexStart; oldRowIndex != oldRowIndexEnd; oldRowIndex++) {
//std::cout << "\t\tconsider old action " << oldRowIndex << std::endl;
//std::cout << "\t\tconsider new row nr " << newRowCount << std::endl;
#ifdef _VERBOSE_OBSERVATION_UNFOLDING
std::cout << "\t\tconsider old action " << oldRowIndex << std::endl;
std::cout << "\t\tconsider new row nr " << newRowCount << std::endl;
#endif
ValueType resetProb = storm::utility::zero<ValueType>(); ValueType resetProb = storm::utility::zero<ValueType>();
// We first find the reset probability // We first find the reset probability
@ -76,14 +87,17 @@ namespace storm {
resetProb += oldRowEntry.getValue(); resetProb += oldRowEntry.getValue();
} }
} }
//std::cout << "\t\t\t add reset" << std::endl;
#ifdef _VERBOSE_OBSERVATION_UNFOLDING
std::cout << "\t\t\t add reset with probability " << resetProb << std::endl;
#endif
// Add the resets // Add the resets
if (resetProb != storm::utility::zero<ValueType>()) { if (resetProb != storm::utility::zero<ValueType>()) {
transitionMatrixBuilder.addNextValue(newRowCount, 0, resetProb); transitionMatrixBuilder.addNextValue(newRowCount, 0, resetProb);
} }
//std::cout << "\t\t\t add other transitions..." << std::endl;
#ifdef _VERBOSE_OBSERVATION_UNFOLDING
std::cout << "\t\t\t add other transitions..." << std::endl;
#endif
// Now, we build the outgoing transitions. // Now, we build the outgoing transitions.
for (auto const &oldRowEntry : model.getTransitionMatrix().getRow(oldRowIndex)) { for (auto const &oldRowEntry : model.getTransitionMatrix().getRow(oldRowIndex)) {
@ -101,7 +115,9 @@ namespace storm {
} else { } else {
column = entryIt->second; column = entryIt->second;
} }
//std::cout << "\t\t\t\t transition to " << column << std::endl;
#ifdef _VERBOSE_OBSERVATION_UNFOLDING
std::cout << "\t\t\t\t transition to " << column << "with probability " << oldRowEntry.getValue() << std::endl;
#endif
transitionMatrixBuilder.addNextValue(newRowCount, column, transitionMatrixBuilder.addNextValue(newRowCount, column,
oldRowEntry.getValue()); oldRowEntry.getValue());
} }
@ -112,7 +128,6 @@ namespace storm {
} }
} }
std::cout << "Adding last step..." << std::endl;
// Now, take care of the last step. // Now, take care of the last step.
uint64_t sinkState = newStateIndex; uint64_t sinkState = newStateIndex;
uint64_t targetState = newStateIndex + 1; uint64_t targetState = newStateIndex + 1;
@ -120,7 +135,11 @@ namespace storm {
svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast<int64_t>(unfoldedToOldEntry.second)}); svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast<int64_t>(unfoldedToOldEntry.second)});
transitionMatrixBuilder.newRowGroup(newRowGroupStart); transitionMatrixBuilder.newRowGroup(newRowGroupStart);
if (!storm::utility::isZero(storm::utility::one<ValueType>() - risk[unfoldedToOldEntry.second])) {
STORM_LOG_ASSERT(risk.size() > unfoldedToOldEntry.second, "Must be a state");
STORM_LOG_ASSERT(risk[unfoldedToOldEntry.second] <= storm::utility::one<ValueType>(), "Risk must be a probability");
STORM_LOG_ASSERT(risk[unfoldedToOldEntry.second] >= storm::utility::zero<ValueType>(), "Risk must be a probability");
//std::cout << "risk is" << risk[unfoldedToOldEntry.second] << std::endl;
if (!storm::utility::isOne(risk[unfoldedToOldEntry.second])) {
transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState,
storm::utility::one<ValueType>() - risk[unfoldedToOldEntry.second]); storm::utility::one<ValueType>() - risk[unfoldedToOldEntry.second]);
} }
@ -140,12 +159,15 @@ namespace storm {
// target state // target state
transitionMatrixBuilder.addNextValue(newRowGroupStart, targetState, storm::utility::one<ValueType>()); transitionMatrixBuilder.addNextValue(newRowGroupStart, targetState, storm::utility::one<ValueType>());
svbuilder.addState(targetState, {}, {-1}); svbuilder.addState(targetState, {}, {-1});
#ifdef _VERBOSE_OBSERVATION_UNFOLDING
std::cout << "build matrix..." << std::endl;
#endif
storm::storage::sparse::ModelComponents<ValueType> components; storm::storage::sparse::ModelComponents<ValueType> components;
components.transitionMatrix = transitionMatrixBuilder.build(); components.transitionMatrix = transitionMatrixBuilder.build();
#ifdef _VERBOSE_OBSERVATION_UNFOLDING
std::cout << components.transitionMatrix << std::endl;
#endif
STORM_LOG_ASSERT(components.transitionMatrix.getRowGroupCount() == targetState + 1, "Expect row group count (" << components.transitionMatrix.getRowGroupCount() << ") one more as target state index " << targetState << ")"); STORM_LOG_ASSERT(components.transitionMatrix.getRowGroupCount() == targetState + 1, "Expect row group count (" << components.transitionMatrix.getRowGroupCount() << ") one more as target state index " << targetState << ")");
storm::models::sparse::StateLabeling labeling(components.transitionMatrix.getRowGroupCount()); storm::models::sparse::StateLabeling labeling(components.transitionMatrix.getRowGroupCount());
@ -157,12 +179,21 @@ namespace storm {
components.stateValuations = svbuilder.build( components.transitionMatrix.getRowGroupCount()); components.stateValuations = svbuilder.build( components.transitionMatrix.getRowGroupCount());
return std::make_shared<storm::models::sparse::Mdp<ValueType>>(std::move(components)); return std::make_shared<storm::models::sparse::Mdp<ValueType>>(std::move(components));
}
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<ValueType>::extend(uint32_t observation) {
traceSoFar.push_back(observation);
return transform(traceSoFar);
}
template<typename ValueType>
void ObservationTraceUnfolder<ValueType>::reset(uint32_t observation) {
traceSoFar = {observation};
} }
template class ObservationTraceUnfolder<double>; template class ObservationTraceUnfolder<double>;
template class ObservationTraceUnfolder<storm::RationalNumber>;
template class ObservationTraceUnfolder<storm::RationalFunction>; template class ObservationTraceUnfolder<storm::RationalFunction>;
} }

9
src/storm-pomdp/transformer/ObservationTraceUnfolder.h
View File

@ -6,12 +6,17 @@ namespace storm {
class ObservationTraceUnfolder { class ObservationTraceUnfolder {
public: public:
ObservationTraceUnfolder(storm::models::sparse::Pomdp<ValueType> const& model, std::shared_ptr<storm::expressions::ExpressionManager>& exprManager);
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> transform(std::vector<uint32_t> const& observations, std::vector<ValueType> const& risk);
ObservationTraceUnfolder(storm::models::sparse::Pomdp<ValueType> const& model, std::vector<ValueType> const& risk, std::shared_ptr<storm::expressions::ExpressionManager>& exprManager);
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> transform(std::vector<uint32_t> const& observations);
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> extend(uint32_t observation);
void reset(uint32_t observation);
private: private:
storm::models::sparse::Pomdp<ValueType> const& model; storm::models::sparse::Pomdp<ValueType> const& model;
std::vector<ValueType> risk; // TODO reconsider holding this as a reference, but there were some strange bugs
std::shared_ptr<storm::expressions::ExpressionManager>& exprManager; std::shared_ptr<storm::expressions::ExpressionManager>& exprManager;
std::vector<storm::storage::BitVector> statesPerObservation; std::vector<storm::storage::BitVector> statesPerObservation;
std::vector<uint32_t> traceSoFar;
storm::expressions::Variable svvar;
}; };

2
src/storm/storage/expressions/ExpressionManager.cpp
View File

@ -296,7 +296,7 @@ namespace storm {
Type const& ExpressionManager::getVariableType(uint_fast64_t index) const { Type const& ExpressionManager::getVariableType(uint_fast64_t index) const {
auto indexTypePair = indexToTypeMapping.find(index); auto indexTypePair = indexToTypeMapping.find(index);
STORM_LOG_ASSERT(indexTypePair != indexToTypeMapping.end(), "Unable to retrieve type of unknown variable index.");
STORM_LOG_ASSERT(indexTypePair != indexToTypeMapping.end(), "Unable to retrieve type of unknown variable index '" << index << "'.");
return indexTypePair->second; return indexTypePair->second;
} }

27
src/storm/storage/geometry/ReduceVertexCloud.cpp
View File

@ -23,7 +23,7 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
storm::storage::BitVector ReduceVertexCloud<ValueType>::eliminate(std::vector<std::map<uint64_t, ValueType>> const& input, uint64_t maxdimension) {
std::pair<storm::storage::BitVector, bool> ReduceVertexCloud<ValueType>::eliminate(std::vector<std::map<uint64_t, ValueType>> const& input, uint64_t maxdimension) {
std::shared_ptr<storm::expressions::ExpressionManager> expressionManager = std::make_shared<storm::expressions::ExpressionManager>(); std::shared_ptr<storm::expressions::ExpressionManager> expressionManager = std::make_shared<storm::expressions::ExpressionManager>();
std::vector<storm::storage::BitVector> supports; std::vector<storm::storage::BitVector> supports;
std::vector<storm::expressions::Variable> weightVariables; std::vector<storm::expressions::Variable> weightVariables;
@ -48,14 +48,23 @@ namespace storm {
smtSolver->add((weightVariableExpr >= expressionManager->rational(0.0))); smtSolver->add((weightVariableExpr >= expressionManager->rational(0.0)));
smtSolver->add(weightVariableExpr < expressionManager->rational(1.0)); smtSolver->add(weightVariableExpr < expressionManager->rational(1.0));
} }
smtSolver->add(storm::expressions::sum(weightVariableExpressions) <= expressionManager->rational(1.0 + wiggle));
smtSolver->add(storm::expressions::sum(weightVariableExpressions) >= expressionManager->rational(1 - wiggle));
if (storm::utility::isZero(wiggle)) {
smtSolver->add(storm::expressions::sum(weightVariableExpressions) <=
expressionManager->rational(1));
} else {
smtSolver->add(storm::expressions::sum(weightVariableExpressions) <=
expressionManager->rational(1.0 + wiggle));
smtSolver->add(storm::expressions::sum(weightVariableExpressions) >=
expressionManager->rational(1 - wiggle));
}
storm::utility::Stopwatch solverTime; storm::utility::Stopwatch solverTime;
storm::utility::Stopwatch totalTime(true); storm::utility::Stopwatch totalTime(true);
storm::storage::BitVector vertices(input.size()); storm::storage::BitVector vertices(input.size());
for (uint64_t pointIndex = 0; pointIndex < input.size(); ++pointIndex) { for (uint64_t pointIndex = 0; pointIndex < input.size(); ++pointIndex) {
#ifdef _DEBUG_REUCE_VERTEX_CLOUD
std::cout << pointIndex << " out of " << input.size() << std::endl; std::cout << pointIndex << " out of " << input.size() << std::endl;
#endif
smtSolver->push(); smtSolver->push();
std::map<uint64_t, std::vector<storm::expressions::Expression>> dimensionTerms; std::map<uint64_t, std::vector<storm::expressions::Expression>> dimensionTerms;
for (auto const& entry : input[pointIndex]) { for (auto const& entry : input[pointIndex]) {
@ -104,16 +113,26 @@ namespace storm {
} }
std::cout << std::endl; std::cout << std::endl;
} }
if (timeOut > )
#endif #endif
if (timeOut > 0 && totalTime.getTimeInMilliseconds() > timeOut) {
for (uint64_t remainingPoint = pointIndex + 1; remainingPoint < input.size(); ++remainingPoint) {
vertices.set(remainingPoint);
}
return {vertices, true};
}
smtSolver->pop(); smtSolver->pop();
#ifdef _DEBUG_REDUCE_VERTEX_CLOUD
std::cout << "Solver time " << solverTime.getTimeInMilliseconds() << std::endl; std::cout << "Solver time " << solverTime.getTimeInMilliseconds() << std::endl;
std::cout << "Total time " << totalTime.getTimeInMilliseconds() << std::endl; std::cout << "Total time " << totalTime.getTimeInMilliseconds() << std::endl;
#endif
} }
return vertices;
return {vertices, false};
} }
template class ReduceVertexCloud<double>; template class ReduceVertexCloud<double>;
template class ReduceVertexCloud<storm::RationalNumber>;
} }
} }
} }

13
src/storm/storage/geometry/ReduceVertexCloud.h
View File

@ -10,17 +10,24 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
class ReduceVertexCloud { class ReduceVertexCloud {
public: public:
ReduceVertexCloud(std::shared_ptr<storm::utility::solver::SmtSolverFactory>& smtSolverFactory, ValueType wiggle = storm::utility::convertNumber<ValueType>(0.001))
: smtSolverFactory(smtSolverFactory), wiggle(wiggle)
/*!
*
* @param smtSolverFactory
* @param wiggle
* @param timeout: Maximal time in milliseconds, 0 is no timeout
*/
ReduceVertexCloud(std::shared_ptr<storm::utility::solver::SmtSolverFactory>& smtSolverFactory, ValueType wiggle = storm::utility::convertNumber<ValueType>(0.0), uint64_t timeout = 0)
: smtSolverFactory(smtSolverFactory), wiggle(wiggle), timeOut(timeout)
{ {
} }
storm::storage::BitVector eliminate(std::vector<std::map<uint64_t, ValueType>> const& input, uint64_t maxdimension);
std::pair<storm::storage::BitVector,bool> eliminate(std::vector<std::map<uint64_t, ValueType>> const& input, uint64_t maxdimension);
private: private:
std::shared_ptr<storm::utility::solver::SmtSolverFactory>& smtSolverFactory; std::shared_ptr<storm::utility::solver::SmtSolverFactory>& smtSolverFactory;
ValueType wiggle; ValueType wiggle;
uint64_t timeOut;
}; };

Write Preview
Loading…
Cancel
Save