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

refined cut-off of builders a little. Now, based on the property, more of the states are treated as terminal states of the model 

Former-commit-id: 4b68d6f1e8
main
dehnert 10 years ago
parent
7ac6dd94ab
commit
e51a3cfa85
4 changed files with 85 additions and 23 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. 36
      src/builder/DdPrismModelBuilder.cpp
  2. 8
      src/builder/DdPrismModelBuilder.h
  3. 40
      src/builder/ExplicitPrismModelBuilder.cpp
  4. 8
      src/builder/ExplicitPrismModelBuilder.h

36
src/builder/DdPrismModelBuilder.cpp
View File

@ -190,18 +190,18 @@ namespace storm {
};
template <storm::dd::DdType Type>
DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates() {
DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
// Intentionally left empty.
}
template <storm::dd::DdType Type>
DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates() {
DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
this->preserveFormula(formula);
this->setTerminalStatesFromFormula(formula);
}
template <storm::dd::DdType Type>
DdPrismModelBuilder<Type>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates() {
DdPrismModelBuilder<Type>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
this->buildAllLabels = true;
@ -221,6 +221,9 @@ namespace storm {
if (terminalStates) {
terminalStates.reset();
}
if (negatedTerminalStates) {
negatedTerminalStates.reset();
}
// If we are not required to build all reward models, we determine the reward models we need to build.
if (!buildAllRewardModels) {
@ -261,10 +264,16 @@ namespace storm {
this->setTerminalStatesFromFormula(sub);
}
} else if (formula.isUntilFormula()) {
storm::logic::Formula const& right = formula.asUntilFormula().getLeftSubformula();
storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula();
if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) {
this->setTerminalStatesFromFormula(right);
}
storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula();
if (left.isAtomicExpressionFormula()) {
negatedTerminalStates = left.asAtomicExpressionFormula().getExpression();
} else if (left.isAtomicLabelFormula()) {
negatedTerminalStates = left.asAtomicLabelFormula().getLabel();
}
} else if (formula.isProbabilityOperatorFormula()) {
storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula();
if (sub.isEventuallyFormula() || sub.isUntilFormula()) {
@ -1023,6 +1032,8 @@ namespace storm {
storm::dd::Add<Type> stateActionDd = system.stateActionDd;
// If we were asked to treat some states as terminal states, we cut away their transitions now.
if (options.terminalStates || options.negatedTerminalStates) {
storm::dd::Add<Type> terminalStatesAdd = generationInfo.manager->getAddZero();
if (options.terminalStates) {
storm::expressions::Expression terminalExpression;
if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) {
@ -1031,8 +1042,23 @@ namespace storm {
std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
terminalExpression = preparedProgram.getLabelExpression(labelName);
}
STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
storm::dd::Add<Type> terminalStatesAdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression);
terminalStatesAdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression);
}
if (options.negatedTerminalStates) {
storm::expressions::Expression nonTerminalExpression;
if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) {
nonTerminalExpression = boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
} else {
std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
nonTerminalExpression = preparedProgram.getLabelExpression(labelName);
}
STORM_LOG_TRACE("Making the states *not* satisfying " << nonTerminalExpression << " terminal.");
terminalStatesAdd |= !generationInfo.rowExpressionAdapter->translateExpression(nonTerminalExpression);
}
transitionMatrix *= !terminalStatesAdd;
}

8
src/builder/DdPrismModelBuilder.h
View File

@ -99,9 +99,13 @@ namespace storm {
// An optional set of expressions for which labels need to be built.
boost::optional<std::vector<storm::expressions::Expression>> expressionLabels;
// An optional expression or label that characterizes the terminal states of the model. If this is set,
// the outgoing transitions of these states are replaced with a self-loop.
// An optional expression or label that (a subset of) characterizes the terminal states of the model.
// If this is set, the outgoing transitions of these states are replaced with a self-loop.
boost::optional<boost::variant<storm::expressions::Expression, std::string>> terminalStates;
// An optional expression or label whose negation characterizes (a subset of) the terminal states of the
// model. If this is set, the outgoing transitions of these states are replaced with a self-loop.
boost::optional<boost::variant<storm::expressions::Expression, std::string>> negatedTerminalStates;
};
/*!

40
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -106,17 +106,17 @@ namespace storm {
}
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates() {
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
// Intentionally left empty.
}
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates() {
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
this->preserveFormula(formula);
}
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates() {
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
this->buildAllLabels = true;
@ -142,10 +142,16 @@ namespace storm {
this->setTerminalStatesFromFormula(sub);
}
} else if (formula.isUntilFormula()) {
storm::logic::Formula const& right = formula.asUntilFormula().getLeftSubformula();
storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula();
if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) {
this->setTerminalStatesFromFormula(right);
}
storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula();
if (left.isAtomicExpressionFormula()) {
negatedTerminalStates = left.asAtomicExpressionFormula().getExpression();
} else if (left.isAtomicLabelFormula()) {
negatedTerminalStates = left.asAtomicLabelFormula().getLabel();
}
} else if (formula.isProbabilityOperatorFormula()) {
storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula();
if (sub.isEventuallyFormula() || sub.isUntilFormula()) {
@ -160,6 +166,9 @@ namespace storm {
if (terminalStates) {
terminalStates.reset();
}
if (negatedTerminalStates) {
negatedTerminalStates.reset();
}
// If we are not required to build all reward models, we determine the reward models we need to build.
if (!buildAllRewardModels) {
@ -932,7 +941,8 @@ namespace storm {
rewardModelBuilders.emplace_back(deterministicModel, rewardModel.get().hasStateRewards(), rewardModel.get().hasStateActionRewards(), rewardModel.get().hasTransitionRewards());
}
// If we were asked to treat some states as terminal states, we cut away their transitions now.
// If we were asked to treat some states as terminal states, we determine an expression characterizing the
// terminal states of the model that we pass on to the matrix building routine.
boost::optional<storm::expressions::Expression> terminalExpression;
if (options.terminalStates) {
if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) {
@ -942,9 +952,27 @@ namespace storm {
terminalExpression = program.getLabelExpression(labelName);
}
}
if (options.negatedTerminalStates) {
if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) {
if (terminalExpression) {
terminalExpression = terminalExpression.get() || !boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
} else {
terminalExpression = !boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
}
} else {
std::string const& labelName = boost::get<std::string>(options.negatedTerminalStates.get());
if (terminalExpression) {
terminalExpression = terminalExpression.get() || !program.getLabelExpression(labelName);
} else {
terminalExpression = !program.getLabelExpression(labelName);
}
}
}
if (terminalExpression) {
STORM_LOG_TRACE("Making the states satisfying " << terminalExpression.get() << " terminal.");
}
modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, stateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders, terminalExpression);
modelComponents.transitionMatrix = transitionMatrixBuilder.build();
// Now finalize all reward models.

8
src/builder/ExplicitPrismModelBuilder.h
View File

@ -193,9 +193,13 @@ namespace storm {
// An optional set of expressions for which labels need to be built.
boost::optional<std::vector<storm::expressions::Expression>> expressionLabels;
// An optional expression or label that characterizes the terminal states of the model. If this is set,
// the outgoing transitions of these states are replaced with a self-loop.
// An optional expression or label that characterizes (a subset of) the terminal states of the model. If
// this is set, the outgoing transitions of these states are replaced with a self-loop.
boost::optional<boost::variant<storm::expressions::Expression, std::string>> terminalStates;
// An optional expression or label whose negation characterizes (a subset of) the terminal states of the
// model. If this is set, the outgoing transitions of these states are replaced with a self-loop.
boost::optional<boost::variant<storm::expressions::Expression, std::string>> negatedTerminalStates;
};
/*!

Write Preview
Loading…
Cancel
Save