Browse Source

bunch of fixes (prominently in prism -> jani conversion)

main
dehnert 8 years ago
parent
commit
43354d0c20
  1. 32
      src/storm/builder/DdPrismModelBuilder.cpp
  2. 4
      src/storm/builder/DdPrismModelBuilder.h
  3. 10
      src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
  4. 13
      src/storm/builder/jit/StateBehaviour.cpp
  5. 3
      src/storm/generator/JaniNextStateGenerator.cpp
  6. 1
      src/storm/logic/FragmentSpecification.cpp
  7. 2
      src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  8. 12
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  9. 5
      src/storm/models/sparse/StandardRewardModel.cpp
  10. 27
      src/storm/models/symbolic/Ctmc.cpp
  11. 37
      src/storm/models/symbolic/Ctmc.h
  12. 8
      src/storm/parser/FormulaParser.cpp
  13. 3
      src/storm/parser/FormulaParser.h
  14. 2
      src/storm/storage/expressions/ToExprtkStringVisitor.cpp
  15. 9
      src/storm/storage/expressions/ToRationalNumberVisitor.cpp
  16. 6
      src/storm/storage/prism/ToJaniConverter.cpp
  17. 36
      src/storm/utility/constants.cpp
  18. 8
      src/storm/utility/constants.h

32
src/storm/builder/DdPrismModelBuilder.cpp

@ -1103,7 +1103,16 @@ namespace storm {
} }
template <storm::dd::DdType Type, typename ValueType> template <storm::dd::DdType Type, typename ValueType>
storm::models::symbolic::StandardRewardModel<Type, ValueType> DdPrismModelBuilder<Type, ValueType>::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& transitionMatrix, boost::optional<storm::dd::Add<Type, ValueType>> stateActionDd) {
std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> DdPrismModelBuilder<Type, ValueType>::createRewardModelDecisionDiagrams(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, SystemResult& system, GenerationInformation& generationInfo, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& transitionMatrix) {
std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
for (auto const& rewardModel : selectedRewardModels) {
rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, reachableStatesAdd, transitionMatrix, system.stateActionDd));
}
return rewardModels;
}
template <storm::dd::DdType Type, typename ValueType>
storm::models::symbolic::StandardRewardModel<Type, ValueType> DdPrismModelBuilder<Type, ValueType>::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& transitionMatrix, boost::optional<storm::dd::Add<Type, ValueType>>& stateActionDd) {
// Start by creating the state reward vector. // Start by creating the state reward vector.
boost::optional<storm::dd::Add<Type, ValueType>> stateRewards; boost::optional<storm::dd::Add<Type, ValueType>> stateRewards;
@ -1141,15 +1150,16 @@ namespace storm {
} }
ActionDecisionDiagram const& actionDd = stateActionReward.isLabeled() ? globalModule.synchronizingActionToDecisionDiagramMap.at(stateActionReward.getActionIndex()) : globalModule.independentAction; ActionDecisionDiagram const& actionDd = stateActionReward.isLabeled() ? globalModule.synchronizingActionToDecisionDiagramMap.at(stateActionReward.getActionIndex()) : globalModule.independentAction;
states *= actionDd.guardDd * reachableStatesAdd; states *= actionDd.guardDd * reachableStatesAdd;
storm::dd::Add<Type, ValueType> stateActionRewardDd = synchronization * (reachableStatesAdd * states * rewards);
storm::dd::Add<Type, ValueType> stateActionRewardDd = synchronization * states * rewards;
// If we are building the state-action rewards for an MDP, we need to make sure that the encoding // If we are building the state-action rewards for an MDP, we need to make sure that the encoding
// of the nondeterminism is present in the reward vector, so we ne need to multiply it with the // of the nondeterminism is present in the reward vector, so we ne need to multiply it with the
// legal state-actions. // legal state-actions.
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
// FIXME: get synchronization encoding differently.
// stateActionRewardDd *= stateActionDd;
stateActionRewardDd *= transitionMatrix.notZero().existsAbstract(generationInfo.columnMetaVariables).template toAdd<ValueType>();
if (!stateActionDd) {
stateActionDd = transitionMatrix.notZero().existsAbstract(generationInfo.columnMetaVariables).template toAdd<ValueType>();
}
stateActionRewardDd *= stateActionDd.get();
} else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
// For CTMCs, we need to multiply the entries with the exit rate of the corresponding action. // For CTMCs, we need to multiply the entries with the exit rate of the corresponding action.
stateActionRewardDd *= actionDd.transitionsDd.sumAbstract(generationInfo.columnMetaVariables); stateActionRewardDd *= actionDd.transitionsDd.sumAbstract(generationInfo.columnMetaVariables);
@ -1165,7 +1175,10 @@ namespace storm {
// Scale state-action rewards for DTMCs and CTMCs. // Scale state-action rewards for DTMCs and CTMCs.
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
// stateActionRewards.get() /= stateActionDd;
if (!stateActionDd) {
stateActionDd = transitionMatrix.sumAbstract(generationInfo.columnMetaVariables);
}
stateActionRewards.get() /= stateActionDd.get();
} }
} }
@ -1381,10 +1394,7 @@ namespace storm {
selectedRewardModels.push_back(program.getRewardModel(0)); selectedRewardModels.push_back(program.getRewardModel(0));
} }
std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
for (auto const& rewardModel : selectedRewardModels) {
rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, reachableStatesAdd, transitionMatrix, system.stateActionDd));
}
std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels = createRewardModelDecisionDiagrams(selectedRewardModels, system, generationInfo, globalModule, reachableStatesAdd, transitionMatrix);
// Build the labels that can be accessed as a shortcut. // Build the labels that can be accessed as a shortcut.
std::map<std::string, storm::expressions::Expression> labelToExpressionMapping; std::map<std::string, storm::expressions::Expression> labelToExpressionMapping;
@ -1395,7 +1405,7 @@ namespace storm {
if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { if (program.getModelType() == storm::prism::Program::ModelType::DTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
} else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) { } else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, system.stateActionDd, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
} else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels)); return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels));
} else { } else {

4
src/storm/builder/DdPrismModelBuilder.h

@ -230,7 +230,9 @@ namespace storm {
static storm::dd::Add<Type, ValueType> createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module); static storm::dd::Add<Type, ValueType> createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module);
static storm::models::symbolic::StandardRewardModel<Type, ValueType> createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& transitionMatrix, boost::optional<storm::dd::Add<Type, ValueType>> stateActionDd);
static std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> createRewardModelDecisionDiagrams(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, SystemResult& system, GenerationInformation& generationInfo, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& transitionMatrix);
static storm::models::symbolic::StandardRewardModel<Type, ValueType> createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& transitionMatrix, boost::optional<storm::dd::Add<Type, ValueType>>& stateActionDd);
static SystemResult createSystemDecisionDiagram(GenerationInformation& generationInfo); static SystemResult createSystemDecisionDiagram(GenerationInformation& generationInfo);

10
src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp

@ -32,6 +32,8 @@ namespace storm {
namespace builder { namespace builder {
namespace jit { namespace jit {
static const std::string JIT_VARIABLE_EXTENSION = "_jit_";
#ifdef LINUX #ifdef LINUX
static const std::string DYLIB_EXTENSION = ".so"; static const std::string DYLIB_EXTENSION = ".so";
#endif #endif
@ -924,19 +926,19 @@ namespace storm {
if (hasLocationRewards) { if (hasLocationRewards) {
cpptempl::data_map locationReward; cpptempl::data_map locationReward;
locationReward["variable"] = variable.getName();
locationReward["variable"] = variable.getName() + JIT_VARIABLE_EXTENSION;
locationRewards.push_back(locationReward); locationRewards.push_back(locationReward);
} }
if (hasEdgeRewards) { if (hasEdgeRewards) {
cpptempl::data_map edgeReward; cpptempl::data_map edgeReward;
edgeReward["variable"] = variable.getName();
edgeReward["variable"] = variable.getName() + JIT_VARIABLE_EXTENSION;
edgeReward["index"] = asString(rewardModelIndex); edgeReward["index"] = asString(rewardModelIndex);
edgeRewards.push_back(edgeReward); edgeRewards.push_back(edgeReward);
} }
if (hasDestinationRewards) { if (hasDestinationRewards) {
cpptempl::data_map destinationReward; cpptempl::data_map destinationReward;
destinationReward["index"] = asString(rewardModelIndex); destinationReward["index"] = asString(rewardModelIndex);
destinationReward["variable"] = variable.getName();
destinationReward["variable"] = variable.getName() + JIT_VARIABLE_EXTENSION;
destinationRewards.push_back(destinationReward); destinationRewards.push_back(destinationReward);
} }
++rewardModelIndex; ++rewardModelIndex;
@ -1578,7 +1580,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType> template <typename ValueType, typename RewardModelType>
std::string const& ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::registerVariable(storm::expressions::Variable const& variable, bool transient) { std::string const& ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::registerVariable(storm::expressions::Variable const& variable, bool transient) {
// Since the variable name might be illegal as a C++ identifier, we need to prepare it a bit. // Since the variable name might be illegal as a C++ identifier, we need to prepare it a bit.
variableToName[variable] = variable.getName() + "_jit_";
variableToName[variable] = variable.getName() + JIT_VARIABLE_EXTENSION;
if (transient) { if (transient) {
transientVariables.insert(variable); transientVariables.insert(variable);
variablePrefixes[variable] = "transientIn."; variablePrefixes[variable] = "transientIn.";

13
src/storm/builder/jit/StateBehaviour.cpp

@ -73,13 +73,14 @@ namespace storm {
if (modelType == storm::jani::ModelType::CTMC) { if (modelType == storm::jani::ModelType::CTMC) {
for (auto const& choice : choices) { for (auto const& choice : choices) {
ValueType massOfChoice = storm::utility::zero<ValueType>(); ValueType massOfChoice = storm::utility::zero<ValueType>();
for (auto const& entry : choices.front().getDistribution()) {
for (auto const& entry : choice.getDistribution()) {
massOfChoice += entry.getValue(); massOfChoice += entry.getValue();
} }
totalExitRate += massOfChoice;
auto outIt = newRewards.begin(); auto outIt = newRewards.begin();
for (auto const& reward : choice.getRewards()) { for (auto const& reward : choice.getRewards()) {
*outIt += reward * massOfChoice / totalExitRate;
*outIt += reward * massOfChoice;
++outIt; ++outIt;
} }
} }
@ -87,12 +88,16 @@ namespace storm {
for (auto const& choice : choices) { for (auto const& choice : choices) {
auto outIt = newRewards.begin(); auto outIt = newRewards.begin();
for (auto const& reward : choice.getRewards()) { for (auto const& reward : choice.getRewards()) {
*outIt += reward / totalExitRate;
*outIt += reward;
++outIt; ++outIt;
} }
} }
} }
for (auto& entry : newRewards) {
entry /= totalExitRate;
}
choices.front().setRewards(std::move(newRewards)); choices.front().setRewards(std::move(newRewards));
} }

3
src/storm/generator/JaniNextStateGenerator.cpp

@ -467,6 +467,9 @@ namespace storm {
// If the new state was already found as a successor state, update the probability // If the new state was already found as a successor state, update the probability
// and otherwise insert it. // and otherwise insert it.
auto probability = stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability()); auto probability = stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability());
if (edge.hasRate()) {
probability *= this->evaluator->asRational(edge.getRate());
}
if (probability != storm::utility::zero<ValueType>()) { if (probability != storm::utility::zero<ValueType>()) {
auto targetStateIt = newTargetStates->find(newTargetState); auto targetStateIt = newTargetStates->find(newTargetState);
if (targetStateIt != newTargetStates->end()) { if (targetStateIt != newTargetStates->end()) {

1
src/storm/logic/FragmentSpecification.cpp

@ -325,7 +325,6 @@ namespace storm {
return *this; return *this;
} }
bool FragmentSpecification::areTotalRewardFormulasAllowed() const { bool FragmentSpecification::areTotalRewardFormulasAllowed() const {
return totalRewardFormula; return totalRewardFormula;
} }

2
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp

@ -49,7 +49,7 @@ namespace storm {
template<typename CValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type> template<typename CValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const { bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true));
return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true));
} }
template <typename SparseCtmcModelType> template <typename SparseCtmcModelType>

12
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp

@ -496,12 +496,6 @@ namespace storm {
solver->solveEquations(bsccEquationSystemSolution, bsccEquationSystemRightSide); solver->solveEquations(bsccEquationSystemSolution, bsccEquationSystemRightSide);
} }
// std::vector<ValueType> tmp(probabilityMatrix.getRowCount(), storm::utility::zero<ValueType>());
// probabilityMatrix.multiplyVectorWithMatrix(bsccEquationSystemSolution, tmp);
// for (uint64_t i = 0; i < tmp.size(); ++i) {
// std::cout << tmp[i] << " vs. " << bsccEquationSystemSolution[i] << std::endl;
// }
// If exit rates were given, we need to 'fix' the results to also account for the timing behaviour. // If exit rates were given, we need to 'fix' the results to also account for the timing behaviour.
if (exitRateVector != nullptr) { if (exitRateVector != nullptr) {
std::vector<ValueType> bsccTotalValue(bsccDecomposition.size(), zero); std::vector<ValueType> bsccTotalValue(bsccDecomposition.size(), zero);
@ -513,11 +507,7 @@ namespace storm {
bsccEquationSystemSolution[indexInStatesInBsccs[*stateIter]] = (bsccEquationSystemSolution[indexInStatesInBsccs[*stateIter]] * (one / (*exitRateVector)[*stateIter])) / bsccTotalValue[stateToBsccIndexMap[indexInStatesInBsccs[*stateIter]]]; bsccEquationSystemSolution[indexInStatesInBsccs[*stateIter]] = (bsccEquationSystemSolution[indexInStatesInBsccs[*stateIter]] * (one / (*exitRateVector)[*stateIter])) / bsccTotalValue[stateToBsccIndexMap[indexInStatesInBsccs[*stateIter]]];
} }
} }
// for (auto const& val : bsccEquationSystemSolution) {
// std::cout << "val: " << val << std::endl;
// }
// Calculate LRA Value for each BSCC from steady state distribution in BSCCs. // Calculate LRA Value for each BSCC from steady state distribution in BSCCs.
for (uint_fast64_t bsccIndex = 0; bsccIndex < bsccDecomposition.size(); ++bsccIndex) { for (uint_fast64_t bsccIndex = 0; bsccIndex < bsccDecomposition.size(); ++bsccIndex) {
storm::storage::StronglyConnectedComponent const& bscc = bsccDecomposition[bsccIndex]; storm::storage::StronglyConnectedComponent const& bscc = bsccDecomposition[bsccIndex];

5
src/storm/models/sparse/StandardRewardModel.cpp

@ -165,11 +165,6 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
template<typename MatrixValueType> template<typename MatrixValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const { std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const {
if (this->hasStateActionRewards()) {
for (auto const& e : this->getStateActionRewardVector()) {
std::cout << "e " << e << std::endl;
}
}
std::vector<ValueType> result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector<ValueType>(transitionMatrix.getRowCount())); std::vector<ValueType> result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector<ValueType>(transitionMatrix.getRowCount()));
if (this->hasStateActionRewards() && this->hasTransitionRewards()) { if (this->hasStateActionRewards() && this->hasTransitionRewards()) {
storm::utility::vector::addVectors(result, this->getStateActionRewardVector(), result); storm::utility::vector::addVectors(result, this->getStateActionRewardVector(), result);

27
src/storm/models/symbolic/Ctmc.cpp

@ -24,12 +24,33 @@ namespace storm {
std::map<std::string, storm::expressions::Expression> labelToExpressionMap, std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels) std::unordered_map<std::string, RewardModelType> const& rewardModels)
: DeterministicModel<Type, ValueType>(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { : DeterministicModel<Type, ValueType>(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) {
exitRates = this->getTransitionMatrix().sumAbstract(this->getColumnVariables());
// Intentionally left empty.
} }
template<storm::dd::DdType Type, typename ValueType>
Ctmc<Type, ValueType>::Ctmc(std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
boost::optional<storm::dd::Add<Type, ValueType>> exitRateVector,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
std::set<storm::expressions::Variable> const& columnVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> columnExpressionAdapter,
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
: DeterministicModel<Type, ValueType>(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels), exitRates(exitRateVector) {
// Intentionally left empty.
}
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
storm::dd::Add<Type, ValueType> const& Ctmc<Type, ValueType>::getExitRateVector() const { storm::dd::Add<Type, ValueType> const& Ctmc<Type, ValueType>::getExitRateVector() const {
return exitRates;
if (!exitRates) {
exitRates = this->getTransitionMatrix().sumAbstract(this->getColumnVariables());
}
return exitRates.get();
} }
// Explicitly instantiate the template class. // Explicitly instantiate the template class.

37
src/storm/models/symbolic/Ctmc.h

@ -54,7 +54,40 @@ namespace storm {
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(), std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(),
std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>()); std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
/*!
* Constructs a model from the given data.
*
* @param manager The manager responsible for the decision diagrams.
* @param reachableStates A DD representing the reachable states.
* @param initialStates A DD representing the initial states of the model.
* @param deadlockStates A DD representing the deadlock states of the model.
* @param transitionMatrix The matrix representing the transitions in the model.
* @param exitRateVector The vector specifying the exit rates for the states.
* @param rowVariables The set of row meta variables used in the DDs.
* @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row
* meta variables.
* @param columVariables The set of column meta variables used in the DDs.
* @param columnExpressionAdapter An object that can be used to translate expressions in terms of the
* column meta variables.
* @param rowColumnMetaVariablePairs All pairs of row/column meta variables.
* @param labelToExpressionMap A mapping from label names to their defining expressions.
* @param rewardModels The reward models associated with the model.
*/
Ctmc(std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
boost::optional<storm::dd::Add<Type, ValueType>> exitRateVector,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
std::set<storm::expressions::Variable> const& columnVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> columnExpressionAdapter,
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(),
std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
/*! /*!
* Retrieves the exit rate vector of the CTMC. * Retrieves the exit rate vector of the CTMC.
* *
@ -63,7 +96,7 @@ namespace storm {
storm::dd::Add<Type, ValueType> const& getExitRateVector() const; storm::dd::Add<Type, ValueType> const& getExitRateVector() const;
private: private:
storm::dd::Add<Type, ValueType> exitRates;
mutable boost::optional<storm::dd::Add<Type, ValueType>> exitRates;
}; };
} // namespace symbolic } // namespace symbolic

8
src/storm/parser/FormulaParser.cpp

@ -32,6 +32,14 @@ namespace storm {
} }
FormulaParser::FormulaParser(storm::prism::Program const& program) : manager(program.getManager().getSharedPointer()), grammar(new FormulaParserGrammar(manager)) { FormulaParser::FormulaParser(storm::prism::Program const& program) : manager(program.getManager().getSharedPointer()), grammar(new FormulaParserGrammar(manager)) {
this->addFormulasAsIdentifiers(program);
}
FormulaParser::FormulaParser(storm::prism::Program& program) : manager(program.getManager().getSharedPointer()), grammar(new FormulaParserGrammar(manager)) {
this->addFormulasAsIdentifiers(program);
}
void FormulaParser::addFormulasAsIdentifiers(storm::prism::Program const& program) {
// Make the formulas of the program available to the parser. // Make the formulas of the program available to the parser.
for (auto const& formula : program.getFormulas()) { for (auto const& formula : program.getFormulas()) {
this->addIdentifierExpression(formula.getName(), formula.getExpression()); this->addIdentifierExpression(formula.getName(), formula.getExpression());

3
src/storm/parser/FormulaParser.h

@ -29,6 +29,7 @@ namespace storm {
explicit FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager); explicit FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager);
explicit FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager> const& manager); explicit FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager> const& manager);
explicit FormulaParser(storm::prism::Program const& program); explicit FormulaParser(storm::prism::Program const& program);
explicit FormulaParser(storm::prism::Program& program);
FormulaParser(FormulaParser const& other); FormulaParser(FormulaParser const& other);
FormulaParser& operator=(FormulaParser const& other); FormulaParser& operator=(FormulaParser const& other);
@ -67,6 +68,8 @@ namespace storm {
void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression); void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression);
private: private:
void addFormulasAsIdentifiers(storm::prism::Program const& program);
// The manager used to parse expressions. // The manager used to parse expressions.
std::shared_ptr<storm::expressions::ExpressionManager const> manager; std::shared_ptr<storm::expressions::ExpressionManager const> manager;

2
src/storm/storage/expressions/ToExprtkStringVisitor.cpp

@ -213,7 +213,7 @@ namespace storm {
} }
boost::any ToExprtkStringVisitor::visit(RationalLiteralExpression const& expression, boost::any const&) { boost::any ToExprtkStringVisitor::visit(RationalLiteralExpression const& expression, boost::any const&) {
stream << expression.getValue();
stream << "(" << expression.getValue() << ")";
return boost::any(); return boost::any();
} }
} }

9
src/storm/storage/expressions/ToRationalNumberVisitor.cpp

@ -78,8 +78,13 @@ namespace storm {
} }
template<typename RationalNumberType> template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(UnaryNumericalFunctionExpression const&, boost::any const& ) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
RationalNumberType operandAsRationalNumber = boost::any_cast<RationalNumberType>(expression.getOperand()->accept(*this, data));
switch (expression.getOperatorType()) {
case UnaryNumericalFunctionExpression::OperatorType::Minus: return -operandAsRationalNumber;
case UnaryNumericalFunctionExpression::OperatorType::Floor: return storm::utility::floor(operandAsRationalNumber);
case UnaryNumericalFunctionExpression::OperatorType::Ceil: return storm::utility::ceil(operandAsRationalNumber);
}
} }
template<typename RationalNumberType> template<typename RationalNumberType>

6
src/storm/storage/prism/ToJaniConverter.cpp

@ -141,6 +141,7 @@ namespace storm {
// Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the // Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the
// previously built mapping to make variables global that are read by more than one module. // previously built mapping to make variables global that are read by more than one module.
std::set<uint64_t> firstModules;
bool firstModule = true; bool firstModule = true;
for (auto const& module : program.getModules()) { for (auto const& module : program.getModules()) {
// Keep track of the action indices contained in this module. // Keep track of the action indices contained in this module.
@ -179,7 +180,7 @@ namespace storm {
uint64_t onlyLocationIndex = automaton.addLocation(storm::jani::Location("l")); uint64_t onlyLocationIndex = automaton.addLocation(storm::jani::Location("l"));
automaton.addInitialLocation(onlyLocationIndex); automaton.addInitialLocation(onlyLocationIndex);
// If we are translating the first module, we need to add the transient assignments to the location.
// If we are translating the first module that has the action, we need to add the transient assignments to the location.
if (firstModule) { if (firstModule) {
storm::jani::Location& onlyLocation = automaton.getLocation(onlyLocationIndex); storm::jani::Location& onlyLocation = automaton.getLocation(onlyLocationIndex);
for (auto const& assignment : transientLocationAssignments) { for (auto const& assignment : transientLocationAssignments) {
@ -189,7 +190,7 @@ namespace storm {
for (auto const& command : module.getCommands()) { for (auto const& command : module.getCommands()) {
std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(command.getGuardExpression()); std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(command.getGuardExpression());
actionIndicesOfModule.insert(command.getActionIndex());
actionIndicesOfModule.insert(janiModel.getActionIndex(command.getActionName()));
boost::optional<storm::expressions::Expression> rateExpression; boost::optional<storm::expressions::Expression> rateExpression;
if (program.getModelType() == Program::ModelType::CTMC || program.getModelType() == Program::ModelType::CTMDP || (program.getModelType() == Program::ModelType::MA && command.isMarkovian())) { if (program.getModelType() == Program::ModelType::CTMC || program.getModelType() == Program::ModelType::CTMDP || (program.getModelType() == Program::ModelType::MA && command.isMarkovian())) {
@ -226,7 +227,6 @@ namespace storm {
for (auto const& assignment : transientEdgeAssignmentsToAdd->second) { for (auto const& assignment : transientEdgeAssignmentsToAdd->second) {
templateEdge->addTransientAssignment(assignment); templateEdge->addTransientAssignment(assignment);
} }
transientEdgeAssignments.erase(transientEdgeAssignmentsToAdd);
} }
// Create the edge object. // Create the edge object.

36
src/storm/utility/constants.cpp

@ -195,6 +195,16 @@ namespace storm {
return std::fabs(number); return std::fabs(number);
} }
template<typename ValueType>
ValueType floor(ValueType const& number) {
return std::floor(number);
}
template<typename ValueType>
ValueType ceil(ValueType const& number) {
return std::ceil(number);
}
template<> template<>
std::pair<storm::RationalFunction, storm::RationalFunction> minmax(std::vector<storm::RationalFunction> const&) { std::pair<storm::RationalFunction, storm::RationalFunction> minmax(std::vector<storm::RationalFunction> const&) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum/maximum for rational functions is not defined."); STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum/maximum for rational functions is not defined.");
@ -376,7 +386,17 @@ namespace storm {
RationalNumber abs(storm::RationalNumber const& number) { RationalNumber abs(storm::RationalNumber const& number) {
return carl::abs(number); return carl::abs(number);
} }
template<>
RationalNumber floor(storm::RationalNumber const& number) {
return carl::floor(number);
}
template<>
RationalNumber ceil(storm::RationalNumber const& number) {
return carl::ceil(number);
}
template<> template<>
RationalNumber pow(RationalNumber const& value, uint_fast64_t exponent) { RationalNumber pow(RationalNumber const& value, uint_fast64_t exponent) {
return carl::pow(value, exponent); return carl::pow(value, exponent);
@ -502,15 +522,13 @@ namespace storm {
template std::pair<double, double> minmax(std::map<uint64_t, double> const&); template std::pair<double, double> minmax(std::map<uint64_t, double> const&);
template double minimum(std::map<uint64_t, double> const&); template double minimum(std::map<uint64_t, double> const&);
template double maximum(std::map<uint64_t, double> const&); template double maximum(std::map<uint64_t, double> const&);
#ifdef STORM_HAVE_CARL
// Instantiations for rational number.
template std::pair<storm::RationalNumber, storm::RationalNumber> minmax(std::map<uint64_t, storm::RationalNumber> const&); template std::pair<storm::RationalNumber, storm::RationalNumber> minmax(std::map<uint64_t, storm::RationalNumber> const&);
template storm::RationalNumber minimum(std::map<uint64_t, storm::RationalNumber> const&); template storm::RationalNumber minimum(std::map<uint64_t, storm::RationalNumber> const&);
template storm::RationalNumber maximum(std::map<uint64_t, storm::RationalNumber> const&); template storm::RationalNumber maximum(std::map<uint64_t, storm::RationalNumber> const&);
template storm::RationalFunction minimum(std::map<uint64_t, storm::RationalFunction> const&);
template storm::RationalFunction maximum(std::map<uint64_t, storm::RationalFunction> const&);
#ifdef STORM_HAVE_CARL
// Instantiations for rational number.
template bool isOne(storm::RationalNumber const& value); template bool isOne(storm::RationalNumber const& value);
template bool isZero(storm::RationalNumber const& value); template bool isZero(storm::RationalNumber const& value);
template bool isConstant(storm::RationalNumber const& value); template bool isConstant(storm::RationalNumber const& value);
@ -526,8 +544,9 @@ namespace storm {
RationalNumber convertNumber(std::string const& number); RationalNumber convertNumber(std::string const& number);
template storm::RationalNumber sqrt(storm::RationalNumber const& number); template storm::RationalNumber sqrt(storm::RationalNumber const& number);
template storm::RationalNumber abs(storm::RationalNumber const& number); template storm::RationalNumber abs(storm::RationalNumber const& number);
template storm::RationalNumber floor(storm::RationalNumber const& number);
template storm::RationalNumber ceil(storm::RationalNumber const& number);
template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent); template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent);
@ -561,6 +580,9 @@ namespace storm {
template Interval one(); template Interval one();
template Interval zero(); template Interval zero();
template storm::RationalFunction minimum(std::map<uint64_t, storm::RationalFunction> const&);
template storm::RationalFunction maximum(std::map<uint64_t, storm::RationalFunction> const&);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);

8
src/storm/utility/constants.h

@ -85,7 +85,13 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
ValueType abs(ValueType const& number); ValueType abs(ValueType const& number);
template<typename ValueType>
ValueType floor(ValueType const& number);
template<typename ValueType>
ValueType ceil(ValueType const& number);
template<typename ValueType> template<typename ValueType>
bool isInteger(ValueType const& number); bool isInteger(ValueType const& number);

Loading…
Cancel
Save