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

Merge branch 'jani_support' of https://sselab.de/lab9/private/git/storm into jani_support 

Former-commit-id: f7a8ed9e92 [formerly d56c6434d4]
Former-commit-id: 3c94be0ffa
main
sjunges 9 years ago
parent
f0132cf2a5 59a92a8941
commit
f20e9107ba
15 changed files with 269 additions and 61 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. 75
      src/builder/DdJaniModelBuilder.cpp
  2. 18
      src/builder/DdJaniModelBuilder.h
  3. 14
      src/generator/CompressedState.cpp
  4. 87
      src/generator/JaniNextStateGenerator.cpp
  5. 12
      src/generator/NextStateGenerator.cpp
  6. 2
      src/generator/NextStateGenerator.h
  7. 35
      src/generator/PrismNextStateGenerator.cpp
  8. 5
      src/generator/VariableInformation.cpp
  9. 5
      src/generator/VariableInformation.h
  10. 2
      src/storage/BitVector.h
  11. 33
      src/storage/jani/Model.cpp
  12. 6
      src/storage/jani/Model.h
  13. 20
      src/storage/jani/VariableSet.cpp
  14. 10
      src/storage/jani/VariableSet.h

75
src/builder/DdJaniModelBuilder.cpp
View File

@ -15,6 +15,8 @@
#include "src/storage/dd/Bdd.h"
#include "src/adapters/AddExpressionAdapter.h"
#include "src/storage/expressions/ExpressionManager.h"
#include "src/models/symbolic/Dtmc.h"
#include "src/models/symbolic/Ctmc.h"
#include "src/models/symbolic/Mdp.h"
@ -28,6 +30,7 @@
#include "src/utility/dd.h"
#include "src/utility/math.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/InvalidSettingsException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/NotSupportedException.h"
@ -36,7 +39,7 @@ namespace storm {
namespace builder {
template <storm::dd::DdType Type, typename ValueType>
DdJaniModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
DdJaniModelBuilder<Type, ValueType>::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
// Intentionally left empty.
}
@ -47,7 +50,7 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
} else {
@ -75,6 +78,12 @@ namespace storm {
std::set<std::string> referencedRewardModels = formula.getReferencedRewardModels();
rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end());
}
// 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());
}
}
template <storm::dd::DdType Type, typename ValueType>
@ -113,6 +122,17 @@ namespace storm {
return buildAllRewardModels;
}
template <storm::dd::DdType Type, typename ValueType>
bool DdJaniModelBuilder<Type, ValueType>::Options::isBuildAllLabelsSet() const {
return buildAllLabels;
}
template <storm::dd::DdType Type, typename ValueType>
void DdJaniModelBuilder<Type, ValueType>::Options::addLabel(std::string const& labelName) {
STORM_LOG_THROW(!buildAllLabels, storm::exceptions::InvalidSettingsException, "Cannot add label, because all labels are built anyway.");
labelNames.insert(labelName);
}
template <storm::dd::DdType Type, typename ValueType>
struct CompositionVariables {
CompositionVariables() : manager(std::make_shared<storm::dd::DdManager<Type>>()),
@ -138,8 +158,9 @@ namespace storm {
// All pairs of row/column meta variables.
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
// A mapping from automata to the meta variable encoding their location.
std::map<std::string, std::pair<storm::expressions::Variable, storm::expressions::Variable>> automatonToLocationVariableMap;
// A mapping from automata to the meta variables encoding their location.
std::map<std::string, storm::expressions::Variable> automatonToLocationVariableMap;
std::map<std::string, std::pair<storm::expressions::Variable, storm::expressions::Variable>> automatonToLocationDdVariableMap;
// A mapping from action indices to the meta variables used to encode these actions.
std::map<uint64_t, storm::expressions::Variable> actionVariablesMap;
@ -245,10 +266,15 @@ namespace storm {
for (auto const& automaton : this->model.getAutomata()) {
// Start by creating a meta variable for the location of the automaton.
storm::expressions::Variable locationExpressionVariable = model.getManager().declareFreshIntegerVariable(false, "loc");
result.automatonToLocationVariableMap[automaton.getName()] = locationExpressionVariable;
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1);
result.automatonToLocationVariableMap[automaton.getName()] = variablePair;
result.automatonToLocationDdVariableMap[automaton.getName()] = variablePair;
result.rowColumnMetaVariablePairs.push_back(variablePair);
result.variableToRowMetaVariableMap->emplace(locationExpressionVariable, variablePair.first);
result.variableToColumnMetaVariableMap->emplace(locationExpressionVariable, variablePair.second);
// Add the location variable to the row/column variables.
result.rowMetaVariables.insert(variablePair.first);
result.columnMetaVariables.insert(variablePair.second);
@ -277,7 +303,7 @@ namespace storm {
storm::dd::Bdd<Type> range = result.manager->getBddOne();
// Add the identity and ranges of the location variables to the ones of the automaton.
std::pair<storm::expressions::Variable, storm::expressions::Variable> const& locationVariables = result.automatonToLocationVariableMap[automaton.getName()];
std::pair<storm::expressions::Variable, storm::expressions::Variable> const& locationVariables = result.automatonToLocationDdVariableMap[automaton.getName()];
storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(locationVariables.first).equals(result.manager->template getIdentity<ValueType>(locationVariables.second)).template toAdd<ValueType>() * result.manager->getRange(locationVariables.first).template toAdd<ValueType>() * result.manager->getRange(locationVariables.second).template toAdd<ValueType>();
identity &= variableIdentity.toBdd();
range &= result.manager->getRange(locationVariables.first);
@ -458,7 +484,7 @@ namespace storm {
}
}
transitions *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationIndex()).template toAdd<ValueType>();
transitions *= variables.manager->getEncoding(variables.automatonToLocationDdVariableMap.at(automaton.getName()).second, destination.getLocationIndex()).template toAdd<ValueType>();
return EdgeDestinationDd<Type, ValueType>(transitions, assignedGlobalVariables);
}
@ -1081,7 +1107,7 @@ namespace storm {
}
// Add the source location and the guard.
transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
// If we multiply the ranges of global variables, make sure everything stays within its bounds.
if (!globalVariablesInSomeDestination.empty()) {
@ -1475,7 +1501,7 @@ namespace storm {
for (uint64_t locationIndex = 0; locationIndex < automaton.getNumberOfLocations(); ++locationIndex) {
auto const& location = automaton.getLocation(locationIndex);
performTransientAssignments(location.getAssignments().getTransientAssignments(), [this,&automatonName,locationIndex,&result] (storm::jani::Assignment const& assignment) {
storm::dd::Add<Type, ValueType> assignedValues = this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automatonName).first, locationIndex).template toAdd<ValueType>() * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
storm::dd::Add<Type, ValueType> assignedValues = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automatonName).first, locationIndex).template toAdd<ValueType>() * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
auto it = result.transientLocationAssignments.find(assignment.getExpressionVariable());
if (it != result.transientLocationAssignments.end()) {
it->second += assignedValues;
@ -1557,17 +1583,18 @@ namespace storm {
storm::dd::Bdd<Type> deadlockStates;
storm::dd::Add<Type, ValueType> transitionMatrix;
std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
std::map<std::string, storm::expressions::Expression> labelToExpressionMap;
};
template <storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> createModel(storm::jani::ModelType const& modelType, CompositionVariables<Type, ValueType> const& variables, ModelComponents<Type, ValueType> const& modelComponents) {
if (modelType == storm::jani::ModelType::DTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
} else if (modelType == storm::jani::ModelType::CTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
} else if (modelType == storm::jani::ModelType::MDP) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
}
@ -1635,7 +1662,7 @@ namespace storm {
for (auto const& automaton : model.getAutomata()) {
storm::dd::Bdd<Type> initialLocationIndices = variables.manager->getBddZero();
for (auto const& locationIndex : automaton.getInitialLocationIndices()) {
initialLocationIndices |= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, locationIndex);
initialLocationIndices |= variables.manager->getEncoding(variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, locationIndex);
}
initialStates &= initialLocationIndices;
}
@ -1698,7 +1725,7 @@ namespace storm {
std::vector<storm::expressions::Variable> result;
if (options.isBuildAllRewardModelsSet()) {
for (auto const& variable : model.getGlobalVariables()) {
if (variable.isTransient()) {
if (variable.isTransient() && (variable.isRealVariable() || variable.isUnboundedIntegerVariable())) {
result.push_back(variable.getExpressionVariable());
}
}
@ -1709,7 +1736,7 @@ namespace storm {
result.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable());
} else {
STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
STORM_LOG_THROW(globalVariables.getNumberOfTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
STORM_LOG_THROW(globalVariables.getNumberOfRealTransientVariables() + globalVariables.getNumberOfUnboundedIntegerTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
}
}
@ -1748,6 +1775,21 @@ namespace storm {
return result;
}
template <storm::dd::DdType Type, typename ValueType>
std::map<std::string, storm::expressions::Expression> buildLabelExpressions(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
std::map<std::string, storm::expressions::Expression> result;
for (auto const& variable : model.getGlobalVariables().getTransientVariables()) {
if (variable->isBooleanVariable()) {
if (options.buildAllLabels || options.labelNames.find(variable->getName()) != options.labelNames.end()) {
result[variable->getName()] = model.getLabelExpression(variable->asBooleanVariable(), variables.automatonToLocationVariableMap);
}
}
}
return result;
}
template <storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::build(storm::jani::Model const& model, Options const& options) {
if (model.hasUndefinedConstants()) {
@ -1814,6 +1856,9 @@ namespace storm {
// Build the reward models.
modelComponents.rewardModels = buildRewardModels(system, rewardVariables);
// Build the label to expressions mapping.
modelComponents.labelToExpressionMap = buildLabelExpressions(model, variables, options);
// Finally, create the model.
return createModel(model.getModelType(), variables, modelComponents);
}

18
src/builder/DdJaniModelBuilder.h
View File

@ -25,7 +25,7 @@ namespace storm {
/*!
* Creates an object representing the default building options.
*/
Options();
Options(bool buildAllLabels = false, bool buildAllRewardModels = false);
/*! 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>.
@ -64,6 +64,22 @@ namespace storm {
*/
std::set<std::string> const& getRewardModelNames() const;
/*!
* Adds the given label to the ones that are supposed to be built.
*/
void addLabel(std::string const& labelName);
/*!
* Retrieves whether the flag to build all labels is set.
*/
bool isBuildAllLabelsSet() const;
/// A flag that indicates whether all labels are to be built. In this case, the label names are to be ignored.
bool buildAllLabels;
/// A set of labels to build.
std::set<std::string> labelNames;
/*!
* Retrieves whether the flag to build all reward models is set.
*/

14
src/generator/CompressedState.cpp
View File

@ -10,6 +10,13 @@ namespace storm {
template<typename ValueType>
void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) {
for (auto const& locationVariable : variableInformation.locationVariables) {
if (locationVariable.bitWidth != 0) {
evaluator.setIntegerValue(locationVariable.variable, state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth));
} else {
evaluator.setIntegerValue(locationVariable.variable, 0);
}
}
for (auto const& booleanVariable : variableInformation.booleanVariables) {
evaluator.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset));
}
@ -20,6 +27,13 @@ namespace storm {
storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager) {
storm::expressions::SimpleValuation result(manager.getSharedPointer());
for (auto const& locationVariable : variableInformation.locationVariables) {
if (locationVariable.bitWidth != 0) {
result.setIntegerValue(locationVariable.variable, state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth));
} else {
result.setIntegerValue(locationVariable.variable, 0);
}
}
for (auto const& booleanVariable : variableInformation.booleanVariables) {
result.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset));
}

87
src/generator/JaniNextStateGenerator.cpp
View File

@ -32,6 +32,9 @@ namespace storm {
this->checkValid();
this->variableInformation = VariableInformation(model);
// Create a proper evalator.
this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(model.getManager());
if (this->options.isBuildAllRewardModelsSet()) {
for (auto const& variable : model.getGlobalVariables()) {
if (variable.isTransient()) {
@ -46,14 +49,22 @@ namespace storm {
rewardVariables.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable());
} else {
STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
STORM_LOG_THROW(globalVariables.getNumberOfTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
STORM_LOG_THROW(globalVariables.getNumberOfRealTransientVariables() + globalVariables.getNumberOfUnboundedIntegerTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
}
}
// If no reward model was yet added, but there was one that was given in the options, we try to build the
// standard reward model.
if (rewardVariables.empty() && !this->options.getRewardModelNames().empty()) {
rewardVariables.push_back(globalVariables.getTransientVariables().front()->getExpressionVariable());
bool foundTransientVariable = false;
for (auto const& transientVariable : globalVariables.getTransientVariables()) {
if (transientVariable->isUnboundedIntegerVariable() || transientVariable->isRealVariable()) {
rewardVariables.push_back(transientVariable->getExpressionVariable());
foundTransientVariable = true;
break;
}
}
STORM_LOG_ASSERT(foundTransientVariable, "Expected to find a fitting transient variable.");
}
}
@ -62,11 +73,28 @@ namespace storm {
// If there are terminal states we need to handle, we now need to translate all labels to expressions.
if (this->options.hasTerminalStates()) {
std::map<std::string, storm::expressions::Variable> locationVariables;
auto locationVariableIt = this->variableInformation.locationVariables.begin();
for (auto const& automaton : this->model.getAutomata()) {
locationVariables[automaton.getName()] = locationVariableIt->variable;
++locationVariableIt;
}
for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
if (expressionOrLabelAndBool.first.isExpression()) {
this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
} else {
STORM_LOG_THROW(expressionOrLabelAndBool.first.getLabel() == "init" || expressionOrLabelAndBool.first.getLabel() == "deadlock", storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'.");
// If it's a label, i.e. refers to a transient boolean variable we need to derive the expression
// for the label so we can cut off the exploration there.
if (expressionOrLabelAndBool.first.getLabel() != "init" && expressionOrLabelAndBool.first.getLabel() != "deadlock") {
STORM_LOG_THROW(model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()) , storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'.");
storm::jani::Variable const& variable = model.getGlobalVariables().getVariable(expressionOrLabelAndBool.first.getLabel());
STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), locationVariables), expressionOrLabelAndBool.second));
}
}
}
}
@ -116,7 +144,11 @@ namespace storm {
auto resultIt = result.begin();
for (auto it = this->variableInformation.locationVariables.begin(), ite = this->variableInformation.locationVariables.end(); it != ite; ++it, ++resultIt) {
*resultIt = getLocation(state, *it);
if (it->bitWidth == 0) {
*resultIt = 0;
} else {
*resultIt = state.getAsInt(it->bitOffset, it->bitWidth);
}
}
return result;
@ -221,7 +253,7 @@ namespace storm {
while (assignmentIt->getExpressionVariable() != boolIt->variable) {
++boolIt;
}
newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getAssignedExpression()));
newState.set(boolIt->bitOffset, this->evaluator->asBool(assignmentIt->getAssignedExpression()));
}
// Iterate over all integer assignments and carry them out.
@ -230,7 +262,7 @@ namespace storm {
while (assignmentIt->getExpressionVariable() != integerIt->variable) {
++integerIt;
}
int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getAssignedExpression());
int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getAssignedExpression());
STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
@ -266,7 +298,7 @@ namespace storm {
// If a terminal expression was set and we must not expand this state, return now.
if (!this->terminalStates.empty()) {
for (auto const& expressionBool : this->terminalStates) {
if (this->evaluator.asBool(expressionBool.first) == expressionBool.second) {
if (this->evaluator->asBool(expressionBool.first) == expressionBool.second) {
return result;
}
}
@ -356,14 +388,14 @@ namespace storm {
}
// Skip the command, if it is not enabled.
if (!this->evaluator.asBool(edge.getGuard())) {
if (!this->evaluator->asBool(edge.getGuard())) {
continue;
}
// Determine the exit rate if it's a Markovian edge.
boost::optional<ValueType> exitRate = boost::none;
if (edge.hasRate()) {
exitRate = this->evaluator.asRational(edge.getRate());
exitRate = this->evaluator->asRational(edge.getRate());
}
result.push_back(Choice<ValueType>(edge.getActionIndex(), static_cast<bool>(exitRate)));
@ -377,7 +409,7 @@ namespace storm {
StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]));
// Update the choice by adding the probability/target state to it.
ValueType probability = this->evaluator.asRational(destination.getProbability());
ValueType probability = this->evaluator->asRational(destination.getProbability());
probability = exitRate ? exitRate.get() * probability : probability;
choice.addProbability(stateIndex, probability);
probabilitySum += probability;
@ -437,9 +469,9 @@ namespace storm {
// and otherwise insert it.
auto targetStateIt = newTargetStates->find(newTargetState);
if (targetStateIt != newTargetStates->end()) {
targetStateIt->second += stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability());
targetStateIt->second += stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability());
} else {
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability()));
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability()));
}
}
@ -525,7 +557,7 @@ namespace storm {
std::vector<storm::jani::Edge const*> edgePointers;
for (auto const& edge : edges) {
if (this->evaluator.asBool(edge.getGuard())) {
if (this->evaluator->asBool(edge.getGuard())) {
edgePointers.push_back(&edge);
}
}
@ -574,7 +606,32 @@ namespace storm {
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, {});
// Prepare a mapping from automata names to the location variables.
std::map<std::string, storm::expressions::Variable> locationVariables;
auto locationVariableIt = this->variableInformation.locationVariables.begin();
for (auto const& automaton : model.getAutomata()) {
locationVariables[automaton.getName()] = locationVariableIt->variable;
++locationVariableIt;
}
// As in JANI we can use transient boolean variable assignments in locations to identify states, we need to
// create a list of boolean transient variables and the expressions that define them.
std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> transientVariableToExpressionMap;
for (auto const& variable : model.getGlobalVariables().getTransientVariables()) {
if (variable->isBooleanVariable()) {
if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable->getName()) != this->options.getLabelNames().end()) {
transientVariableToExpressionMap[variable->getExpressionVariable()] = model.getLabelExpression(variable->asBooleanVariable(), locationVariables);
}
}
}
std::vector<std::pair<std::string, storm::expressions::Expression>> transientVariableExpressions;
for (auto const& element : transientVariableToExpressionMap) {
transientVariableExpressions.push_back(std::make_pair(element.first.getName(), element.second));
}
return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, transientVariableExpressions);
}
template<typename ValueType, typename StateType>
@ -595,7 +652,7 @@ namespace storm {
if (rewardVariableIt == rewardVariableIte) {
break;
} else if (*rewardVariableIt == assignment.getExpressionVariable()) {
callback(ValueType(this->evaluator.asRational(assignment.getAssignedExpression())));
callback(ValueType(this->evaluator->asRational(assignment.getAssignedExpression())));
++rewardVariableIt;
}
}

12
src/generator/NextStateGenerator.cpp
View File

@ -224,12 +224,12 @@ namespace storm {
}
template<typename ValueType, typename StateType>
NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(variableInformation), evaluator(expressionManager), state(nullptr) {
NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(variableInformation), evaluator(nullptr), state(nullptr) {
// Intentionally left empty.
}
template<typename ValueType, typename StateType>
NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(), evaluator(expressionManager), state(nullptr) {
NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(), evaluator(nullptr), state(nullptr) {
// Intentionally left empty.
}
@ -246,7 +246,7 @@ namespace storm {
template<typename ValueType, typename StateType>
void NextStateGenerator<ValueType, StateType>::load(CompressedState const& state) {
// Since almost all subsequent operations are based on the evaluator, we load the state into it now.
unpackStateIntoEvaluator(state, variableInformation, evaluator);
unpackStateIntoEvaluator(state, variableInformation, *evaluator);
// Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it.
this->state = &state;
@ -257,7 +257,7 @@ namespace storm {
if (expression.isTrue()) {
return true;
}
return evaluator.asBool(expression);
return evaluator->asBool(expression);
}
template<typename ValueType, typename StateType>
@ -282,11 +282,11 @@ namespace storm {
result.addLabel(label.first);
}
for (auto const& stateIndexPair : states) {
unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, this->evaluator);
unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator);
for (auto const& label : labelsAndExpressions) {
// Add label to state, if the corresponding expression is true.
if (evaluator.asBool(label.second)) {
if (evaluator->asBool(label.second)) {
result.addLabelToState(label.first, stateIndexPair.second);
}
}

2
src/generator/NextStateGenerator.h
View File

@ -211,7 +211,7 @@ namespace storm {
VariableInformation variableInformation;
/// An evaluator used to evaluate expressions.
storm::expressions::ExpressionEvaluator<ValueType> evaluator;
std::unique_ptr<storm::expressions::ExpressionEvaluator<ValueType>> evaluator;
/// The currently loaded state.
CompressedState const* state;

35
src/generator/PrismNextStateGenerator.cpp
View File

@ -30,6 +30,9 @@ namespace storm {
this->checkValid();
this->variableInformation = VariableInformation(program);
// Create a proper evalator.
this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(program.getManager());
if (this->options.isBuildAllRewardModelsSet()) {
for (auto const& rewardModel : this->program.getRewardModels()) {
rewardModels.push_back(rewardModel);
@ -186,8 +189,8 @@ namespace storm {
ValueType stateRewardValue = storm::utility::zero<ValueType>();
if (rewardModel.get().hasStateRewards()) {
for (auto const& stateReward : rewardModel.get().getStateRewards()) {
if (this->evaluator.asBool(stateReward.getStatePredicateExpression())) {
stateRewardValue += ValueType(this->evaluator.asRational(stateReward.getRewardValueExpression()));
if (this->evaluator->asBool(stateReward.getStatePredicateExpression())) {
stateRewardValue += ValueType(this->evaluator->asRational(stateReward.getRewardValueExpression()));
}
}
}
@ -197,7 +200,7 @@ namespace storm {
// If a terminal expression was set and we must not expand this state, return now.
if (!this->terminalStates.empty()) {
for (auto const& expressionBool : this->terminalStates) {
if (this->evaluator.asBool(expressionBool.first) == expressionBool.second) {
if (this->evaluator->asBool(expressionBool.first) == expressionBool.second) {
return result;
}
}
@ -252,8 +255,8 @@ namespace storm {
if (rewardModel.get().hasStateActionRewards()) {
for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
for (auto const& choice : allChoices) {
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate;
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator->asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate;
}
}
@ -295,7 +298,7 @@ namespace storm {
while (assignmentIt->getVariable() != boolIt->variable) {
++boolIt;
}
newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getExpression()));
newState.set(boolIt->bitOffset, this->evaluator->asBool(assignmentIt->getExpression()));
}
// Iterate over all integer assignments and carry them out.
@ -304,7 +307,7 @@ namespace storm {
while (assignmentIt->getVariable() != integerIt->variable) {
++integerIt;
}
int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getExpression());
int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getExpression());
STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
@ -343,7 +346,7 @@ namespace storm {
// Look up commands by their indices and add them if the guard evaluates to true in the given state.
for (uint_fast64_t commandIndex : commandIndices) {
storm::prism::Command const& command = module.getCommand(commandIndex);
if (this->evaluator.asBool(command.getGuardExpression())) {
if (this->evaluator->asBool(command.getGuardExpression())) {
commands.push_back(command);
}
}
@ -376,7 +379,7 @@ namespace storm {
if (command.isLabeled()) continue;
// Skip the command, if it is not enabled.
if (!this->evaluator.asBool(command.getGuardExpression())) {
if (!this->evaluator->asBool(command.getGuardExpression())) {
continue;
}
@ -398,7 +401,7 @@ namespace storm {
StateType stateIndex = stateToIdCallback(applyUpdate(state, update));
// Update the choice by adding the probability/target state to it.
ValueType probability = this->evaluator.asRational(update.getLikelihoodExpression());
ValueType probability = this->evaluator->asRational(update.getLikelihoodExpression());
choice.addProbability(stateIndex, probability);
probabilitySum += probability;
}
@ -408,8 +411,8 @@ namespace storm {
ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
if (rewardModel.get().hasStateActionRewards()) {
for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression()));
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator->asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression()));
}
}
}
@ -462,9 +465,9 @@ namespace storm {
// and otherwise insert it.
auto targetStateIt = newTargetStates->find(newTargetState);
if (targetStateIt != newTargetStates->end()) {
targetStateIt->second += stateProbabilityPair.second * this->evaluator.asRational(update.getLikelihoodExpression());
targetStateIt->second += stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression());
} else {
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(update.getLikelihoodExpression()));
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression()));
}
}
}
@ -509,8 +512,8 @@ namespace storm {
ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
if (rewardModel.get().hasStateActionRewards()) {
for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression()));
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator->asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression()));
}
}
}

5
src/generator/VariableInformation.cpp
View File

@ -2,6 +2,7 @@
#include "src/storage/prism/Program.h"
#include "src/storage/jani/Model.h"
#include "src/storage/expressions/ExpressionManager.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
@ -19,7 +20,7 @@ namespace storm {
// Intentionally left empty.
}
LocationVariableInformation::LocationVariableInformation(uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth) {
LocationVariableInformation::LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth) {
// Intentionally left empty.
}
@ -74,7 +75,7 @@ namespace storm {
}
for (auto const& automaton : model.getAutomata()) {
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(automaton.getNumberOfLocations())));
locationVariables.emplace_back(automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth);
locationVariables.emplace_back(model.getManager().declareFreshIntegerVariable(false, "loc"), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth);
totalBitOffset += bitwidth;
for (auto const& variable : automaton.getVariables().getBooleanVariables()) {

5
src/generator/VariableInformation.h
View File

@ -56,7 +56,10 @@ namespace storm {
// A structure storing information about the location variables of the model.
struct LocationVariableInformation {
LocationVariableInformation(uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
// The expression variable for this location.
storm::expressions::Variable variable;
// The highest possible location value.
uint64_t highestValue;

2
src/storage/BitVector.h
View File

@ -472,7 +472,7 @@ namespace storm {
* value is equal to a call to size(), then there is no bit set after the specified position.
*
* @param startingIndex The index at which to start the search for the next bit that is set. The
* bit at this index itself is already considered.
* bit at this index itself is included in the search range.
* @return The index of the next bit that is set after the given index.
*/
uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const;

33
src/storage/jani/Model.cpp
View File

@ -7,6 +7,7 @@
#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidOperationException.h"
#include "src/exceptions/InvalidTypeException.h"
@ -456,7 +457,39 @@ namespace storm {
STORM_LOG_ASSERT(getModelType() != storm::jani::ModelType::UNDEFINED, "Model type not set");
STORM_LOG_ASSERT(!automata.empty(), "No automata set");
STORM_LOG_ASSERT(composition != nullptr, "Composition is not set");
}
storm::expressions::Expression Model::getLabelExpression(BooleanVariable const& transientVariable, std::map<std::string, storm::expressions::Variable> const& automatonToLocationVariableMap) const {
STORM_LOG_THROW(transientVariable.isTransient(), storm::exceptions::InvalidArgumentException, "Expected transient variable.");
storm::expressions::Expression result;
bool negate = transientVariable.getInitExpression().isTrue();
for (auto const& automaton : this->getAutomata()) {
storm::expressions::Variable const& locationVariable = automatonToLocationVariableMap.at(automaton.getName());
for (auto const& location : automaton.getLocations()) {
for (auto const& assignment : location.getAssignments().getTransientAssignments()) {
if (assignment.getExpressionVariable() == transientVariable.getExpressionVariable()) {
auto newExpression = (locationVariable == this->getManager().integer(automaton.getLocationIndex(location.getName()))) && (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression());
if (result.isInitialized()) {
result = result || newExpression;
} else {
result = newExpression;
}
}
}
}
}
if (result.isInitialized()) {
if (negate) {
result = !result;
}
} else {
result = this->getManager().boolean(negate);
}
return result;
}
bool Model::hasStandardComposition() const {

6
src/storage/jani/Model.h
View File

@ -326,6 +326,12 @@ namespace storm {
*/
void checkValid() const;
/*!
* Creates the expression that characterizes all states in which the provided transient boolean variable is
* true. The provided location variables are used to encode the location of the automata.
*/
storm::expressions::Expression getLabelExpression(BooleanVariable const& transientVariable, std::map<std::string, storm::expressions::Variable> const& automatonToLocationVariableMap) const;
/*!
* Checks that undefined constants (parameters) of the model preserve the graph of the underlying model.
* That is, undefined constants may only appear in the probability expressions of edge destinations as well

20
src/storage/jani/VariableSet.cpp
View File

@ -176,6 +176,26 @@ namespace storm {
return result;
}
uint_fast64_t VariableSet::getNumberOfRealTransientVariables() const {
uint_fast64_t result = 0;
for (auto const& variable : variables) {
if (variable->isTransient() && variable->isRealVariable()) {
++result;
}
}
return result;
}
uint_fast64_t VariableSet::getNumberOfUnboundedIntegerTransientVariables() const {
uint_fast64_t result = 0;
for (auto const& variable : variables) {
if (variable->isTransient() && variable->isUnboundedIntegerVariable()) {
++result;
}
}
return result;
}
std::vector<std::shared_ptr<Variable const>> VariableSet::getTransientVariables() const {
std::vector<std::shared_ptr<Variable const>> result;
for (auto const& variable : variables) {

10
src/storage/jani/VariableSet.h
View File

@ -173,6 +173,16 @@ namespace storm {
*/
uint_fast64_t getNumberOfTransientVariables() const;
/*!
* Retrieves the number of real transient variables in this variable set.
*/
uint_fast64_t getNumberOfRealTransientVariables() const;
/*!
* Retrieves the number of unbounded integer transient variables in this variable set.
*/
uint_fast64_t getNumberOfUnboundedIntegerTransientVariables() const;
/*!
* Retrieves a vector of transient variables in this variable set.
*/

Write Preview
Loading…
Cancel
Save