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

adding translation of expressions used in formulas to symbolic-to-sparse transformers

main
dehnert 7 years ago
parent
e609a240a9
commit
9d528db2fc
4 changed files with 77 additions and 28 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. 16
      src/storm-cli-utilities/model-handling.h
  2. 8
      src/storm/api/transformation.h
  3. 74
      src/storm/transformer/SymbolicToSparseTransformer.cpp
  4. 7
      src/storm/transformer/SymbolicToSparseTransformer.h

16
src/storm-cli-utilities/model-handling.h
View File

@ -359,18 +359,12 @@ namespace storm {
result->second = true;
std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> symbolicModel = result->first->template as<storm::models::symbolic::Model<DdType, ExportValueType>>();
if (symbolicModel->isOfType(storm::models::ModelType::Dtmc)) {
storm::transformer::SymbolicDtmcToSparseDtmcTransformer<DdType, ExportValueType> transformer;
result->first = transformer.translate(*symbolicModel->template as<storm::models::symbolic::Dtmc<DdType, ExportValueType>>());
} else if (symbolicModel->isOfType(storm::models::ModelType::Ctmc)) {
storm::transformer::SymbolicCtmcToSparseCtmcTransformer<DdType, ExportValueType> transformer;
result->first = transformer.translate(*symbolicModel->template as<storm::models::symbolic::Ctmc<DdType, ExportValueType>>());
} else if (symbolicModel->isOfType(storm::models::ModelType::Mdp)) {
storm::transformer::SymbolicMdpToSparseMdpTransformer<DdType, ExportValueType> transformer;
result->first = transformer.translate(*symbolicModel->template as<storm::models::symbolic::Mdp<DdType, ExportValueType>>());
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The translation to a sparse model is not supported for the given model type.");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
for (auto const& property : input.properties) {
formulas.emplace_back(property.getRawFormula());
}
result->first = storm::api::transformSymbolicToSparseModel(symbolicModel, formulas);
STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "The translation to a sparse model is not supported for the given model type.");
}
return *result;

8
src/storm/api/transformation.h
View File

@ -62,14 +62,14 @@ namespace storm {
* Transforms the given symbolic model to a sparse model.
*/
template<storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> transformSymbolicToSparseModel(std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> const& symbolicModel) {
std::shared_ptr<storm::models::sparse::Model<ValueType>> transformSymbolicToSparseModel(std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> const& symbolicModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas = std::vector<std::shared_ptr<storm::logic::Formula const>>()) {
switch (symbolicModel->getType()) {
case storm::models::ModelType::Dtmc:
return storm::transformer::SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>().translate(*symbolicModel->template as<storm::models::symbolic::Dtmc<Type, ValueType>>());
return storm::transformer::SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>().translate(*symbolicModel->template as<storm::models::symbolic::Dtmc<Type, ValueType>>(), formulas);
case storm::models::ModelType::Mdp:
return storm::transformer::SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Mdp<Type, ValueType>>());
return storm::transformer::SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Mdp<Type, ValueType>>(), formulas);
case storm::models::ModelType::Ctmc:
return storm::transformer::SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Ctmc<Type, ValueType>>());
return storm::transformer::SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Ctmc<Type, ValueType>>(), formulas);
default:
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of symbolic " << symbolicModel->getType() << " to sparse model is not supported.");
}

74
src/storm/transformer/SymbolicToSparseTransformer.cpp
View File

@ -7,12 +7,35 @@
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/logic/AtomicExpressionFormula.h"
#include "storm/logic/AtomicLabelFormula.h"
namespace storm {
namespace transformer {
struct LabelInformation {
LabelInformation(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
for (auto const& formula : formulas) {
std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula->getAtomicLabelFormulas();
for (auto const& labelFormula : atomicLabelFormulas) {
atomicLabels.insert(labelFormula->getLabel());
}
std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> atomicExpressionFormulas = formula->getAtomicExpressionFormulas();
for (auto const& expressionFormula : atomicExpressionFormulas) {
std::stringstream ss;
ss << expressionFormula->getExpression();
expressionLabels[ss.str()] = expressionFormula->getExpression();
}
}
}
std::set<std::string> atomicLabels;
std::map<std::string, storm::expressions::Expression> expressionLabels;
};
template<storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>::translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc) {
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>::translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
this->odd = symbolicDtmc.getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicDtmc.getTransitionMatrix().toMatrix(this->odd, this->odd);
@ -36,8 +59,18 @@ namespace storm {
labelling.addLabel("init", symbolicDtmc.getInitialStates().toVector(this->odd));
labelling.addLabel("deadlock", symbolicDtmc.getDeadlockStates().toVector(this->odd));
for(auto const& label : symbolicDtmc.getLabels()) {
labelling.addLabel(label, symbolicDtmc.getStates(label).toVector(this->odd));
if (formulas.empty()) {
for (auto const& label : symbolicDtmc.getLabels()) {
labelling.addLabel(label, symbolicDtmc.getStates(label).toVector(this->odd));
}
} else {
LabelInformation labelInfo(formulas);
for (auto const& label : labelInfo.atomicLabels) {
labelling.addLabel(label, symbolicDtmc.getStates(label).toVector(this->odd));
}
for (auto const& expressionLabel : labelInfo.expressionLabels) {
labelling.addLabel(expressionLabel.first, symbolicDtmc.getStates(expressionLabel.second).toVector(this->odd));
}
}
return std::make_shared<storm::models::sparse::Dtmc<ValueType>>(transitionMatrix, labelling, rewardModels);
}
@ -48,7 +81,7 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp) {
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
storm::dd::Odd odd = symbolicMdp.getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicMdp.getTransitionMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd);
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
@ -69,15 +102,25 @@ namespace storm {
labelling.addLabel("init", symbolicMdp.getInitialStates().toVector(odd));
labelling.addLabel("deadlock", symbolicMdp.getDeadlockStates().toVector(odd));
for(auto const& label : symbolicMdp.getLabels()) {
labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd));
if (formulas.empty()) {
for (auto const& label : symbolicMdp.getLabels()) {
labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd));
}
} else {
LabelInformation labelInfo(formulas);
for (auto const& label : labelInfo.atomicLabels) {
labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd));
}
for (auto const& expressionLabel : labelInfo.expressionLabels) {
labelling.addLabel(expressionLabel.first, symbolicMdp.getStates(expressionLabel.second).toVector(odd));
}
}
return std::make_shared<storm::models::sparse::Mdp<ValueType>>(transitionMatrix, labelling, rewardModels);
}
template<storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(
storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc) {
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
storm::dd::Odd odd = symbolicCtmc.getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicCtmc.getTransitionMatrix().toMatrix(odd, odd);
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
@ -100,9 +143,20 @@ namespace storm {
labelling.addLabel("init", symbolicCtmc.getInitialStates().toVector(odd));
labelling.addLabel("deadlock", symbolicCtmc.getDeadlockStates().toVector(odd));
for(auto const& label : symbolicCtmc.getLabels()) {
labelling.addLabel(label, symbolicCtmc.getStates(label).toVector(odd));
if (formulas.empty()) {
for (auto const& label : symbolicCtmc.getLabels()) {
labelling.addLabel(label, symbolicCtmc.getStates(label).toVector(odd));
}
} else {
LabelInformation labelInfo(formulas);
for (auto const& label : labelInfo.atomicLabels) {
labelling.addLabel(label, symbolicCtmc.getStates(label).toVector(odd));
}
for (auto const& expressionLabel : labelInfo.expressionLabels) {
labelling.addLabel(expressionLabel.first, symbolicCtmc.getStates(expressionLabel.second).toVector(odd));
}
}
return std::make_shared<storm::models::sparse::Ctmc<ValueType>>(transitionMatrix, labelling, rewardModels);
}

7
src/storm/transformer/SymbolicToSparseTransformer.h
View File

@ -1,5 +1,6 @@
#pragma once
#include "storm/logic/Formula.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/symbolic/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
@ -15,7 +16,7 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
class SymbolicDtmcToSparseDtmcTransformer {
public:
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc);
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas = std::vector<std::shared_ptr<storm::logic::Formula const>>());
storm::dd::Odd const& getOdd() const;
private:
@ -25,13 +26,13 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
class SymbolicMdpToSparseMdpTransformer {
public:
static std::shared_ptr<storm::models::sparse::Mdp<ValueType>> translate(storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp);
static std::shared_ptr<storm::models::sparse::Mdp<ValueType>> translate(storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas = std::vector<std::shared_ptr<storm::logic::Formula const>>());
};
template<storm::dd::DdType Type, typename ValueType>
class SymbolicCtmcToSparseCtmcTransformer {
public:
static std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> translate(storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc);
static std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> translate(storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas = std::vector<std::shared_ptr<storm::logic::Formula const>>());
};
}
}
Write Preview
Loading…
Cancel
Save