#ifndef STORM_ADAPTERS_EXPLICITPRISMMODELBUILDER_H #define STORM_ADAPTERS_EXPLICITPRISMMODELBUILDER_H #include #include #include #include #include #include #include #include #include #include "src/storage/prism/Program.h" #include "src/storage/expressions/SimpleValuation.h" #include "src/storage/expressions/ExpressionEvaluator.h" #include "src/storage/BitVectorHashMap.h" #include "src/logic/Formulas.h" #include "src/models/sparse/StateAnnotation.h" #include "src/models/sparse/Model.h" #include "src/models/sparse/StateLabeling.h" #include "src/storage/SparseMatrix.h" #include "src/settings/SettingsManager.h" #include "src/utility/constants.h" #include "src/utility/prism.h" namespace storm { namespace utility { template class ConstantsComparator; } namespace builder { using namespace storm::utility::prism; // Forward-declare classes. template struct RewardModelBuilder; template, typename IndexType = uint32_t> class ExplicitPrismModelBuilder { public: typedef storm::storage::BitVector CompressedState; // A structure holding information about the reachable state space while building it. struct InternalStateInformation { InternalStateInformation(uint64_t bitsPerState); // This member stores all the states and maps them to their unique indices. storm::storage::BitVectorHashMap stateStorage; // A list of initial states in terms of their global indices. std::vector initialStateIndices; // The number of bits of each state. uint64_t bitsPerState; // A list of reachable states as indices in the stateToIndexMap. std::vector reachableStates; }; // A structure holding information about the reachable state space that can be retrieved from the outside. struct StateInformation : public storm::models::sparse::StateAnnotation { /*! * Constructs a state information object for the given number of states. */ StateInformation(uint_fast64_t numberOfStates); // A mapping from state indices to their variable valuations. std::vector valuations; std::string stateInfo(uint_fast64_t state) const override { return valuations[state].toString(); } }; // A structure storing information about the used variables of the program. struct VariableInformation { VariableInformation(storm::expressions::ExpressionManager const& manager); struct BooleanVariableInformation { BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset); // The boolean variable. storm::expressions::Variable variable; // Its initial value. bool initialValue; // Its bit offset in the compressed state. uint_fast64_t bitOffset; }; struct IntegerVariableInformation { IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth); // The integer variable. storm::expressions::Variable variable; // Its initial value. int_fast64_t initialValue; // The lower bound of its range. int_fast64_t lowerBound; // The upper bound of its range. int_fast64_t upperBound; // Its bit offset in the compressed state. uint_fast64_t bitOffset; // Its bit width in the compressed state. uint_fast64_t bitWidth; }; // Provide methods to access the bit offset and width of variables in the compressed state. uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const; uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const; // The known boolean variables. boost::container::flat_map booleanVariableToIndexMap; std::vector booleanVariables; // The known integer variables. boost::container::flat_map integerVariableToIndexMap; std::vector integerVariables; storm::expressions::ExpressionManager const& manager; }; // A structure holding the individual components of a model. struct ModelComponents { ModelComponents(); // The transition matrix. storm::storage::SparseMatrix transitionMatrix; // The state labeling. storm::models::sparse::StateLabeling stateLabeling; // The reward models associated with the model. std::unordered_map> rewardModels; // A vector that stores a labeling for each choice. boost::optional>> choiceLabeling; }; struct Options { /*! * Creates an object representing the default building options. */ Options(); /*! Creates an object representing the suggested building options assuming that the given formula is the * only one to check. Additional formulas may be preserved by calling preserveFormula. * * @param formula The formula based on which to choose the building options. */ Options(storm::logic::Formula const& formula); /*! Creates an object representing the suggested building options assuming that the given formulas are * the only ones to check. Additional formulas may be preserved by calling preserveFormula. * * @param formula Thes formula based on which to choose the building options. */ Options(std::vector> const& formulas); /*! * Sets the constants definitions from the given string. The string must be of the form 'X=a,Y=b,Z=c', * etc. where X,Y,Z are the variable names and a,b,c are the values of the constants. * * @param program The program managing the constants that shall be defined. Note that the program itself * is not modified whatsoever. * @param constantDefinitionString The string from which to parse the constants' values. */ void addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString); /*! * Changes the options in a way that ensures that the given formula can be checked on the model once it * has been built. * * @param formula The formula that is to be ''preserved''. */ void preserveFormula(storm::logic::Formula const& formula); /*! * Analyzes the given formula and sets an expression for the states states of the model that can be * treated as terminal states. Note that this may interfere with checking properties different than the * one provided. * * @param formula The formula used to (possibly) derive an expression for the terminal states of the * model. */ void setTerminalStatesFromFormula(storm::logic::Formula const& formula); // A flag that indicates whether or not command labels are to be built. bool buildCommandLabels; // A flag that indicates whether or not all reward models are to be build. bool buildAllRewardModels; // A flag that indicates whether or not to store the state information after successfully building the // model. If it is to be preserved, it can be retrieved via the appropriate methods after a successful // call to translateProgram. bool buildStateInformation; // A list of reward models to be build in case not all reward models are to be build. std::set rewardModelsToBuild; // An optional mapping that, if given, contains defining expressions for undefined constants. boost::optional> constantDefinitions; // A flag that indicates whether all labels are to be build. bool buildAllLabels; // An optional set of labels that, if given, restricts the labels that are built. boost::optional> labelsToBuild; // An optional set of expressions for which labels need to be built. boost::optional> expressionLabels; // An optional expression or label that characterizes (a subset of) the terminal states of the model. If // this is set, the outgoing transitions of these states are replaced with a self-loop. boost::optional> terminalStates; // An optional expression or label whose negation characterizes (a subset of) the terminal states of the // model. If this is set, the outgoing transitions of these states are replaced with a self-loop. boost::optional> negatedTerminalStates; }; /*! * Convert the program given at construction time to an abstract model. The type of the model is the one * specified in the program. The given reward model name selects the rewards that the model will contain. * * @param program The program to translate. * @param constantDefinitionString A string that contains a comma-separated definition of all undefined * constants in the model. * @param rewardModel The reward model that is to be built. * @return The explicit model that was given by the probabilistic program. */ std::shared_ptr> translateProgram(storm::prism::Program program, Options const& options = Options()); /*! * If requested in the options, information about the variable valuations in the reachable states can be * retrieved via this function. * * @return A structure that stores information about all reachable states. */ StateInformation const& getStateInformation() const; /*! * Retrieves the program that was actually translated (i.e. including constant substitutions etc.). Note * that this function may only be called after a succesful translation. * * @return The translated program. */ storm::prism::Program const& getTranslatedProgram() const; private: static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); static storm::expressions::SimpleValuation unpackStateIntoValuation(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation); /*! * Applies an update to the given state and returns the resulting new state object. This methods does not * modify the given state but returns a new one. * * @params state The state to which to apply the update. * @params update The update to apply. * @return The resulting state. */ static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator const& evaluator); /*! * Applies an update to the given state and returns the resulting new state object. The update is evaluated * over the variable values of the given base state. This methods does not modify the given state but * returns a new one. * * @param state The state to which to apply the update. * @param baseState The state used for evaluating the update. * @param update The update to apply. * @return The resulting state. */ static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator const& evaluator); /*! * Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to * the lists of all states with a new id. If the state was already known, the object that is pointed to by * the given state pointer is deleted and the old state id is returned. Note that the pointer should not be * used after invoking this method. * * @param state A pointer to a state for which to retrieve the index. This must not be used after the call. * @param internalStateInformation The information about the already explored part of the reachable state space. * @return A pair indicating whether the state was already discovered before and the state id of the state. */ static IndexType getOrAddStateIndex(CompressedState const& state, InternalStateInformation& internalStateInformation, std::queue& stateQueue); /*! * Retrieves all commands that are labeled with the given label and enabled in the given state, grouped by * modules. * * This function will iterate over all modules and retrieve all commands that are labeled with the given * action and active (i.e. enabled) in the current state. The result is a list of lists of commands in which * the inner lists contain all commands of exactly one module. If a module does not have *any* (including * disabled) commands, there will not be a list of commands of that module in the result. If, however, the * module has a command with a relevant label, but no enabled one, nothing is returned to indicate that there * is no legal transition possible. * * @param The program in which to search for active commands. * @param state The current state. * @param actionIndex The index of the action label to select. * @return A list of lists of active commands or nothing. */ static boost::optional>>> getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator const& evaluator, uint_fast64_t const& actionIndex); static std::vector> getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator); static std::vector> getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator); /*! * Builds the transition matrix and the transition reward matrix based for the given program. * * @param program The program for which to build the matrices. * @param variableInformation A structure containing information about the variables in the program. * @param transitionRewards A list of transition rewards that are to be considered in the transition reward * matrix. * @param internalStateInformation A structure containing information about the states of the program. * @param deterministicModel A flag indicating whether the model is supposed to be deterministic or not. * @param transitionMatrix A reference to an initialized matrix which is filled with all transitions by this * function. * @param rewardModelBuilders A vector of reward model builders that is used to build the vector of selected * reward models. * @param terminalExpression If given, terminal states are not explored further. * @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin * and a vector containing the labels associated with each choice. */ static boost::optional>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector> const& selectedRewardModels, InternalStateInformation& internalStateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression); /*! * Explores the state space of the given program and returns the components of the model as a result. * * @param program The program whose state space to explore. * @param selectedRewardModels The reward models that are to be considered. * @param options A set of options used to customize the building process. * @return A structure containing the components of the resulting model. */ ModelComponents buildModelComponents(storm::prism::Program const& program, std::vector> const& selectedRewardModels, Options const& options); /*! * Builds the state labeling for the given program. * * @param program The program for which to build the state labeling. * @param variableInformation Information about the variables in the program. * @param internalStateInformation Information about the state space of the program. * @return The state labeling of the given program. */ static storm::models::sparse::StateLabeling buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, InternalStateInformation const& internalStateInformation); // This member holds information about reachable states that can be retrieved from the outside after a // successful build. boost::optional stateInformation; // This member holds the program that was most recently translated (if any). boost::optional preparedProgram; }; } // namespace adapters } // namespace storm #endif /* STORM_ADAPTERS_EXPLICITPRISMMODELBUILDER_H */