From b62f8819b9f68c8f7fad584d127708053edd4c7a Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 14 Jun 2016 21:41:27 +0200
Subject: [PATCH] JANI next-state generator can now generate transitions from
silent edges
Former-commit-id: 57e37b58506d56b41c0612e8a2c1b2dc64280062
---
src/builder/DdJaniModelBuilder.cpp | 14 +--
src/generator/JaniNextStateGenerator.cpp | 113 ++++++++++++++++++
src/generator/JaniNextStateGenerator.h | 1 +
src/generator/NextStateGenerator.h | 1 +
src/generator/PrismNextStateGenerator.cpp | 13 +-
src/generator/PrismNextStateGenerator.h | 1 +
src/generator/VariableInformation.cpp | 10 +-
src/generator/VariableInformation.h | 27 ++++-
src/models/sparse/Model.h | 2 +-
src/storage/jani/Automaton.cpp | 12 +-
src/storage/jani/Automaton.h | 2 +-
.../jani/CompositionInformationVisitor.cpp | 43 +++++--
.../jani/CompositionInformationVisitor.h | 4 +-
src/storage/jani/Edge.cpp | 10 +-
src/storage/jani/Edge.h | 16 +--
src/storage/jani/EdgeDestination.cpp | 6 +-
src/storage/jani/EdgeDestination.h | 8 +-
src/storage/jani/Exporter.cpp | 6 +-
src/storage/jani/Model.cpp | 23 +++-
src/storage/jani/Model.h | 11 ++
src/storage/jani/RewardIncrement.cpp | 10 +-
src/storage/jani/RewardIncrement.h | 20 +++-
22 files changed, 286 insertions(+), 67 deletions(-)
diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index f981f4c60..fea680429 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -437,7 +437,7 @@ namespace storm {
}
}
- transitions *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationId()).template toAdd<ValueType>();
+ transitions *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationIndex()).template toAdd<ValueType>();
return EdgeDestinationDd<Type, ValueType>(transitions, assignedGlobalVariables);
}
@@ -841,7 +841,7 @@ namespace storm {
// If the edge is not labeled with the silent action, we have to analyze which portion of the global
// variables was written by any of the updates and make all update results equal w.r.t. this set. If
// the edge is labeled with the silent action, we can already multiply the identities of all global variables.
- if (edge.getActionId() != this->model.getSilentActionIndex()) {
+ if (edge.getActionIndex() != this->model.getSilentActionIndex()) {
for (auto const& edgeDestinationDd : destinationDds) {
globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end());
}
@@ -867,7 +867,7 @@ namespace storm {
}
// Add the source location and the guard.
- transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd<ValueType>() * guard;
+ transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.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 (!globalVariablesInSomeUpdate.empty()) {
@@ -895,7 +895,7 @@ namespace storm {
// Build the edge and add it if it adds transitions.
EdgeDd edgeDd = buildEdgeDd(automaton, edge);
if (!edgeDd.guard.isZero()) {
- result.actionIndexToEdges[edge.getActionId()].push_back(edgeDd);
+ result.actionIndexToEdges[edge.getActionIndex()].push_back(edgeDd);
}
}
@@ -1271,7 +1271,7 @@ namespace storm {
// If the edge is not labeled with the silent action, we have to analyze which portion of the global
// variables was written by any of the updates and make all update results equal w.r.t. this set. If
// the edge is labeled with the silent action, we can already multiply the identities of all global variables.
- if (edge.getActionId() != this->model.getSilentActionIndex()) {
+ if (edge.getActionIndex() != this->model.getSilentActionIndex()) {
for (auto const& edgeDestinationDd : destinationDds) {
globalVariablesInSomeDestination.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end());
}
@@ -1297,7 +1297,7 @@ namespace storm {
}
// Add the source location and the guard.
- transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd<ValueType>() * guard;
+ transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.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()) {
@@ -1319,7 +1319,7 @@ namespace storm {
// Translate the individual edges.
std::vector<EdgeDd> edgeDds;
for (auto const& edge : automaton.getEdges()) {
- if (edge.getActionId() == actionIndex) {
+ if (edge.getActionIndex() == actionIndex) {
edgeDds.push_back(buildEdgeDd(automaton, edge));
}
}
diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index eea91cb0b..a71112cb8 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/src/generator/JaniNextStateGenerator.cpp
@@ -24,6 +24,7 @@ namespace storm {
JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), VariableInformation(model), options), model(model) {
STORM_LOG_THROW(!this->model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
STORM_LOG_THROW(!this->options.isBuildAllRewardModelsSet() && this->options.getRewardModelNames().empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support building reward models.");
+ STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels.");
// If there are terminal states we need to handle, we now need to translate all labels to expressions.
if (this->options.hasTerminalStates()) {
@@ -53,6 +54,11 @@ namespace storm {
bool JaniNextStateGenerator<ValueType, StateType>::isDeterministicModel() const {
return model.isDeterministicModel();
}
+
+ template<typename ValueType, typename StateType>
+ bool JaniNextStateGenerator<ValueType, StateType>::isDiscreteTimeModel() const {
+ return model.isDiscreteTimeModel();
+ }
template<typename ValueType, typename StateType>
std::vector<StateType> JaniNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
@@ -104,6 +110,11 @@ namespace storm {
CompressedState JaniNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination) {
CompressedState newState(state);
+ // NOTE: the following process assumes that the assignments of the destination are ordered in such a way
+ // that the assignments to boolean variables precede the assignments to all integer variables and that
+ // within the types, the assignments to variables are ordered (in ascending order) by the expression variables.
+ // This is guaranteed for JANI models, by sorting the assignments as soon as an edge destination is created.
+
auto assignmentIt = destination.getAssignments().begin();
auto assignmentIte = destination.getAssignments().end();
@@ -136,12 +147,114 @@ namespace storm {
template<typename ValueType, typename StateType>
StateBehavior<ValueType, StateType> JaniNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
+ // Prepare the result, in case we return early.
+ StateBehavior<ValueType, StateType> result;
+
+ // 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) {
+ return result;
+ }
+ }
+ }
+ // Get all choices for the state.
+ std::vector<Choice<ValueType>> allChoices = getSilentActionChoices(*this->state, stateToIdCallback);
+ std::vector<Choice<ValueType>> allLabeledChoices = getNonsilentActionChoices(*this->state, stateToIdCallback);
+ for (auto& choice : allLabeledChoices) {
+ allChoices.push_back(std::move(choice));
+ }
+
+ std::size_t totalNumberOfChoices = allChoices.size();
+
+ // If there is not a single choice, we return immediately, because the state has no behavior (other than
+ // the state reward).
+ if (totalNumberOfChoices == 0) {
+ return result;
+ }
+
+ // If the model is a deterministic model, we need to fuse the choices into one.
+ if (this->isDeterministicModel() && totalNumberOfChoices > 1) {
+ Choice<ValueType> globalChoice;
+
+ // Iterate over all choices and combine the probabilities/rates into one choice.
+ for (auto const& choice : allChoices) {
+ for (auto const& stateProbabilityPair : choice) {
+ if (this->isDiscreteTimeModel()) {
+ globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second / totalNumberOfChoices);
+ } else {
+ globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second);
+ }
+ }
+
+ if (this->options.isBuildChoiceLabelsSet()) {
+ globalChoice.addChoiceLabels(choice.getChoiceLabels());
+ }
+ }
+
+ // Move the newly fused choice in place.
+ allChoices.clear();
+ allChoices.push_back(std::move(globalChoice));
+ }
+
+ // Move all remaining choices in place.
+ for (auto& choice : allChoices) {
+ result.addChoice(std::move(choice));
+ }
+
+ result.setExpanded();
+ return result;
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getSilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) {
+ std::vector<Choice<ValueType>> result;
+
+ // Iterate over all automata.
+ auto locationVariableIt = this->variableInformation.locationVariables.begin();
+ for (auto const& automaton : model.getAutomata()) {
+
+ // Determine the location of the automaton in the given state.
+ uint64_t locationIndex = state.getAsInt(locationVariableIt->bitOffset, locationVariableIt->bitWidth);
+
+ // Iterate over all edges from the source location.
+ for (auto const& edge : automaton.getEdgesFromLocation(locationIndex)) {
+ // Skip the edge if it is labeled with a non-silent action.
+ if (edge.getActionIndex() != model.getSilentActionIndex()) {
+ continue;
+ }
+
+ // Skip the command, if it is not enabled.
+ if (!this->evaluator.asBool(edge.getGuard())) {
+ continue;
+ }
+
+ result.push_back(Choice<ValueType>(edge.getActionIndex()));
+ Choice<ValueType>& choice = result.back();
+
+ // Iterate over all updates of the current command.
+ ValueType probabilitySum = storm::utility::zero<ValueType>();
+ for (auto const& destination : edge.getDestinations()) {
+ // Obtain target state index and add it to the list of known states. If it has not yet been
+ // seen, we also add it to the set of states that have yet to be explored.
+ StateType stateIndex = stateToIdCallback(applyUpdate(state, destination));
+
+ // Update the choice by adding the probability/target state to it.
+ ValueType probability = this->evaluator.asRational(destination.getProbability());
+ choice.addProbability(stateIndex, probability);
+ probabilitySum += probability;
+ }
+
+ // Check that the resulting distribution is in fact a distribution.
+ STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ").");
+ }
+
+ // After we have processed all edges of the current automaton, move to the next location variable.
+ ++locationVariableIt;
+ }
+ return result;
}
template<typename ValueType, typename StateType>
diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h
index 24d62d456..1d6241ab7 100644
--- a/src/generator/JaniNextStateGenerator.h
+++ b/src/generator/JaniNextStateGenerator.h
@@ -16,6 +16,7 @@ namespace storm {
virtual ModelType getModelType() const override;
virtual bool isDeterministicModel() const override;
+ virtual bool isDiscreteTimeModel() const override;
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h
index 7e5c1e869..218efe32d 100644
--- a/src/generator/NextStateGenerator.h
+++ b/src/generator/NextStateGenerator.h
@@ -165,6 +165,7 @@ namespace storm {
uint64_t getStateSize() const;
virtual ModelType getModelType() const = 0;
virtual bool isDeterministicModel() const = 0;
+ virtual bool isDiscreteTimeModel() const = 0;
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
void load(CompressedState const& state);
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
index 7a530432b..dcac0ebc6 100644
--- a/src/generator/PrismNextStateGenerator.cpp
+++ b/src/generator/PrismNextStateGenerator.cpp
@@ -82,6 +82,11 @@ namespace storm {
return program.isDeterministicModel();
}
+ template<typename ValueType, typename StateType>
+ bool PrismNextStateGenerator<ValueType, StateType>::isDiscreteTimeModel() const {
+ return program.isDiscreteTimeModel();
+ }
+
template<typename ValueType, typename StateType>
std::vector<StateType> PrismNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
// Prepare an SMT solver to enumerate all initial states.
@@ -172,24 +177,24 @@ namespace storm {
}
// If the model is a deterministic model, we need to fuse the choices into one.
- if (program.isDeterministicModel() && totalNumberOfChoices > 1) {
+ if (this->isDeterministicModel() && totalNumberOfChoices > 1) {
Choice<ValueType> globalChoice;
// For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs
// this is equal to the number of choices, which is why we initialize it like this here.
- ValueType totalExitRate = program.isDiscreteTimeModel() ? static_cast<ValueType>(totalNumberOfChoices) : storm::utility::zero<ValueType>();
+ ValueType totalExitRate = this->isDiscreteTimeModel() ? static_cast<ValueType>(totalNumberOfChoices) : storm::utility::zero<ValueType>();
// Iterate over all choices and combine the probabilities/rates into one choice.
for (auto const& choice : allChoices) {
for (auto const& stateProbabilityPair : choice) {
- if (program.isDiscreteTimeModel()) {
+ if (this->isDiscreteTimeModel()) {
globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second / totalNumberOfChoices);
} else {
globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second);
}
}
- if (hasStateActionRewards && !program.isDiscreteTimeModel()) {
+ if (hasStateActionRewards && !this->isDiscreteTimeModel()) {
totalExitRate += choice.getTotalMass();
}
diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h
index 273ac5bf6..1a49225d0 100644
--- a/src/generator/PrismNextStateGenerator.h
+++ b/src/generator/PrismNextStateGenerator.h
@@ -17,6 +17,7 @@ namespace storm {
virtual ModelType getModelType() const override;
virtual bool isDeterministicModel() const override;
+ virtual bool isDiscreteTimeModel() const override;
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp
index 1c7fc7a60..f941cc653 100644
--- a/src/generator/VariableInformation.cpp
+++ b/src/generator/VariableInformation.cpp
@@ -17,6 +17,10 @@ namespace storm {
// Intentionally left empty.
}
+ LocationVariableInformation::LocationVariableInformation(uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth) {
+ // Intentionally left empty.
+ }
+
VariableInformation::VariableInformation(storm::prism::Program const& program) : totalBitOffset(0) {
for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset);
@@ -42,7 +46,7 @@ namespace storm {
totalBitOffset += bitwidth;
}
}
-
+
sortVariables();
}
@@ -59,6 +63,10 @@ namespace storm {
totalBitOffset += bitwidth;
}
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);
+ totalBitOffset += bitwidth;
+
for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset);
++totalBitOffset;
diff --git a/src/generator/VariableInformation.h b/src/generator/VariableInformation.h
index 8ee9ac8f6..fa913f86c 100644
--- a/src/generator/VariableInformation.h
+++ b/src/generator/VariableInformation.h
@@ -17,7 +17,7 @@ namespace storm {
namespace generator {
- // A structure storing information about the boolean variables of the program.
+ // A structure storing information about the boolean variables of the model.
struct BooleanVariableInformation {
BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset);
@@ -28,7 +28,7 @@ namespace storm {
uint_fast64_t bitOffset;
};
- // A structure storing information about the integer variables of the program.
+ // A structure storing information about the integer variables of the model.
struct IntegerVariableInformation {
IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
@@ -48,6 +48,20 @@ namespace storm {
uint_fast64_t bitWidth;
};
+ // 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);
+
+ // The highest possible location value.
+ uint64_t highestValue;
+
+ // Its bit offset in the compressed state.
+ uint_fast64_t bitOffset;
+
+ // Its bit width in the compressed state.
+ uint_fast64_t bitWidth;
+ };
+
// A structure storing information about the used variables of the program.
struct VariableInformation {
VariableInformation(storm::prism::Program const& program);
@@ -56,13 +70,16 @@ namespace storm {
VariableInformation() = default;
uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const;
- // The total bit offset over all variables.
+ /// The total bit offset over all variables.
uint_fast64_t totalBitOffset;
- // The known boolean variables.
+ /// The location variables.
+ std::vector<LocationVariableInformation> locationVariables;
+
+ /// The boolean variables.
std::vector<BooleanVariableInformation> booleanVariables;
- // The known integer variables.
+ /// The integer variables.
std::vector<IntegerVariableInformation> integerVariables;
private:
diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h
index a73b10c8f..bd4c9921b 100644
--- a/src/models/sparse/Model.h
+++ b/src/models/sparse/Model.h
@@ -342,7 +342,7 @@ namespace storm {
* @param out The stream the information is to be printed to.
*/
void printRewardModelsInformationToStream(std::ostream& out) const;
-
+
private:
// A matrix representing transition relation.
storm::storage::SparseMatrix<ValueType> transitionMatrix;
diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp
index 1db2c5bfb..372252a14 100644
--- a/src/storage/jani/Automaton.cpp
+++ b/src/storage/jani/Automaton.cpp
@@ -90,7 +90,7 @@ namespace storm {
return locations.size() - 1;
}
- uint64_t Automaton::getLocationId(std::string const& name) const {
+ uint64_t Automaton::getLocationIndex(std::string const& name) const {
assert(hasLocation(name));
return locationToIndex.at(name);
}
@@ -143,20 +143,20 @@ namespace storm {
}
void Automaton::addEdge(Edge const& edge) {
- STORM_LOG_THROW(edge.getSourceLocationId() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationId() << "'.");
+ STORM_LOG_THROW(edge.getSourceLocationIndex() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationIndex() << "'.");
// Find the right position for the edge and insert it properly.
auto posIt = edges.begin();
- std::advance(posIt, locationToStartingIndex[edge.getSourceLocationId() + 1]);
+ std::advance(posIt, locationToStartingIndex[edge.getSourceLocationIndex() + 1]);
edges.insert(posIt, edge);
// Now update the starting indices of all subsequent locations.
- for (uint64_t locationIndex = edge.getSourceLocationId() + 1; locationIndex < locationToStartingIndex.size(); ++locationIndex) {
+ for (uint64_t locationIndex = edge.getSourceLocationIndex() + 1; locationIndex < locationToStartingIndex.size(); ++locationIndex) {
++locationToStartingIndex[locationIndex];
}
// Update the set of action indices of this automaton.
- actionIndices.insert(edge.getActionId());
+ actionIndices.insert(edge.getActionIndex());
}
std::vector<Edge>& Automaton::getEdges() {
@@ -170,7 +170,7 @@ namespace storm {
std::set<uint64_t> Automaton::getActionIndices() const {
std::set<uint64_t> result;
for (auto const& edge : edges) {
- result.insert(edge.getActionId());
+ result.insert(edge.getActionIndex());
}
return result;
}
diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h
index 86e3f4a7c..0fdb3ecfc 100644
--- a/src/storage/jani/Automaton.h
+++ b/src/storage/jani/Automaton.h
@@ -123,7 +123,7 @@ namespace storm {
*
* @name the name of the location
*/
- uint64_t getLocationId(std::string const& name) const;
+ uint64_t getLocationIndex(std::string const& name) const;
/*!
* Retrieves the locations of the automaton.
diff --git a/src/storage/jani/CompositionInformationVisitor.cpp b/src/storage/jani/CompositionInformationVisitor.cpp
index 496332fd1..541b55698 100644
--- a/src/storage/jani/CompositionInformationVisitor.cpp
+++ b/src/storage/jani/CompositionInformationVisitor.cpp
@@ -15,15 +15,26 @@ namespace storm {
}
void CompositionInformation::addNonsilentAction(std::string const& actionName) {
- // FIXME
+ nonsilentActions.insert(actionName);
}
std::set<std::string> const& CompositionInformation::getNonsilentActions() const {
- // FIXME
+ return nonsilentActions;
}
- void CompositionInformation::renameNonsilentActions(std::map<std::string, std::string> const& renaming) {
- // FIXME
+ std::set<std::string> CompositionInformation::renameNonsilentActions(std::set<std::string> const& nonsilentActions, std::map<std::string, boost::optional<std::string>> const& renaming) {
+ std::set<std::string> newNonsilentActions;
+ for (auto const& entry : nonsilentActions) {
+ auto it = renaming.find(entry);
+ if (it != renaming.end()) {
+ if (it->second) {
+ newNonsilentActions.insert(it->second.get());
+ }
+ } else {
+ newNonsilentActions.insert(entry);
+ }
+ }
+ return newNonsilentActions;
}
void CompositionInformation::setContainsRenameComposition() {
@@ -59,19 +70,26 @@ namespace storm {
}
boost::any CompositionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) {
+ Model const& model = boost::any_cast<Model const&>(data);
+ Automaton const& automaton = model.getAutomaton(composition.getAutomatonName());
+
CompositionInformation result;
result.increaseAutomatonMultiplicity(composition.getAutomatonName());
+ for (auto const& actionIndex : automaton.getActionIndices()) {
+ if (actionIndex != model.getSilentActionIndex()) {
+ result.addNonsilentAction(model.getAction(actionIndex).getName());
+ }
+ }
return result;
}
boost::any CompositionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) {
CompositionInformation subresult = boost::any_cast<CompositionInformation>(composition.getSubcomposition().accept(*this, data));
- subresult.setContainsRenameComposition();
- return subresult;
+ std::set<std::string> nonsilentActions = CompositionInformation::renameNonsilentActions(subresult.getNonsilentActions(), composition.getRenaming());
+ return CompositionInformation(subresult.getAutomatonToMultiplicityMap(), nonsilentActions, true, subresult.containsRestrictedParallelComposition());
}
boost::any CompositionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) {
- Model const& model = boost::any_cast<Model const&>(data);
CompositionInformation left = boost::any_cast<CompositionInformation>(composition.getLeftSubcomposition().accept(*this, data));
CompositionInformation right = boost::any_cast<CompositionInformation>(composition.getRightSubcomposition().accept(*this, data));
@@ -80,12 +98,19 @@ namespace storm {
bool containsRestrictedParallelComposition = left.containsRestrictedParallelComposition() || right.containsRestrictedParallelComposition();
std::map<std::string, uint64_t> joinedAutomatonToMultiplicity = CompositionInformation::joinMultiplicityMaps(left.getAutomatonToMultiplicityMap(), right.getAutomatonToMultiplicityMap());
+ std::set<std::string> nonsilentActions;
+ std::set_union(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(nonsilentActions, nonsilentActions.begin()));
+
// If there was no restricted parallel composition yet, maybe the current composition is one, so check it.
if (!containsRestrictedParallelComposition) {
- // FIXME.
+ std::set<std::string> commonNonsilentActions;
+ std::set_intersection(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(commonNonsilentActions, commonNonsilentActions.begin()));
+ if (commonNonsilentActions != composition.getSynchronizationAlphabet()) {
+ containsRestrictedParallelComposition = true;
+ }
}
- return CompositionInformation(joinedAutomatonToMultiplicity, containsRenameComposition, containsRestrictedParallelComposition);
+ return CompositionInformation(joinedAutomatonToMultiplicity, nonsilentActions, containsRenameComposition, containsRestrictedParallelComposition);
}
}
diff --git a/src/storage/jani/CompositionInformationVisitor.h b/src/storage/jani/CompositionInformationVisitor.h
index 8454fbc9e..9baa2c363 100644
--- a/src/storage/jani/CompositionInformationVisitor.h
+++ b/src/storage/jani/CompositionInformationVisitor.h
@@ -4,6 +4,8 @@
#include <set>
#include <cstdint>
+#include <boost/optional.hpp>
+
#include "src/storage/jani/CompositionVisitor.h"
namespace storm {
@@ -20,7 +22,7 @@ namespace storm {
void addNonsilentAction(std::string const& actionName);
std::set<std::string> const& getNonsilentActions() const;
- void renameNonsilentActions(std::map<std::string, std::string> const& renaming);
+ static std::set<std::string> renameNonsilentActions(std::set<std::string> const& nonsilentActions, std::map<std::string, boost::optional<std::string>> const& renaming);
void setContainsRenameComposition();
bool containsRenameComposition() const;
diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp
index 8176952a8..deaac34e5 100644
--- a/src/storage/jani/Edge.cpp
+++ b/src/storage/jani/Edge.cpp
@@ -3,16 +3,16 @@
namespace storm {
namespace jani {
- Edge::Edge(uint64_t sourceLocationId, uint64_t actionId, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations) : sourceLocationId(sourceLocationId), actionId(actionId), rate(rate), guard(guard), destinations(destinations) {
+ Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations) : sourceLocationIndex(sourceLocationIndex), actionIndex(actionIndex), rate(rate), guard(guard), destinations(destinations) {
// Intentionally left empty.
}
- uint64_t Edge::getSourceLocationId() const {
- return sourceLocationId;
+ uint64_t Edge::getSourceLocationIndex() const {
+ return sourceLocationIndex;
}
- uint64_t Edge::getActionId() const {
- return actionId;
+ uint64_t Edge::getActionIndex() const {
+ return actionIndex;
}
bool Edge::hasRate() const {
diff --git a/src/storage/jani/Edge.h b/src/storage/jani/Edge.h
index 1571bf9c1..5e835fa80 100644
--- a/src/storage/jani/Edge.h
+++ b/src/storage/jani/Edge.h
@@ -9,17 +9,17 @@ namespace storm {
class Edge {
public:
- Edge(uint64_t sourceLocationId, uint64_t actionId, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations = {});
+ Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations = {});
/*!
- * Retrieves the id of the source location.
+ * Retrieves the index of the source location.
*/
- uint64_t getSourceLocationId() const;
+ uint64_t getSourceLocationIndex() const;
/*!
* Retrieves the id of the action with which this edge is labeled.
*/
- uint64_t getActionId() const;
+ uint64_t getActionIndex() const;
/*!
* Retrieves whether this edge has an associated rate.
@@ -62,11 +62,11 @@ namespace storm {
void addDestination(EdgeDestination const& destination);
private:
- // The id of the source location.
- uint64_t sourceLocationId;
+ // The index of the source location.
+ uint64_t sourceLocationIndex;
- // The id of the action with which this edge is labeled.
- uint64_t actionId;
+ // The index of the action with which this edge is labeled.
+ uint64_t actionIndex;
// The rate with which this edge is taken. This only applies to continuous-time models. For discrete-time
// models, this must be set to none.
diff --git a/src/storage/jani/EdgeDestination.cpp b/src/storage/jani/EdgeDestination.cpp
index cdd295349..1166488e3 100644
--- a/src/storage/jani/EdgeDestination.cpp
+++ b/src/storage/jani/EdgeDestination.cpp
@@ -6,7 +6,7 @@
namespace storm {
namespace jani {
- EdgeDestination::EdgeDestination(uint64_t locationId, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments, std::vector<RewardIncrement> const& rewardIncrements) : locationId(locationId), probability(probability), assignments(assignments), rewardIncrements(rewardIncrements) {
+ EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments, std::vector<RewardIncrement> const& rewardIncrements) : locationIndex(locationIndex), probability(probability), assignments(assignments), rewardIncrements(rewardIncrements) {
sortAssignments();
}
@@ -23,8 +23,8 @@ namespace storm {
rewardIncrements.push_back(rewardIncrement);
}
- uint64_t EdgeDestination::getLocationId() const {
- return locationId;
+ uint64_t EdgeDestination::getLocationIndex() const {
+ return locationIndex;
}
storm::expressions::Expression const& EdgeDestination::getProbability() const {
diff --git a/src/storage/jani/EdgeDestination.h b/src/storage/jani/EdgeDestination.h
index 5ccd79da2..eb33bb7fc 100644
--- a/src/storage/jani/EdgeDestination.h
+++ b/src/storage/jani/EdgeDestination.h
@@ -15,7 +15,7 @@ namespace storm {
/*!
* Creates a new edge destination.
*/
- EdgeDestination(uint64_t locationId, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments = {}, std::vector<RewardIncrement> const& rewardIncrements = {});
+ EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments = {}, std::vector<RewardIncrement> const& rewardIncrements = {});
/*!
* Additionally performs the given assignment when choosing this destination.
@@ -30,7 +30,7 @@ namespace storm {
/*!
* Retrieves the id of the destination location.
*/
- uint64_t getLocationId() const;
+ uint64_t getLocationIndex() const;
/*!
* Retrieves the probability of choosing this destination.
@@ -64,8 +64,8 @@ namespace storm {
*/
void sortAssignments();
- // The id of the destination location.
- uint64_t locationId;
+ // The index of the destination location.
+ uint64_t locationIndex;
// The probability to go to the destination.
storm::expressions::Expression probability;
diff --git a/src/storage/jani/Exporter.cpp b/src/storage/jani/Exporter.cpp
index bf7eb6c00..217f61465 100644
--- a/src/storage/jani/Exporter.cpp
+++ b/src/storage/jani/Exporter.cpp
@@ -242,7 +242,7 @@ namespace storm {
appendIndent(out, indent + 1);
appendField(out, "location");
- appendValue(out, automaton.getLocation(destination.getLocationId()).getName());
+ appendValue(out, automaton.getLocation(destination.getLocationIndex()).getName());
out << ",";
clearLine(out);
@@ -275,13 +275,13 @@ namespace storm {
appendIndent(out, indent + 1);
appendField(out, "location");
- appendValue(out, automaton.getLocation(edge.getSourceLocationId()).getName());
+ appendValue(out, automaton.getLocation(edge.getSourceLocationIndex()).getName());
out << ",";
clearLine(out);
appendIndent(out, indent + 1);
appendField(out, "action");
- appendValue(out, model.getAction(edge.getActionId()).getName());
+ appendValue(out, model.getAction(edge.getActionIndex()).getName());
out << ",";
clearLine(out);
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index 079f9d7ec..b83fead78 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -2,9 +2,8 @@
#include "src/storage/expressions/ExpressionManager.h"
-#include "src/storage/jani/AutomatonComposition.h"
-#include "src/storage/jani/ParallelComposition.h"
-#include "src/storage/jani/RenameComposition.h"
+#include "src/storage/jani/Compositions.h"
+#include "src/storage/jani/CompositionInformationVisitor.h"
#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
@@ -357,6 +356,10 @@ namespace storm {
return this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::CTMC;
}
+ bool Model::isDiscreteTimeModel() const {
+ return this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::MDP;
+ }
+
std::vector<storm::expressions::Expression> Model::getAllRangeExpressions() const {
std::vector<storm::expressions::Expression> result;
for (auto const& variable : this->getGlobalVariables().getBoundedIntegerVariables()) {
@@ -392,5 +395,19 @@ namespace storm {
}
+ bool Model::hasDefaultComposition() const {
+ CompositionInformationVisitor visitor;
+ CompositionInformation info = visitor.getInformation(this->getSystemComposition(), *this);
+ if (info.containsRestrictedParallelComposition() || info.containsRenameComposition()) {
+ return false;
+ }
+ for (auto const& multiplicity : info.getAutomatonToMultiplicityMap()) {
+ if (multiplicity.second > 1) {
+ return false;
+ }
+ }
+ return true;
+ }
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h
index caa5c730b..094c650ce 100644
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@@ -248,11 +248,22 @@ namespace storm {
*/
bool isDeterministicModel() const;
+ /*!
+ * Determines whether this model is a discrete-time model.
+ */
+ bool isDiscreteTimeModel() const;
+
/*!
* Retrieves a list of expressions that characterize the legal values of the variables in this model.
*/
std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
+ /*!
+ * Retrieves whether this model has the default composition, that is it composes all automata in parallel
+ * and synchronizes over all common actions.
+ */
+ bool hasDefaultComposition() const;
+
/*!
* Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.
*/
diff --git a/src/storage/jani/RewardIncrement.cpp b/src/storage/jani/RewardIncrement.cpp
index 500cc9b33..b82743d45 100644
--- a/src/storage/jani/RewardIncrement.cpp
+++ b/src/storage/jani/RewardIncrement.cpp
@@ -3,9 +3,17 @@
namespace storm {
namespace jani {
- RewardIncrement::RewardIncrement(uint64_t rewardId, storm::expressions::Expression const& value) : rewardId(rewardId), value(value) {
+ RewardIncrement::RewardIncrement(uint64_t rewardIndex, storm::expressions::Expression const& value) : rewardIndex(rewardIndex), value(value) {
// Intentionally left empty.
}
+ uint64_t RewardIncrement::getRewardIndex() const {
+ return rewardIndex;
+ }
+
+ storm::expressions::Expression const& RewardIncrement::getValue() const {
+ return value;
+ }
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/RewardIncrement.h b/src/storage/jani/RewardIncrement.h
index 43b2211c1..383ce9fe0 100644
--- a/src/storage/jani/RewardIncrement.h
+++ b/src/storage/jani/RewardIncrement.h
@@ -10,16 +10,26 @@ namespace storm {
class RewardIncrement {
public:
/*!
- * Creates an increment of a reward (given by its id) by the given expression.
+ * Creates an increment of a reward (given by its index) by the given expression.
*
- * @param rewardId The id of the reward to increment.
+ * @param rewardIndex The index of the reward to increment.
* @param value The expression defining the amount the reward is the incremented.
*/
- RewardIncrement(uint64_t rewardId, storm::expressions::Expression const& value);
+ RewardIncrement(uint64_t rewardIndex, storm::expressions::Expression const& value);
+
+ /*!
+ * Retrieves the index of the reward to increment.
+ */
+ uint64_t getRewardIndex() const;
+
+ /*!
+ * Retrieves the expression defining the amount by which the reward is to be incremented.
+ */
+ storm::expressions::Expression const& getValue() const;
private:
- // The id of the reward that is to be incremented.
- uint64_t rewardId;
+ // The index of the reward that is to be incremented.
+ uint64_t rewardIndex;
// The expression defining the amount the reward is to be incremented.
storm::expressions::Expression value;