From ae8a963c33a800eee41536f5bc1170f6f3733d4e Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 16 Nov 2016 11:53:56 +0100 Subject: [PATCH] added some debug output to JaniNextStateGenerator Former-commit-id: 2c116cf22b78d452bf441d1919a819efec178d95 [formerly 98c11d0ce2c041adf8cc32899325a28f9cbfb2fb] Former-commit-id: bc3a09342a3f36da5913c5f6b3a796c2993ddece --- src/builder/jit/StateBehaviour.cpp | 2 +- src/generator/JaniNextStateGenerator.cpp | 16 ++++++++++- src/generator/NextStateGenerator.cpp | 2 +- src/generator/PrismNextStateGenerator.cpp | 6 ++-- src/storage/expressions/SimpleValuation.cpp | 31 ++++++--------------- src/utility/storm.h | 2 +- 6 files changed, 31 insertions(+), 28 deletions(-) diff --git a/src/builder/jit/StateBehaviour.cpp b/src/builder/jit/StateBehaviour.cpp index 6ad82405e..ddb976a96 100644 --- a/src/builder/jit/StateBehaviour.cpp +++ b/src/builder/jit/StateBehaviour.cpp @@ -133,8 +133,8 @@ namespace storm { // If there is no previous Markovian choice, just move the Markovian choice to the front. if (index != 0) { std::swap(choices.front(), choice); - foundPreviousMarkovianChoice = true; } + foundPreviousMarkovianChoice = true; ++index; } } else { diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 2cf113f7d..539e01d9f 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -390,6 +390,9 @@ namespace storm { // Iterate over all automata. uint64_t automatonIndex = 0; + std::cout << "getting silent choices of state" << std::endl; + std::cout << unpackStateIntoValuation(state, this->variableInformation, *this->expressionManager).toString(true) << std::endl; + for (auto const& automaton : model.getAutomata()) { uint64_t location = locations[automatonIndex]; @@ -402,8 +405,10 @@ namespace storm { // Skip the command, if it is not enabled. if (!this->evaluator->asBool(edge.getGuard())) { + std::cout << "guard " << edge.getGuard() << " evaluates to false" << std::endl; continue; } + std::cout << "guard " << edge.getGuard() << " evaluates to true" << std::endl; // Determine the exit rate if it's a Markovian edge. boost::optional exitRate = boost::none; @@ -422,6 +427,7 @@ namespace storm { if (probability != storm::utility::zero()) { // Obtain target state index and add it to the list of known states. If it has not yet been // seen, we also add it to the set of states that have yet to be explored. + std::cout << "got new state " << unpackStateIntoValuation(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]), this->variableInformation, *this->expressionManager).toString(true) << std::endl; StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex])); // Update the choice by adding the probability/target state to it. @@ -453,6 +459,9 @@ namespace storm { std::vector> JaniNextStateGenerator::getNonsilentActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) { std::vector> result; + std::cout << "getting nonsilent choices of state" << std::endl; + std::cout << unpackStateIntoValuation(state, this->variableInformation, *this->expressionManager).toString(true) << std::endl; + for (uint64_t actionIndex : model.getNonsilentActionIndices()) { std::vector> enabledEdges = getEnabledEdges(locations, actionIndex); @@ -530,9 +539,14 @@ namespace storm { // Add the probabilities/rates to the newly created choice. ValueType probabilitySum = storm::utility::zero(); for (auto const& stateProbabilityPair : *newTargetStates) { + std::cout << "got new state (sync)" << std::endl; + std::cout << unpackStateIntoValuation(stateProbabilityPair.first, this->variableInformation, *this->expressionManager).toString(true) << std::endl; StateType actualIndex = stateToIdCallback(stateProbabilityPair.first); choice.addProbability(actualIndex, stateProbabilityPair.second); - probabilitySum += stateProbabilityPair.second; + + if (this->options.isExplorationChecksSet()) { + probabilitySum += stateProbabilityPair.second; + } } if (this->options.isExplorationChecksSet()) { diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index 0c2d62601..8c13d62d8 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -127,8 +127,8 @@ namespace storm { // If there is no previous Markovian choice, just move the Markovian choice to the front. if (index != 0) { std::swap(result.getChoices().front(), choice); - foundPreviousMarkovianChoice = true; } + foundPreviousMarkovianChoice = true; ++index; } } else { diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index b9fa22957..da6c32214 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -385,7 +385,7 @@ namespace storm { if (!this->evaluator->asBool(command.getGuardExpression())) { continue; } - + result.push_back(Choice(command.getActionIndex(), command.isMarkovian())); Choice& choice = result.back(); @@ -407,7 +407,9 @@ namespace storm { // Update the choice by adding the probability/target state to it. choice.addProbability(stateIndex, probability); - probabilitySum += probability; + if (this->options.isExplorationChecksSet()) { + probabilitySum += probability; + } } } diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index 2f241958a..e92251f54 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/src/storage/expressions/SimpleValuation.cpp @@ -110,27 +110,16 @@ namespace storm { return "[" + boost::join(assignments, ", ") + "]"; } - std::string SimpleValuation::toString(bool pretty) const { - std::stringstream sstr; - if(pretty) { - sstr << "valuation {" << std::endl; - for(auto const& e : getManager()) { - sstr << e.first.getName() << "="; - if (e.first.hasBooleanType()) { - sstr << std::boolalpha << this->getBooleanValue(e.first) << std::noboolalpha; - } else if (e.first.hasIntegerType()) { - sstr << this->getIntegerValue(e.first); - } else if (e.first.hasRationalType()) { - sstr << this->getRationalValue(e.first); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type."); - } - sstr << std::endl; + if (pretty) { + std::set allVariables; + for (auto const& e : getManager()) { + allVariables.insert(e.first); } - sstr << "}"; + return toPrettyString(allVariables); } else { - sstr << "valuation {" << std::endl; + std::stringstream sstr; + sstr << "[" << std::endl; sstr << getManager() << std::endl; if (!booleanValues.empty()) { for (auto const& element : booleanValues) { @@ -150,11 +139,9 @@ namespace storm { } sstr << std::endl; } - sstr << "}"; + sstr << "]"; + return sstr.str(); } - - - return sstr.str(); } std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation) { diff --git a/src/utility/storm.h b/src/utility/storm.h index 7d8ac5526..14176636e 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -226,7 +226,7 @@ namespace storm { if (model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) { std::shared_ptr> ma = model->template as>(); if (ma->hasOnlyTrivialNondeterminism()) { - // Markov automaton can be converted into CTMC + // Markov automaton can be converted into CTMC. model = ma->convertToCTMC(); } }