diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp
index 84e48e8a6..e50620db8 100644
--- a/src/adapters/AddExpressionAdapter.cpp
+++ b/src/adapters/AddExpressionAdapter.cpp
@@ -12,7 +12,7 @@ namespace storm {
namespace adapters {
template<storm::dd::DdType Type, typename ValueType>
- AddExpressionAdapter<Type, ValueType>::AddExpressionAdapter(std::shared_ptr<storm::dd::DdManager<Type>> ddManager, std::map<storm::expressions::Variable, storm::expressions::Variable> const& variableMapping) : ddManager(ddManager), variableMapping(variableMapping) {
+ AddExpressionAdapter<Type, ValueType>::AddExpressionAdapter(std::shared_ptr<storm::dd::DdManager<Type>> ddManager, std::shared_ptr<std::map<storm::expressions::Variable, storm::expressions::Variable>> const& variableMapping) : ddManager(ddManager), variableMapping(variableMapping) {
// Intentionally left empty.
}
@@ -140,8 +140,8 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::VariableExpression const& expression) {
- auto const& variablePair = variableMapping.find(expression.getVariable());
- STORM_LOG_THROW(variablePair != variableMapping.end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains the variable '" << expression.getVariableName() << "' for which no DD counterpart is known.");
+ auto const& variablePair = variableMapping->find(expression.getVariable());
+ STORM_LOG_THROW(variablePair != variableMapping->end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains the variable '" << expression.getVariableName() << "' for which no DD counterpart is known.");
if (expression.hasBooleanType()) {
return ddManager->template getIdentity<ValueType>(variablePair->second).toBdd();
} else {
diff --git a/src/adapters/AddExpressionAdapter.h b/src/adapters/AddExpressionAdapter.h
index ad82146f3..89d825d96 100644
--- a/src/adapters/AddExpressionAdapter.h
+++ b/src/adapters/AddExpressionAdapter.h
@@ -1,6 +1,8 @@
#ifndef STORM_ADAPTERS_DDEXPRESSIONADAPTER_H_
#define STORM_ADAPTERS_DDEXPRESSIONADAPTER_H_
+#include <memory>
+
#include "src/storage/expressions/Variable.h"
#include "src/storage/expressions/Expressions.h"
#include "src/storage/expressions/ExpressionVisitor.h"
@@ -15,7 +17,7 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType = double>
class AddExpressionAdapter : public storm::expressions::ExpressionVisitor {
public:
- AddExpressionAdapter(std::shared_ptr<storm::dd::DdManager<Type>> ddManager, std::map<storm::expressions::Variable, storm::expressions::Variable> const& variableMapping);
+ AddExpressionAdapter(std::shared_ptr<storm::dd::DdManager<Type>> ddManager, std::shared_ptr<std::map<storm::expressions::Variable, storm::expressions::Variable>> const& variableMapping);
storm::dd::Add<Type, ValueType> translateExpression(storm::expressions::Expression const& expression);
storm::dd::Bdd<Type> translateBooleanExpression(storm::expressions::Expression const& expression);
@@ -36,7 +38,7 @@ namespace storm {
std::shared_ptr<storm::dd::DdManager<Type>> ddManager;
// This member maps the variables used in the expressions to the variables used by the DD manager.
- std::map<storm::expressions::Variable, storm::expressions::Variable> variableMapping;
+ std::shared_ptr<std::map<storm::expressions::Variable, storm::expressions::Variable>> variableMapping;
};
} // namespace adapters
diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index 3a46a36c5..a2b29f34b 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -130,7 +130,11 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
struct CompositionVariables {
- CompositionVariables() : manager(std::make_shared<storm::dd::DdManager<Type>>()) {
+ CompositionVariables() : manager(std::make_shared<storm::dd::DdManager<Type>>()),
+ variableToRowMetaVariableMap(std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>()),
+ rowExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type>>(manager, variableToRowMetaVariableMap)),
+ variableToColumnMetaVariableMap(std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>()),
+ columnExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type>>(manager, variableToColumnMetaVariableMap)) {
// Intentionally left empty.
}
@@ -138,12 +142,12 @@ namespace storm {
// The meta variables for the row encoding.
std::set<storm::expressions::Variable> rowMetaVariables;
- std::map<storm::expressions::Variable, storm::expressions::Variable> variableToRowMetaVariableMap;
+ std::shared_ptr<std::map<storm::expressions::Variable, storm::expressions::Variable>> variableToRowMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter;
// The meta variables for the column encoding.
std::set<storm::expressions::Variable> columnMetaVariables;
- std::map<storm::expressions::Variable, storm::expressions::Variable> variableToColumnMetaVariableMap;
+ std::shared_ptr<std::map<storm::expressions::Variable, storm::expressions::Variable>> variableToColumnMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter;
// All pairs of row/column meta variables.
@@ -197,7 +201,7 @@ namespace storm {
boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
auto it = automata.find(composition.getAutomatonName());
- STORM_LOG_THROW(it != automata.end(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition that refers to the same automaton multiple times.");
+ STORM_LOG_THROW(it == automata.end(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition that refers to the automaton '" << composition.getAutomatonName() << "' multiple times.");
automata.insert(it, composition.getAutomatonName());
return boost::none;
}
@@ -218,14 +222,16 @@ namespace storm {
CompositionVariables<Type, ValueType> result;
for (auto const& action : this->model.getActions()) {
- std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(action.getName());
- result.actionVariables.push_back(variablePair.first);
+ 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);
+ }
}
// FIXME: check how many nondeterminism variables we should actually allocate.
uint64_t numberOfNondeterminismVariables = this->model.getNumberOfAutomata();
for (auto const& automaton : this->model.getAutomata()) {
- numberOfNondeterminismVariables *= automaton.getNumberOfEdges();
+ numberOfNondeterminismVariables += automaton.getNumberOfEdges();
}
for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("nondet" + std::to_string(i));
@@ -256,12 +262,12 @@ namespace storm {
for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) {
createVariable(variable, result);
identity &= result.variableToIdentityMap.at(variable.getExpressionVariable()).toBdd();
- range &= result.manager->getRange(result.variableToRowMetaVariableMap.at(variable.getExpressionVariable()));
+ range &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable()));
}
for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
createVariable(variable, result);
identity &= result.variableToIdentityMap.at(variable.getExpressionVariable()).toBdd();
- range &= result.manager->getRange(result.variableToRowMetaVariableMap.at(variable.getExpressionVariable()));
+ range &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable()));
}
result.automatonToIdentityMap[automaton.getName()] = identity.template toAdd<ValueType>();
@@ -279,10 +285,10 @@ namespace storm {
STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << "] and " << variablePair.second.getName() << ".");
result.rowMetaVariables.insert(variablePair.first);
- result.variableToRowMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.first);
+ result.variableToRowMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.first);
result.columnMetaVariables.insert(variablePair.second);
- result.variableToColumnMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.second);
+ result.variableToColumnMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.second);
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>();
result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity);
@@ -297,10 +303,10 @@ namespace storm {
STORM_LOG_TRACE("Created meta variables for global boolean variable: " << variablePair.first.getName() << " and " << variablePair.second.getName() << ".");
result.rowMetaVariables.insert(variablePair.first);
- result.variableToRowMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.first);
+ result.variableToRowMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.first);
result.columnMetaVariables.insert(variablePair.second);
- result.variableToColumnMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.second);
+ result.variableToColumnMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.second);
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.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity);
@@ -326,11 +332,11 @@ namespace storm {
// This structure represents an edge.
template<storm::dd::DdType Type, typename ValueType>
struct EdgeDd {
- EdgeDd(storm::dd::Add<Type> const& guardDd = storm::dd::Add<Type>(), storm::dd::Add<Type, ValueType> const& transitionsDd = storm::dd::Add<Type, ValueType>(), std::set<storm::expressions::Variable> const& writtenGlobalVariables = {}, std::set<storm::expressions::Variable> const& globalVariablesWrittenMultipleTimes = {}) {
+ EdgeDd(storm::dd::Add<Type> const& guardDd = storm::dd::Add<Type>(), storm::dd::Add<Type, ValueType> const& transitionsDd = storm::dd::Add<Type, ValueType>(), std::set<storm::expressions::Variable> const& writtenGlobalVariables = {}, std::set<storm::expressions::Variable> const& globalVariablesWrittenMultipleTimes = {}) : guardDd(guardDd), transitionsDd(transitionsDd), writtenGlobalVariables(writtenGlobalVariables), globalVariablesWrittenMultipleTimes(globalVariablesWrittenMultipleTimes) {
// Intentionally left empty.
}
- EdgeDd(EdgeDd const& other) : globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes), writtenGlobalVariables(other.writtenGlobalVariables), guardDd(other.guardDd), transitionsDd(other.transitionsDd) {
+ EdgeDd(EdgeDd const& other) : guardDd(other.guardDd), transitionsDd(other.transitionsDd), writtenGlobalVariables(other.writtenGlobalVariables), globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes) {
// Intentionally left empty.
}
@@ -344,10 +350,10 @@ namespace storm {
return *this;
}
- std::set<storm::expressions::Variable> globalVariablesWrittenMultipleTimes;
- std::set<storm::expressions::Variable> writtenGlobalVariables;
storm::dd::Add<Type, ValueType> guardDd;
storm::dd::Add<Type, ValueType> transitionsDd;
+ std::set<storm::expressions::Variable> writtenGlobalVariables;
+ std::set<storm::expressions::Variable> globalVariablesWrittenMultipleTimes;
};
// This structure represents a subcomponent of a composition.
@@ -509,11 +515,11 @@ namespace storm {
std::set<storm::expressions::Variable> assignedVariables;
for (auto const& assignment : destination.getAssignments()) {
// Record the variable as being written.
- STORM_LOG_TRACE("Assigning to variable " << variables.variableToRowMetaVariableMap.at(assignment.getExpressionVariable()).getName());
+ STORM_LOG_TRACE("Assigning to variable " << variables.variableToRowMetaVariableMap->at(assignment.getExpressionVariable()).getName());
assignedVariables.insert(assignment.getExpressionVariable());
// Translate the written variable.
- auto const& primedMetaVariable = variables.variableToColumnMetaVariableMap.at(assignment.getExpressionVariable());
+ auto const& primedMetaVariable = variables.variableToColumnMetaVariableMap->at(assignment.getExpressionVariable());
storm::dd::Add<Type, ValueType> writtenVariable = variables.manager->template getIdentity<ValueType>(primedMetaVariable);
// Translate the expression that is being assigned.
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index b013735d9..39a425380 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -31,7 +31,7 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
class DdPrismModelBuilder<Type, ValueType>::GenerationInformation {
public:
- GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared<storm::dd::DdManager<Type>>()), rowMetaVariables(), variableToRowMetaVariableMap(), rowExpressionAdapter(nullptr), columnMetaVariables(), variableToColumnMetaVariableMap(), columnExpressionAdapter(nullptr), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() {
+ GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared<storm::dd::DdManager<Type>>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>()), rowExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type>>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>())), columnExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type>>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() {
// Initializes variables and identity DDs.
createMetaVariablesAndIdentities();
@@ -47,12 +47,12 @@ namespace storm {
// The meta variables for the row encoding.
std::set<storm::expressions::Variable> rowMetaVariables;
- std::map<storm::expressions::Variable, storm::expressions::Variable> variableToRowMetaVariableMap;
+ std::shared_ptr<std::map<storm::expressions::Variable, storm::expressions::Variable>> variableToRowMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter;
// The meta variables for the column encoding.
std::set<storm::expressions::Variable> columnMetaVariables;
- std::map<storm::expressions::Variable, storm::expressions::Variable> variableToColumnMetaVariableMap;
+ std::shared_ptr<std::map<storm::expressions::Variable, storm::expressions::Variable>> variableToColumnMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter;
// All pairs of row/column meta variables.
@@ -116,10 +116,10 @@ namespace storm {
STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]");
rowMetaVariables.insert(variablePair.first);
- variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first);
+ variableToRowMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.first);
columnMetaVariables.insert(variablePair.second);
- variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second);
+ variableToColumnMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.second);
storm::dd::Add<Type, ValueType> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * manager->getRange(variablePair.first).template toAdd<ValueType>() * manager->getRange(variablePair.second).template toAdd<ValueType>();
variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
@@ -133,10 +133,10 @@ namespace storm {
STORM_LOG_TRACE("Created meta variables for global boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]");
rowMetaVariables.insert(variablePair.first);
- variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first);
+ variableToRowMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.first);
columnMetaVariables.insert(variablePair.second);
- variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second);
+ variableToColumnMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.second);
storm::dd::Add<Type, ValueType> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>();
variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity);
@@ -157,10 +157,10 @@ namespace storm {
STORM_LOG_TRACE("Created meta variables for integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]");
rowMetaVariables.insert(variablePair.first);
- variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first);
+ variableToRowMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.first);
columnMetaVariables.insert(variablePair.second);
- variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second);
+ variableToColumnMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.second);
storm::dd::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
@@ -174,10 +174,10 @@ namespace storm {
STORM_LOG_TRACE("Created meta variables for boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]");
rowMetaVariables.insert(variablePair.first);
- variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first);
+ variableToRowMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.first);
columnMetaVariables.insert(variablePair.second);
- variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second);
+ variableToColumnMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.second);
storm::dd::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
@@ -591,11 +591,11 @@ namespace storm {
std::set<storm::expressions::Variable> assignedVariables;
for (auto const& assignment : assignments) {
// Record the variable as being written.
- STORM_LOG_TRACE("Assigning to variable " << generationInfo.variableToRowMetaVariableMap.at(assignment.getVariable()).getName());
+ STORM_LOG_TRACE("Assigning to variable " << generationInfo.variableToRowMetaVariableMap->at(assignment.getVariable()).getName());
assignedVariables.insert(assignment.getVariable());
// Translate the written variable.
- auto const& primedMetaVariable = generationInfo.variableToColumnMetaVariableMap.at(assignment.getVariable());
+ auto const& primedMetaVariable = generationInfo.variableToColumnMetaVariableMap->at(assignment.getVariable());
storm::dd::Add<Type, ValueType> writtenVariable = generationInfo.manager->template getIdentity<ValueType>(primedMetaVariable);
// Translate the expression that is being assigned.
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index 1d976d084..dc5c4f352 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -170,6 +170,10 @@ namespace storm {
return *composition;
}
+ void Model::setSystemComposition(std::shared_ptr<Composition> const& composition) {
+ this->composition = composition;
+ }
+
std::set<std::string> Model::getActionNames(bool includeSilent) const {
std::set<std::string> result;
for (auto const& entry : actionToIndex) {
@@ -257,7 +261,6 @@ namespace storm {
// Substitute constants in all global variables.
for (auto& variable : result.getGlobalVariables()) {
- std::cout << "init: " << variable.getInitialValue() << std::endl;
variable.setInitialValue(variable.getInitialValue().substitute(constantSubstitution));
}
for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) {
diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp
index e3e183558..e7f2b42b7 100644
--- a/src/storage/jani/VariableSet.cpp
+++ b/src/storage/jani/VariableSet.cpp
@@ -36,12 +36,12 @@ namespace storm {
template<typename VariableType>
typename ConstVariables<VariableType>::const_iterator ConstVariables<VariableType>::begin() {
- return boost::make_transform_iterator(it, Dereferencer<VariableType>());
+ return boost::make_transform_iterator(it, Dereferencer<VariableType const>());
}
template<typename VariableType>
typename ConstVariables<VariableType>::const_iterator ConstVariables<VariableType>::end() {
- return boost::make_transform_iterator(ite, Dereferencer<VariableType>());
+ return boost::make_transform_iterator(ite, Dereferencer<VariableType const>());
}
}
@@ -148,6 +148,21 @@ namespace storm {
bool VariableSet::containsUnboundedIntegerVariables() const {
return !unboundedIntegerVariables.empty();
}
+
+ template class detail::Dereferencer<Variable>;
+ template class detail::Dereferencer<BooleanVariable>;
+ template class detail::Dereferencer<BoundedIntegerVariable>;
+ template class detail::Dereferencer<UnboundedIntegerVariable>;
+ template class detail::Dereferencer<Variable const>;
+ template class detail::Dereferencer<BooleanVariable const>;
+ template class detail::Dereferencer<BoundedIntegerVariable const>;
+ template class detail::Dereferencer<UnboundedIntegerVariable const>;
+ template class detail::Variables<BooleanVariable>;
+ template class detail::Variables<BoundedIntegerVariable>;
+ template class detail::Variables<UnboundedIntegerVariable>;
+ template class detail::ConstVariables<BooleanVariable>;
+ template class detail::ConstVariables<BoundedIntegerVariable>;
+ template class detail::ConstVariables<UnboundedIntegerVariable>;
}
}
diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h
index 8d5aa3aed..eeedcdc6f 100644
--- a/src/storage/jani/VariableSet.h
+++ b/src/storage/jani/VariableSet.h
@@ -26,9 +26,7 @@ namespace storm {
class Variables {
public:
typedef typename std::vector<std::shared_ptr<VariableType>>::iterator input_iterator;
- typedef typename std::vector<std::shared_ptr<VariableType>>::const_iterator const_input_iterator;
typedef boost::transform_iterator<Dereferencer<VariableType>, input_iterator> iterator;
- typedef boost::transform_iterator<Dereferencer<VariableType const>, const_input_iterator> const_iterator;
Variables(input_iterator it, input_iterator ite);
@@ -43,9 +41,7 @@ namespace storm {
template<typename VariableType>
class ConstVariables {
public:
- typedef typename std::vector<std::shared_ptr<VariableType>>::iterator input_iterator;
typedef typename std::vector<std::shared_ptr<VariableType>>::const_iterator const_input_iterator;
- typedef boost::transform_iterator<Dereferencer<VariableType>, input_iterator> iterator;
typedef boost::transform_iterator<Dereferencer<VariableType const>, const_input_iterator> const_iterator;
ConstVariables(const_input_iterator it, const_input_iterator ite);
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 42cd1eb8a..711f68ad8 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -1610,6 +1610,9 @@ namespace storm {
janiModel.addAutomaton(automaton);
}
+ // Set the standard system composition. This is possible, because we reject non-standard compositions anyway.
+ janiModel.setSystemComposition(janiModel.getStandardSystemComposition());
+
return janiModel;
}
diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp
index 6b73c1a59..486a1b26e 100644
--- a/test/functional/builder/DdJaniModelBuilderTest.cpp
+++ b/test/functional/builder/DdJaniModelBuilderTest.cpp
@@ -16,34 +16,108 @@ TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) {
storm::jani::Model janiModel = program.toJani();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel);
+ auto t1 = std::chrono::high_resolution_clock::now();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.translate();
- EXPECT_EQ(13ul, model->getNumberOfStates());
- EXPECT_EQ(20ul, model->getNumberOfTransitions());
+ auto t2 = std::chrono::high_resolution_clock::now();
+ std::cout << "die: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
+
+// EXPECT_EQ(13ul, model->getNumberOfStates());
+// EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
janiModel = program.toJani();
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
+ t1 = std::chrono::high_resolution_clock::now();
+ 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::Sylvan, 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::Sylvan, 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();
+
+ t1 = std::chrono::high_resolution_clock::now();
+ builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
+ 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(DdJaniModelBuilderTest_Cudd, Dtmc) {
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+ storm::jani::Model janiModel = program.toJani();
+
+ storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
+ auto t1 = std::chrono::high_resolution_clock::now();
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.translate();
+ auto t2 = std::chrono::high_resolution_clock::now();
+ std::cout << "die: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
+
+ // EXPECT_EQ(13ul, model->getNumberOfStates());
+ // EXPECT_EQ(20ul, model->getNumberOfTransitions());
+
+ program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-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();
- EXPECT_EQ(677ul, model->getNumberOfStates());
- EXPECT_EQ(867ul, model->getNumberOfTransitions());
+ 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();
- EXPECT_EQ(8607ul, model->getNumberOfStates());
- EXPECT_EQ(15113ul, model->getNumberOfTransitions());
+ 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();
- EXPECT_EQ(273ul, model->getNumberOfStates());
- EXPECT_EQ(397ul, model->getNumberOfTransitions());
+ 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();
- EXPECT_EQ(1728ul, model->getNumberOfStates());
- EXPECT_EQ(2505ul, model->getNumberOfTransitions());
+ 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 b95039058..f89bb19ab 100644
--- a/test/functional/builder/DdPrismModelBuilderTest.cpp
+++ b/test/functional/builder/DdPrismModelBuilderTest.cpp
@@ -13,27 +13,42 @@
TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+ auto t1 = std::chrono::high_resolution_clock::now();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
+ auto t2 = std::chrono::high_resolution_clock::now();
+ std::cout << "die: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
+ t1 = std::chrono::high_resolution_clock::now();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
+ 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");
+ t1 = std::chrono::high_resolution_clock::now();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
+ 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");
+ t1 = std::chrono::high_resolution_clock::now();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
+ 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");
+ t1 = std::chrono::high_resolution_clock::now();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
+ 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());
}