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

created symbolic native solver to factor out numerical solution; prepared the code-path that stores rational functions in DDs (hybrid + dd engines)

tempestpy_adaptions
dehnert 8 years ago
parent
fd74476340
commit
1a803f4270
24 changed files with 479 additions and 153 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. 1
      src/storm/adapters/AddExpressionAdapter.cpp
  2. 100
      src/storm/builder/DdJaniModelBuilder.cpp
  3. 38
      src/storm/builder/DdPrismModelBuilder.cpp
  4. 29
      src/storm/cli/entrypoints.h
  5. 4
      src/storm/models/symbolic/Ctmc.cpp
  6. 6
      src/storm/models/symbolic/DeterministicModel.cpp
  7. 6
      src/storm/models/symbolic/Dtmc.cpp
  8. 4
      src/storm/models/symbolic/Mdp.cpp
  9. 3
      src/storm/models/symbolic/Model.cpp
  10. 5
      src/storm/models/symbolic/StandardRewardModel.cpp
  11. 87
      src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp
  12. 44
      src/storm/solver/SymbolicLinearEquationSolver.cpp
  13. 2
      src/storm/solver/SymbolicLinearEquationSolver.h
  14. 68
      src/storm/solver/SymbolicNativeLinearEquationSolver.cpp
  15. 58
      src/storm/solver/SymbolicNativeLinearEquationSolver.h
  16. 25
      src/storm/storage/dd/Add.cpp
  17. 9
      src/storm/storage/dd/Add.h
  18. 18
      src/storm/storage/dd/cudd/InternalCuddAdd.cpp
  19. 10
      src/storm/storage/dd/cudd/InternalCuddAdd.h
  20. 11
      src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
  21. 12
      src/storm/storage/dd/sylvan/InternalSylvanAdd.h
  22. 1
      src/storm/utility/constants.h
  23. 7
      src/storm/utility/solver.cpp
  24. 84
      src/storm/utility/storm.h

1
src/storm/adapters/AddExpressionAdapter.cpp
View File

@ -204,6 +204,7 @@ namespace storm {
// Explicitly instantiate the symbolic expression adapter
template class AddExpressionAdapter<storm::dd::DdType::CUDD, double>;
template class AddExpressionAdapter<storm::dd::DdType::Sylvan, double>;
#ifdef STORM_HAVE_CARL
template class AddExpressionAdapter<storm::dd::DdType::Sylvan, storm::RationalFunction>;
#endif

100
src/storm/builder/DdJaniModelBuilder.cpp
View File

@ -35,6 +35,8 @@
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/adapters/CarlAdapter.h"
namespace storm {
namespace builder {
@ -135,9 +137,9 @@ namespace storm {
struct CompositionVariables {
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)),
rowExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToRowMetaVariableMap)),
variableToColumnMetaVariableMap(std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>()),
columnExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type>>(manager, variableToColumnMetaVariableMap)) {
columnExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToColumnMetaVariableMap)) {
// Intentionally left empty.
}
@ -146,12 +148,12 @@ namespace storm {
// The meta variables for the row encoding.
std::set<storm::expressions::Variable> rowMetaVariables;
std::shared_ptr<std::map<storm::expressions::Variable, storm::expressions::Variable>> variableToRowMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter;
// The meta variables for the column encoding.
std::set<storm::expressions::Variable> columnMetaVariables;
std::shared_ptr<std::map<storm::expressions::Variable, storm::expressions::Variable>> variableToColumnMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> columnExpressionAdapter;
// All pairs of row/column meta variables.
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
@ -429,7 +431,7 @@ namespace storm {
};
template <storm::dd::DdType Type, typename ValueType>
EdgeDestinationDd<Type, ValueType> buildEdgeDestinationDd(storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, storm::dd::Add<Type, ValueType> const& guard, CompositionVariables<Type, ValueType> const& variables) {
EdgeDestinationDd<Type, ValueType> buildEdgeDestinationDd(storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, storm::dd::Bdd<Type> const& guard, CompositionVariables<Type, ValueType> const& variables) {
storm::dd::Add<Type, ValueType> transitions = variables.rowExpressionAdapter->translateExpression(destination.getProbability());
STORM_LOG_TRACE("Translating edge destination.");
@ -449,11 +451,11 @@ namespace storm {
storm::dd::Add<Type, ValueType> assignedExpression = variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
// Combine the assigned expression with the guard.
storm::dd::Add<Type, ValueType> result = assignedExpression * guard;
storm::dd::Add<Type, ValueType> result = assignedExpression * guard.template toAdd<ValueType>();
// Combine the variable and the assigned expression.
result = result.equals(writtenVariable).template toAdd<ValueType>();
result *= guard;
result *= guard.template toAdd<ValueType>();
// Restrict the transitions to the range of the written variable.
result = result * variables.variableToRangeMap.at(primedMetaVariable).template toAdd<ValueType>();
@ -515,7 +517,7 @@ namespace storm {
}
}
result.setValue(metaVariableNameToValueMap, 1);
result.setValue(metaVariableNameToValueMap, storm::utility::one<ValueType>());
return result;
}
@ -524,15 +526,15 @@ namespace storm {
public:
// This structure represents an edge.
struct EdgeDd {
EdgeDd(bool isMarkovian, storm::dd::Add<Type> const& guard, storm::dd::Add<Type, ValueType> const& transitions, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientEdgeAssignments, std::set<storm::expressions::Variable> const& writtenGlobalVariables) : isMarkovian(isMarkovian), guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), variableToWritingFragment() {
EdgeDd(bool isMarkovian, storm::dd::Bdd<Type> const& guard, storm::dd::Add<Type, ValueType> const& transitions, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientEdgeAssignments, std::set<storm::expressions::Variable> const& writtenGlobalVariables) : isMarkovian(isMarkovian), guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), variableToWritingFragment() {
// Convert the set of written variables to a mapping from variable to the writing fragments.
for (auto const& variable : writtenGlobalVariables) {
variableToWritingFragment[variable] = guard.toBdd();
variableToWritingFragment[variable] = guard;
}
}
EdgeDd(bool isMarkovian, storm::dd::Add<Type> const& guard, storm::dd::Add<Type, ValueType> const& transitions, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientEdgeAssignments, std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& variableToWritingFragment) : isMarkovian(isMarkovian), guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), variableToWritingFragment(variableToWritingFragment) {
EdgeDd(bool isMarkovian, storm::dd::Bdd<Type> const& guard, storm::dd::Add<Type, ValueType> const& transitions, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientEdgeAssignments, std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& variableToWritingFragment) : isMarkovian(isMarkovian), guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), variableToWritingFragment(variableToWritingFragment) {
// Intentionally left empty.
}
@ -540,7 +542,7 @@ namespace storm {
bool isMarkovian;
// A DD that represents all states that have this edge enabled.
storm::dd::Add<Type, ValueType> guard;
storm::dd::Bdd<Type> guard;
// A DD that represents the transitions of this edge.
storm::dd::Add<Type, ValueType> transitions;
@ -554,7 +556,7 @@ namespace storm {
// This structure represents an edge.
struct ActionDd {
ActionDd(storm::dd::Add<Type> const& guard = storm::dd::Add<Type>(), storm::dd::Add<Type, ValueType> const& transitions = storm::dd::Add<Type, ValueType>(), std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientEdgeAssignments = {}, std::pair<uint64_t, uint64_t> localNondeterminismVariables = std::pair<uint64_t, uint64_t>(0, 0), std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& variableToWritingFragment = {}, storm::dd::Bdd<Type> const& illegalFragment = storm::dd::Bdd<Type>()) : guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), localNondeterminismVariables(localNondeterminismVariables), variableToWritingFragment(variableToWritingFragment), illegalFragment(illegalFragment), inputEnabled(false) {
ActionDd(storm::dd::Bdd<Type> const& guard = storm::dd::Bdd<Type>(), storm::dd::Add<Type, ValueType> const& transitions = storm::dd::Add<Type, ValueType>(), std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientEdgeAssignments = {}, std::pair<uint64_t, uint64_t> localNondeterminismVariables = std::pair<uint64_t, uint64_t>(0, 0), std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& variableToWritingFragment = {}, storm::dd::Bdd<Type> const& illegalFragment = storm::dd::Bdd<Type>()) : guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), localNondeterminismVariables(localNondeterminismVariables), variableToWritingFragment(variableToWritingFragment), illegalFragment(illegalFragment), inputEnabled(false) {
// Intentionally left empty.
}
@ -583,7 +585,7 @@ namespace storm {
}
// A DD that represents all states that have this edge enabled.
storm::dd::Add<Type, ValueType> guard;
storm::dd::Bdd<Type> guard;
// A DD that represents the transitions of this edge.
storm::dd::Add<Type, ValueType> transitions;
@ -909,9 +911,8 @@ namespace storm {
for (auto const& actionIndexPair : actions) {
auto componentIndex = actionIndexPair.first;
auto const& action = actionIndexPair.second.get();
storm::dd::Bdd<Type> actionGuard = action.guard.toBdd();
if (guardDisjunction) {
guardDisjunction.get() |= actionGuard;
guardDisjunction.get() |= action.guard;
}
lowestNondeterminismVariable = std::min(lowestNondeterminismVariable, action.getLowestLocalNondeterminismVariable());
@ -920,7 +921,7 @@ namespace storm {
if (action.isInputEnabled()) {
// If the action is input-enabled, we add self-loops to all states.
transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * subautomata[componentIndex].identity);
transitions *= action.guard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * subautomata[componentIndex].identity);
} else {
transitions *= action.transitions;
}
@ -956,12 +957,12 @@ namespace storm {
// guard of the current action if the current action is not input enabled.
for (auto& entry : globalVariableToWritingFragment) {
if (action.variableToWritingFragment.find(entry.first) == action.variableToWritingFragment.end() && !action.isInputEnabled()) {
entry.second &= actionGuard;
entry.second &= action.guard;
}
}
if (!action.isInputEnabled()) {
inputEnabledGuard &= actionGuard;
inputEnabledGuard &= action.guard;
}
}
@ -976,7 +977,7 @@ namespace storm {
// such a combined transition.
illegalFragment &= inputEnabledGuard;
return ActionDd(inputEnabledGuard.template toAdd<ValueType>(), transitions * nonSynchronizingIdentity, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment);
return ActionDd(inputEnabledGuard, transitions * nonSynchronizingIdentity, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment);
}
ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2, storm::dd::Add<Type, ValueType> const& identity1, storm::dd::Add<Type, ValueType> const& identity2) {
@ -1001,7 +1002,7 @@ namespace storm {
ActionDd result(*actionIt);
for (++actionIt; actionIt != actions.end(); ++actionIt) {
result = ActionDd(result.guard + actionIt->guard, result.transitions + actionIt->transitions, joinTransientAssignmentMaps(result.transientEdgeAssignments, actionIt->transientEdgeAssignments), std::make_pair<uint64_t, uint64_t>(0, 0), joinVariableWritingFragmentMaps(result.variableToWritingFragment, actionIt->variableToWritingFragment), result.illegalFragment || actionIt->illegalFragment);
result = ActionDd(result.guard || actionIt->guard, result.transitions + actionIt->transitions, joinTransientAssignmentMaps(result.transientEdgeAssignments, actionIt->transientEdgeAssignments), std::make_pair<uint64_t, uint64_t>(0, 0), joinVariableWritingFragmentMaps(result.variableToWritingFragment, actionIt->variableToWritingFragment), result.illegalFragment || actionIt->illegalFragment);
}
return result;
} else if (this->model.getModelType() == storm::jani::ModelType::MDP) {
@ -1041,7 +1042,7 @@ namespace storm {
for (uint64_t actionIndex = 0; actionIndex < actions.size(); ++actionIndex) {
ActionDd& action = actions[actionIndex];
guard |= action.guard.toBdd();
guard |= action.guard;
storm::dd::Add<Type, ValueType> nondeterminismEncoding = encodeIndex(actionIndex, highestLocalNondeterminismVariable, numberOfLocalNondeterminismVariables, this->variables);
transitions += nondeterminismEncoding * action.transitions;
@ -1056,7 +1057,7 @@ namespace storm {
illegalFragment |= action.illegalFragment;
}
return ActionDd(guard.template toAdd<ValueType>(), transitions, transientEdgeAssignments, std::make_pair(lowestLocalNondeterminismVariable, highestLocalNondeterminismVariable + numberOfLocalNondeterminismVariables), variableToWritingFragment, illegalFragment);
return ActionDd(guard, transitions, transientEdgeAssignments, std::make_pair(lowestLocalNondeterminismVariable, highestLocalNondeterminismVariable + numberOfLocalNondeterminismVariables), variableToWritingFragment, illegalFragment);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type.");
}
@ -1084,8 +1085,8 @@ namespace storm {
// We keep the guard and a "ranged" version seperate, because building the destinations tends to be
// slower when the full range is applied.
storm::dd::Add<Type, ValueType> guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard());
storm::dd::Add<Type, ValueType> rangedGuard = guard * this->variables.automatonToRangeMap.at(automaton.getName());
storm::dd::Bdd<Type> guard = this->variables.rowExpressionAdapter->translateBooleanExpression(edge.getGuard());
storm::dd::Bdd<Type> rangedGuard = guard && this->variables.automatonToRangeMap.at(automaton.getName()).toBdd();
STORM_LOG_WARN_COND(!rangedGuard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable.");
if (!rangedGuard.isZero()) {
@ -1132,7 +1133,7 @@ namespace storm {
}
// Add the source location and the guard.
storm::dd::Add<Type, ValueType> sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
storm::dd::Add<Type, ValueType> sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard.template toAdd<ValueType>();
transitions *= sourceLocationAndGuard;
// If we multiply the ranges of global variables, make sure everything stays within its bounds.
@ -1155,9 +1156,9 @@ namespace storm {
} );
}
return EdgeDd(isMarkovian, guard, guard * transitions, transientEdgeAssignments, globalVariablesInSomeDestination);
return EdgeDd(isMarkovian, guard, guard.template toAdd<ValueType>() * transitions, transientEdgeAssignments, globalVariablesInSomeDestination);
} else {
return EdgeDd(false, rangedGuard, rangedGuard, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>>(), std::set<storm::expressions::Variable>());
return EdgeDd(false, rangedGuard, rangedGuard.template toAdd<ValueType>(), std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>>(), std::set<storm::expressions::Variable>());
}
}
@ -1172,10 +1173,10 @@ namespace storm {
STORM_LOG_THROW(edge.isMarkovian, storm::exceptions::WrongFormatException, "Can only combine Markovian edges.");
if (!overlappingGuards) {
overlappingGuards |= !(guard && edge.guard.toBdd()).isZero();
overlappingGuards |= !(guard && edge.guard).isZero();
}
guard |= edge.guard.toBdd();
guard |= edge.guard;
transitions += edge.transitions;
variableToWritingFragment = joinVariableWritingFragmentMaps(variableToWritingFragment, edge.variableToWritingFragment);
joinTransientAssignmentMaps(transientEdgeAssignments, edge.transientEdgeAssignments);
@ -1184,7 +1185,7 @@ namespace storm {
// Currently, we can only combine the transient edge assignments if there is no overlap of the guards of the edges.
STORM_LOG_THROW(!overlappingGuards || transientEdgeAssignments.empty(), storm::exceptions::NotSupportedException, "Cannot have transient edge assignments when combining Markovian edges with overlapping guards.");
return EdgeDd(true, guard.template toAdd<ValueType>(), transitions, transientEdgeAssignments, variableToWritingFragment);
return EdgeDd(true, guard, transitions, transientEdgeAssignments, variableToWritingFragment);
}
ActionDd buildActionDdForActionIndex(storm::jani::Automaton const& automaton, uint64_t actionIndex, uint64_t localNondeterminismVariableOffset) {
@ -1228,7 +1229,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Cannot translate model of this type.");
}
} else {
return ActionDd(this->variables.manager->template getAddZero<ValueType>(), this->variables.manager->template getAddZero<ValueType>(), {}, std::make_pair<uint64_t, uint64_t>(0, 0), {}, this->variables.manager->getBddZero());
return ActionDd(this->variables.manager->template getBddZero(), this->variables.manager->template getAddZero<ValueType>(), {}, std::make_pair<uint64_t, uint64_t>(0, 0), {}, this->variables.manager->getBddZero());
}
}
@ -1279,14 +1280,13 @@ namespace storm {
STORM_LOG_THROW((this->model.getModelType() == storm::jani::ModelType::CTMC) == edgeDd.isMarkovian, storm::exceptions::WrongFormatException, "Unexpected non-Markovian edge in CTMC.");
// Check for overlapping guards.
storm::dd::Bdd<Type> guardBdd = edgeDd.guard.toBdd();
overlappingGuards = !(guardBdd && allGuards).isZero();
overlappingGuards = !(edgeDd.guard && allGuards).isZero();
// Issue a warning if there are overlapping guards in a DTMC.
STORM_LOG_WARN_COND(!overlappingGuards || this->model.getModelType() == storm::jani::ModelType::CTMC, "Guard of an edge in a DTMC overlaps with previous guards.");
// Add the elements of the current edge to the global ones.
allGuards |= guardBdd;
allGuards |= edgeDd.guard;
allTransitions += edgeDd.transitions;
// Add the transient variable assignments to the resulting one. This transformation is illegal for
@ -1300,7 +1300,7 @@ namespace storm {
STORM_LOG_THROW(this->model.getModelType() == storm::jani::ModelType::DTMC || !overlappingGuards || transientEdgeAssignments.empty(), storm::exceptions::NotSupportedException, "Cannot have transient edge assignments when combining Markovian edges with overlapping guards.");
return ActionDd(allGuards.template toAdd<ValueType>(), allTransitions, transientEdgeAssignments, std::make_pair<uint64_t, uint64_t>(0, 0), globalVariableToWritingFragment, this->variables.manager->getBddZero());
return ActionDd(allGuards, allTransitions, transientEdgeAssignments, std::make_pair<uint64_t, uint64_t>(0, 0), globalVariableToWritingFragment, this->variables.manager->getBddZero());
}
void addToVariableWritingFragmentMap(std::map<storm::expressions::Variable, storm::dd::Bdd<Type>>& globalVariableToWritingFragment, storm::expressions::Variable const& variable, storm::dd::Bdd<Type> const& partToAdd) const {
@ -1333,7 +1333,7 @@ namespace storm {
return result;
}
ActionDd combineEdgesBySummation(storm::dd::Add<Type, ValueType> const& guard, std::vector<EdgeDd> const& edges, boost::optional<EdgeDd> const& markovianEdge) {
ActionDd combineEdgesBySummation(storm::dd::Bdd<Type> const& guard, std::vector<EdgeDd> const& edges, boost::optional<EdgeDd> const& markovianEdge) {
bool addMarkovianFlag = this->model.getModelType() == storm::jani::ModelType::MA;
STORM_LOG_ASSERT(addMarkovianFlag || !markovianEdge, "Illegally adding Markovian edge without marker.");
@ -1374,18 +1374,18 @@ namespace storm {
ActionDd combineEdgesToActionNondeterministic(std::vector<EdgeDd> const& nonMarkovianEdges, boost::optional<EdgeDd> const& markovianEdge, uint64_t localNondeterminismVariableOffset) {
// Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state.
storm::dd::Bdd<Type> allGuards = this->variables.manager->getBddZero();
storm::dd::Add<Type, ValueType> sumOfGuards = this->variables.manager->template getAddZero<ValueType>();
storm::dd::Add<Type, uint_fast64_t> sumOfGuards = this->variables.manager->template getAddZero<uint_fast64_t>();
for (auto const& edge : nonMarkovianEdges) {
STORM_LOG_ASSERT(!edge.isMarkovian, "Unexpected Markovian edge.");
sumOfGuards += edge.guard;
allGuards |= edge.guard.toBdd();
sumOfGuards += edge.guard.template toAdd<uint_fast64_t>();
allGuards |= edge.guard;
}
uint_fast64_t maxChoices = static_cast<uint_fast64_t>(sumOfGuards.getMax());
uint_fast64_t maxChoices = sumOfGuards.getMax();
STORM_LOG_TRACE("Found " << maxChoices << " non-Markovian local choices.");
// Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism.
if (maxChoices <= 1) {
return combineEdgesBySummation(allGuards.template toAdd<ValueType>(), nonMarkovianEdges, markovianEdge);
return combineEdgesBySummation(allGuards, nonMarkovianEdges, markovianEdge);
} else {
// Calculate number of required variables to encode the nondeterminism.
uint_fast64_t numberOfBinaryVariables = static_cast<uint_fast64_t>(std::ceil(storm::utility::math::log2(maxChoices)));
@ -1405,7 +1405,7 @@ namespace storm {
for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) {
// Determine the set of states with exactly currentChoices choices.
equalsNumberOfChoicesDd = sumOfGuards.equals(this->variables.manager->getConstant(static_cast<double>(currentChoices)));
equalsNumberOfChoicesDd = sumOfGuards.equals(this->variables.manager->getConstant(currentChoices));
// If there is no such state, continue with the next possible number of choices.
if (equalsNumberOfChoicesDd.isZero()) {
@ -1423,7 +1423,7 @@ namespace storm {
// Check if edge guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices
// choices such that one outgoing choice is given by the j-th edge.
storm::dd::Bdd<Type> guardChoicesIntersection = currentEdge.guard.toBdd() && equalsNumberOfChoicesDd;
storm::dd::Bdd<Type> guardChoicesIntersection = currentEdge.guard && equalsNumberOfChoicesDd;
// If there is no such state, continue with the next command.
if (guardChoicesIntersection.isZero()) {
@ -1470,7 +1470,7 @@ namespace storm {
}
// Delete currentChoices out of overlapping DD
sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd<ValueType>();
sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd<uint_fast64_t>();
}
// Extend the transitions with the appropriate flag if needed.
@ -1503,7 +1503,7 @@ namespace storm {
}
}
return ActionDd(allGuards.template toAdd<ValueType>(), allEdges, transientAssignments, std::make_pair(localNondeterminismVariableOffset, localNondeterminismVariableOffset + numberOfBinaryVariables), globalVariableToWritingFragment, this->variables.manager->getBddZero());
return ActionDd(allGuards, allEdges, transientAssignments, std::make_pair(localNondeterminismVariableOffset, localNondeterminismVariableOffset + numberOfBinaryVariables), globalVariableToWritingFragment, this->variables.manager->getBddZero());
}
}
@ -1633,11 +1633,11 @@ namespace storm {
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> createModel(storm::jani::ModelType const& modelType, CompositionVariables<Type, ValueType> const& variables, ModelComponents<Type, ValueType> const& modelComponents) {
if (modelType == storm::jani::ModelType::DTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
return std::make_shared<storm::models::symbolic::Dtmc<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
} else if (modelType == storm::jani::ModelType::CTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
return std::make_shared<storm::models::symbolic::Ctmc<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
} else if (modelType == storm::jani::ModelType::MDP) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
return std::make_shared<storm::models::symbolic::Mdp<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type.");
}
@ -1927,5 +1927,7 @@ namespace storm {
template class DdJaniModelBuilder<storm::dd::DdType::CUDD, double>;
template class DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>;
template class DdJaniModelBuilder<storm::dd::DdType::Sylvan, storm::RationalFunction>;
}
}

38
src/storm/builder/DdPrismModelBuilder.cpp
View File

@ -26,6 +26,8 @@
#include "storm/settings/modules/CoreSettings.h"
#include "storm/adapters/CarlAdapter.h"
namespace storm {
namespace builder {
@ -786,7 +788,7 @@ namespace storm {
}
}
result.setValue(metaVariableNameToValueMap, ValueType(1));
result.setValue(metaVariableNameToValueMap, storm::utility::one<ValueType>());
return result;
}
@ -799,12 +801,12 @@ namespace storm {
std::set<storm::expressions::Variable> assignedGlobalVariables = equalizeAssignedGlobalVariables(generationInfo, commandDds);
// Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state.
storm::dd::Add<Type, ValueType> sumOfGuards = generationInfo.manager->template getAddZero<ValueType>();
storm::dd::Add<Type, uint_fast64_t> sumOfGuards = generationInfo.manager->template getAddZero<uint_fast64_t>();
for (auto const& commandDd : commandDds) {
sumOfGuards += commandDd.guardDd.template toAdd<ValueType>();
sumOfGuards += commandDd.guardDd.template toAdd<uint_fast64_t>();
allGuards |= commandDd.guardDd;
}
uint_fast64_t maxChoices = static_cast<uint_fast64_t>(sumOfGuards.getMax());
uint_fast64_t maxChoices = sumOfGuards.getMax();
STORM_LOG_TRACE("Found " << maxChoices << " local choices.");
@ -827,7 +829,7 @@ namespace storm {
for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) {
// Determine the set of states with exactly currentChoices choices.
equalsNumberOfChoicesDd = sumOfGuards.equals(generationInfo.manager->getConstant(ValueType(currentChoices)));
equalsNumberOfChoicesDd = sumOfGuards.equals(generationInfo.manager->getConstant(currentChoices));
// If there is no such state, continue with the next possible number of choices.
if (equalsNumberOfChoicesDd.isZero()) {
@ -880,7 +882,7 @@ namespace storm {
}
// Delete currentChoices out of overlapping DD
sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd<ValueType>();
sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd<uint_fast64_t>();
}
return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables);
@ -1111,6 +1113,17 @@ namespace storm {
return rewardModels;
}
template <storm::dd::DdType Type, typename ValueType>
void checkRewards(storm::dd::Add<Type, ValueType> const& rewards) {
STORM_LOG_WARN_COND(rewards.getMin() >= 0, "The reward model assigns negative rewards to some states.");
STORM_LOG_WARN_COND(!rewards.isZero(), "The reward model does not assign any non-zero rewards.");
}
template <storm::dd::DdType Type>
void checkRewards(storm::dd::Add<Type, storm::RationalFunction> const& rewards) {
STORM_LOG_WARN_COND(!rewards.isZero(), "The reward model does not assign any non-zero rewards.");
}
template <storm::dd::DdType Type, typename ValueType>
storm::models::symbolic::StandardRewardModel<Type, ValueType> DdPrismModelBuilder<Type, ValueType>::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& transitionMatrix, boost::optional<storm::dd::Add<Type, ValueType>>& stateActionDd) {
@ -1127,8 +1140,7 @@ namespace storm {
rewards = reachableStatesAdd * states * rewards;
// Perform some sanity checks.
STORM_LOG_WARN_COND(rewards.getMin() >= 0, "The reward model assigns negative rewards to some states.");
STORM_LOG_WARN_COND(!rewards.isZero(), "The reward model does not assign any non-zero rewards.");
checkRewards(rewards);
// Add the rewards to the global state reward vector.
stateRewards.get() += rewards;
@ -1165,8 +1177,7 @@ namespace storm {
}
// Perform some sanity checks.
STORM_LOG_WARN_COND(stateActionRewardDd.getMin() >= 0, "The reward model assigns negative rewards to some states.");
STORM_LOG_WARN_COND(!stateActionRewardDd.isZero(), "The reward model does not assign any non-zero rewards.");
checkRewards(stateActionRewardDd);
// Add the rewards to the global transition reward matrix.
stateActionRewards.get() += stateActionRewardDd;
@ -1217,8 +1228,7 @@ namespace storm {
}
// Perform some sanity checks.
STORM_LOG_WARN_COND(transitionRewardDd.getMin() >= 0, "The reward model assigns negative rewards to some states.");
STORM_LOG_WARN_COND(!transitionRewardDd.isZero(), "The reward model does not assign any non-zero rewards.");
checkRewards(transitionRewardDd);
// Add the rewards to the global transition reward matrix.
transitionRewards.get() += transitionRewardDd;
@ -1427,7 +1437,9 @@ namespace storm {
// Explicitly instantiate the symbolic model builder.
template class DdPrismModelBuilder<storm::dd::DdType::CUDD>;
template class DdPrismModelBuilder<storm::dd::DdType::Sylvan>;
template class DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalFunction>;
} // namespace adapters
} // namespace storm

29
src/storm/cli/entrypoints.h
View File

@ -196,8 +196,8 @@ namespace storm {
}
#endif
template<storm::dd::DdType DdType>
void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) {
template<storm::dd::DdType DdType, typename ValueType>
void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) {
for (auto const& property : formulas) {
STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush();
@ -217,8 +217,8 @@ namespace storm {
}
}
template<storm::dd::DdType DdType>
void verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) {
template<storm::dd::DdType DdType, typename ValueType>
void verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) {
for (auto const& property : formulas) {
STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush();
@ -277,11 +277,11 @@ namespace storm {
STORM_LOG_ASSERT(false, "Unknown model type."); \
}
template<storm::dd::DdType LibraryType>
template<storm::dd::DdType LibraryType, typename ValueType = double>
void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
// Start by building the model.
storm::utility::Stopwatch modelBuildingWatch(true);
auto markovModel = buildSymbolicModel<double, LibraryType>(model, extractFormulasFromProperties(properties));
auto markovModel = buildSymbolicModel<ValueType, LibraryType>(model, extractFormulasFromProperties(properties));
modelBuildingWatch.stop();
STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl);
@ -290,9 +290,9 @@ namespace storm {
// Then select the correct engine.
if (hybrid) {
verifySymbolicModelWithHybridEngine(markovModel, properties, onlyInitialStatesRelevant);
verifySymbolicModelWithHybridEngine<LibraryType, ValueType>(markovModel, properties, onlyInitialStatesRelevant);
} else {
verifySymbolicModelWithDdEngine(markovModel, properties, onlyInitialStatesRelevant);
verifySymbolicModelWithDdEngine<LibraryType, ValueType>(markovModel, properties, onlyInitialStatesRelevant);
}
}
@ -376,8 +376,17 @@ namespace storm {
template<>
void buildAndCheckSymbolicModel<storm::RationalFunction>(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant) {
STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one.");
buildAndCheckSymbolicModelWithSparseEngine<storm::RationalFunction>(model, formulas, onlyInitialStatesRelevant);
auto engine = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine();
if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
auto ddlib = storm::settings::getModule<storm::settings::modules::CoreSettings>().getDdLibraryType();
STORM_LOG_THROW(ddlib == storm::dd::DdType::Sylvan, storm::exceptions::InvalidSettingsException, "This data-type is only available when selecting sylvan.");
buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::Sylvan, storm::RationalFunction>(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, model, formulas, onlyInitialStatesRelevant);
} else {
STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Illegal engine.");
buildAndCheckSymbolicModelWithSparseEngine<storm::RationalFunction>(model, formulas, onlyInitialStatesRelevant);
}
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot use this data type with this engine.");
}
#endif

4
src/storm/models/symbolic/Ctmc.cpp
View File

@ -6,6 +6,8 @@
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/adapters/CarlAdapter.h"
namespace storm {
namespace models {
namespace symbolic {
@ -57,6 +59,8 @@ namespace storm {
template class Ctmc<storm::dd::DdType::CUDD, double>;
template class Ctmc<storm::dd::DdType::Sylvan, double>;
template class Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction>;
} // namespace symbolic
} // namespace models
} // namespace storm

6
src/storm/models/symbolic/DeterministicModel.cpp
View File

@ -6,6 +6,8 @@
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/adapters/CarlAdapter.h"
namespace storm {
namespace models {
namespace symbolic {
@ -31,7 +33,9 @@ namespace storm {
// Explicitly instantiate the template class.
template class DeterministicModel<storm::dd::DdType::CUDD>;
template class DeterministicModel<storm::dd::DdType::Sylvan>;
template class DeterministicModel<storm::dd::DdType::Sylvan, storm::RationalFunction>;
} // namespace symbolic
} // namespace models
} // namespace storm

6
src/storm/models/symbolic/Dtmc.cpp
View File

@ -6,6 +6,8 @@
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/adapters/CarlAdapter.h"
namespace storm {
namespace models {
namespace symbolic {
@ -30,7 +32,9 @@ namespace storm {
// Explicitly instantiate the template class.
template class Dtmc<storm::dd::DdType::CUDD, double>;
template class Dtmc<storm::dd::DdType::Sylvan, double>;
template class Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>;
} // namespace symbolic
} // namespace models
} // namespace storm

4
src/storm/models/symbolic/Mdp.cpp
View File

@ -6,6 +6,8 @@
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/adapters/CarlAdapter.h"
namespace storm {
namespace models {
namespace symbolic {
@ -31,6 +33,8 @@ namespace storm {
// Explicitly instantiate the template class.
template class Mdp<storm::dd::DdType::CUDD, double>;
template class Mdp<storm::dd::DdType::Sylvan, double>;
template class Mdp<storm::dd::DdType::Sylvan, storm::RationalFunction>;
} // namespace symbolic
} // namespace models

3
src/storm/models/symbolic/Model.cpp
View File

@ -271,9 +271,8 @@ namespace storm {
// Explicitly instantiate the template class.
template class Model<storm::dd::DdType::CUDD, double>;
template class Model<storm::dd::DdType::Sylvan, double>;
#ifdef STORM_HAVE_CARL
template class Model<storm::dd::DdType::Sylvan, storm::RationalFunction>;
#endif
} // namespace symbolic
} // namespace models
} // namespace storm

5
src/storm/models/symbolic/StandardRewardModel.cpp
View File

@ -4,6 +4,8 @@
#include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/adapters/CarlAdapter.h"
namespace storm {
namespace models {
namespace symbolic {
@ -157,6 +159,9 @@ namespace storm {
template class StandardRewardModel<storm::dd::DdType::CUDD, double>;
template class StandardRewardModel<storm::dd::DdType::Sylvan, double>;
template class StandardRewardModel<storm::dd::DdType::Sylvan, storm::RationalFunction>;
}
}
}

87
src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp
View File

@ -5,6 +5,8 @@
#include "storm/utility/dd.h"
#include "storm/adapters/CarlAdapter.h"
namespace storm {
namespace solver {
@ -20,45 +22,100 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicEliminationLinearEquationSolver<DdType, ValueType>::solveEquations(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
storm::dd::DdManager<DdType>& ddManager = x.getDdManager();
// We start by creating triple-layered meta variables for all original meta variables. We will use them later in the elimination process.
std::vector<std::vector<storm::expressions::Variable>> oldToNewMapping;
std::set<storm::expressions::Variable> newRowVariables;
std::set<storm::expressions::Variable> newColumnVariables;
std::set<storm::expressions::Variable> helperVariables;
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> newRowColumnMetaVariablePairs;
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> columnHelperMetaVariablePairs;
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowRowMetaVariablePairs;
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> columnColumnMetaVariablePairs;
for (auto const& metaVariablePair : this->rowColumnMetaVariablePairs) {
auto rowVariable = metaVariablePair.first;
storm::dd::DdMetaVariable<DdType> const& metaVariable = ddManager.getMetaVariable(rowVariable);
std::vector<storm::expressions::Variable> newMetaVariables;
if (metaVariable.getType() == storm::dd::MetaVariableType::Bool) {
newMetaVariables = ddManager.addMetaVariable("tmp_" + metaVariable.getName(), 3);
} else {
newMetaVariables = ddManager.addMetaVariable("tmp_" + metaVariable.getName(), metaVariable.getLow(), metaVariable.getHigh(), 3);
}
newRowVariables.insert(newMetaVariables[0]);
newColumnVariables.insert(newMetaVariables[1]);
helperVariables.insert(newMetaVariables[2]);
newRowColumnMetaVariablePairs.emplace_back(newMetaVariables[0], newMetaVariables[1]);
columnHelperMetaVariablePairs.emplace_back(newMetaVariables[1], newMetaVariables[2]);
rowRowMetaVariablePairs.emplace_back(metaVariablePair.first, newMetaVariables[0]);
columnColumnMetaVariablePairs.emplace_back(metaVariablePair.second, newMetaVariables[1]);
oldToNewMapping.emplace_back(std::move(newMetaVariables));
}
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> oldNewMetaVariablePairs = rowRowMetaVariablePairs;
for (auto const& entry : columnColumnMetaVariablePairs) {
oldNewMetaVariablePairs.emplace_back(entry.first, entry.second);
}
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> shiftMetaVariablePairs = newRowColumnMetaVariablePairs;
for (auto const& entry : columnHelperMetaVariablePairs) {
shiftMetaVariablePairs.emplace_back(entry.first, entry.second);
}
// Build diagonal BDD over new meta variables.
storm::dd::Bdd<DdType> diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), this->rowColumnMetaVariablePairs);
diagonal &= this->allRows;
diagonal = diagonal.swapVariables(oldNewMetaVariablePairs);
storm::dd::Add<DdType, ValueType> rowsAdd = this->allRows.template toAdd<ValueType>();
storm::dd::Add<DdType, ValueType> rowsAdd = this->allRows.swapVariables(rowRowMetaVariablePairs).template toAdd<ValueType>();
storm::dd::Add<DdType, ValueType> diagonalAdd = diagonal.template toAdd<ValueType>();
// Revert the conversion to an equation system.
storm::dd::Add<DdType, ValueType> matrix = diagonalAdd - this->A;
// Revert the conversion to an equation system and move it to the new meta variables.
storm::dd::Add<DdType, ValueType> matrix = diagonalAdd - this->A.swapVariables(oldNewMetaVariablePairs);
storm::dd::Add<DdType, ValueType> solution = b;
// Initialize solution over the new meta variables.
storm::dd::Add<DdType, ValueType> solution = b.swapVariables(oldNewMetaVariablePairs);
// As long as there are transitions, we eliminate them.
uint64_t iterations = 0;
while (!matrix.isZero()) {
// Determine inverse loop probabilies
storm::dd::Add<DdType, ValueType> inverseLoopProbabilities = rowsAdd / (rowsAdd - (diagonalAdd * matrix).sumAbstract(this->columnMetaVariables));
inverseLoopProbabilities.swapVariables(this->rowColumnMetaVariablePairs);
storm::dd::Add<DdType, ValueType> inverseLoopProbabilities = rowsAdd / (rowsAdd - (diagonalAdd * matrix).sumAbstract(newColumnVariables));
// Scale all transitions with the inverse loop probabilities.
matrix *= inverseLoopProbabilities;
solution *= inverseLoopProbabilities;
// Delete diagonal elements, i.e. remove self-loops.
matrix = diagonal.ite(x.getDdManager().template getAddZero<ValueType>(), matrix);
matrix = diagonal.ite(ddManager.template getAddZero<ValueType>(), matrix);
// Update the one-step probabilities.
solution += (matrix * solution.swapVariables(this->rowColumnMetaVariablePairs)).sumAbstract(this->columnMetaVariables);
solution += (matrix * solution.swapVariables(newRowColumnMetaVariablePairs)).sumAbstract(newColumnVariables);
// Shortcut all transitions by eliminating one intermediate step.
matrix = matrix.multiplyMatrix(matrix.permuteVariables(shiftMetaVariablePairs), newColumnVariables);
matrix = matrix.swapVariables(columnHelperMetaVariablePairs);
// Now eliminate all direct transitions of all states.
storm::dd::Add<DdType, ValueType> matrixWithRemoved;
++iterations;
std::cout << "iteration: " << iterations << std::endl;
}
std::cout << "here" << std::endl;
solution.exportToDot("solution.dot");
STORM_LOG_DEBUG("Elimination completed in " << iterations << " iterations.");
exit(-1);
return solution.swapVariables(rowRowMetaVariablePairs);
}
template class SymbolicEliminationLinearEquationSolver<storm::dd::DdType::CUDD, double>;
template class SymbolicEliminationLinearEquationSolver<storm::dd::DdType::Sylvan, double>;
template class SymbolicEliminationLinearEquationSolver<storm::dd::DdType::Sylvan, storm::RationalFunction>;
}
}

44
src/storm/solver/SymbolicLinearEquationSolver.cpp
View File

@ -8,6 +8,8 @@
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/NativeEquationSolverSettings.h"
#include "storm/adapters/CarlAdapter.h"
namespace storm {
namespace solver {
@ -26,47 +28,7 @@ namespace storm {
precision = settings.getPrecision();
relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative;
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicLinearEquationSolver<DdType, ValueType>::solveEquations(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
// Start by computing the Jacobi decomposition of the matrix A.
storm::dd::Bdd<DdType> diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), rowColumnMetaVariablePairs);
diagonal &= allRows;
storm::dd::Add<DdType, ValueType> lu = diagonal.ite(this->A.getDdManager().template getAddZero<ValueType>(), this->A);
storm::dd::Add<DdType> diagonalAdd = diagonal.template toAdd<ValueType>();
storm::dd::Add<DdType, ValueType> diag = diagonalAdd.multiplyMatrix(this->A, this->columnMetaVariables);
storm::dd::Add<DdType, ValueType> scaledLu = lu / diag;
storm::dd::Add<DdType, ValueType> scaledB = b / diag;
// Set up additional environment variables.
storm::dd::Add<DdType, ValueType> xCopy = x;
uint_fast64_t iterationCount = 0;
bool converged = false;
while (!converged && iterationCount < maximalNumberOfIterations) {
storm::dd::Add<DdType, ValueType> xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs);
storm::dd::Add<DdType, ValueType> tmp = scaledB - scaledLu.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables);
// Now check if the process already converged within our precision.
converged = tmp.equalModuloPrecision(xCopy, precision, relative);
xCopy = tmp;
// Increase iteration count so we can abort if convergence is too slow.
++iterationCount;
}
if (converged) {
STORM_LOG_TRACE("Iterative solver converged in " << iterationCount << " iterations.");
} else {
STORM_LOG_WARN("Iterative solver did not converge in " << iterationCount << " iterations.");
}
return xCopy;
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicLinearEquationSolver<DdType, ValueType>::multiply(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const* b, uint_fast64_t n) const {
storm::dd::Add<DdType, ValueType> xCopy = x;
@ -86,5 +48,7 @@ namespace storm {
template class SymbolicLinearEquationSolver<storm::dd::DdType::CUDD, double>;
template class SymbolicLinearEquationSolver<storm::dd::DdType::Sylvan, double>;
template class SymbolicLinearEquationSolver<storm::dd::DdType::Sylvan, storm::RationalFunction>;
}
}

2
src/storm/solver/SymbolicLinearEquationSolver.h
View File

@ -63,7 +63,7 @@ namespace storm {
* @param b The right-hand side of the equation system. Its length must be equal to the number of rows of A.
* @return The solution of the equation system.
*/
virtual storm::dd::Add<DdType, ValueType> solveEquations(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
virtual storm::dd::Add<DdType, ValueType> solveEquations(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const = 0;
/*!
* Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After

68
src/storm/solver/SymbolicNativeLinearEquationSolver.cpp
View File

@ -0,0 +1,68 @@
#include "storm/solver/SymbolicNativeLinearEquationSolver.h"
#include "storm/storage/dd/DdManager.h"
#include "storm/storage/dd/Add.h"
#include "storm/utility/dd.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/NativeEquationSolverSettings.h"
namespace storm {
namespace solver {
template<storm::dd::DdType DdType, typename ValueType>
SymbolicNativeLinearEquationSolver<DdType, ValueType>::SymbolicNativeLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : SymbolicLinearEquationSolver<DdType, ValueType>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, precision, maximalNumberOfIterations, relative) {
// Intentionally left empty.
}
template<storm::dd::DdType DdType, typename ValueType>
SymbolicNativeLinearEquationSolver<DdType, ValueType>::SymbolicNativeLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) : SymbolicLinearEquationSolver<DdType, ValueType>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs) {
// Intentionally left empty.
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquations(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
// Start by computing the Jacobi decomposition of the matrix A.
storm::dd::Bdd<DdType> diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), this->rowColumnMetaVariablePairs);
diagonal &= this->allRows;
storm::dd::Add<DdType, ValueType> lu = diagonal.ite(this->A.getDdManager().template getAddZero<ValueType>(), this->A);
storm::dd::Add<DdType> diagonalAdd = diagonal.template toAdd<ValueType>();
storm::dd::Add<DdType, ValueType> diag = diagonalAdd.multiplyMatrix(this->A, this->columnMetaVariables);
storm::dd::Add<DdType, ValueType> scaledLu = lu / diag;
storm::dd::Add<DdType, ValueType> scaledB = b / diag;
// Set up additional environment variables.
storm::dd::Add<DdType, ValueType> xCopy = x;
uint_fast64_t iterationCount = 0;
bool converged = false;
while (!converged && iterationCount < this->maximalNumberOfIterations) {
storm::dd::Add<DdType, ValueType> xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs);
storm::dd::Add<DdType, ValueType> tmp = scaledB - scaledLu.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables);
// Now check if the process already converged within our precision.
converged = tmp.equalModuloPrecision(xCopy, this->precision, this->relative);
xCopy = tmp;
// Increase iteration count so we can abort if convergence is too slow.
++iterationCount;
}
if (converged) {
STORM_LOG_TRACE("Iterative solver converged in " << iterationCount << " iterations.");
} else {
STORM_LOG_WARN("Iterative solver did not converge in " << iterationCount << " iterations.");
}
return xCopy;
}
template class SymbolicNativeLinearEquationSolver<storm::dd::DdType::CUDD, double>;
template class SymbolicNativeLinearEquationSolver<storm::dd::DdType::Sylvan, double>;
}
}

58
src/storm/solver/SymbolicNativeLinearEquationSolver.h
View File

@ -0,0 +1,58 @@
#pragma once
#include "storm/solver/SymbolicLinearEquationSolver.h"
namespace storm {
namespace solver {
/*!
* An interface that represents an abstract symbolic linear equation solver. In addition to solving a system of
* linear equations, the functionality to repeatedly multiply a matrix with a given vector is provided.
*/
template<storm::dd::DdType DdType, typename ValueType = double>
class SymbolicNativeLinearEquationSolver : public SymbolicLinearEquationSolver<DdType, ValueType> {
public:
/*!
* Constructs a symbolic linear equation solver with the given meta variable sets and pairs.
*
* @param A The matrix defining the coefficients of the linear equation system.
* @param diagonal An ADD characterizing the elements on the diagonal of the matrix.
* @param allRows A BDD characterizing all rows of the equation system.
* @param rowMetaVariables The meta variables used to encode the rows of the matrix.
* @param columnMetaVariables The meta variables used to encode the columns of the matrix.
* @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta
* variables.
*/
SymbolicNativeLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
/*!
* Constructs a symbolic linear equation solver with the given meta variable sets and pairs.
*
* @param A The matrix defining the coefficients of the linear equation system.
* @param allRows A BDD characterizing all rows of the equation system.
* @param rowMetaVariables The meta variables used to encode the rows of the matrix.
* @param columnMetaVariables The meta variables used to encode the columns of the matrix.
* @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta
* variables.
* @param precision The precision to achieve.
* @param maximalNumberOfIterations The maximal number of iterations to perform when solving a linear
* equation system iteratively.
* @param relative Sets whether or not to use a relativ stopping criterion rather than an absolute one.
*/
SymbolicNativeLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative);
/*!
* Solves the equation system A*x = b. The matrix A is required to be square and have a unique solution.
* The solution of the set of linear equations will be written to the vector x. Note that the matrix A has
* to be given upon construction time of the solver object.
*
* @param x The initial guess for the solution vector. Its length must be equal to the number of rows of A.
* @param b The right-hand side of the equation system. Its length must be equal to the number of rows of A.
* @return The solution of the equation system.
*/
virtual storm::dd::Add<DdType, ValueType> solveEquations(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
};
} // namespace solver
} // namespace storm

25
src/storm/storage/dd/Add.cpp
View File

@ -219,6 +219,31 @@ namespace storm {
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.swapVariables(from, to), newContainedMetaVariables);
}
template<DdType LibraryType, typename ValueType>
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::permuteVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const {
std::set<storm::expressions::Variable> newContainedMetaVariables;
std::vector<InternalBdd<LibraryType>> from;
std::vector<InternalBdd<LibraryType>> to;
for (auto const& metaVariablePair : metaVariablePairs) {
DdMetaVariable<LibraryType> const& variable1 = this->getDdManager().getMetaVariable(metaVariablePair.first);
DdMetaVariable<LibraryType> const& variable2 = this->getDdManager().getMetaVariable(metaVariablePair.second);
// Keep track of the contained meta variables in the DD.
if (this->containsMetaVariable(metaVariablePair.first)) {
newContainedMetaVariables.insert(metaVariablePair.second);
}
for (auto const& ddVariable : variable1.getDdVariables()) {
from.push_back(ddVariable);
}
for (auto const& ddVariable : variable2.getDdVariables()) {
to.push_back(ddVariable);
}
}
STORM_LOG_THROW(from.size() == to.size(), storm::exceptions::InvalidArgumentException, "Unable to swap mismatching meta variables.");
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.permuteVariables(from, to), newContainedMetaVariables);
}
template<DdType LibraryType, typename ValueType>
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::multiplyMatrix(Add<LibraryType, ValueType> const& otherMatrix, std::set<storm::expressions::Variable> const& summationMetaVariables) const {
// Create the CUDD summation variables.

9
src/storm/storage/dd/Add.h
View File

@ -329,6 +329,15 @@ namespace storm {
*/
Add<LibraryType, ValueType> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const;
/*!
* Permutes the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have
* the same number of underlying ADD variables. The first component of the i-th entry is substituted by the second component.
*
* @param metaVariablePairs A vector of meta variable pairs that are to be permuted.
* @return The resulting ADD.
*/
Add<LibraryType, ValueType> permuteVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const;
/*!
* Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta
* variables.

18
src/storm/storage/dd/cudd/InternalCuddAdd.cpp
View File

@ -188,6 +188,24 @@ namespace storm {
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().SwapVariables(fromAdd, toAdd));
}
template<typename ValueType>
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::permuteVariables(std::vector<InternalBdd<DdType::CUDD>> const& from, std::vector<InternalBdd<DdType::CUDD>> const& to) const {
// Build the full permutation.
uint64_t numberOfVariables = ddManager->getCuddManager().ReadSize();
int* permutation = new int[numberOfVariables];
for (uint64_t variable = 0; variable < numberOfVariables; ++variable) {
permutation[variable] = variable;
}
for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) {
permutation[it1->getIndex()] = it2->getIndex();
}
InternalAdd<DdType::CUDD, ValueType> result(ddManager, this->getCuddAdd().Permute(permutation));
delete[] permutation;
return result;
}
template<typename ValueType>
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::multiplyMatrix(InternalAdd<DdType::CUDD, ValueType> const& otherMatrix, std::vector<InternalBdd<DdType::CUDD>> const& summationDdVariables) const {
// Create the CUDD summation variables.

10
src/storm/storage/dd/cudd/InternalCuddAdd.h
View File

@ -309,6 +309,16 @@ namespace storm {
*/
InternalAdd<DdType::CUDD, ValueType> swapVariables(std::vector<InternalBdd<DdType::CUDD>> const& from, std::vector<InternalBdd<DdType::CUDD>> const& to) const;
/*!
* Permutes the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by
* ADDs must have equal length.
*
* @param from The vector that specifies the 'from' part of the variable renaming.
* @param to The vector that specifies the 'to' part of the variable renaming.
* @return The resulting ADD.
*/
InternalAdd<DdType::CUDD, ValueType> permuteVariables(std::vector<InternalBdd<DdType::CUDD>> const& from, std::vector<InternalBdd<DdType::CUDD>> const& to) const;
/*!
* Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta
* variables.

11
src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
View File

@ -405,6 +405,17 @@ namespace storm {
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Permute(fromIndices, toIndices));
}
template<typename ValueType>
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::permuteVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from, std::vector<InternalBdd<DdType::Sylvan>> const& to) const {
std::vector<uint32_t> fromIndices;
std::vector<uint32_t> toIndices;
for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) {
fromIndices.push_back(it1->getIndex());
toIndices.push_back(it2->getIndex());
}
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Permute(fromIndices, toIndices));
}
template<typename ValueType>
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::multiplyMatrix(InternalAdd<DdType::Sylvan, ValueType> const& otherMatrix, std::vector<InternalBdd<DdType::Sylvan>> const& summationDdVariables) const {
InternalBdd<DdType::Sylvan> summationVariables = ddManager->getBddOne();

12
src/storm/storage/dd/sylvan/InternalSylvanAdd.h
View File

@ -327,7 +327,17 @@ namespace storm {
* @return The resulting ADD.
*/
InternalAdd<DdType::Sylvan, ValueType> swapVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from, std::vector<InternalBdd<DdType::Sylvan>> const& to) const;
/*!
* Permutes the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by
* ADDs must have equal length.
*
* @param from The vector that specifies the 'from' part of the variable renaming.
* @param to The vector that specifies the 'to' part of the variable renaming.
* @return The resulting ADD.
*/
InternalAdd<DdType::Sylvan, ValueType> permuteVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from, std::vector<InternalBdd<DdType::Sylvan>> const& to) const;
/*!
* Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta
* variables.

1
src/storm/utility/constants.h
View File

@ -70,7 +70,6 @@ namespace storm {
template<typename K, typename ValueType>
ValueType maximum(std::map<K, ValueType> const& values);
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);

7
src/storm/utility/solver.cpp
View File

@ -2,7 +2,7 @@
#include <vector>
#include "storm/solver/SymbolicLinearEquationSolver.h"
#include "storm/solver/SymbolicNativeLinearEquationSolver.h"
#include "storm/solver/SymbolicEliminationLinearEquationSolver.h"
#include "storm/solver/SymbolicMinMaxLinearEquationSolver.h"
#include "storm/solver/SymbolicGameSolver.h"
@ -25,7 +25,6 @@ namespace storm {
namespace utility {
namespace solver {
template<storm::dd::DdType Type, typename ValueType>
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<Type, ValueType>> SymbolicLinearEquationSolverFactory<Type, ValueType>::create(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const {
@ -33,8 +32,10 @@ namespace storm {
switch (equationSolver) {
case storm::solver::EquationSolverType::Elimination: return std::make_unique<storm::solver::SymbolicEliminationLinearEquationSolver<Type, ValueType>>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs);
break;
case storm::solver::EquationSolverType::Native: return std::make_unique<storm::solver::SymbolicNativeLinearEquationSolver<Type, ValueType>>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs);
default:
return std::make_unique<storm::solver::SymbolicLinearEquationSolver<Type, ValueType>>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs);
STORM_LOG_WARN("The selected equation solver is not available in the DD setting. Falling back to native solver.");
return std::make_unique<storm::solver::SymbolicNativeLinearEquationSolver<Type, ValueType>>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs);
}
}

84
src/storm/utility/storm.h
View File

@ -550,25 +550,25 @@ namespace storm {
#endif
template<storm::dd::DdType DdType>
std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant = false) {
template<storm::dd::DdType DdType, typename ValueType = double>
std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant = false) {
std::unique_ptr<storm::modelchecker::CheckResult> result;
storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> task(*formula, onlyInitialStatesRelevant);
if (model->getType() == storm::models::ModelType::Dtmc) {
std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
storm::modelchecker::HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType>> modelchecker(*dtmc);
std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType, ValueType>>();
storm::modelchecker::HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> modelchecker(*dtmc);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}
} else if (model->getType() == storm::models::ModelType::Ctmc) {
std::shared_ptr<storm::models::symbolic::Ctmc<DdType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType>>();
storm::modelchecker::HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<DdType>> modelchecker(*ctmc);
std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType, ValueType>>();
storm::modelchecker::HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<DdType, ValueType>> modelchecker(*ctmc);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}
} else if (model->getType() == storm::models::ModelType::Mdp) {
std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType>> modelchecker(*mdp);
std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType, ValueType>>();
storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> modelchecker(*mdp);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}
@ -577,20 +577,49 @@ namespace storm {
}
return result;
}
template<storm::dd::DdType DdType>
std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant) {
std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant = false) {
// std::unique_ptr<storm::modelchecker::CheckResult> result;
// storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> task(*formula, onlyInitialStatesRelevant);
// if (model->getType() == storm::models::ModelType::Dtmc) {
// std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType, ValueType>>();
// storm::modelchecker::HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> modelchecker(*dtmc);
// if (modelchecker.canHandle(task)) {
// result = modelchecker.check(task);
// }
// } else if (model->getType() == storm::models::ModelType::Ctmc) {
// std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType, ValueType>>();
// storm::modelchecker::HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<DdType, ValueType>> modelchecker(*ctmc);
// if (modelchecker.canHandle(task)) {
// result = modelchecker.check(task);
// }
// } else if (model->getType() == storm::models::ModelType::Mdp) {
// std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType, ValueType>>();
// storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> modelchecker(*mdp);
// if (modelchecker.canHandle(task)) {
// result = modelchecker.check(task);
// }
// } else {
// STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
// }
// return result;
return nullptr;
}
template<storm::dd::DdType DdType, typename ValueType = double>
std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant) {
std::unique_ptr<storm::modelchecker::CheckResult> result;
storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> task(*formula, onlyInitialStatesRelevant);
if (model->getType() == storm::models::ModelType::Dtmc) {
std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType>> modelchecker(*dtmc);
std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType, ValueType>>();
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> modelchecker(*dtmc);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}
} else if (model->getType() == storm::models::ModelType::Mdp) {
std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType>> modelchecker(*mdp);
std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType, ValueType>>();
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> modelchecker(*mdp);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}
@ -600,6 +629,29 @@ namespace storm {
return result;
}
template<storm::dd::DdType DdType>
std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant) {
// std::unique_ptr<storm::modelchecker::CheckResult> result;
// storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> task(*formula, onlyInitialStatesRelevant);
// if (model->getType() == storm::models::ModelType::Dtmc) {
// std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType, ValueType>>();
// storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> modelchecker(*dtmc);
// if (modelchecker.canHandle(task)) {
// result = modelchecker.check(task);
// }
// } else if (model->getType() == storm::models::ModelType::Mdp) {
// std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType, ValueType>>();
// storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> modelchecker(*mdp);
// if (modelchecker.canHandle(task)) {
// result = modelchecker.check(task);
// }
// } else {
// STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
// }
// return result;
return nullptr;
}
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant = false) {

Write Preview
Loading…
Cancel
Save