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

Apply maximum progress assumption while building a Markov Automaton explicitly.

tempestpy_adaptions
TimQu 6 years ago
parent
b84ce33956
commit
02977da3d7
7 changed files with 95 additions and 20 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. 5
      src/storm-cli-utilities/model-handling.h
  2. 17
      src/storm/builder/BuilderOptions.cpp
  3. 12
      src/storm/builder/BuilderOptions.h
  4. 26
      src/storm/generator/JaniNextStateGenerator.cpp
  5. 4
      src/storm/generator/JaniNextStateGenerator.h
  6. 40
      src/storm/generator/PrismNextStateGenerator.cpp
  7. 7
      src/storm/generator/PrismNextStateGenerator.h

5
src/storm-cli-utilities/model-handling.h
View File

@ -232,11 +232,12 @@ namespace storm {
} else {
options.setBuildChoiceOrigins(false);
}
options.setBuildAllLabels(buildSettings.isBuildFullModelSet());
options.setBuildAllRewardModels(buildSettings.isBuildFullModelSet());
options.setAddOutOfBoundsState(buildSettings.isBuildOutOfBoundsStateSet());
if (buildSettings.isBuildFullModelSet()) {
options.clearTerminalStates();
options.setApplyMaximalProgressAssumption(false);
options.setBuildAllLabels(true);
options.setBuildAllRewardModels(true);
}
return storm::api::buildSparseModel<ValueType>(input.model.get(), options, buildSettings.isJitSet(), storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet());
}

17
src/storm/builder/BuilderOptions.cpp
View File

@ -38,13 +38,12 @@ namespace storm {
}
BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), scaleAndLiftTransitionRewards(true), explorationChecks(false), inferObservationsFromActions(false), addOverlappingGuardsLabel(false), addOutOfBoundsState(false), reservedBitsForUnboundedVariables(32), showProgress(false), showProgressDelay(0) {
BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), applyMaximalProgressAssumption(false), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), scaleAndLiftTransitionRewards(true), explorationChecks(false), inferObservationsFromActions(false), addOverlappingGuardsLabel(false), addOutOfBoundsState(false), reservedBitsForUnboundedVariables(32), showProgress(false), showProgressDelay(0) {
// Intentionally left empty.
}
BuilderOptions::BuilderOptions(storm::logic::Formula const& formula, storm::storage::SymbolicModelDescription const& modelDescription) : BuilderOptions() {
this->preserveFormula(formula, modelDescription);
this->setTerminalStatesFromFormula(formula);
BuilderOptions::BuilderOptions(storm::logic::Formula const& formula, storm::storage::SymbolicModelDescription const& modelDescription) : BuilderOptions({formula.asSharedPointer()}, modelDescription) {
// Intentionally left empty.
}
BuilderOptions::BuilderOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::SymbolicModelDescription const& modelDescription) : BuilderOptions() {
@ -59,6 +58,7 @@ namespace storm {
auto const& buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
this->setApplyMaximalProgressAssumption(modelDescription.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MA);
explorationChecks = buildSettings.isExplorationChecksSet();
reservedBitsForUnboundedVariables = buildSettings.getBitsForUnboundedVariables();
showProgress = generalSettings.isVerboseSet();
@ -145,6 +145,10 @@ namespace storm {
terminalStates.clear();
}
bool BuilderOptions::isApplyMaximalProgressAssumptionSet() const {
return applyMaximalProgressAssumption;
}
bool BuilderOptions::isBuildChoiceLabelsSet() const {
return buildChoiceLabels;
}
@ -241,6 +245,11 @@ namespace storm {
return *this;
}
BuilderOptions& BuilderOptions::setApplyMaximalProgressAssumption(bool newValue) {
applyMaximalProgressAssumption = newValue;
return *this;
}
BuilderOptions& BuilderOptions::setBuildChoiceLabels(bool newValue) {
buildChoiceLabels = newValue;
return *this;

12
src/storm/builder/BuilderOptions.h
View File

@ -103,6 +103,7 @@ namespace storm {
std::vector<std::pair<LabelOrExpression, bool>> const& getTerminalStates() const;
bool hasTerminalStates() const;
void clearTerminalStates();
bool isApplyMaximalProgressAssumptionSet() const;
bool isBuildChoiceLabelsSet() const;
bool isBuildStateValuationsSet() const;
bool isBuildChoiceOriginsSet() const;
@ -139,6 +140,13 @@ namespace storm {
BuilderOptions& addLabel(std::string const& labelName);
BuilderOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value);
BuilderOptions& addTerminalLabel(std::string const& label, bool value);
/**
* Should the maximal progress assumption be applied when building a Markov Automaton?
* @param newValue If this is true, Markovian edges are not explored from probabilistic states
* @return this
*/
BuilderOptions& setApplyMaximalProgressAssumption(bool newValue = true);
/**
* Should the choice labels be built?
* @param newValue The new value (default true)
@ -219,6 +227,10 @@ namespace storm {
/// If one of these labels/expressions evaluates to the given bool, the builder can abort the exploration.
std::vector<std::pair<LabelOrExpression, bool>> terminalStates;
/// A flag indicating whether the maximal progress assumption is applied when building a Markov Automaton.
/// If this is true, Markovian edges are not explored from probabilistic states.
bool applyMaximalProgressAssumption;
/// A flag indicating whether or not to build choice labels.
bool buildChoiceLabels;

26
src/storm/generator/JaniNextStateGenerator.cpp
View File

@ -457,7 +457,17 @@ namespace storm {
// Get all choices for the state.
result.setExpanded();
std::vector<Choice<ValueType>> allChoices = getActionChoices(locations, *this->state, stateToIdCallback);
std::vector<Choice<ValueType>> allChoices;
if (this->getOptions().isApplyMaximalProgressAssumptionSet()) {
// First explore only edges without a rate
allChoices = getActionChoices(locations, *this->state, stateToIdCallback, EdgeFilter::WithoutRate);
if (allChoices.empty()) {
// Expand the Markovian edges if there are no probabilistic ones.
allChoices = getActionChoices(locations, *this->state, stateToIdCallback, EdgeFilter::WithRate);
}
} else {
allChoices = getActionChoices(locations, *this->state, stateToIdCallback);
}
std::size_t totalNumberOfChoices = allChoices.size();
// If there is not a single choice, we return immediately, because the state has no behavior (other than
@ -800,7 +810,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) {
std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback, EdgeFilter const& edgeFilter) {
std::vector<Choice<ValueType>> result;
for (auto const& outputAndEdges : edges) {
@ -813,6 +823,12 @@ namespace storm {
auto edgesIt = nonsychingEdges.second.find(locations[automatonIndex]);
if (edgesIt != nonsychingEdges.second.end()) {
for (auto const& indexAndEdge : edgesIt->second) {
if (edgeFilter != EdgeFilter::All) {
STORM_LOG_ASSERT(edgeFilter == EdgeFilter::WithRate || edgeFilter == EdgeFilter::WithoutRate, "Unexpected edge filter.");
if ((edgeFilter == EdgeFilter::WithRate) != indexAndEdge.second->hasRate()) {
continue;
}
}
if (!this->evaluator->asBool(indexAndEdge.second->getGuard())) {
continue;
}
@ -842,6 +858,12 @@ namespace storm {
auto edgesIt = automatonAndEdges.second.find(locations[automatonIndex]);
if (edgesIt != automatonAndEdges.second.end()) {
for (auto const& indexAndEdge : edgesIt->second) {
if (edgeFilter != EdgeFilter::All) {
STORM_LOG_ASSERT(edgeFilter == EdgeFilter::WithRate || edgeFilter == EdgeFilter::WithoutRate, "Unexpected edge filter.");
if ((edgeFilter == EdgeFilter::WithRate) != indexAndEdge.second->hasRate()) {
continue;
}
}
if (!this->evaluator->asBool(indexAndEdge.second->getGuard())) {
continue;
}

4
src/storm/generator/JaniNextStateGenerator.h
View File

@ -29,6 +29,7 @@ namespace storm {
public:
typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
typedef boost::container::flat_set<uint_fast64_t> EdgeIndexSet;
enum class EdgeFilter {All, WithRate, WithoutRate};
JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options = NextStateGeneratorOptions());
@ -97,9 +98,10 @@ namespace storm {
*
* @param locations The current locations of all automata.
* @param state The state for which to retrieve the silent choices.
* @param edgeFilter Restricts the kind of edges to be considered.
* @return The action choices of the state.
*/
std::vector<Choice<ValueType>> getActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback);
std::vector<Choice<ValueType>> getActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback, EdgeFilter const& edgeFilter = EdgeFilter::All);
/*!
* Retrieves the choice generated by the given edge.

40
src/storm/generator/PrismNextStateGenerator.cpp
View File

@ -279,11 +279,26 @@ namespace storm {
// Get all choices for the state.
result.setExpanded();
std::vector<Choice<ValueType>> allChoices = getUnlabeledChoices(*this->state, stateToIdCallback);
std::vector<Choice<ValueType>> allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback);
std::vector<Choice<ValueType>> allChoices;
std::vector<Choice<ValueType>> allLabeledChoices;
if (this->getOptions().isApplyMaximalProgressAssumptionSet()) {
// First explore only edges without a rate
allChoices = getUnlabeledChoices(*this->state, stateToIdCallback, CommandFilter::Probabilistic);
allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback, CommandFilter::Probabilistic);
if (allChoices.empty() && allLabeledChoices.empty()) {
// Expand the Markovian edges if there are no probabilistic ones.
allChoices = getUnlabeledChoices(*this->state, stateToIdCallback, CommandFilter::Markovian);
allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback, CommandFilter::Markovian);
}
} else {
allChoices = getUnlabeledChoices(*this->state, stateToIdCallback);
allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback);
}
for (auto& choice : allLabeledChoices) {
allChoices.push_back(std::move(choice));
}
std::size_t totalNumberOfChoices = allChoices.size();
// If there is not a single choice, we return immediately, because the state has no behavior (other than
@ -407,7 +422,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> PrismNextStateGenerator<ValueType, StateType>::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex) {
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> PrismNextStateGenerator<ValueType, StateType>::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex, CommandFilter const& commandFilter) {
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> result((std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>()));
// Iterate over all modules.
@ -432,6 +447,12 @@ namespace storm {
// Look up commands by their indices and add them if the guard evaluates to true in the given state.
for (uint_fast64_t commandIndex : commandIndices) {
storm::prism::Command const& command = module.getCommand(commandIndex);
if (commandFilter != CommandFilter::All) {
STORM_LOG_ASSERT(commandFilter == CommandFilter::Markovian || commandFilter == CommandFilter::Probabilistic, "Unexpected command filter.");
if ((commandFilter == CommandFilter::Markovian) != command.isMarkovian()) {
continue;
}
}
if (this->evaluator->asBool(command.getGuardExpression())) {
commands.push_back(command);
}
@ -451,7 +472,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) {
std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter) {
std::vector<Choice<ValueType>> result;
// Iterate over all modules.
@ -465,6 +486,13 @@ namespace storm {
// Only consider unlabeled commands.
if (command.isLabeled()) continue;
if (commandFilter != CommandFilter::All) {
STORM_LOG_ASSERT(commandFilter == CommandFilter::Markovian || commandFilter == CommandFilter::Probabilistic, "Unexpected command filter.");
if ((commandFilter == CommandFilter::Markovian) != command.isMarkovian()) {
continue;
}
}
// Skip the command, if it is not enabled.
if (!this->evaluator->asBool(command.getGuardExpression())) {
continue;
@ -541,11 +569,11 @@ namespace storm {
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) {
std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter) {
std::vector<Choice<ValueType>> result;
for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) {
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(actionIndex);
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(actionIndex, commandFilter);
// Only process this action label, if there is at least one feasible solution.
if (optionalActiveCommandLists) {

7
src/storm/generator/PrismNextStateGenerator.h
View File

@ -22,6 +22,7 @@ namespace storm {
public:
typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
typedef boost::container::flat_set<uint_fast64_t> CommandSet;
enum class CommandFilter {All, Markovian, Probabilistic};
PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options = NextStateGeneratorOptions());
@ -75,7 +76,7 @@ namespace storm {
* @param actionIndex The index of the action label to select.
* @return A list of lists of active commands or nothing.
*/
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex);
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex, CommandFilter const& commandFilter = CommandFilter::All);
/*!
* Retrieves all unlabeled choices possible from the given state.
@ -83,7 +84,7 @@ namespace storm {
* @param state The state for which to retrieve the unlabeled choices.
* @return The unlabeled choices of the state.
*/
std::vector<Choice<ValueType>> getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
std::vector<Choice<ValueType>> getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter = CommandFilter::All);
/*!
* Retrieves all labeled choices possible from the given state.
@ -91,7 +92,7 @@ namespace storm {
* @param state The state for which to retrieve the unlabeled choices.
* @return The labeled choices of the state.
*/
std::vector<Choice<ValueType>> getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
std::vector<Choice<ValueType>> getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter = CommandFilter::All);
/*!
* A recursive helper function to generate a synchronziing distribution.

Write Preview
Loading…
Cancel
Save