Browse Source
Improved detection of terminal states for Dd engine. Also reduced code duplication.
tempestpy_adaptions
Improved detection of terminal states for Dd engine. Also reduced code duplication.
tempestpy_adaptions
Tim Quatmann
5 years ago
7 changed files with 202 additions and 195 deletions
-
56src/storm/builder/BuilderOptions.cpp
-
86src/storm/builder/DdJaniModelBuilder.cpp
-
8src/storm/builder/DdJaniModelBuilder.h
-
90src/storm/builder/DdPrismModelBuilder.cpp
-
10src/storm/builder/DdPrismModelBuilder.h
-
94src/storm/builder/TerminalStatesGetter.cpp
-
53src/storm/builder/TerminalStatesGetter.h
@ -0,0 +1,94 @@ |
|||
#include "storm/builder/TerminalStatesGetter.h"
|
|||
|
|||
#include "storm/storage/expressions/Expression.h"
|
|||
#include "storm/logic/Formulas.h"
|
|||
|
|||
namespace storm { |
|||
namespace builder { |
|||
void getTerminalStatesFromFormula(storm::logic::Formula const& formula, std::function<void(storm::expressions::Expression const&, bool)> const& terminalExpressionCallback, std::function<void(std::string const&, bool)> const& terminalLabelCallback) { |
|||
if (formula.isAtomicExpressionFormula()) { |
|||
terminalExpressionCallback(formula.asAtomicExpressionFormula().getExpression(), true); |
|||
} else if (formula.isAtomicLabelFormula()) { |
|||
terminalLabelCallback(formula.asAtomicLabelFormula().getLabel(), true); |
|||
} else if (formula.isEventuallyFormula()) { |
|||
storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); |
|||
if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { |
|||
getTerminalStatesFromFormula(sub, terminalExpressionCallback, terminalLabelCallback); |
|||
} |
|||
} else if (formula.isUntilFormula()) { |
|||
storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); |
|||
if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { |
|||
getTerminalStatesFromFormula(right, terminalExpressionCallback, terminalLabelCallback); |
|||
} |
|||
storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); |
|||
if (left.isAtomicExpressionFormula()) { |
|||
terminalExpressionCallback(left.asAtomicExpressionFormula().getExpression(), false); |
|||
} else if (left.isAtomicLabelFormula()) { |
|||
terminalLabelCallback(left.asAtomicLabelFormula().getLabel(), false); |
|||
} |
|||
} else if (formula.isBoundedUntilFormula()) { |
|||
storm::logic::BoundedUntilFormula const& boundedUntil = formula.asBoundedUntilFormula(); |
|||
bool hasLowerBound = false; |
|||
for (uint64_t i = 0; i < boundedUntil.getDimension(); ++i) { |
|||
if (boundedUntil.hasLowerBound(i) && (boundedUntil.getLowerBound(i).containsVariables() || !storm::utility::isZero(boundedUntil.getLowerBound(i).evaluateAsRational()))) { |
|||
hasLowerBound = true; |
|||
break; |
|||
} |
|||
} |
|||
if (!hasLowerBound) { |
|||
storm::logic::Formula const& right = boundedUntil.getRightSubformula(); |
|||
if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { |
|||
getTerminalStatesFromFormula(right, terminalExpressionCallback, terminalLabelCallback); |
|||
} |
|||
} |
|||
storm::logic::Formula const& left = boundedUntil.getLeftSubformula(); |
|||
if (left.isAtomicExpressionFormula()) { |
|||
terminalExpressionCallback(left.asAtomicExpressionFormula().getExpression(), false); |
|||
} else if (left.isAtomicLabelFormula()) { |
|||
terminalLabelCallback(left.asAtomicLabelFormula().getLabel(), false); |
|||
} |
|||
} else if (formula.isProbabilityOperatorFormula()) { |
|||
storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); |
|||
if (sub.isEventuallyFormula() || sub.isUntilFormula() || sub.isBoundedUntilFormula()) { |
|||
getTerminalStatesFromFormula(sub, terminalExpressionCallback, terminalLabelCallback); |
|||
} |
|||
} else if (formula.isRewardOperatorFormula() || formula.isTimeOperatorFormula()) { |
|||
storm::logic::Formula const& sub = formula.asOperatorFormula().getSubformula(); |
|||
if (sub.isEventuallyFormula()) { |
|||
getTerminalStatesFromFormula(sub, terminalExpressionCallback, terminalLabelCallback); |
|||
} |
|||
} |
|||
} |
|||
|
|||
bool TerminalStates::empty() const { |
|||
return terminalExpressions.empty() && negatedTerminalExpressions.empty() && terminalLabels.empty() && negatedTerminalLabels.empty(); |
|||
} |
|||
|
|||
storm::expressions::Expression TerminalStates::asExpression(std::function<storm::expressions::Expression(std::string const&)> const& labelToExpressionMap) const { |
|||
auto allTerminalExpressions = terminalExpressions; |
|||
for (auto const& e : negatedTerminalExpressions) { |
|||
allTerminalExpressions.push_back(!e); |
|||
} |
|||
for (auto const& l : terminalLabels) { |
|||
allTerminalExpressions.push_back(labelToExpressionMap(l)); |
|||
} |
|||
for (auto const& l : negatedTerminalLabels) { |
|||
allTerminalExpressions.push_back(!labelToExpressionMap(l)); |
|||
} |
|||
STORM_LOG_ASSERT(!allTerminalExpressions.empty(), "Unable to convert empty terminal state set to expression"); |
|||
return storm::expressions::disjunction(allTerminalExpressions); |
|||
} |
|||
|
|||
TerminalStates getTerminalStatesFromFormula(storm::logic::Formula const& formula) { |
|||
TerminalStates result; |
|||
getTerminalStatesFromFormula(formula, [&result](storm::expressions::Expression const& expr, bool inverted){ if(inverted) { result.terminalExpressions.push_back(expr);} else {result.negatedTerminalExpressions.push_back(expr);} }, |
|||
[&result](std::string const& label, bool inverted){ if(inverted) { result.terminalLabels.push_back(label);} else {result.negatedTerminalLabels.push_back(label);} }); |
|||
return result; |
|||
} |
|||
|
|||
|
|||
|
|||
|
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,53 @@ |
|||
#pragma once |
|||
|
|||
#include <functional> |
|||
#include <string> |
|||
#include <vector> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace expressions { |
|||
class Expression; |
|||
} |
|||
namespace logic { |
|||
class Formula; |
|||
} |
|||
|
|||
namespace builder { |
|||
|
|||
/*! |
|||
* Traverses the formula. If an expression (or label) is found such that checking the formula does not require further exploration from a state |
|||
* satisfying (or violating) the expression (or label), the corresponding callback function is called. |
|||
* @param formula The formula to analyzed |
|||
* @param terminalExpressionCallback called on terminal expressions. The corresponding flag indicates whether exploration can stop from states satisfying (true) or violating (false) the expression |
|||
* @param terminalLabelCallback called on terminal labels. The corresponding flag indicates whether exploration can stop from states having (true) or not having (false) the label |
|||
*/ |
|||
void getTerminalStatesFromFormula(storm::logic::Formula const& formula, std::function<void(storm::expressions::Expression const&, bool)> const& terminalExpressionCallback, std::function<void(std::string const&, bool)> const& terminalLabelCallback); |
|||
|
|||
|
|||
struct TerminalStates { |
|||
std::vector<storm::expressions::Expression> terminalExpressions; // if one of these is true, we can stop exploration |
|||
std::vector<storm::expressions::Expression> negatedTerminalExpressions; // if one of these is false, we can stop exploration |
|||
std::vector<std::string> terminalLabels; // if a state has one of these labels, we can stop exploration |
|||
std::vector<std::string> negatedTerminalLabels; // if a state does not have all of these labels, we can stop exploration |
|||
|
|||
/*! |
|||
* True if no terminal states are specified |
|||
*/ |
|||
bool empty() const; |
|||
|
|||
/*! |
|||
* Returns an expression that evaluates to true only if the exploration can stop at the corresponding state |
|||
* Should only be called if this is not empty. |
|||
*/ |
|||
storm::expressions::Expression asExpression(std::function<storm::expressions::Expression(std::string const&)> const& labelToExpressionMap) const; |
|||
}; |
|||
|
|||
/*! |
|||
* Traverses the formula. If an expression (or label) is found such that checking the formula does not require further exploration from a state |
|||
* satisfying (or violating) the expression (or label), it is inserted into the returned struct. |
|||
*/ |
|||
TerminalStates getTerminalStatesFromFormula(storm::logic::Formula const& formula); |
|||
|
|||
} |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue