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

more work on symbolic JANI model builder 

Former-commit-id: 4fe002c4f8
tempestpy_adaptions
dehnert 9 years ago
parent
1c01a54b53
commit
c4327e91a9
10 changed files with 168 additions and 54 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      src/adapters/AddExpressionAdapter.cpp
  2. 6
      src/adapters/AddExpressionAdapter.h
  3. 44
      src/builder/DdJaniModelBuilder.cpp
  4. 26
      src/builder/DdPrismModelBuilder.cpp
  5. 5
      src/storage/jani/Model.cpp
  6. 19
      src/storage/jani/VariableSet.cpp
  7. 4
      src/storage/jani/VariableSet.h
  8. 3
      src/storage/prism/Program.cpp
  9. 94
      test/functional/builder/DdJaniModelBuilderTest.cpp
  10. 15
      test/functional/builder/DdPrismModelBuilderTest.cpp

6
src/adapters/AddExpressionAdapter.cpp
View File

@ -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 {

6
src/adapters/AddExpressionAdapter.h
View File

@ -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

44
src/builder/DdJaniModelBuilder.cpp
View File

@ -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.

26
src/builder/DdPrismModelBuilder.cpp
View File

@ -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.

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

@ -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()) {

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

@ -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>;
}
}

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

@ -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);

3
src/storage/prism/Program.cpp
View File

@ -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;
}

94
test/functional/builder/DdJaniModelBuilderTest.cpp
View File

@ -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) {

15
test/functional/builder/DdPrismModelBuilderTest.cpp
View File

@ -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());
}

Write Preview
Loading…
Cancel
Save