|
|
@ -17,7 +17,7 @@ namespace storm { |
|
|
namespace menu_games { |
|
|
namespace menu_games { |
|
|
|
|
|
|
|
|
template <storm::dd::DdType DdType, typename ValueType> |
|
|
template <storm::dd::DdType DdType, typename ValueType> |
|
|
AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared<storm::dd::DdManager<DdType>>(), initialPredicates), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, program.getAllGuards(true), *this->smtSolverFactory), currentGame(nullptr) { |
|
|
|
|
|
|
|
|
AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared<storm::dd::DdManager<DdType>>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, program.getAllGuards(true), *this->smtSolverFactory), currentGame(nullptr) { |
|
|
|
|
|
|
|
|
// For now, we assume that there is a single module. If the program has more than one module, it needs
|
|
|
// For now, we assume that there is a single module. If the program has more than one module, it needs
|
|
|
// to be flattened before the procedure.
|
|
|
// to be flattened before the procedure.
|
|
|
@ -30,7 +30,8 @@ namespace storm { |
|
|
// If we were requested to add all guards to the set of predicates, we do so now.
|
|
|
// If we were requested to add all guards to the set of predicates, we do so now.
|
|
|
for (auto const& command : module.getCommands()) { |
|
|
for (auto const& command : module.getCommands()) { |
|
|
if (addAllGuards) { |
|
|
if (addAllGuards) { |
|
|
expressionInformation.predicates.push_back(command.getGuardExpression()); |
|
|
|
|
|
|
|
|
expressionInformation.getPredicates().push_back(command.getGuardExpression()); |
|
|
|
|
|
allGuards.push_back(command.getGuardExpression()); |
|
|
} |
|
|
} |
|
|
maximalUpdateCount = std::max(maximalUpdateCount, static_cast<uint_fast64_t>(command.getNumberOfUpdates())); |
|
|
maximalUpdateCount = std::max(maximalUpdateCount, static_cast<uint_fast64_t>(command.getNumberOfUpdates())); |
|
|
} |
|
|
} |
|
|
@ -39,18 +40,28 @@ namespace storm { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
// Create DD variable for the command encoding.
|
|
|
// Create DD variable for the command encoding.
|
|
|
ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1, std::make_pair(storm::dd::MetaVariablePosition::Above, ddInformation.predicateDdVariables.front().first)).first; |
|
|
|
|
|
|
|
|
ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1).first; |
|
|
|
|
|
|
|
|
// Create DD variable for update encoding.
|
|
|
// Create DD variable for update encoding.
|
|
|
ddInformation.updateDdVariable = ddInformation.manager->addMetaVariable("update", 0, maximalUpdateCount - 1, std::make_pair(storm::dd::MetaVariablePosition::Above, ddInformation.predicateDdVariables.front().first)).first; |
|
|
|
|
|
|
|
|
ddInformation.updateDdVariable = ddInformation.manager->addMetaVariable("update", 0, maximalUpdateCount - 1).first; |
|
|
|
|
|
|
|
|
// Create DD variables encoding the nondeterministic choices of player 2.
|
|
|
// Create DD variables encoding the nondeterministic choices of player 2.
|
|
|
// NOTE: currently we assume that 100 variables suffice, which corresponds to 2^100 possible choices.
|
|
|
// NOTE: currently we assume that 100 variables suffice, which corresponds to 2^100 possible choices.
|
|
|
// If for some reason this should not be enough, we could grow this vector dynamically, but odds are
|
|
|
// If for some reason this should not be enough, we could grow this vector dynamically, but odds are
|
|
|
// that it's impossible to treat such models in any event.
|
|
|
// that it's impossible to treat such models in any event.
|
|
|
for (uint_fast64_t index = 0; index < 100; ++index) { |
|
|
for (uint_fast64_t index = 0; index < 100; ++index) { |
|
|
storm::expressions::Variable newOptionVar = ddInformation.manager->addMetaVariable("opt" + std::to_string(index), std::make_pair(storm::dd::MetaVariablePosition::Above, ddInformation.predicateDdVariables.front().first)).first; |
|
|
|
|
|
ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->template getIdentity<ValueType>(newOptionVar).toBdd())); |
|
|
|
|
|
|
|
|
storm::expressions::Variable newOptionVar = ddInformation.manager->addMetaVariable("opt" + std::to_string(index)).first; |
|
|
|
|
|
ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->getEncoding(newOptionVar, 1))); |
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
// Now that we have created all other DD variables, we create the DD variables for the predicates.
|
|
|
|
|
|
if (addAllGuards) { |
|
|
|
|
|
for (auto const& guard : allGuards) { |
|
|
|
|
|
ddInformation.addPredicate(guard); |
|
|
|
|
|
} |
|
|
|
|
|
} |
|
|
|
|
|
for (auto const& predicate : initialPredicates) { |
|
|
|
|
|
ddInformation.addPredicate(predicate); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
// For each module of the concrete program, we create an abstract counterpart.
|
|
|
// For each module of the concrete program, we create an abstract counterpart.
|
|
|
@ -70,7 +81,7 @@ namespace storm { |
|
|
STORM_LOG_THROW(!predicates.empty(), storm::exceptions::InvalidArgumentException, "Cannot refine without predicates."); |
|
|
STORM_LOG_THROW(!predicates.empty(), storm::exceptions::InvalidArgumentException, "Cannot refine without predicates."); |
|
|
|
|
|
|
|
|
// Add the predicates to the global list of predicates.
|
|
|
// Add the predicates to the global list of predicates.
|
|
|
uint_fast64_t firstNewPredicateIndex = expressionInformation.predicates.size(); |
|
|
|
|
|
|
|
|
uint_fast64_t firstNewPredicateIndex = expressionInformation.getPredicates().size(); |
|
|
expressionInformation.addPredicates(predicates); |
|
|
expressionInformation.addPredicates(predicates); |
|
|
|
|
|
|
|
|
// Create DD variables and some auxiliary data structures for the new predicates.
|
|
|
// Create DD variables and some auxiliary data structures for the new predicates.
|
|
|
@ -81,7 +92,7 @@ namespace storm { |
|
|
|
|
|
|
|
|
// Create a list of indices of the predicates, so we can refine the abstract modules and the state set abstractors.
|
|
|
// Create a list of indices of the predicates, so we can refine the abstract modules and the state set abstractors.
|
|
|
std::vector<uint_fast64_t> newPredicateIndices; |
|
|
std::vector<uint_fast64_t> newPredicateIndices; |
|
|
for (uint_fast64_t index = firstNewPredicateIndex; index < expressionInformation.predicates.size(); ++index) { |
|
|
|
|
|
|
|
|
for (uint_fast64_t index = firstNewPredicateIndex; index < expressionInformation.getPredicates().size(); ++index) { |
|
|
newPredicateIndices.push_back(index); |
|
|
newPredicateIndices.push_back(index); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
@ -110,7 +121,7 @@ namespace storm { |
|
|
storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getStates(storm::expressions::Expression const& predicate) { |
|
|
storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getStates(storm::expressions::Expression const& predicate) { |
|
|
STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); |
|
|
STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); |
|
|
uint_fast64_t index = 0; |
|
|
uint_fast64_t index = 0; |
|
|
for (auto const& knownPredicate : expressionInformation.predicates) { |
|
|
|
|
|
|
|
|
for (auto const& knownPredicate : expressionInformation.getPredicates()) { |
|
|
if (knownPredicate.areSame(predicate)) { |
|
|
if (knownPredicate.areSame(predicate)) { |
|
|
return currentGame->getReachableStates() && ddInformation.predicateBdds[index].first; |
|
|
return currentGame->getReachableStates() && ddInformation.predicateBdds[index].first; |
|
|
} |
|
|
} |
|
|
|
dehnert
9 years ago