From f8a442ae0bca4da9ce1663aa9f9b313b63d1f844 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 26 Sep 2018 20:39:10 +0200 Subject: [PATCH] clean-up of jani next state generator --- .../generator/JaniNextStateGenerator.cpp | 76 ------------------- src/storm/generator/JaniNextStateGenerator.h | 7 -- 2 files changed, 83 deletions(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 799a82e93..1d74a59b5 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -539,10 +539,6 @@ namespace storm { if (!edge.getAssignments().empty()) { transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator); } - - - auto valueIt = stateActionRewards.begin(); - // performTransientAssignments(edge.getAssignments().getTransientAssignments(), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); // Iterate over all updates of the current command. ValueType probabilitySum = storm::utility::zero(); @@ -563,9 +559,6 @@ namespace storm { applyTransientUpdate(transientVariableValuation, destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator); transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet()); evaluatorChanged = true; - // Create the rewards for this destination - auto valueIt = stateActionRewards.begin(); - // performTransientAssignments(destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&] (ValueType const& value) { *valueIt += (value * probability); ++valueIt; } ); } if (assignmentLevel < highestLevel) { while (assignmentLevel < highestLevel) { @@ -578,9 +571,6 @@ namespace storm { applyTransientUpdate(transientVariableValuation, destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator); transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet()); evaluatorChanged = true; - // update the rewards for this destination - auto valueIt = stateActionRewards.begin(); - // performTransientAssignments(destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&] (ValueType const& value) { *valueIt += (value * probability); ++valueIt; } ); } } } @@ -618,33 +608,6 @@ namespace storm { return choice; } - template - void JaniNextStateGenerator::generateSynchronizedDistribution(storm::storage::BitVector const& state, ValueType const& probability, uint64_t position, AutomataEdgeSets const& edgeCombination, std::vector const& iteratorList, storm::builder::jit::Distribution& distribution, std::vector& stateActionRewards, EdgeIndexSet& edgeIndices, StateToIdCallback stateToIdCallback) { - - if (storm::utility::isZero(probability)) { - return; - } - - if (position >= iteratorList.size()) { - StateType id = stateToIdCallback(state); - distribution.add(id, probability); - } else { - auto const& indexAndEdge = *iteratorList[position]; - auto const& edge = *indexAndEdge.second; - - for (auto const& destination : edge.getDestinations()) { - generateSynchronizedDistribution(applyUpdate(state, destination, this->variableInformation.locationVariables[edgeCombination[position].first], 0, *this->evaluator), probability * this->evaluator->asRational(destination.getProbability()), position + 1, edgeCombination, iteratorList, distribution, stateActionRewards, edgeIndices, stateToIdCallback); - } - - if (this->getOptions().isBuildChoiceOriginsSet()) { - edgeIndices.insert(model.encodeAutomatonAndEdgeIndices(edgeCombination[position].first, indexAndEdge.first)); - } - - auto valueIt = stateActionRewards.begin(); - performTransientAssignments(edge.getAssignments().getTransientAssignments(), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); - } - } - template void JaniNextStateGenerator::generateSynchronizedDistribution(storm::storage::BitVector const& state, AutomataEdgeSets const& edgeCombination, std::vector const& iteratorList, storm::builder::jit::Distribution& distribution, std::vector& stateActionRewards, EdgeIndexSet& edgeIndices, StateToIdCallback stateToIdCallback) { @@ -716,10 +679,6 @@ namespace storm { successorState = applyUpdate(successorState, *destinations.back(), *locationVars.back(), lowestDestinationAssignmentLevel, *this->evaluator); applyTransientUpdate(transientVariableValuation, destinations.back()->getOrderedAssignments().getTransientAssignments(lowestDestinationAssignmentLevel), *this->evaluator); - - // add the reward for this destination to the destination rewards - //auto valueIt = destinationRewards.begin(); - //performTransientAssignments(destinations.back()->getOrderedAssignments().getTransientAssignments(lowestDestinationAssignmentLevel), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); } @@ -735,9 +694,6 @@ namespace storm { for (auto const& destPtr : destinations) { successorState = applyUpdate(successorState, *destPtr, **locationVarIt, assignmentLevel, *this->evaluator); applyTransientUpdate(transientVariableValuation, destinations.back()->getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator); - // add the reward for this destination to the destination rewards - // auto valueIt = destinationRewards.begin(); - // performTransientAssignments(destinations.back()->getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); ++locationVarIt; } } @@ -966,38 +922,6 @@ namespace storm { return NextStateGenerator::label(stateStorage, initialStateIndices, deadlockStateIndices, transientVariableExpressions); } - template - void JaniNextStateGenerator::performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator const& expressionEvaluator, std::function const& callback) { - /* - // If there are no reward variables, there is no need to iterate at all. - if (rewardExpressions.empty()) { - return; - } - - // Otherwise, perform the callback for all selected reward variables. - auto rewardVariableIt = rewardExpressions.begin(); - auto rewardVariableIte = rewardExpressions.end(); - for (auto const& assignment : transientAssignments) { - STORM_LOG_ASSERT(assignment.getLValue().isVariable(), "Transient assignments to non-variable LValues are not supported."); - while (rewardVariableIt != rewardVariableIte && *rewardVariableIt < assignment.getExpressionVariable()) { - callback(storm::utility::zero()); - ++rewardVariableIt; - } - if (rewardVariableIt == rewardVariableIte) { - break; - } else if (*rewardVariableIt == assignment.getExpressionVariable()) { - callback(ValueType(expressionEvaluator.asRational(assignment.getAssignedExpression()))); - ++rewardVariableIt; - } - } - // Add a value of zero for all variables that have no assignment. - for (; rewardVariableIt != rewardVariableIte; ++rewardVariableIt) { - callback(storm::utility::zero()); - } - */ - } - - template std::vector JaniNextStateGenerator::evaluateRewardExpressions() const { std::vector result; diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index 628032575..290ea3cdd 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -114,7 +114,6 @@ namespace storm { typedef std::vector AutomataEdgeSets; std::vector> expandSynchronizingEdgeCombination(AutomataEdgeSets const& edgeCombination, uint64_t outputActionIndex, CompressedState const& state, StateToIdCallback stateToIdCallback); - void generateSynchronizedDistribution(storm::storage::BitVector const& state, ValueType const& probability, uint64_t position, AutomataEdgeSets const& edgeCombination, std::vector const& iteratorList, storm::builder::jit::Distribution& distribution, std::vector& stateActionRewards, EdgeIndexSet& edgeIndices, StateToIdCallback stateToIdCallback); void generateSynchronizedDistribution(storm::storage::BitVector const& state, AutomataEdgeSets const& edgeCombination, std::vector const& iteratorList, storm::builder::jit::Distribution& distribution, std::vector& stateActionRewards, EdgeIndexSet& edgeIndices, StateToIdCallback stateToIdCallback); /*! @@ -122,12 +121,6 @@ namespace storm { */ void checkGlobalVariableWritesValid(AutomataEdgeSets const& enabledEdges) const; - /*! - * Treats the given transient assignments by calling the callback function whenever a transient assignment - * to one of the reward variables of this generator is performed. - */ - void performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator const& expressionEvaluator, std::function const& callback); - /*! * Evaluates the reward expressions using the current evaluator */