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

adding precision to less/greater in vector reduction, adding export to json

tempestpy_adaptions
dehnert 7 years ago
parent
09876f6808
commit
9f72f67d9f
3 changed files with 235 additions and 11 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. 192
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  2. 40
      src/storm/utility/constants.h
  3. 10
      src/storm/utility/vector.h

192
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -843,7 +843,181 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
void postProcessStrategies(storm::OptimizationDirection const& player1Direction, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector<uint64_t> const& player1Groups, std::vector<uint64_t> const& player2Groups, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax<ValueType> const& quantitativeResult, bool redirectPlayer1, bool redirectPlayer2, bool sanityCheck) {
class ExplicitGameExporter {
public:
void exportToJson(std::string const& filename, std::vector<uint64_t> const& player1Groups, std::vector<uint64_t> const& player2Groups, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax<ValueType> const& quantitativeResult, ExplicitGameStrategyPair const* minStrategyPair, ExplicitGameStrategyPair const* maxStrategyPair) {
// Export game as json.
std::ofstream outfile(filename);
// Export nodes.
outfile << "{\n\t\"nodes\": [" << std::endl;
exportNodes(outfile, player1Groups, player2Groups, transitionMatrix, initialStates, constraintStates, targetStates, quantitativeResult, minStrategyPair, maxStrategyPair);
outfile << "\n\t]," << std::endl;
// Export edges.
outfile << "\t\"edges\": [" << std::endl;
exportEdges(outfile, player1Groups, player2Groups, transitionMatrix, initialStates, constraintStates, targetStates, quantitativeResult, minStrategyPair, maxStrategyPair);
outfile << "\n\t]\n}" << std::endl;
}
private:
void exportEdge(std::ofstream& out, uint64_t id, uint64_t source, uint64_t target, std::string const& name, bool& first) {
if (!first) {
out << "," << std::endl;
} else {
first = false;
}
out << "\t\t{" << std::endl;
out << "\t\t\t\"data\": {" << std::endl;
out << "\t\t\t\t\"id\": \"" << id << "\"," << std::endl;
out << "\t\t\t\t\"name\": \"" << name << "\"," << std::endl;
out << "\t\t\t\t\"source\": \"" << source << "\"," << std::endl;
out << "\t\t\t\t\"target\": \"" << target << "\"" << std::endl;
out << "\t\t\t}" << std::endl;
out << "\t\t}";
}
void exportEdges(std::ofstream& out, std::vector<uint64_t> const& player1Groups, std::vector<uint64_t> const& player2Groups, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax<ValueType> const& quantitativeResult, ExplicitGameStrategyPair const* minStrategyPair, ExplicitGameStrategyPair const* maxStrategyPair) {
std::vector<uint64_t> stack;
for (auto state : initialStates) {
stack.push_back(state);
}
storm::storage::BitVector reachablePlayer1(player1Groups.size() - 1);
bool first = true;
uint64_t edgeId = 0;
while (!stack.empty()) {
uint64_t currentState = stack.back();
stack.pop_back();
// Follow lower.
if (minStrategyPair) {
if (minStrategyPair->getPlayer1Strategy().hasDefinedChoice(currentState)) {
uint64_t player2State = minStrategyPair->getPlayer1Strategy().getChoice(currentState);
exportEdge(out, edgeId++, currentState, player2State, "lo", first);
uint64_t playerPState = minStrategyPair->getPlayer2Strategy().getChoice(player2State);
exportEdge(out, edgeId++, player2State, playerPState, "lo", first);
for (auto const& entry : transitionMatrix.getRow(playerPState)) {
auto player1Successor = entry.getColumn();
exportEdge(out, edgeId++, playerPState, player1Successor, std::to_string(entry.getValue()), first);
if (!reachablePlayer1.get(player1Successor)) {
reachablePlayer1.set(player1Successor);
stack.push_back(player1Successor);
}
}
}
}
// Follow upper.
if (maxStrategyPair) {
if (maxStrategyPair->getPlayer1Strategy().hasDefinedChoice(currentState)) {
uint64_t player2State = maxStrategyPair->getPlayer1Strategy().getChoice(currentState);
exportEdge(out, edgeId++, currentState, player2State, "hi", first);
uint64_t playerPState = maxStrategyPair->getPlayer2Strategy().getChoice(player2State);
exportEdge(out, edgeId++, player2State, playerPState, "hi", first);
for (auto const& entry : transitionMatrix.getRow(playerPState)) {
auto player1Successor = entry.getColumn();
exportEdge(out, edgeId++, playerPState, player1Successor, std::to_string(entry.getValue()), first);
if (!reachablePlayer1.get(player1Successor)) {
reachablePlayer1.set(player1Successor);
stack.push_back(player1Successor);
}
}
}
}
}
}
void exportNode(std::ofstream& out, uint64_t state, ExplicitQuantitativeResultMinMax<ValueType> const* quantitativeResult, bool& first, bool target = false) {
if (!first) {
out << "," << std::endl;
} else {
first = false;
}
out << "\t\t{" << std::endl;
out << "\t\t\t\"data\": {" << std::endl;
out << "\t\t\t\t\"id\": \"" << state << "\"," << std::endl;
out << "\t\t\t\t\"name\": \"" << state;
if (quantitativeResult) {
out << " [" << quantitativeResult->getMin().getValues()[state] << ", " << quantitativeResult->getMax().getValues()[state] << "]";
if (target) {
out << ", T";
}
}
out << "\"" << std::endl;
out << "\t\t\t}," << std::endl;
out << "\t\t\t\"group\": \"nodes\"," << std::endl;
out << "\t\t\t\"classes\": \"node\"" << std::endl;
out << "\t\t}";
}
void exportNodes(std::ofstream& out, std::vector<uint64_t> const& player1Groups, std::vector<uint64_t> const& player2Groups, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax<ValueType> const& quantitativeResult, ExplicitGameStrategyPair const* minStrategyPair, ExplicitGameStrategyPair const* maxStrategyPair) {
std::vector<uint64_t> stack;
for (auto state : initialStates) {
stack.push_back(state);
}
storm::storage::BitVector reachablePlayer1(player1Groups.size() - 1);
bool first = true;
while (!stack.empty()) {
uint64_t currentState = stack.back();
stack.pop_back();
exportNode(out, currentState, &quantitativeResult, first, targetStates.get(currentState));
// Follow lower.
if (minStrategyPair) {
if (minStrategyPair->getPlayer1Strategy().hasDefinedChoice(currentState)) {
uint64_t player2State = minStrategyPair->getPlayer1Strategy().getChoice(currentState);
exportNode(out, player2State, nullptr, first);
uint64_t playerPState = minStrategyPair->getPlayer2Strategy().getChoice(player2State);
exportNode(out, playerPState, nullptr, first);
for (auto const& entry : transitionMatrix.getRow(playerPState)) {
auto player1Successor = entry.getColumn();
if (!reachablePlayer1.get(player1Successor)) {
reachablePlayer1.set(player1Successor);
stack.push_back(player1Successor);
}
}
}
}
// Follow upper.
if (maxStrategyPair) {
if (maxStrategyPair->getPlayer1Strategy().hasDefinedChoice(currentState)) {
uint64_t player2State = maxStrategyPair->getPlayer1Strategy().getChoice(currentState);
exportNode(out, player2State, nullptr, first);
uint64_t playerPState = maxStrategyPair->getPlayer2Strategy().getChoice(player2State);
exportNode(out, playerPState, nullptr, first);
for (auto const& entry : transitionMatrix.getRow(playerPState)) {
auto player1Successor = entry.getColumn();
if (!reachablePlayer1.get(player1Successor)) {
reachablePlayer1.set(player1Successor);
stack.push_back(player1Successor);
}
}
}
}
}
}
};
template <typename ValueType>
void postProcessStrategies(uint64_t iteration, storm::OptimizationDirection const& player1Direction, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector<uint64_t> const& player1Groups, std::vector<uint64_t> const& player2Groups, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax<ValueType> const& quantitativeResult, bool redirectPlayer1, bool redirectPlayer2, bool sanityCheck) {
if (!redirectPlayer1 && !redirectPlayer2) { if (!redirectPlayer1 && !redirectPlayer2) {
return; return;
@ -948,7 +1122,7 @@ namespace storm {
} }
} }
STORM_LOG_TRACE("Got maximal deviation of " << maxDiff << "."); STORM_LOG_TRACE("Got maximal deviation of " << maxDiff << ".");
STORM_LOG_WARN_COND(sanityComparator.isZero(maxDiff), "Deviation " << maxDiff << " between computed value (" << quantitativeResult.getMin().getValues()[maxState] << ") and sanity check value (" << sanityValues[maxState] << ") in state " << maxState << " appears to be too high. (Obtained bounds were [" << quantitativeResult.getMin().getValues()[maxState] << ", " << quantitativeResult.getMax().getValues()[maxState] << "]");
STORM_LOG_WARN_COND(sanityComparator.isZero(maxDiff), "Deviation " << maxDiff << " between computed value (" << quantitativeResult.getMin().getValues()[maxState] << ") and sanity check value (" << sanityValues[maxState] << ") in state " << maxState << " appears to be too high. (Obtained bounds were [" << quantitativeResult.getMin().getValues()[maxState] << ", " << quantitativeResult.getMax().getValues()[maxState] << "].)");
if (!sanityComparator.isZero(maxDiff)) { if (!sanityComparator.isZero(maxDiff)) {
exit(-1); exit(-1);
} }
@ -996,8 +1170,16 @@ namespace storm {
} }
} }
STORM_LOG_TRACE("Got maximal deviation of " << maxDiff << "."); STORM_LOG_TRACE("Got maximal deviation of " << maxDiff << ".");
STORM_LOG_WARN_COND(sanityComparator.isZero(maxDiff), "Deviation " << maxDiff << " between computed value (" << quantitativeResult.getMax().getValues()[maxState] << ") and sanity check value (" << sanityValues[maxState] << ") in state " << maxState << " appears to be too high. (Obtained bounds were [" << quantitativeResult.getMin().getValues()[maxState] << ", " << quantitativeResult.getMax().getValues()[maxState] << "]");
STORM_LOG_WARN_COND(sanityComparator.isZero(maxDiff), "Deviation " << maxDiff << " between computed value (" << quantitativeResult.getMax().getValues()[maxState] << ") and sanity check value (" << sanityValues[maxState] << ") in state " << maxState << " appears to be too high. (Obtained bounds were [" << quantitativeResult.getMin().getValues()[maxState] << ", " << quantitativeResult.getMax().getValues()[maxState] << "].)");
if (!sanityComparator.isZero(maxDiff)) { if (!sanityComparator.isZero(maxDiff)) {
ExplicitGameExporter<ValueType> exporter;
storm::storage::BitVector newInitialStates(player1Groups.size() - 1);
newInitialStates.set(maxState);
exporter.exportToJson("game" + std::to_string(iteration) + "_min.json", player1Groups, player2Groups, transitionMatrix, newInitialStates, constraintStates, targetStates, quantitativeResult, &minStrategyPair, static_cast<ExplicitGameStrategyPair const*>(nullptr));
exporter.exportToJson("game" + std::to_string(iteration) + "_max.json", player1Groups, player2Groups, transitionMatrix, newInitialStates, constraintStates, targetStates, quantitativeResult, static_cast<ExplicitGameStrategyPair const*>(nullptr), &maxStrategyPair);
// Perform DFS from max diff state in upper system. // Perform DFS from max diff state in upper system.
std::vector<uint64_t> stack; std::vector<uint64_t> stack;
stack.push_back(maxState); stack.push_back(maxState);
@ -1019,6 +1201,8 @@ namespace storm {
if (!targetStates.get(successor)) { if (!targetStates.get(successor)) {
reachable.set(successor); reachable.set(successor);
stack.push_back(successor); stack.push_back(successor);
} else {
std::cout << "found target state " << std::endl;
} }
} }
} }
@ -1176,7 +1360,7 @@ namespace storm {
// Post-process strategies for better refinements. // Post-process strategies for better refinements.
storm::utility::Stopwatch strategyProcessingWatch(true); storm::utility::Stopwatch strategyProcessingWatch(true);
postProcessStrategies(player1Direction, minStrategyPair, maxStrategyPair, player1Groups, player2RowGrouping, transitionMatrix, constraintStates, targetStates, quantitativeResult, this->fixPlayer1Strategy, this->fixPlayer2Strategy, this->debug);
postProcessStrategies(this->iteration, player1Direction, minStrategyPair, maxStrategyPair, player1Groups, player2RowGrouping, transitionMatrix, initialStates, constraintStates, targetStates, quantitativeResult, this->fixPlayer1Strategy, this->fixPlayer2Strategy, this->debug);
strategyProcessingWatch.stop(); strategyProcessingWatch.stop();
totalStrategyProcessingWatch.add(strategyProcessingWatch); totalStrategyProcessingWatch.add(strategyProcessingWatch);
STORM_LOG_DEBUG("Postprocessed strategies in " << strategyProcessingWatch.getTimeInMilliseconds() << "ms."); STORM_LOG_DEBUG("Postprocessed strategies in " << strategyProcessingWatch.getTimeInMilliseconds() << "ms.");

40
src/storm/utility/constants.h
View File

@ -30,6 +30,46 @@ namespace storm {
namespace utility { namespace utility {
namespace detail {
template<typename ValueType>
struct ElementLess {
typedef std::less<ValueType> type;
};
struct DoubleLess {
bool operator()(double a, double b) const {
return b - a > 1e-17;
}
};
template<>
struct ElementLess<double> {
typedef DoubleLess type;
};
template<typename ValueType>
struct ElementGreater {
typedef std::greater<ValueType> type;
};
struct DoubleGreater {
bool operator()(double a, double b) const {
return a - b > 1e-17;
}
};
template<>
struct ElementGreater<double> {
typedef DoubleGreater type;
};
}
template<typename ValueType>
using ElementLess = typename detail::ElementLess<ValueType>::type;
template<typename ValueType>
using ElementGreater = typename detail::ElementGreater<ValueType>::type;
template<typename ValueType> template<typename ValueType>
ValueType one(); ValueType one();

10
src/storm/utility/vector.h
View File

@ -727,7 +727,7 @@ namespace storm {
if (choices && f(*targetIt, oldSelectedChoiceValue)) { if (choices && f(*targetIt, oldSelectedChoiceValue)) {
uint64_t distance = std::distance(target.begin(), targetIt); uint64_t distance = std::distance(target.begin(), targetIt);
if (distance == 1693 || distance == 4715 || distance == 4713) { if (distance == 1693 || distance == 4715 || distance == 4713) {
std::cout << "improving value at " << distance << ": moving from " << *choiceIt << " to " << selectedChoice << " because " << *targetIt << " is better than " << oldSelectedChoiceValue << std::endl;
std::cout << std::setprecision(50) << "improving value at " << distance << ": moving from " << *choiceIt << " to " << selectedChoice << " because " << *targetIt << " is better than " << oldSelectedChoiceValue << std::endl;
} }
*choiceIt = selectedChoice; *choiceIt = selectedChoice;
} }
@ -755,13 +755,13 @@ namespace storm {
*/ */
template<class T> template<class T>
void reduceVectorMin(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) { void reduceVectorMin(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) {
reduceVector<T, std::less<T>>(source, target, rowGrouping, choices);
reduceVector<T, storm::utility::ElementLess<T>>(source, target, rowGrouping, choices);
} }
#ifdef STORM_HAVE_INTELTBB #ifdef STORM_HAVE_INTELTBB
template<class T> template<class T>
void reduceVectorMinParallel(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) { void reduceVectorMinParallel(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) {
reduceVector<T, std::less<T>>(source, target, rowGrouping, choices);
reduceVector<T, storm::utility::ElementLess<T>>(source, target, rowGrouping, choices);
} }
#endif #endif
@ -775,13 +775,13 @@ namespace storm {
*/ */
template<class T> template<class T>
void reduceVectorMax(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) { void reduceVectorMax(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) {
reduceVector<T, std::greater<T>>(source, target, rowGrouping, choices);
reduceVector<T, storm::utility::ElementGreater<T>>(source, target, rowGrouping, choices);
} }
#ifdef STORM_HAVE_INTELTBB #ifdef STORM_HAVE_INTELTBB
template<class T> template<class T>
void reduceVectorMaxParallel(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) { void reduceVectorMaxParallel(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) {
reduceVector<T, std::greater<T>>(source, target, rowGrouping, choices);
reduceVector<T, storm::utility::ElementGreater<T>>(source, target, rowGrouping, choices);
} }
#endif #endif

Write Preview
Loading…
Cancel
Save