From adf82328967fee2db5cf29acab07086b548e837e Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 31 May 2016 16:27:17 +0200
Subject: [PATCH] more work and fixes for symbolic JANI builder
Former-commit-id: 5ca11938c18c989dffd6cf9c7360a84bfbdfbc8a
---
src/builder/DdJaniModelBuilder.cpp | 136 ++++++++++++++++--
src/builder/DdPrismModelBuilder.cpp | 34 ++++-
src/storage/dd/DdManager.cpp | 7 +-
src/storage/jani/Automaton.cpp | 8 ++
src/storage/jani/Automaton.h | 5 +
src/storage/jani/BooleanVariable.cpp | 4 +
src/storage/jani/BooleanVariable.h | 2 +
src/storage/jani/BoundedIntegerVariable.cpp | 4 +
src/storage/jani/BoundedIntegerVariable.h | 2 +
src/storage/jani/Model.cpp | 27 +++-
src/storage/jani/ParallelComposition.cpp | 2 +-
src/storage/jani/UnboundedIntegerVariable.cpp | 4 +
src/storage/jani/UnboundedIntegerVariable.h | 2 +
src/storage/jani/Variable.cpp | 40 +++++-
src/storage/jani/Variable.h | 17 +++
src/storage/prism/Program.cpp | 37 ++---
.../builder/DdJaniModelBuilderTest.cpp | 73 +++++-----
.../builder/DdPrismModelBuilderTest.cpp | 5 +
18 files changed, 336 insertions(+), 73 deletions(-)
diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index a2b29f34b..c3bc7fc91 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -154,10 +154,10 @@ namespace storm {
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, storm::expressions::Variable> automatonToLocationVariableMap;
+ std::map<std::string, std::pair<storm::expressions::Variable, storm::expressions::Variable>> automatonToLocationVariableMap;
- // The meta variables used to encode the actions.
- std::vector<storm::expressions::Variable> actionVariables;
+ // A mapping from action indices to the meta variables used to encode these actions.
+ std::map<uint64_t, storm::expressions::Variable> actionVariablesMap;
// The meta variables used to encode the remaining nondeterminism.
std::vector<storm::expressions::Variable> nondeterminismVariables;
@@ -224,7 +224,7 @@ namespace storm {
for (auto const& action : this->model.getActions()) {
if (this->model.getActionIndex(action.getName()) != this->model.getSilentActionIndex()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(action.getName());
- result.actionVariables.push_back(variablePair.first);
+ result.actionVariablesMap[this->model.getActionIndex(action.getName())] = variablePair.first;
}
}
@@ -252,8 +252,8 @@ namespace storm {
storm::dd::Bdd<Type> range = result.manager->getBddOne();
// Start by creating a meta variable for the location of the automaton.
- std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations());
- result.automatonToLocationVariableMap[automaton.getName()] = variablePair.first;
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1);
+ result.automatonToLocationVariableMap[automaton.getName()] = variablePair;
storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(variablePair.first).equals(result.manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * result.manager->getRange(variablePair.first).template toAdd<ValueType>() * result.manager->getRange(variablePair.second).template toAdd<ValueType>();
identity &= variableIdentity.toBdd();
range &= result.manager->getRange(variablePair.first);
@@ -278,6 +278,7 @@ namespace storm {
}
void createVariable(storm::jani::BoundedIntegerVariable const& variable, CompositionVariables<Type, ValueType>& result) {
+ std::cout << "creating int variable " << variable.getName() << std::endl;
int_fast64_t low = variable.getLowerBound().evaluateAsInt();
int_fast64_t high = variable.getUpperBound().evaluateAsInt();
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getName(), low, high);
@@ -298,6 +299,7 @@ namespace storm {
}
void createVariable(storm::jani::BooleanVariable const& variable, CompositionVariables<Type, ValueType>& result) {
+ std::cout << "creating bool variable " << variable.getName() << std::endl;
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getName());
STORM_LOG_TRACE("Created meta variables for global boolean variable: " << variablePair.first.getName() << " and " << variablePair.second.getName() << ".");
@@ -405,6 +407,8 @@ namespace storm {
return result;
}
+ static int c = 0;
+
// A class that is responsible for performing the actual composition.
template <storm::dd::DdType Type, typename ValueType>
class AutomatonComposer : public storm::jani::CompositionVisitor {
@@ -523,11 +527,11 @@ namespace storm {
storm::dd::Add<Type, ValueType> writtenVariable = variables.manager->template getIdentity<ValueType>(primedMetaVariable);
// Translate the expression that is being assigned.
- storm::dd::Add<Type, ValueType> updateExpression = variables.rowExpressionAdapter->translateExpression(assignment.getExpressionVariable());
+ storm::dd::Add<Type, ValueType> updateExpression = variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
// Combine the update expression with the guard.
storm::dd::Add<Type, ValueType> result = updateExpression * guard;
-
+
// Combine the variable and the assigned expression.
result = result.equals(writtenVariable).template toAdd<ValueType>();
result *= guard;
@@ -535,6 +539,7 @@ namespace storm {
// Restrict the transitions to the range of the written variable.
result = result * variables.manager->getRange(primedMetaVariable).template toAdd<ValueType>();
+ // Combine the assignment DDs.
transitionsDd *= result;
}
@@ -558,7 +563,7 @@ namespace storm {
}
}
- return EdgeDestinationDd<Type, ValueType>(transitionsDd * variables.rowExpressionAdapter->translateExpression(destination.getProbability()), assignedGlobalVariables);
+ return EdgeDestinationDd<Type, ValueType>(variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationId()).template toAdd<ValueType>() * transitionsDd * variables.rowExpressionAdapter->translateExpression(destination.getProbability()), assignedGlobalVariables);
}
/*!
@@ -607,7 +612,10 @@ namespace storm {
transitionsDd += destinationDd.transitionsDd;
}
- return EdgeDd<Type, ValueType>(guard, guard * transitionsDd, globalVariablesInSomeUpdate);
+ transitionsDd.exportToDot("trans_edge" + std::to_string(c) + ".dot");
+ ++c;
+
+ return EdgeDd<Type, ValueType>(guard, variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd<ValueType>() * guard * transitionsDd, globalVariablesInSomeUpdate);
} else {
return EdgeDd<Type, ValueType>(variables.manager->template getAddZero<ValueType>(), variables.manager->template getAddZero<ValueType>());
}
@@ -638,6 +646,111 @@ namespace storm {
CompositionVariables<Type, ValueType> const& variables;
};
+ template <storm::dd::DdType Type, typename ValueType>
+ storm::dd::Add<Type, ValueType> encodeAction(uint64_t trueIndex, std::vector<storm::expressions::Variable> const& actionVariables, CompositionVariables<Type, ValueType> const& variables) {
+ storm::dd::Add<Type, ValueType> encoding = variables.manager->template getAddZero<ValueType>();
+
+ trueIndex = actionVariables.size() - (trueIndex + 1);
+ uint64_t index = 0;
+ for (auto it = actionVariables.rbegin(), ite = actionVariables.rend(); it != ite; ++it, ++index) {
+ if (index == trueIndex) {
+ encoding *= variables.manager->getEncoding(*it, 1).template toAdd<ValueType>();
+ } else {
+ encoding *= variables.manager->getEncoding(*it, 0).template toAdd<ValueType>();
+ }
+ }
+
+ return encoding;
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ storm::dd::Add<Type, ValueType> computeMissingGlobalVariableIdentities(EdgeDd<Type, ValueType> const& edge, CompositionVariables<Type, ValueType> const& variables) {
+ std::set<storm::expressions::Variable> missingIdentities;
+ std::set_difference(variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), edge.writtenGlobalVariables.begin(), edge.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
+ storm::dd::Add<Type, ValueType> identityEncoding = variables.manager->template getAddOne<ValueType>();
+ for (auto const& variable : missingIdentities) {
+ identityEncoding *= variables.variableToIdentityMap.at(variable);
+ }
+ return identityEncoding;
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ storm::dd::Add<Type, ValueType> encodeIndex(uint64_t index, std::vector<storm::expressions::Variable> const& nondeterminismVariables, CompositionVariables<Type, ValueType> const& variables) {
+ storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
+
+ STORM_LOG_TRACE("Encoding " << index << " with " << nondeterminismVariables.size() << " binary variable(s).");
+
+ std::map<storm::expressions::Variable, int_fast64_t> metaVariableNameToValueMap;
+ for (uint_fast64_t i = 0; i < nondeterminismVariables.size(); ++i) {
+ if (index & (1ull << (nondeterminismVariables.size() - i - 1))) {
+ metaVariableNameToValueMap.emplace(nondeterminismVariables[i], 1);
+ } else {
+ metaVariableNameToValueMap.emplace(nondeterminismVariables[i], 0);
+ }
+ }
+
+ result.setValue(metaVariableNameToValueMap, 1);
+ return result;
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ storm::dd::Add<Type, ValueType> createGlobalTransitionRelation(storm::jani::Model const& model, AutomatonDd<Type, ValueType> const& automatonDd, CompositionVariables<Type, ValueType> const& variables) {
+ // If the model is an MDP, we need to encode the nondeterminism using additional variables.
+ if (model.getModelType() == storm::jani::ModelType::MDP) {
+ // Determine how many nondeterminism variables we need.
+ std::vector<storm::expressions::Variable> actionVariables;
+ std::map<uint64_t, uint64_t> actionIndexToVariableIndex;
+ uint64_t maximalNumberOfEdgesPerAction = 0;
+ for (auto const& action : automatonDd.actionIndexToEdges) {
+ actionVariables.push_back(variables.actionVariablesMap.at(action.first));
+ actionIndexToVariableIndex[action.first] = actionVariables.size() - 1;
+ maximalNumberOfEdgesPerAction = std::max(maximalNumberOfEdgesPerAction, static_cast<uint64_t>(action.second.size()));
+ }
+ uint64_t numberOfNondeterminismVariables = static_cast<uint64_t>(std::ceil(std::log2(maximalNumberOfEdgesPerAction)));
+ std::vector<storm::expressions::Variable> nondeterminismVariables(numberOfNondeterminismVariables);
+ std::copy(variables.nondeterminismVariables.begin(), variables.nondeterminismVariables.begin() + numberOfNondeterminismVariables, nondeterminismVariables.begin());
+
+ // Prepare result.
+ storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
+
+ // Add edges to the result.
+ for (auto const& action : automatonDd.actionIndexToEdges) {
+ storm::dd::Add<Type, ValueType> edgesForAction = variables.manager->template getAddZero<ValueType>();
+
+ uint64_t edgeIndex = 0;
+ for (auto const& edge : action.second) {
+ edgesForAction += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables) * encodeIndex(edgeIndex, nondeterminismVariables, variables);
+ ++edgeIndex;
+ }
+
+ result += edgesForAction * encodeAction<Type, ValueType>(actionIndexToVariableIndex.at(action.first), actionVariables, variables);
+ }
+ } else if (model.getModelType() == storm::jani::ModelType::DTMC || model.getModelType() == storm::jani::ModelType::CTMC) {
+ // Simply add all actions, but make sure to include the missing global variable identities.
+ storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
+ for (auto const& action : automatonDd.actionIndexToEdges) {
+ uint64_t edgeIndex = 0;
+ for (auto const& edge : action.second) {
+ result += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables);
+ edge.transitionsDd.exportToDot("edge_" + std::to_string(edgeIndex) + ".dot");
+ ++edgeIndex;
+ }
+ }
+ result.exportToDot("result.dot");
+ std::cout << "nnz: " << result.getNonZeroCount() << std::endl;
+ std::cout << "nodecnt: " << result.getNodeCount() << std::endl;
+ std::cout << "meta var: " << std::endl;
+ for (auto const& var : result.getContainedMetaVariables()) {
+ std::cout << var.getName() << std::endl;
+ }
+ std::cout << std::endl;
+ return result;
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
+ }
+ return storm::dd::Add<Type, ValueType>();
+ }
+
template <storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::translate() {
CompositionVariableCreator<Type, ValueType> variableCreator(*this->model);
@@ -646,6 +759,9 @@ namespace storm {
AutomatonComposer<Type, ValueType> composer(*this->model, variables);
AutomatonDd<Type, ValueType> system = composer.compose();
+ storm::dd::Add<Type, ValueType> transitions = createGlobalTransitionRelation(*this->model, system, variables);
+ transitions.exportToDot("trans.dot");
+
// FIXME
return nullptr;
}
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 39a425380..5561d7fb1 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -1067,10 +1067,30 @@ namespace storm {
return result;
} else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
- // Simply add all actions.
- storm::dd::Add<Type, ValueType> result = module.independentAction.transitionsDd;
+ // Simply add all actions, but make sure to include the missing global variable identities.
+
+ // Compute missing global variable identities in independent action.
+ std::set<storm::expressions::Variable> missingIdentities;
+ std::set_difference(generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), module.independentAction.assignedGlobalVariables.begin(), module.independentAction.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
+ storm::dd::Add<Type, ValueType> identityEncoding = generationInfo.manager->template getAddOne<ValueType>();
+ for (auto const& variable : missingIdentities) {
+ STORM_LOG_TRACE("Multiplying identity of global variable " << variable.getName() << " to independent action.");
+ identityEncoding *= generationInfo.variableToIdentityMap.at(variable);
+ }
+
+ storm::dd::Add<Type, ValueType> result = identityEncoding * module.independentAction.transitionsDd;
+
for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
- result += synchronizingAction.second.transitionsDd;
+ // Compute missing global variable identities in synchronizing actions.
+ missingIdentities = std::set<storm::expressions::Variable>();
+ std::set_difference(generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), synchronizingAction.second.assignedGlobalVariables.begin(), synchronizingAction.second.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
+ identityEncoding = generationInfo.manager->template getAddOne<ValueType>();
+ for (auto const& variable : missingIdentities) {
+ STORM_LOG_TRACE("Multiplying identity of global variable " << variable.getName() << " to synchronizing action '" << synchronizingAction.first << "'.");
+ identityEncoding *= generationInfo.variableToIdentityMap.at(variable);
+ }
+
+ result += identityEncoding * synchronizingAction.second.transitionsDd;
}
return result;
} else {
@@ -1084,6 +1104,14 @@ namespace storm {
ModuleDecisionDiagram system = composer.compose(generationInfo.program.specifiesSystemComposition() ? generationInfo.program.getSystemCompositionConstruct().getSystemComposition() : *generationInfo.program.getDefaultSystemComposition());
storm::dd::Add<Type, ValueType> result = createSystemFromModule(generationInfo, system);
+ result.exportToDot("result_prism.dot");
+ std::cout << "nnz: " << result.getNonZeroCount() << std::endl;
+ std::cout << "nodecnt: " << result.getNodeCount() << std::endl;
+ std::cout << "meta var: " << std::endl;
+ for (auto const& var : result.getContainedMetaVariables()) {
+ std::cout << var.getName() << std::endl;
+ }
+ std::cout << std::endl;
// Create an auxiliary DD that is used later during the construction of reward models.
storm::dd::Add<Type, ValueType> stateActionDd = result.sumAbstract(generationInfo.columnMetaVariables);
diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp
index 17e237986..f28a8b8be 100644
--- a/src/storage/dd/DdManager.cpp
+++ b/src/storage/dd/DdManager.cpp
@@ -103,10 +103,15 @@ namespace storm {
STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
// Check that the range is legal.
- STORM_LOG_THROW(high != low, storm::exceptions::InvalidArgumentException, "Range of meta variable must be at least 2 elements.");
+ STORM_LOG_THROW(high >= low, storm::exceptions::InvalidArgumentException, "Illegal empty range for meta variable.");
std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
+ // For the case where low and high coincide, we need to have a single bit.
+ if (numberOfBits == 0) {
+ ++numberOfBits;
+ }
+
storm::expressions::Variable unprimed = manager->declareBitVectorVariable(name, numberOfBits);
storm::expressions::Variable primed = manager->declareBitVectorVariable(name + "'", numberOfBits);
diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp
index ccdec51aa..7b336b1c5 100644
--- a/src/storage/jani/Automaton.cpp
+++ b/src/storage/jani/Automaton.cpp
@@ -164,6 +164,14 @@ namespace storm {
return edges;
}
+ std::set<uint64_t> Automaton::getActionIndices() const {
+ std::set<uint64_t> result;
+ for (auto const& edge : edges) {
+ result.insert(edge.getActionId());
+ }
+ return result;
+ }
+
uint64_t Automaton::getNumberOfLocations() const {
return locations.size();
}
diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h
index 08b803248..09caef1b3 100644
--- a/src/storage/jani/Automaton.h
+++ b/src/storage/jani/Automaton.h
@@ -195,6 +195,11 @@ namespace storm {
*/
std::vector<Edge> const& getEdges() const;
+ /*!
+ * Retrieves the set of action indices that are labels of edges of this automaton.
+ */
+ std::set<uint64_t> getActionIndices() const;
+
/*!
* Retrieves the number of locations.
*/
diff --git a/src/storage/jani/BooleanVariable.cpp b/src/storage/jani/BooleanVariable.cpp
index d3d37f64e..cdc5ff062 100644
--- a/src/storage/jani/BooleanVariable.cpp
+++ b/src/storage/jani/BooleanVariable.cpp
@@ -7,5 +7,9 @@ namespace storm {
// Intentionally left empty.
}
+ bool BooleanVariable::isBooleanVariable() const {
+ return true;
+ }
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/BooleanVariable.h b/src/storage/jani/BooleanVariable.h
index 844fe55d1..fd94c447c 100644
--- a/src/storage/jani/BooleanVariable.h
+++ b/src/storage/jani/BooleanVariable.h
@@ -11,6 +11,8 @@ namespace storm {
* Creates a boolean variable.
*/
BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue = storm::expressions::Expression());
+
+ virtual bool isBooleanVariable() const;
};
}
diff --git a/src/storage/jani/BoundedIntegerVariable.cpp b/src/storage/jani/BoundedIntegerVariable.cpp
index 4ab7e5717..dbe3f3855 100644
--- a/src/storage/jani/BoundedIntegerVariable.cpp
+++ b/src/storage/jani/BoundedIntegerVariable.cpp
@@ -23,5 +23,9 @@ namespace storm {
this->upperBound = expression;
}
+ bool BoundedIntegerVariable::isBoundedIntegerVariable() const {
+ return true;
+ }
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h
index 5e62c855a..b6e7ca6f4 100644
--- a/src/storage/jani/BoundedIntegerVariable.h
+++ b/src/storage/jani/BoundedIntegerVariable.h
@@ -33,6 +33,8 @@ namespace storm {
*/
void setUpperBound(storm::expressions::Expression const& expression);
+ virtual bool isBoundedIntegerVariable() const;
+
private:
// The expression defining the lower bound of the variable.
storm::expressions::Expression lowerBound;
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index dc5c4f352..182355681 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -156,12 +156,33 @@ namespace storm {
}
std::shared_ptr<Composition> Model::getStandardSystemComposition() const {
- std::set<std::string> fullSynchronizationAlphabet = getActionNames(false);
-
std::shared_ptr<Composition> current;
current = std::make_shared<AutomatonComposition>(this->automata.front().getName());
+ std::set<uint64_t> leftHandActionIndices = this->automata.front().getActionIndices();
+
for (uint64_t index = 1; index < automata.size(); ++index) {
- current = std::make_shared<ParallelComposition>(current, std::make_shared<AutomatonComposition>(automata[index].getName()), fullSynchronizationAlphabet);
+ std::set<uint64_t> newActionIndices = automata[index].getActionIndices();
+
+ // Compute the intersection of actions of the left- and right-hand side.
+ std::set<uint64_t> intersectionActions;
+ std::set_intersection(leftHandActionIndices.begin(), leftHandActionIndices.end(), newActionIndices.begin(), newActionIndices.end(), std::inserter(intersectionActions, intersectionActions.begin()));
+
+ // If the silent action is in the intersection, we remove it since we cannot synchronize over it.
+ auto it = intersectionActions.find(this->getSilentActionIndex());
+ if (it != intersectionActions.end()) {
+ intersectionActions.erase(it);
+ }
+
+ // Then join the actions to reflect the actions of the new left-hand side.
+ leftHandActionIndices.insert(newActionIndices.begin(), newActionIndices.end());
+
+ // Create the set of strings that represents the actions over which to synchronize.
+ std::set<std::string> intersectionActionNames;
+ for (auto const& actionIndex : intersectionActions) {
+ intersectionActionNames.insert(this->getAction(actionIndex).getName());
+ }
+
+ current = std::make_shared<ParallelComposition>(current, std::make_shared<AutomatonComposition>(automata[index].getName()), intersectionActionNames);
}
return current;
}
diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp
index 76a17185c..f767e32cc 100644
--- a/src/storage/jani/ParallelComposition.cpp
+++ b/src/storage/jani/ParallelComposition.cpp
@@ -5,7 +5,7 @@
namespace storm {
namespace jani {
- ParallelComposition::ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& alphabet) : leftSubcomposition(leftSubcomposition), rightSubcomposition(rightSubcomposition) {
+ ParallelComposition::ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& alphabet) : leftSubcomposition(leftSubcomposition), rightSubcomposition(rightSubcomposition), alphabet(alphabet) {
// Intentionally left empty.
}
diff --git a/src/storage/jani/UnboundedIntegerVariable.cpp b/src/storage/jani/UnboundedIntegerVariable.cpp
index 9a2497a1b..2dd297d96 100644
--- a/src/storage/jani/UnboundedIntegerVariable.cpp
+++ b/src/storage/jani/UnboundedIntegerVariable.cpp
@@ -7,5 +7,9 @@ namespace storm {
// Intentionally left empty.
}
+ bool UnboundedIntegerVariable::isUnboundedIntegerVariable() const {
+ return true;
+ }
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/UnboundedIntegerVariable.h b/src/storage/jani/UnboundedIntegerVariable.h
index 94bb52836..bb6a79e4e 100644
--- a/src/storage/jani/UnboundedIntegerVariable.h
+++ b/src/storage/jani/UnboundedIntegerVariable.h
@@ -11,6 +11,8 @@ namespace storm {
* Creates an unbounded integer variable.
*/
UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue = storm::expressions::Expression());
+
+ virtual bool isUnboundedIntegerVariable() const override;
};
}
diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp
index 84f927802..5988cf45b 100644
--- a/src/storage/jani/Variable.cpp
+++ b/src/storage/jani/Variable.cpp
@@ -1,6 +1,8 @@
#include "src/storage/jani/Variable.h"
-#include <iostream>
+#include "src/storage/jani/BooleanVariable.h"
+#include "src/storage/jani/BoundedIntegerVariable.h"
+#include "src/storage/jani/UnboundedIntegerVariable.h"
namespace storm {
namespace jani {
@@ -29,5 +31,41 @@ namespace storm {
this->initialValue = initialValue;
}
+ bool Variable::isBooleanVariable() const {
+ return false;
+ }
+
+ bool Variable::isBoundedIntegerVariable() const {
+ return false;
+ }
+
+ bool Variable::isUnboundedIntegerVariable() const {
+ return false;
+ }
+
+ BooleanVariable& Variable::asBooleanVariable() {
+ return dynamic_cast<BooleanVariable&>(*this);
+ }
+
+ BooleanVariable const& Variable::asBooleanVariable() const {
+ return dynamic_cast<BooleanVariable const&>(*this);
+ }
+
+ BoundedIntegerVariable& Variable::asBoundedIntegerVariable() {
+ return dynamic_cast<BoundedIntegerVariable&>(*this);
+ }
+
+ BoundedIntegerVariable const& Variable::asBoundedIntegerVariable() const {
+ return dynamic_cast<BoundedIntegerVariable const&>(*this);
+ }
+
+ UnboundedIntegerVariable& Variable::asUnboundedIntegerVariable() {
+ return dynamic_cast<UnboundedIntegerVariable&>(*this);
+ }
+
+ UnboundedIntegerVariable const& Variable::asUnboundedIntegerVariable() const {
+ return dynamic_cast<UnboundedIntegerVariable const&>(*this);
+ }
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h
index c77e21e93..f113de4a6 100644
--- a/src/storage/jani/Variable.h
+++ b/src/storage/jani/Variable.h
@@ -9,6 +9,10 @@
namespace storm {
namespace jani {
+ class BooleanVariable;
+ class BoundedIntegerVariable;
+ class UnboundedIntegerVariable;
+
class Variable {
public:
/*!
@@ -41,6 +45,19 @@ namespace storm {
*/
bool hasInitialValue() const;
+ // Methods to determine the type of the variable.
+ virtual bool isBooleanVariable() const;
+ virtual bool isBoundedIntegerVariable() const;
+ virtual bool isUnboundedIntegerVariable() const;
+
+ // Methods to get the variable as a different type.
+ BooleanVariable& asBooleanVariable();
+ BooleanVariable const& asBooleanVariable() const;
+ BoundedIntegerVariable& asBoundedIntegerVariable();
+ BoundedIntegerVariable const& asBoundedIntegerVariable() const;
+ UnboundedIntegerVariable& asUnboundedIntegerVariable();
+ UnboundedIntegerVariable const& asUnboundedIntegerVariable() const;
+
private:
// The name of the variable.
std::string name;
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 711f68ad8..57d870b07 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -1518,31 +1518,24 @@ namespace storm {
// Because of the rules of JANI, we have to make all variables of modules global that are read by other modules.
- // Create a mapping from variables to the indices of module indices that read the variable.
- std::map<storm::expressions::Variable, std::set<uint_fast64_t>> variablesToReadingModuleIndices;
- for (auto const& module : modules) {
- for (auto const& variable : module.getBooleanVariables()) {
- variablesToReadingModuleIndices.emplace(variable.getExpressionVariable(), std::set<uint_fast64_t>());
- }
- for (auto const& variable : module.getIntegerVariables()) {
- variablesToReadingModuleIndices.emplace(variable.getExpressionVariable(), std::set<uint_fast64_t>());
- }
- }
+ // Create a mapping from variables to the indices of module indices that write/read the variable.
+ std::map<storm::expressions::Variable, std::set<uint_fast64_t>> variablesToAccessingModuleIndices;
for (uint_fast64_t index = 0; index < modules.size(); ++index) {
storm::prism::Module const& module = modules[index];
for (auto const& command : module.getCommands()) {
std::set<storm::expressions::Variable> variables = command.getGuardExpression().getVariables();
for (auto const& variable : variables) {
- variablesToReadingModuleIndices[variable].insert(index);
+ variablesToAccessingModuleIndices[variable].insert(index);
}
for (auto const& update : command.getUpdates()) {
for (auto const& assignment : update.getAssignments()) {
variables = assignment.getExpression().getVariables();
for (auto const& variable : variables) {
- variablesToReadingModuleIndices[variable].insert(index);
+ variablesToAccessingModuleIndices[variable].insert(index);
}
+ variablesToAccessingModuleIndices[assignment.getVariable()].insert(index);
}
}
}
@@ -1554,23 +1547,23 @@ namespace storm {
storm::jani::Automaton automaton(module.getName());
for (auto const& variable : module.getBooleanVariables()) {
storm::jani::BooleanVariable newBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression());
- std::set<uint_fast64_t> const& readingModuleIndices = variablesToReadingModuleIndices[variable.getExpressionVariable()];
- if (readingModuleIndices.size() == 1) {
- // In this case, we can move the variable to the automaton.
+ std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
+ // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
+ if (accessingModuleIndices.size() == 1) {
automaton.addBooleanVariable(newBooleanVariable);
- } else {
- // In this case, we need to make the variable global.
+ } else { // if (accessingModuleIndices.size() > 1) {
+ // Otherwise, we need to make it global.
janiModel.addBooleanVariable(newBooleanVariable);
}
}
for (auto const& variable : module.getIntegerVariables()) {
storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression(), variable.getInitialValueExpression());
- std::set<uint_fast64_t> const& readingModuleIndices = variablesToReadingModuleIndices[variable.getExpressionVariable()];
- if (readingModuleIndices.size() == 1) {
- // In this case, we can move the variable to the automaton.
+ std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
+ // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
+ if (accessingModuleIndices.size() == 1) {
automaton.addBoundedIntegerVariable(newIntegerVariable);
- } else {
- // In this case, we need to make the variable global.
+ } else { //if (accessingModuleIndices.size() > 1) {
+ // Otherwise, we need to make it global.
janiModel.addBoundedIntegerVariable(newIntegerVariable);
}
}
diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp
index 486a1b26e..ac138d842 100644
--- a/test/functional/builder/DdJaniModelBuilderTest.cpp
+++ b/test/functional/builder/DdJaniModelBuilderTest.cpp
@@ -78,6 +78,15 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
// EXPECT_EQ(13ul, model->getNumberOfStates());
// EXPECT_EQ(20ul, model->getNumberOfTransitions());
+
+// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-2-2.pm");
+// janiModel = program.toJani();
+//
+// builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
+// t1 = std::chrono::high_resolution_clock::now();
+// builder.translate();
+// t2 = std::chrono::high_resolution_clock::now();
+// std::cout << "brp2: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
janiModel = program.toJani();
@@ -86,38 +95,38 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
model = builder.translate();
t2 = std::chrono::high_resolution_clock::now();
std::cout << "brp: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
- // EXPECT_EQ(677ul, model->getNumberOfStates());
- // EXPECT_EQ(867ul, model->getNumberOfTransitions());
-
- program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
- janiModel = program.toJani();
- builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
- t1 = std::chrono::high_resolution_clock::now();
- model = builder.translate();
- t2 = std::chrono::high_resolution_clock::now();
- std::cout << "crowds: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
- // EXPECT_EQ(8607ul, model->getNumberOfStates());
- // EXPECT_EQ(15113ul, model->getNumberOfTransitions());
-
- program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
- janiModel = program.toJani();
- builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
- t1 = std::chrono::high_resolution_clock::now();
- model = builder.translate();
- t2 = std::chrono::high_resolution_clock::now();
- std::cout << "lead: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
- // EXPECT_EQ(273ul, model->getNumberOfStates());
- // EXPECT_EQ(397ul, model->getNumberOfTransitions());
-
- program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
- janiModel = program.toJani();
- builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
- t1 = std::chrono::high_resolution_clock::now();
- model = builder.translate();
- t2 = std::chrono::high_resolution_clock::now();
- std::cout << "nand: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
- // EXPECT_EQ(1728ul, model->getNumberOfStates());
- // EXPECT_EQ(2505ul, model->getNumberOfTransitions());
+// // EXPECT_EQ(677ul, model->getNumberOfStates());
+// // EXPECT_EQ(867ul, model->getNumberOfTransitions());
+//
+// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+// janiModel = program.toJani();
+// builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
+// t1 = std::chrono::high_resolution_clock::now();
+// model = builder.translate();
+// t2 = std::chrono::high_resolution_clock::now();
+// std::cout << "crowds: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
+// // EXPECT_EQ(8607ul, model->getNumberOfStates());
+// // EXPECT_EQ(15113ul, model->getNumberOfTransitions());
+//
+// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+// janiModel = program.toJani();
+// builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
+// t1 = std::chrono::high_resolution_clock::now();
+// model = builder.translate();
+// t2 = std::chrono::high_resolution_clock::now();
+// std::cout << "lead: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
+// // EXPECT_EQ(273ul, model->getNumberOfStates());
+// // EXPECT_EQ(397ul, model->getNumberOfTransitions());
+//
+// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
+// janiModel = program.toJani();
+// builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
+// t1 = std::chrono::high_resolution_clock::now();
+// model = builder.translate();
+// t2 = std::chrono::high_resolution_clock::now();
+// std::cout << "nand: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
+// // EXPECT_EQ(1728ul, model->getNumberOfStates());
+// // EXPECT_EQ(2505ul, model->getNumberOfTransitions());
}
//TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {
diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp
index f89bb19ab..c6e729743 100644
--- a/test/functional/builder/DdPrismModelBuilderTest.cpp
+++ b/test/functional/builder/DdPrismModelBuilderTest.cpp
@@ -59,6 +59,11 @@ TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
+
+// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-2-2.pm");
+// model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
+//
+// exit(-1);
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);