Browse Source
started to restructure explicit model builder to make it fit for JANI models
started to restructure explicit model builder to make it fit for JANI models
Former-commit-id: 69603dd97b
main
dehnert
9 years ago
22 changed files with 628 additions and 616 deletions
-
165src/builder/ExplicitModelBuilder.cpp
-
178src/builder/ExplicitModelBuilder.h
-
268src/builder/ExplicitPrismModelBuilder.h
-
174src/generator/NextStateGenerator.cpp
-
111src/generator/NextStateGenerator.h
-
74src/generator/PrismNextStateGenerator.cpp
-
21src/generator/PrismNextStateGenerator.h
-
50src/generator/PrismStateLabelingGenerator.cpp
-
31src/generator/PrismStateLabelingGenerator.h
-
20src/generator/StateLabelingGenerator.h
-
4src/storage/prism/Program.cpp
-
8src/utility/storm.h
-
44test/functional/builder/ExplicitPrismModelBuilderTest.cpp
-
22test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
-
4test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
-
6test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
-
22test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
-
8test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
-
8test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
-
4test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
-
10test/functional/utility/GraphTest.cpp
-
12test/functional/utility/ModelInstantiatorTest.cpp
@ -0,0 +1,178 @@ |
|||||
|
#ifndef STORM_BUILDER_ExplicitModelBuilder_H |
||||
|
#define STORM_BUILDER_ExplicitModelBuilder_H |
||||
|
|
||||
|
#include <memory> |
||||
|
#include <utility> |
||||
|
#include <vector> |
||||
|
#include <deque> |
||||
|
#include <cstdint> |
||||
|
#include <boost/functional/hash.hpp> |
||||
|
#include <boost/container/flat_set.hpp> |
||||
|
#include <boost/container/flat_map.hpp> |
||||
|
#include <boost/variant.hpp> |
||||
|
#include <src/models/sparse/StandardRewardModel.h> |
||||
|
|
||||
|
#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/storage/sparse/StateValuations.h" |
||||
|
#include "src/storage/sparse/StateStorage.h" |
||||
|
#include "src/settings/SettingsManager.h" |
||||
|
|
||||
|
#include "src/utility/prism.h" |
||||
|
|
||||
|
#include "src/builder/ExplorationOrder.h" |
||||
|
|
||||
|
#include "src/generator/CompressedState.h" |
||||
|
#include "src/generator/VariableInformation.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace utility { |
||||
|
template<typename ValueType> class ConstantsComparator; |
||||
|
} |
||||
|
|
||||
|
namespace generator { |
||||
|
template<typename ValueType, typename StateType> |
||||
|
class NextStateGenerator; |
||||
|
} |
||||
|
|
||||
|
namespace builder { |
||||
|
|
||||
|
using namespace storm::utility::prism; |
||||
|
using namespace storm::generator; |
||||
|
|
||||
|
// Forward-declare classes. |
||||
|
template <typename ValueType> struct RewardModelBuilder; |
||||
|
|
||||
|
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t> |
||||
|
class ExplicitModelBuilder { |
||||
|
public: |
||||
|
// A structure holding the individual components of a model. |
||||
|
struct ModelComponents { |
||||
|
ModelComponents(); |
||||
|
|
||||
|
// The transition matrix. |
||||
|
storm::storage::SparseMatrix<ValueType> transitionMatrix; |
||||
|
|
||||
|
// The state labeling. |
||||
|
storm::models::sparse::StateLabeling stateLabeling; |
||||
|
|
||||
|
// The reward models associated with the model. |
||||
|
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<typename RewardModelType::ValueType>> rewardModels; |
||||
|
|
||||
|
// A vector that stores a labeling for each choice. |
||||
|
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling; |
||||
|
}; |
||||
|
|
||||
|
struct Options { |
||||
|
/*! |
||||
|
* Creates an object representing the default building options. |
||||
|
*/ |
||||
|
Options(); |
||||
|
|
||||
|
// The order in which to explore the model. |
||||
|
ExplorationOrder explorationOrder; |
||||
|
|
||||
|
// 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 <code>translateProgram</code>. |
||||
|
bool buildStateValuations; |
||||
|
}; |
||||
|
|
||||
|
/*! |
||||
|
* Creates an explicit model builder that uses the provided generator.. |
||||
|
* |
||||
|
* @param generator The generator to build. |
||||
|
*/ |
||||
|
ExplicitModelBuilder(std::shared_ptr<storm::generator::NextStateGenerator<ValueType, StateType>> const& generator, Options const& options = Options()); |
||||
|
|
||||
|
/*! |
||||
|
* 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<storm::models::sparse::Model<ValueType, RewardModelType>> translate(); |
||||
|
|
||||
|
/*! |
||||
|
* 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. |
||||
|
*/ |
||||
|
storm::storage::sparse::StateValuations const& getStateValuations() const; |
||||
|
|
||||
|
private: |
||||
|
/*! |
||||
|
* 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. |
||||
|
* @return A pair indicating whether the state was already discovered before and the state id of the state. |
||||
|
*/ |
||||
|
StateType getOrAddStateIndex(CompressedState const& state); |
||||
|
|
||||
|
/*! |
||||
|
* Builds the transition matrix and the transition reward matrix based for the given program. |
||||
|
* |
||||
|
* @param transitionMatrixBuilder The builder of the transition matrix. |
||||
|
* @param rewardModelBuilders The builders for the selected reward models. |
||||
|
* @param terminalExpression If given, states satisfying this expression 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. |
||||
|
*/ |
||||
|
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression); |
||||
|
|
||||
|
/*! |
||||
|
* Explores the state space of the given program and returns the components of the model as a result. |
||||
|
* |
||||
|
* @param selectedRewardModels The reward models that are to be considered. |
||||
|
* @return A structure containing the components of the resulting model. |
||||
|
*/ |
||||
|
ModelComponents buildModelComponents(std::vector<std::string> const& selectedRewardModels); |
||||
|
|
||||
|
/*! |
||||
|
* Builds the state labeling for the given program. |
||||
|
* |
||||
|
* @return The state labeling of the given program. |
||||
|
*/ |
||||
|
storm::models::sparse::StateLabeling buildStateLabeling(); |
||||
|
|
||||
|
/// The generator to use for the building process. |
||||
|
std::shared_ptr<storm::generator::NextStateGenerator<ValueType, StateType>> generator; |
||||
|
|
||||
|
/// The options to be used for the building process. |
||||
|
Options options; |
||||
|
|
||||
|
/// Internal information about the states that were explored. |
||||
|
storm::storage::sparse::StateStorage<StateType> stateStorage; |
||||
|
|
||||
|
/// This member holds information about reachable states that can be retrieved from the outside after a |
||||
|
/// successful build. |
||||
|
boost::optional<storm::storage::sparse::StateValuations> stateValuations; |
||||
|
|
||||
|
/// A set of states that still need to be explored. |
||||
|
std::deque<CompressedState> statesToExplore; |
||||
|
|
||||
|
/// An optional mapping from state indices to the row groups in which they actually reside. This needs to be |
||||
|
/// built in case the exploration order is not BFS. |
||||
|
boost::optional<std::vector<uint_fast64_t>> stateRemapping; |
||||
|
|
||||
|
}; |
||||
|
|
||||
|
} // namespace adapters |
||||
|
} // namespace storm |
||||
|
|
||||
|
#endif /* STORM_BUILDER_ExplicitModelBuilder_H */ |
||||
@ -1,268 +0,0 @@ |
|||||
#ifndef STORM_BUILDER_EXPLICITPRISMMODELBUILDER_H |
|
||||
#define STORM_BUILDER_EXPLICITPRISMMODELBUILDER_H |
|
||||
|
|
||||
#include <memory> |
|
||||
#include <utility> |
|
||||
#include <vector> |
|
||||
#include <deque> |
|
||||
#include <cstdint> |
|
||||
#include <boost/functional/hash.hpp> |
|
||||
#include <boost/container/flat_set.hpp> |
|
||||
#include <boost/container/flat_map.hpp> |
|
||||
#include <boost/variant.hpp> |
|
||||
#include <src/models/sparse/StandardRewardModel.h> |
|
||||
|
|
||||
#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/storage/sparse/StateValuations.h" |
|
||||
#include "src/storage/sparse/StateStorage.h" |
|
||||
#include "src/settings/SettingsManager.h" |
|
||||
|
|
||||
#include "src/utility/prism.h" |
|
||||
|
|
||||
#include "src/builder/ExplorationOrder.h" |
|
||||
|
|
||||
#include "src/generator/CompressedState.h" |
|
||||
#include "src/generator/VariableInformation.h" |
|
||||
|
|
||||
namespace storm { |
|
||||
namespace utility { |
|
||||
template<typename ValueType> class ConstantsComparator; |
|
||||
} |
|
||||
|
|
||||
namespace builder { |
|
||||
|
|
||||
using namespace storm::utility::prism; |
|
||||
using namespace storm::generator; |
|
||||
|
|
||||
// Forward-declare classes. |
|
||||
template <typename ValueType> struct RewardModelBuilder; |
|
||||
|
|
||||
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t> |
|
||||
class ExplicitPrismModelBuilder { |
|
||||
public: |
|
||||
// A structure holding the individual components of a model. |
|
||||
struct ModelComponents { |
|
||||
ModelComponents(); |
|
||||
|
|
||||
// The transition matrix. |
|
||||
storm::storage::SparseMatrix<ValueType> transitionMatrix; |
|
||||
|
|
||||
// The state labeling. |
|
||||
storm::models::sparse::StateLabeling stateLabeling; |
|
||||
|
|
||||
// The reward models associated with the model. |
|
||||
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<typename RewardModelType::ValueType>> rewardModels; |
|
||||
|
|
||||
// A vector that stores a labeling for each choice. |
|
||||
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling; |
|
||||
}; |
|
||||
|
|
||||
struct Options { |
|
||||
/*! |
|
||||
* Creates an object representing the default building options. |
|
||||
*/ |
|
||||
Options(); |
|
||||
|
|
||||
/*! |
|
||||
* Copies the given set of options. |
|
||||
*/ |
|
||||
Options(Options const& other) = default; |
|
||||
|
|
||||
/*! 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 <code>preserveFormula</code>. |
|
||||
* |
|
||||
* @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 <code>preserveFormula</code>. |
|
||||
* |
|
||||
* @param formula Thes formula based on which to choose the building options. |
|
||||
*/ |
|
||||
Options(std::vector<std::shared_ptr<storm::logic::Formula const>> 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); |
|
||||
|
|
||||
// The order in which to explore the model. |
|
||||
ExplorationOrder explorationOrder; |
|
||||
|
|
||||
// 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 <code>translateProgram</code>. |
|
||||
bool buildStateValuations; |
|
||||
|
|
||||
// A list of reward models to be build in case not all reward models are to be build. |
|
||||
std::set<std::string> rewardModelsToBuild; |
|
||||
|
|
||||
// An optional mapping that, if given, contains defining expressions for undefined constants. |
|
||||
boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> 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<std::set<std::string>> labelsToBuild; |
|
||||
|
|
||||
// An optional set of expressions for which labels need to be built. |
|
||||
boost::optional<std::vector<storm::expressions::Expression>> 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<boost::variant<storm::expressions::Expression, std::string>> 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<boost::variant<storm::expressions::Expression, std::string>> negatedTerminalStates; |
|
||||
}; |
|
||||
|
|
||||
/*! |
|
||||
* Creates a builder for the given program. |
|
||||
* |
|
||||
* @param program The program to build. |
|
||||
*/ |
|
||||
ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options = Options()); |
|
||||
|
|
||||
/*! |
|
||||
* 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<storm::models::sparse::Model<ValueType, RewardModelType>> translate(); |
|
||||
|
|
||||
/*! |
|
||||
* 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. |
|
||||
*/ |
|
||||
storm::storage::sparse::StateValuations const& getStateValuations() const; |
|
||||
|
|
||||
/*! |
|
||||
* Retrieves the program that was actually translated (i.e. including constant substitutions etc.). |
|
||||
* |
|
||||
* @return The translated program. |
|
||||
*/ |
|
||||
storm::prism::Program const& getTranslatedProgram() const; |
|
||||
|
|
||||
private: |
|
||||
/*! |
|
||||
* 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. |
|
||||
* @return A pair indicating whether the state was already discovered before and the state id of the state. |
|
||||
*/ |
|
||||
StateType getOrAddStateIndex(CompressedState const& state); |
|
||||
|
|
||||
/*! |
|
||||
* 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 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. |
|
||||
*/ |
|
||||
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> 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(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels); |
|
||||
|
|
||||
/*! |
|
||||
* Builds the state labeling for the given program. |
|
||||
* |
|
||||
* @return The state labeling of the given program. |
|
||||
*/ |
|
||||
storm::models::sparse::StateLabeling buildStateLabeling(); |
|
||||
|
|
||||
// The program to translate. The necessary transformations are performed upon construction of the builder. |
|
||||
storm::prism::Program program; |
|
||||
|
|
||||
// The options to be used for translating the program. |
|
||||
Options options; |
|
||||
|
|
||||
// The variable information. |
|
||||
VariableInformation variableInformation; |
|
||||
|
|
||||
// Internal information about the states that were explored. |
|
||||
storm::storage::sparse::StateStorage<StateType> stateStorage; |
|
||||
|
|
||||
// This member holds information about reachable states that can be retrieved from the outside after a |
|
||||
// successful build. |
|
||||
boost::optional<storm::storage::sparse::StateValuations> stateValuations; |
|
||||
|
|
||||
// A set of states that still need to be explored. |
|
||||
std::deque<CompressedState> statesToExplore; |
|
||||
|
|
||||
// An optional mapping from state indices to the row groups in which they actually reside. This needs to be |
|
||||
// built in case the exploration order is not BFS. |
|
||||
boost::optional<std::vector<uint_fast64_t>> stateRemapping; |
|
||||
|
|
||||
}; |
|
||||
|
|
||||
} // namespace adapters |
|
||||
} // namespace storm |
|
||||
|
|
||||
#endif /* STORM_BUILDER_EXPLICITPRISMMODELBUILDER_H */ |
|
||||
@ -0,0 +1,174 @@ |
|||||
|
#include "src/generator/NextStateGenerator.h"
|
||||
|
|
||||
|
#include "src/adapters/CarlAdapter.h"
|
||||
|
|
||||
|
#include "src/logic/Formulas.h"
|
||||
|
|
||||
|
#include "src/utility/macros.h"
|
||||
|
#include "src/exceptions/InvalidArgumentException.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace generator { |
||||
|
|
||||
|
LabelOrExpression::LabelOrExpression(storm::expressions::Expression const& expression) : labelOrExpression(expression) { |
||||
|
// Intentionally left empty.
|
||||
|
} |
||||
|
|
||||
|
LabelOrExpression::LabelOrExpression(std::string const& label) : labelOrExpression(label) { |
||||
|
// Intentionally left empty.
|
||||
|
} |
||||
|
|
||||
|
bool LabelOrExpression::isLabel() const { |
||||
|
return labelOrExpression.which() == 0; |
||||
|
} |
||||
|
|
||||
|
std::string const& LabelOrExpression::getLabel() const { |
||||
|
return boost::get<std::string const&>(labelOrExpression); |
||||
|
} |
||||
|
|
||||
|
bool LabelOrExpression::isExpression() const { |
||||
|
return labelOrExpression.which() == 1; |
||||
|
} |
||||
|
|
||||
|
storm::expressions::Expression const& LabelOrExpression::getExpression() const { |
||||
|
return boost::get<storm::expressions::Expression const&>(labelOrExpression); |
||||
|
} |
||||
|
|
||||
|
NextStateGeneratorOptions::NextStateGeneratorOptions(storm::logic::Formula const& formula) { |
||||
|
this->preserveFormula(formula); |
||||
|
this->setTerminalStatesFromFormula(formula); |
||||
|
} |
||||
|
|
||||
|
NextStateGeneratorOptions::NextStateGeneratorOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) { |
||||
|
if (!formulas.empty()) { |
||||
|
for (auto const& formula : formulas) { |
||||
|
this->preserveFormula(*formula); |
||||
|
} |
||||
|
if (formulas.size() == 1) { |
||||
|
this->setTerminalStatesFromFormula(*formulas.front()); |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
void NextStateGeneratorOptions::preserveFormula(storm::logic::Formula const& formula) { |
||||
|
// If we already had terminal states, we need to erase them.
|
||||
|
if (hasTerminalStates()) { |
||||
|
clearTerminalStates(); |
||||
|
} |
||||
|
|
||||
|
// Determine the reward models we need to build.
|
||||
|
std::set<std::string> referencedRewardModels = formula.getReferencedRewardModels(); |
||||
|
for (auto const& rewardModelName : referencedRewardModels) { |
||||
|
rewardModelNames.push_back(rewardModelName); |
||||
|
} |
||||
|
|
||||
|
// Extract all the labels used in the formula.
|
||||
|
std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula.getAtomicLabelFormulas(); |
||||
|
for (auto const& formula : atomicLabelFormulas) { |
||||
|
addLabel(formula->getLabel()); |
||||
|
} |
||||
|
|
||||
|
// Extract all the expressions used in the formula.
|
||||
|
std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> atomicExpressionFormulas = formula.getAtomicExpressionFormulas(); |
||||
|
for (auto const& formula : atomicExpressionFormulas) { |
||||
|
addLabel(formula->getExpression()); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
void NextStateGeneratorOptions::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { |
||||
|
if (formula.isAtomicExpressionFormula()) { |
||||
|
addTerminalExpression(formula.asAtomicExpressionFormula().getExpression(), true); |
||||
|
} else if (formula.isAtomicLabelFormula()) { |
||||
|
addTerminalLabel(formula.asAtomicLabelFormula().getLabel(), true); |
||||
|
} else if (formula.isEventuallyFormula()) { |
||||
|
storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); |
||||
|
if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { |
||||
|
this->setTerminalStatesFromFormula(sub); |
||||
|
} |
||||
|
} else if (formula.isUntilFormula()) { |
||||
|
storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); |
||||
|
if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { |
||||
|
this->setTerminalStatesFromFormula(right); |
||||
|
} |
||||
|
storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); |
||||
|
if (left.isAtomicExpressionFormula()) { |
||||
|
addTerminalExpression(left.asAtomicExpressionFormula().getExpression(), false); |
||||
|
} else if (left.isAtomicLabelFormula()) { |
||||
|
addTerminalLabel(left.asAtomicLabelFormula().getLabel(), false); |
||||
|
} |
||||
|
} else if (formula.isProbabilityOperatorFormula()) { |
||||
|
storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); |
||||
|
if (sub.isEventuallyFormula() || sub.isUntilFormula()) { |
||||
|
this->setTerminalStatesFromFormula(sub); |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
std::vector<std::string> const& NextStateGeneratorOptions::getRewardModelNames() const { |
||||
|
return rewardModelNames; |
||||
|
} |
||||
|
|
||||
|
std::set<std::string> const& NextStateGeneratorOptions::getLabels() const { |
||||
|
return labels; |
||||
|
} |
||||
|
|
||||
|
std::vector<storm::expressions::Expression> const& NextStateGeneratorOptions::getLabelExpressions() const { |
||||
|
return labelExpressions; |
||||
|
} |
||||
|
|
||||
|
std::vector<std::pair<LabelOrExpression, bool>> const& NextStateGeneratorOptions::getTerminalStates() const { |
||||
|
return terminalStates; |
||||
|
} |
||||
|
|
||||
|
bool NextStateGeneratorOptions::hasTerminalStates() const { |
||||
|
return !terminalStates.empty(); |
||||
|
} |
||||
|
|
||||
|
void NextStateGeneratorOptions::clearTerminalStates() { |
||||
|
terminalStates.clear(); |
||||
|
} |
||||
|
|
||||
|
bool NextStateGeneratorOptions::isBuildChoiceLabelsSet() const { |
||||
|
return buildChoiceLabels; |
||||
|
} |
||||
|
|
||||
|
NextStateGeneratorOptions& NextStateGeneratorOptions::addRewardModel(std::string const& rewardModelName) { |
||||
|
rewardModelNames.emplace_back(rewardModelName); |
||||
|
return *this; |
||||
|
} |
||||
|
|
||||
|
NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(storm::expressions::Expression const& expression) { |
||||
|
labelExpressions.emplace_back(expression); |
||||
|
return *this; |
||||
|
} |
||||
|
|
||||
|
NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(std::string const& label) { |
||||
|
labels.insert(label); |
||||
|
return *this; |
||||
|
} |
||||
|
|
||||
|
NextStateGeneratorOptions& NextStateGeneratorOptions::addTerminalExpression(storm::expressions::Expression const& expression, bool value) { |
||||
|
terminalStates.push_back(std::make_pair(LabelOrExpression(expression), value)); |
||||
|
return *this; |
||||
|
} |
||||
|
|
||||
|
NextStateGeneratorOptions& NextStateGeneratorOptions::addTerminalLabel(std::string const& label, bool value) { |
||||
|
terminalStates.push_back(std::make_pair(LabelOrExpression(label), value)); |
||||
|
return *this; |
||||
|
} |
||||
|
|
||||
|
NextStateGeneratorOptions& NextStateGeneratorOptions::setBuildChoiceLabels(bool newValue) { |
||||
|
buildChoiceLabels = newValue; |
||||
|
return *this; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
NextStateGenerator<ValueType, StateType>::NextStateGenerator(NextStateGeneratorOptions const& options) : options(options) { |
||||
|
// Intentionally left empty.
|
||||
|
} |
||||
|
|
||||
|
template class NextStateGenerator<double>; |
||||
|
template class NextStateGenerator<storm::RationalFunction>; |
||||
|
|
||||
|
} |
||||
|
} |
||||
@ -1,50 +0,0 @@ |
|||||
#include "src/generator/PrismStateLabelingGenerator.h"
|
|
||||
|
|
||||
#include "src/generator/CompressedState.h"
|
|
||||
|
|
||||
#include "src/storage/expressions/ExpressionEvaluator.h"
|
|
||||
|
|
||||
namespace storm { |
|
||||
namespace generator { |
|
||||
|
|
||||
template<typename ValueType, typename StateType> |
|
||||
PrismStateLabelingGenerator<ValueType, StateType>::PrismStateLabelingGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation) : program(program), variableInformation(variableInformation) { |
|
||||
// Intentionally left empty.
|
|
||||
} |
|
||||
|
|
||||
template<typename ValueType, typename StateType> |
|
||||
storm::models::sparse::StateLabeling PrismStateLabelingGenerator<ValueType, StateType>::generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices) { |
|
||||
std::vector<storm::prism::Label> const& labels = program.getLabels(); |
|
||||
|
|
||||
storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager()); |
|
||||
storm::models::sparse::StateLabeling result(states.size()); |
|
||||
|
|
||||
// Initialize labeling.
|
|
||||
for (auto const& label : labels) { |
|
||||
result.addLabel(label.getName()); |
|
||||
} |
|
||||
for (auto const& stateIndexPair : states) { |
|
||||
unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, evaluator); |
|
||||
|
|
||||
for (auto const& label : labels) { |
|
||||
// Add label to state, if the corresponding expression is true.
|
|
||||
if (evaluator.asBool(label.getStatePredicateExpression())) { |
|
||||
result.addLabelToState(label.getName(), stateIndexPair.second); |
|
||||
} |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
// Also label the initial state with the special label "init".
|
|
||||
result.addLabel("init"); |
|
||||
for (auto index : initialStateIndices) { |
|
||||
result.addLabelToState("init", index); |
|
||||
} |
|
||||
|
|
||||
return result; |
|
||||
} |
|
||||
|
|
||||
template class PrismStateLabelingGenerator<double, uint32_t>; |
|
||||
template class PrismStateLabelingGenerator<storm::RationalFunction, uint32_t>; |
|
||||
|
|
||||
} |
|
||||
} |
|
||||
@ -1,31 +0,0 @@ |
|||||
#ifndef STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_ |
|
||||
#define STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_ |
|
||||
|
|
||||
#include "src/generator/StateLabelingGenerator.h" |
|
||||
|
|
||||
#include "src/generator/VariableInformation.h" |
|
||||
|
|
||||
#include "src/storage/prism/Program.h" |
|
||||
|
|
||||
namespace storm { |
|
||||
namespace generator { |
|
||||
|
|
||||
template<typename ValueType, typename StateType = uint32_t> |
|
||||
class PrismStateLabelingGenerator : public StateLabelingGenerator<StateType> { |
|
||||
public: |
|
||||
PrismStateLabelingGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation); |
|
||||
|
|
||||
virtual storm::models::sparse::StateLabeling generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) override; |
|
||||
|
|
||||
private: |
|
||||
// The program for which to generate the labels. |
|
||||
storm::prism::Program const& program; |
|
||||
|
|
||||
// Information about how the variables are packed. |
|
||||
VariableInformation const& variableInformation; |
|
||||
}; |
|
||||
|
|
||||
} |
|
||||
} |
|
||||
|
|
||||
#endif /* STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_ */ |
|
||||
@ -1,20 +0,0 @@ |
|||||
#ifndef STORM_GENERATOR_STATELABELINGGENERATOR_H_ |
|
||||
#define STORM_GENERATOR_STATELABELINGGENERATOR_H_ |
|
||||
|
|
||||
#include "src/models/sparse/StateLabeling.h" |
|
||||
|
|
||||
#include "src/storage/BitVectorHashMap.h" |
|
||||
|
|
||||
namespace storm { |
|
||||
namespace generator { |
|
||||
|
|
||||
template<typename StateType = uint32_t> |
|
||||
class StateLabelingGenerator { |
|
||||
public: |
|
||||
virtual storm::models::sparse::StateLabeling generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) = 0; |
|
||||
}; |
|
||||
|
|
||||
} |
|
||||
} |
|
||||
|
|
||||
#endif /* STORM_GENERATOR_STATELABELINGGENERATOR_H_ */ |
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue