From 59a92a8941b50129c9092468eedff80515fa3b80 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 11 Oct 2016 16:05:47 +0200
Subject: [PATCH] support for labels in JANI models in sparse and dd engine
Former-commit-id: 34ad80be353fce2b47104e3a3d507450332b33de [formerly 67c09e4ff729c8f76b5f78912ac8062eabbed7f7]
Former-commit-id: 1bf8ab71a17cb4f967eec4ca496ffdcad8453ff6
---
src/builder/DdJaniModelBuilder.cpp | 75 +++++++++++++++----
src/builder/DdJaniModelBuilder.h | 20 +++++-
src/generator/CompressedState.cpp | 14 ++++
src/generator/JaniNextStateGenerator.cpp | 87 +++++++++++++++++++----
src/generator/JaniNextStateGenerator.h | 2 +-
src/generator/NextStateGenerator.cpp | 12 ++--
src/generator/NextStateGenerator.h | 2 +-
src/generator/PrismNextStateGenerator.cpp | 35 ++++-----
src/generator/VariableInformation.cpp | 5 +-
src/generator/VariableInformation.h | 7 +-
src/storage/BitVector.h | 2 +-
src/storage/jani/Model.cpp | 33 +++++++++
src/storage/jani/Model.h | 6 ++
src/storage/jani/VariableSet.cpp | 20 ++++++
src/storage/jani/VariableSet.h | 10 +++
15 files changed, 269 insertions(+), 61 deletions(-)
diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index 325cfb3a5..8b54e0eba 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -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>
@@ -112,7 +121,18 @@ namespace storm {
bool DdJaniModelBuilder<Type, ValueType>::Options::isBuildAllRewardModelsSet() const {
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,9 +266,14 @@ 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);
@@ -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);
}
diff --git a/src/builder/DdJaniModelBuilder.h b/src/builder/DdJaniModelBuilder.h
index dd99f5fcb..85c62b0bd 100644
--- a/src/builder/DdJaniModelBuilder.h
+++ b/src/builder/DdJaniModelBuilder.h
@@ -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>.
@@ -63,7 +63,23 @@ namespace storm {
* Retrieves the names of the reward models to build.
*/
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.
*/
@@ -98,4 +114,4 @@ namespace storm {
};
}
-}
\ No newline at end of file
+}
diff --git a/src/generator/CompressedState.cpp b/src/generator/CompressedState.cpp
index d7707d740..820b2000e 100644
--- a/src/generator/CompressedState.cpp
+++ b/src/generator/CompressedState.cpp
@@ -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));
}
diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index b84ffca3c..bc166cba3 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/src/generator/JaniNextStateGenerator.cpp
@@ -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;
}
}
diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h
index 7855bc5cf..7d5907c21 100644
--- a/src/generator/JaniNextStateGenerator.h
+++ b/src/generator/JaniNextStateGenerator.h
@@ -105,7 +105,7 @@ namespace storm {
* Checks the underlying model for validity for this next-state generator.
*/
void checkValid() const;
-
+
/// The model used for the generation of next states.
storm::jani::Model model;
diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp
index 08fe61ba1..cf15f0a3f 100644
--- a/src/generator/NextStateGenerator.cpp
+++ b/src/generator/NextStateGenerator.cpp
@@ -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);
}
}
diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h
index b2989b256..b9b7bfe23 100644
--- a/src/generator/NextStateGenerator.h
+++ b/src/generator/NextStateGenerator.h
@@ -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;
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
index 6eceb0c26..e344ab13a 100644
--- a/src/generator/PrismNextStateGenerator.cpp
+++ b/src/generator/PrismNextStateGenerator.cpp
@@ -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()));
}
}
}
diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp
index 125e6089d..c1a00e4e6 100644
--- a/src/generator/VariableInformation.cpp
+++ b/src/generator/VariableInformation.cpp
@@ -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()) {
diff --git a/src/generator/VariableInformation.h b/src/generator/VariableInformation.h
index 1aa8ee95c..0bbef3a6e 100644
--- a/src/generator/VariableInformation.h
+++ b/src/generator/VariableInformation.h
@@ -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;
@@ -98,4 +101,4 @@ namespace storm {
}
}
-#endif /* STORM_GENERATOR_VARIABLEINFORMATION_H_ */
\ No newline at end of file
+#endif /* STORM_GENERATOR_VARIABLEINFORMATION_H_ */
diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h
index c8b81709f..ecdd03536 100644
--- a/src/storage/BitVector.h
+++ b/src/storage/BitVector.h
@@ -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;
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index 343d88d78..ee2317df8 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -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 {
diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h
index 9a941a48f..35a74ead0 100644
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@@ -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
diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp
index a5468f63a..582fee73b 100644
--- a/src/storage/jani/VariableSet.cpp
+++ b/src/storage/jani/VariableSet.cpp
@@ -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) {
diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h
index 1c947669e..031d56652 100644
--- a/src/storage/jani/VariableSet.h
+++ b/src/storage/jani/VariableSet.h
@@ -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.
*/