diff --git a/examples/dft/and_approx.dft b/examples/dft/and_approx.dft new file mode 100644 index 000000000..ff6393dd5 --- /dev/null +++ b/examples/dft/and_approx.dft @@ -0,0 +1,5 @@ +toplevel "A"; +"A" and "B" "C" "D"; +"B" lambda=1 dorm=0; +"C" lambda=100 dorm=0; +"D" lambda=50 dorm=0; diff --git a/examples/dft/and_approx_param.dft b/examples/dft/and_approx_param.dft new file mode 100644 index 000000000..bbd00bd80 --- /dev/null +++ b/examples/dft/and_approx_param.dft @@ -0,0 +1,6 @@ +param x; +toplevel "A"; +"A" and "B" "C" "D"; +"B" lambda=1 dorm=0; +"C" lambda=100 dorm=0; +"D" lambda=100*x dorm=0; diff --git a/examples/dft/nonmonoton.dft b/examples/dft/nonmonoton.dft new file mode 100644 index 000000000..0575028e8 --- /dev/null +++ b/examples/dft/nonmonoton.dft @@ -0,0 +1,6 @@ +toplevel "A"; +"A" or "B" "Z"; +"B" pand "D" "S"; +"Z" lambda=1 dorm=0; +"D" lambda=100 dorm=0; +"S" lambda=50 dorm=0; diff --git a/src/generator/DftNextStateGenerator.cpp b/src/generator/DftNextStateGenerator.cpp new file mode 100644 index 000000000..b56f8a358 --- /dev/null +++ b/src/generator/DftNextStateGenerator.cpp @@ -0,0 +1,156 @@ +#include "src/generator/DftNextStateGenerator.h" + +#include "src/utility/constants.h" +#include "src/utility/macros.h" +#include "src/exceptions/WrongFormatException.h" + +namespace storm { + namespace generator { + + template + DftNextStateGenerator::DftNextStateGenerator(storm::storage::DFT const& dft) : mDft(dft), state(nullptr), comparator() { + // Intentionally left empty. + } + + template + bool DftNextStateGenerator::isDeterministicModel() const { + assert(false); + return true; + } + + template + std::vector DftNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { + // FIXME: This only works for models with exactly one initial state. We should make this more general. + /*CompressedState initialState(variableInformation.getTotalBitOffset()); + + // We need to initialize the values of the variables to their initial value. + for (auto const& booleanVariable : variableInformation.booleanVariables) { + initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue); + } + for (auto const& integerVariable : variableInformation.integerVariables) { + initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(integerVariable.initialValue - integerVariable.lowerBound)); + } + + // Register initial state and return it. + StateType id = stateToIdCallback(initialState); + return {id};*/ + } + + template + void DftNextStateGenerator::load(std::shared_ptr> const& state) { + /*// Since almost all subsequent operations are based on the evaluator, we load the state into it now. + unpackStateIntoEvaluator(state, variableInformation, evaluator); + + // Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it. + this->state = &state;*/ + } + + template + bool DftNextStateGenerator::satisfies(storm::expressions::Expression const& expression) const { + /* if (expression.isTrue()) { + return true; + } + return evaluator.asBool(expression);*/ + } + + template + StateBehavior DftNextStateGenerator::expand(StateToIdCallback const& stateToIdCallback) { + /*// Prepare the result, in case we return early. + StateBehavior result; + + // First, construct the state rewards, as we may return early if there are no choices later and we already + // need the state rewards then. + for (auto const& rewardModel : selectedRewardModels) { + ValueType stateRewardValue = storm::utility::zero(); + if (rewardModel.get().hasStateRewards()) { + for (auto const& stateReward : rewardModel.get().getStateRewards()) { + if (evaluator.asBool(stateReward.getStatePredicateExpression())) { + stateRewardValue += ValueType(evaluator.asRational(stateReward.getRewardValueExpression())); + } + } + } + result.addStateReward(stateRewardValue); + } + + // If a terminal expression was set and we must not expand this state, return now. + if (terminalExpression && evaluator.asBool(terminalExpression.get())) { + return result; + } + + // Get all choices for the state. + std::vector> allChoices = getUnlabeledChoices(*this->state, stateToIdCallback); + std::vector> allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback); + for (auto& choice : allLabeledChoices) { + allChoices.push_back(std::move(choice)); + } + + std::size_t totalNumberOfChoices = allChoices.size(); + + // If there is not a single choice, we return immediately, because the state has no behavior (other than + // the state reward). + if (totalNumberOfChoices == 0) { + return result; + } + + // If the model is a deterministic model, we need to fuse the choices into one. + if (program.isDeterministicModel() && totalNumberOfChoices > 1) { + Choice globalChoice; + + // For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs + // this is equal to the number of choices, which is why we initialize it like this here. + ValueType totalExitRate = program.isDiscreteTimeModel() ? static_cast(totalNumberOfChoices) : storm::utility::zero(); + + // Iterate over all choices and combine the probabilities/rates into one choice. + for (auto const& choice : allChoices) { + for (auto const& stateProbabilityPair : choice) { + if (program.isDiscreteTimeModel()) { + globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second / totalNumberOfChoices); + } else { + globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second); + } + } + + if (hasStateActionRewards && !program.isDiscreteTimeModel()) { + totalExitRate += choice.getTotalMass(); + } + + if (buildChoiceLabeling) { + globalChoice.addChoiceLabels(choice.getChoiceLabels()); + } + } + + // Now construct the state-action reward for all selected reward models. + for (auto const& rewardModel : selectedRewardModels) { + ValueType stateActionRewardValue = storm::utility::zero(); + if (rewardModel.get().hasStateActionRewards()) { + for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) { + for (auto const& choice : allChoices) { + if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) { + stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate; + } + } + + } + } + globalChoice.addChoiceReward(stateActionRewardValue); + } + + // Move the newly fused choice in place. + allChoices.clear(); + allChoices.push_back(std::move(globalChoice)); + } + + // Move all remaining choices in place. + for (auto& choice : allChoices) { + result.addChoice(std::move(choice)); + } + + result.setExpanded(); + return result;*/ + } + + + template class DftNextStateGenerator; + template class DftNextStateGenerator; + } +} \ No newline at end of file diff --git a/src/generator/DftNextStateGenerator.h b/src/generator/DftNextStateGenerator.h new file mode 100644 index 000000000..6c8e5538d --- /dev/null +++ b/src/generator/DftNextStateGenerator.h @@ -0,0 +1,40 @@ +#ifndef STORM_GENERATOR_DFTNEXTSTATEGENERATOR_H_ +#define STORM_GENERATOR_DFTNEXTSTATEGENERATOR_H_ + +#include "src/generator/NextStateGenerator.h" +#include "src/storage/dft/DFT.h" + +#include "src/utility/ConstantsComparator.h" + +namespace storm { + namespace generator { + + template + class DftNextStateGenerator : public NextStateGenerator>, StateType> { + public: + typedef typename NextStateGenerator>, StateType>::StateToIdCallback StateToIdCallback; + + DftNextStateGenerator(storm::storage::DFT const& dft); + + virtual bool isDeterministicModel() const override; + virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) override; + + virtual void load(std::shared_ptr> const& state) override; + virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) override; + virtual bool satisfies(storm::expressions::Expression const& expression) const override; + + private: + + // The program used for the generation of next states. + storm::storage::DFT const& mDft; + + CompressedState const* state; + + // A comparator used to compare constants. + storm::utility::ConstantsComparator comparator; + }; + + } +} + +#endif /* STORM_GENERATOR_DFTNEXTSTATEGENERATOR_H_ */ \ No newline at end of file