sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

added observation labels to the prism program

tempestpy_adaptions
Sebastian Junges 5 years ago
parent
95b2c829f1
commit
e177a5420a
2 changed files with 40 additions and 9 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 28
      src/storm/storage/prism/Program.cpp
  2. 21
      src/storm/storage/prism/Program.h

28
src/storm/storage/prism/Program.cpp
View File

@ -137,14 +137,14 @@ namespace storm {
std::set<std::string> appearingModules;
};
Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename, uint_fast64_t lineNumber, bool finalModel)
Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename, uint_fast64_t lineNumber, bool finalModel)
: LocatedInformation(filename, lineNumber), manager(manager),
modelType(modelType), constants(constants), constantToIndexMap(),
globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(),
globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(),
formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(),
rewardModels(rewardModels), rewardModelToIndexMap(), systemCompositionConstruct(compositionConstruct),
labels(labels), labelToIndexMap(), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(),
labels(labels), labelToIndexMap(), observationLabels(observationLabels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(),
synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap(), prismCompatibility(prismCompatibility)
{
@ -748,6 +748,14 @@ namespace storm {
// Move the new labels in place.
this->labels = std::move(newLabels);
}
std::vector<ObservationLabel> const& Program::getObservationLabels() const {
return this->observationLabels;
}
std::size_t Program::getNumberOfObservationLabels() const {
return this->observationLabels.size();
}
Program Program::restrictCommands(storm::storage::FlatSet<uint_fast64_t> const& indexSet) const {
std::vector<storm::prism::Module> newModules;
@ -757,7 +765,7 @@ namespace storm {
newModules.push_back(module.restrictCommands(indexSet));
}
return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
}
void Program::createMappings() {
@ -854,7 +862,7 @@ namespace storm {
}
}
return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
}
Program Program::substituteConstants() const {
@ -926,8 +934,14 @@ namespace storm {
for (auto const& label : this->getLabels()) {
newLabels.emplace_back(label.substitute(substitution));
}
std::vector<ObservationLabel> newObservationLabels;
newObservationLabels.reserve(this->getNumberOfObservationLabels());
for (auto const& label : this->getObservationLabels()) {
newObservationLabels.emplace_back(label.substitute(substitution));
}
return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct(), prismCompatibility);
return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newObservationLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct(), prismCompatibility);
}
void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
@ -1480,7 +1494,7 @@ namespace storm {
}
}
return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, getLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, getLabels(), getObservationLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
}
Program Program::flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {
@ -1688,7 +1702,7 @@ namespace storm {
// Finally, we can create the module and the program and return it.
storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, allClockVariables, newInvariant, newCommands, this->getFilename(), 0);
return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
}
std::vector<Constant> Program::usedConstants() const {

21
src/storm/storage/prism/Program.h
View File

@ -57,7 +57,7 @@ namespace storm {
* @param lineNumber The line number in which the program is defined.
* @param finalModel If set to true, the program is checked for input-validity, as well as some post-processing.
*/
Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true);
Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true);
// Provide default implementations for constructors and assignments.
Program() = default;
@ -522,7 +522,7 @@ namespace storm {
* @return A set of labels that are defined in the program.
*/
std::vector<Label> const& getLabels() const;
/*!
* Retrieves all guards appearing in the program.
*
@ -574,6 +574,20 @@ namespace storm {
* @param labelSet The label set that is to be kept.
*/
void filterLabels(std::set<std::string> const& labelSet);
/*!
* Retrieves all observation labels that are defined by this program
*
* @return A set of observation labels
*/
std::vector<ObservationLabel> const& getObservationLabels() const;
/*!
* Retrieves the number of observation labels in the program.
*
* @return The number of labels in the program.
*/
std::size_t getNumberOfObservationLabels() const;
/*!
* Creates a new program that drops all commands whose indices are not in the given set.
@ -737,6 +751,9 @@ namespace storm {
// A mapping from labels to their indices.
std::map<std::string, uint_fast64_t> labelToIndexMap;
// Observation labels
std::vector<ObservationLabel> observationLabels;
// A mapping from action names to their indices.
std::map<std::string, uint_fast64_t> actionToIndexMap;

Write Preview
Loading…
Cancel
Save