diff --git a/src/logic/BinaryBooleanStateFormula.cpp b/src/logic/BinaryBooleanStateFormula.cpp
index 180ea12c1..d6757e508 100644
--- a/src/logic/BinaryBooleanStateFormula.cpp
+++ b/src/logic/BinaryBooleanStateFormula.cpp
@@ -2,10 +2,13 @@
#include "src/logic/FormulaVisitor.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
namespace storm {
namespace logic {
BinaryBooleanStateFormula::BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula) : BinaryStateFormula(leftSubformula, rightSubformula), operatorType(operatorType) {
- // Intentionally left empty.
+ STORM_LOG_THROW(this->getLeftSubformula().hasQualitativeResult() && this->getRightSubformula().hasQualitativeResult(), storm::exceptions::InvalidPropertyException, "Boolean formula must have subformulas with qualitative result.");
}
bool BinaryBooleanStateFormula::isBinaryBooleanStateFormula() const {
diff --git a/src/logic/BinaryBooleanStateFormula.h b/src/logic/BinaryBooleanStateFormula.h
index 6956e56c6..892d28bc9 100644
--- a/src/logic/BinaryBooleanStateFormula.h
+++ b/src/logic/BinaryBooleanStateFormula.h
@@ -25,7 +25,7 @@ namespace storm {
virtual bool isAnd() const;
virtual bool isOr() const;
-
+
virtual std::ostream& writeToStream(std::ostream& out) const override;
virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
diff --git a/src/logic/BinaryPathFormula.cpp b/src/logic/BinaryPathFormula.cpp
index 4e028d567..40c187013 100644
--- a/src/logic/BinaryPathFormula.cpp
+++ b/src/logic/BinaryPathFormula.cpp
@@ -32,5 +32,13 @@ namespace storm {
this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels);
this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels);
}
+
+ bool BinaryPathFormula::hasQualitativeResult() const {
+ return false;
+ }
+
+ bool BinaryPathFormula::hasQuantitativeResult() const {
+ return true;
+ }
}
}
\ No newline at end of file
diff --git a/src/logic/BinaryPathFormula.h b/src/logic/BinaryPathFormula.h
index fe0526bee..5550bd466 100644
--- a/src/logic/BinaryPathFormula.h
+++ b/src/logic/BinaryPathFormula.h
@@ -24,6 +24,9 @@ namespace storm {
virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+ virtual bool hasQualitativeResult() const override;
+ virtual bool hasQuantitativeResult() const override;
+
private:
std::shared_ptr<Formula const> leftSubformula;
std::shared_ptr<Formula const> rightSubformula;
diff --git a/src/logic/ConditionalFormula.cpp b/src/logic/ConditionalFormula.cpp
index af3e1d95b..b12b831be 100644
--- a/src/logic/ConditionalFormula.cpp
+++ b/src/logic/ConditionalFormula.cpp
@@ -49,6 +49,14 @@ namespace storm {
this->getConditionFormula().gatherReferencedRewardModels(referencedRewardModels);
}
+ bool ConditionalFormula::hasQualitativeResult() const {
+ return false;
+ }
+
+ bool ConditionalFormula::hasQuantitativeResult() const {
+ return true;
+ }
+
std::ostream& ConditionalFormula::writeToStream(std::ostream& out) const {
this->getSubformula().writeToStream(out);
out << " || ";
diff --git a/src/logic/ConditionalFormula.h b/src/logic/ConditionalFormula.h
index fc6b61655..66d71ebba 100644
--- a/src/logic/ConditionalFormula.h
+++ b/src/logic/ConditionalFormula.h
@@ -32,6 +32,9 @@ namespace storm {
virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+ virtual bool hasQualitativeResult() const override;
+ virtual bool hasQuantitativeResult() const override;
+
private:
std::shared_ptr<Formula const> subformula;
std::shared_ptr<Formula const> conditionFormula;
diff --git a/src/logic/EventuallyFormula.cpp b/src/logic/EventuallyFormula.cpp
index 71ff4ac54..56c9decff 100644
--- a/src/logic/EventuallyFormula.cpp
+++ b/src/logic/EventuallyFormula.cpp
@@ -7,10 +7,14 @@
namespace storm {
namespace logic {
EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula, FormulaContext context) : UnaryPathFormula(subformula), context(context) {
- STORM_LOG_THROW(context == FormulaContext::Probability || context == FormulaContext::Reward || context == FormulaContext::ExpectedTime, storm::exceptions::InvalidPropertyException, "Invalid context for formula.");
+ STORM_LOG_THROW(context == FormulaContext::Probability || context == FormulaContext::Reward || context == FormulaContext::Time, storm::exceptions::InvalidPropertyException, "Invalid context for formula.");
}
bool EventuallyFormula::isEventuallyFormula() const {
+ return true;
+ }
+
+ bool EventuallyFormula::isReachabilityProbabilityFormula() const {
return context == FormulaContext::Probability;
}
@@ -18,8 +22,8 @@ namespace storm {
return context == FormulaContext::Reward;
}
- bool EventuallyFormula::isReachbilityExpectedTimeFormula() const {
- return context == FormulaContext::ExpectedTime;
+ bool EventuallyFormula::isReachabilityTimeFormula() const {
+ return context == FormulaContext::Time;
}
bool EventuallyFormula::isProbabilityPathFormula() const {
@@ -30,8 +34,8 @@ namespace storm {
return this->isReachabilityRewardFormula();
}
- bool EventuallyFormula::isExpectedTimePathFormula() const {
- return this->isReachbilityExpectedTimeFormula();
+ bool EventuallyFormula::isTimePathFormula() const {
+ return this->isReachabilityTimeFormula();
}
boost::any EventuallyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
diff --git a/src/logic/EventuallyFormula.h b/src/logic/EventuallyFormula.h
index 5a0070a16..f3716fee9 100644
--- a/src/logic/EventuallyFormula.h
+++ b/src/logic/EventuallyFormula.h
@@ -15,11 +15,12 @@ namespace storm {
}
virtual bool isEventuallyFormula() const override;
+ virtual bool isReachabilityProbabilityFormula() const override;
virtual bool isReachabilityRewardFormula() const override;
- virtual bool isReachbilityExpectedTimeFormula() const override;
+ virtual bool isReachabilityTimeFormula() const override;
virtual bool isProbabilityPathFormula() const override;
virtual bool isRewardPathFormula() const override;
- virtual bool isExpectedTimePathFormula() const override;
+ virtual bool isTimePathFormula() const override;
virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
diff --git a/src/logic/ExpectedTimeOperatorFormula.cpp b/src/logic/ExpectedTimeOperatorFormula.cpp
deleted file mode 100644
index 5dc8161ae..000000000
--- a/src/logic/ExpectedTimeOperatorFormula.cpp
+++ /dev/null
@@ -1,45 +0,0 @@
-#include "src/logic/ExpectedTimeOperatorFormula.h"
-
-#include "src/logic/FormulaVisitor.h"
-
-namespace storm {
- namespace logic {
- ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::none, boost::none, subformula) {
- // Intentionally left empty.
- }
-
- ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::none, bound, subformula) {
- // Intentionally left empty.
- }
-
- ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), bound, subformula) {
- // Intentionally left empty.
- }
-
- ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), boost::none, subformula) {
- // Intentionally left empty.
- }
-
- bool ExpectedTimeOperatorFormula::isExpectedTimeOperatorFormula() const {
- return true;
- }
-
- boost::any ExpectedTimeOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
- return visitor.visit(*this, data);
- }
-
- ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula) {
- // Intentionally left empty.
- }
-
- std::shared_ptr<Formula> ExpectedTimeOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
- return std::make_shared<ExpectedTimeOperatorFormula>(this->optimalityType, this->bound, this->getSubformula().substitute(substitution));
- }
-
- std::ostream& ExpectedTimeOperatorFormula::writeToStream(std::ostream& out) const {
- out << "ET";
- OperatorFormula::writeToStream(out);
- return out;
- }
- }
-}
\ No newline at end of file
diff --git a/src/logic/ExpectedTimeOperatorFormula.h b/src/logic/ExpectedTimeOperatorFormula.h
deleted file mode 100644
index 5e1925b44..000000000
--- a/src/logic/ExpectedTimeOperatorFormula.h
+++ /dev/null
@@ -1,33 +0,0 @@
-#ifndef STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_
-#define STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_
-
-#include "src/logic/OperatorFormula.h"
-
-#include "src/logic/FormulaVisitor.h"
-
-namespace storm {
- namespace logic {
- class ExpectedTimeOperatorFormula : public OperatorFormula {
- public:
- ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula);
- ExpectedTimeOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
- ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
- ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula);
- ExpectedTimeOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
-
- virtual ~ExpectedTimeOperatorFormula() {
- // Intentionally left empty.
- }
-
- virtual bool isExpectedTimeOperatorFormula() const override;
-
- virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
-
- virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-
- virtual std::ostream& writeToStream(std::ostream& out) const override;
- };
- }
-}
-
-#endif /* STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_ */
\ No newline at end of file
diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp
index 6c7084f53..c48548f10 100644
--- a/src/logic/Formula.cpp
+++ b/src/logic/Formula.cpp
@@ -62,6 +62,10 @@ namespace storm {
return false;
}
+ bool Formula::isReachabilityProbabilityFormula() const {
+ return false;
+ }
+
bool Formula::isGloballyFormula() const {
return false;
}
@@ -90,7 +94,7 @@ namespace storm {
return false;
}
- bool Formula::isExpectedTimePathFormula() const {
+ bool Formula::isTimePathFormula() const {
return false;
}
@@ -102,7 +106,7 @@ namespace storm {
return false;
}
- bool Formula::isExpectedTimeOperatorFormula() const {
+ bool Formula::isTimeOperatorFormula() const {
return false;
}
@@ -122,7 +126,7 @@ namespace storm {
return false;
}
- bool Formula::isReachbilityExpectedTimeFormula() const {
+ bool Formula::isReachabilityTimeFormula() const {
return false;
}
@@ -138,6 +142,14 @@ namespace storm {
return false;
}
+ bool Formula::hasQualitativeResult() const {
+ return true;
+ }
+
+ bool Formula::hasQuantitativeResult() const {
+ return false;
+ }
+
bool Formula::isInFragment(FragmentSpecification const& fragment) const {
FragmentChecker checker;
return checker.conformsToSpecification(*this, fragment);
@@ -264,6 +276,22 @@ namespace storm {
return dynamic_cast<EventuallyFormula const&>(*this);
}
+ EventuallyFormula& Formula::asReachabilityProbabilityFormula() {
+ return dynamic_cast<EventuallyFormula&>(*this);
+ }
+
+ EventuallyFormula const& Formula::asReachabilityProbabilityFormula() const {
+ return dynamic_cast<EventuallyFormula const&>(*this);
+ }
+
+ EventuallyFormula& Formula::asReachabilityTimeFormula() {
+ return dynamic_cast<EventuallyFormula&>(*this);
+ }
+
+ EventuallyFormula const& Formula::asReachabilityTimeFormula() const {
+ return dynamic_cast<EventuallyFormula const&>(*this);
+ }
+
GloballyFormula& Formula::asGloballyFormula() {
return dynamic_cast<GloballyFormula&>(*this);
}
@@ -304,12 +332,12 @@ namespace storm {
return dynamic_cast<LongRunAverageOperatorFormula const&>(*this);
}
- ExpectedTimeOperatorFormula& Formula::asExpectedTimeOperatorFormula() {
- return dynamic_cast<ExpectedTimeOperatorFormula&>(*this);
+ TimeOperatorFormula& Formula::asTimeOperatorFormula() {
+ return dynamic_cast<TimeOperatorFormula&>(*this);
}
- ExpectedTimeOperatorFormula const& Formula::asExpectedTimeOperatorFormula() const {
- return dynamic_cast<ExpectedTimeOperatorFormula const&>(*this);
+ TimeOperatorFormula const& Formula::asTimeOperatorFormula() const {
+ return dynamic_cast<TimeOperatorFormula const&>(*this);
}
CumulativeRewardFormula& Formula::asCumulativeRewardFormula() {
diff --git a/src/logic/Formula.h b/src/logic/Formula.h
index 7d77de7b3..b77ecfb20 100644
--- a/src/logic/Formula.h
+++ b/src/logic/Formula.h
@@ -42,7 +42,7 @@ namespace storm {
virtual bool isProbabilityPathFormula() const;
virtual bool isRewardPathFormula() const;
- virtual bool isExpectedTimePathFormula() const;
+ virtual bool isTimePathFormula() const;
virtual bool isBinaryBooleanStateFormula() const;
virtual bool isUnaryBooleanStateFormula() const;
@@ -50,7 +50,7 @@ namespace storm {
// Operator formulas.
virtual bool isOperatorFormula() const;
virtual bool isLongRunAverageOperatorFormula() const;
- virtual bool isExpectedTimeOperatorFormula() const;
+ virtual bool isTimeOperatorFormula() const;
virtual bool isProbabilityOperatorFormula() const;
virtual bool isRewardOperatorFormula() const;
@@ -65,8 +65,9 @@ namespace storm {
virtual bool isNextFormula() const;
virtual bool isUntilFormula() const;
virtual bool isBoundedUntilFormula() const;
- virtual bool isEventuallyFormula() const;
virtual bool isGloballyFormula() const;
+ virtual bool isEventuallyFormula() const;
+ virtual bool isReachabilityProbabilityFormula() const;
// Reward formulas.
virtual bool isCumulativeRewardFormula() const;
@@ -75,7 +76,7 @@ namespace storm {
virtual bool isLongRunAverageRewardFormula() const;
// Expected time formulas.
- virtual bool isReachbilityExpectedTimeFormula() const;
+ virtual bool isReachabilityTimeFormula() const;
// Type checks for abstract intermediate classes.
virtual bool isBinaryPathFormula() const;
@@ -83,6 +84,10 @@ namespace storm {
virtual bool isUnaryPathFormula() const;
virtual bool isUnaryStateFormula() const;
+ // Accessors for the return type of a formula.
+ virtual bool hasQualitativeResult() const;
+ virtual bool hasQuantitativeResult() const;
+
bool isInFragment(FragmentSpecification const& fragment) const;
FormulaInformation info() const;
@@ -126,8 +131,14 @@ namespace storm {
EventuallyFormula& asEventuallyFormula();
EventuallyFormula const& asEventuallyFormula() const;
+ EventuallyFormula& asReachabilityProbabilityFormula();
+ EventuallyFormula const& asReachabilityProbabilityFormula() const;
+
EventuallyFormula& asReachabilityRewardFormula();
EventuallyFormula const& asReachabilityRewardFormula() const;
+
+ EventuallyFormula& asReachabilityTimeFormula();
+ EventuallyFormula const& asReachabilityTimeFormula() const;
GloballyFormula& asGloballyFormula();
GloballyFormula const& asGloballyFormula() const;
@@ -147,8 +158,8 @@ namespace storm {
LongRunAverageOperatorFormula& asLongRunAverageOperatorFormula();
LongRunAverageOperatorFormula const& asLongRunAverageOperatorFormula() const;
- ExpectedTimeOperatorFormula& asExpectedTimeOperatorFormula();
- ExpectedTimeOperatorFormula const& asExpectedTimeOperatorFormula() const;
+ TimeOperatorFormula& asTimeOperatorFormula();
+ TimeOperatorFormula const& asTimeOperatorFormula() const;
CumulativeRewardFormula& asCumulativeRewardFormula();
CumulativeRewardFormula const& asCumulativeRewardFormula() const;
diff --git a/src/logic/FormulaContext.h b/src/logic/FormulaContext.h
index 41113cb8d..70ab01a3d 100644
--- a/src/logic/FormulaContext.h
+++ b/src/logic/FormulaContext.h
@@ -4,7 +4,7 @@
namespace storm {
namespace logic {
- enum class FormulaContext { Undefined, Probability, Reward, LongRunAverage, ExpectedTime };
+ enum class FormulaContext { Undefined, Probability, Reward, LongRunAverage, Time };
}
}
diff --git a/src/logic/FormulaInformationVisitor.cpp b/src/logic/FormulaInformationVisitor.cpp
index f8ef57f92..b44045766 100644
--- a/src/logic/FormulaInformationVisitor.cpp
+++ b/src/logic/FormulaInformationVisitor.cpp
@@ -41,7 +41,7 @@ namespace storm {
return f.getSubformula().accept(*this);
}
- boost::any FormulaInformationVisitor::visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const {
+ boost::any FormulaInformationVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this);
}
diff --git a/src/logic/FormulaInformationVisitor.h b/src/logic/FormulaInformationVisitor.h
index 2e2cc0d6d..8e706cabf 100644
--- a/src/logic/FormulaInformationVisitor.h
+++ b/src/logic/FormulaInformationVisitor.h
@@ -19,7 +19,7 @@ namespace storm {
virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override;
virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
- virtual boost::any visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
diff --git a/src/logic/FormulaVisitor.h b/src/logic/FormulaVisitor.h
index a2e5b1a4f..1208b63a6 100644
--- a/src/logic/FormulaVisitor.h
+++ b/src/logic/FormulaVisitor.h
@@ -18,7 +18,7 @@ namespace storm {
virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const = 0;
- virtual boost::any visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const = 0;
+ virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const = 0;
diff --git a/src/logic/Formulas.h b/src/logic/Formulas.h
index a5218eeb8..7183dcb01 100644
--- a/src/logic/Formulas.h
+++ b/src/logic/Formulas.h
@@ -18,7 +18,7 @@
#include "src/logic/RewardOperatorFormula.h"
#include "src/logic/StateFormula.h"
#include "src/logic/LongRunAverageOperatorFormula.h"
-#include "src/logic/ExpectedTimeOperatorFormula.h"
+#include "src/logic/TimeOperatorFormula.h"
#include "src/logic/UnaryBooleanStateFormula.h"
#include "src/logic/UnaryPathFormula.h"
#include "src/logic/UnaryStateFormula.h"
diff --git a/src/logic/FormulasForwardDeclarations.h b/src/logic/FormulasForwardDeclarations.h
index 13b4c326c..43fcf0ab9 100644
--- a/src/logic/FormulasForwardDeclarations.h
+++ b/src/logic/FormulasForwardDeclarations.h
@@ -15,7 +15,7 @@ namespace storm {
class ConditionalFormula;
class CumulativeRewardFormula;
class EventuallyFormula;
- class ExpectedTimeOperatorFormula;
+ class TimeOperatorFormula;
class GloballyFormula;
class InstantaneousRewardFormula;
class LongRunAverageOperatorFormula;
diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp
index 6bf03ddb7..09bfc31dd 100644
--- a/src/logic/FragmentChecker.cpp
+++ b/src/logic/FragmentChecker.cpp
@@ -73,7 +73,7 @@ namespace storm {
}
if (inherited.getSpecification().areOnlyEventuallyFormuluasInConditionalFormulasAllowed()) {
if (f.isConditionalProbabilityFormula()) {
- result = result && f.getSubformula().isEventuallyFormula() && f.getConditionFormula().isEventuallyFormula();
+ result = result && f.getSubformula().isReachabilityProbabilityFormula() && f.getConditionFormula().isReachabilityProbabilityFormula();
} else if (f.isConditionalRewardFormula()) {
result = result && f.getSubformula().isReachabilityRewardFormula() && f.getConditionFormula().isEventuallyFormula();
}
@@ -91,26 +91,29 @@ namespace storm {
boost::any FragmentChecker::visit(EventuallyFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = true;
- if (f.isEventuallyFormula()) {
- result = inherited.getSpecification().areEventuallyFormulasAllowed();
+ if (f.isReachabilityProbabilityFormula()) {
+ result = inherited.getSpecification().areReachabilityProbabilityFormulasAllowed();
if (!inherited.getSpecification().areNestedPathFormulasAllowed()) {
result = result && !f.getSubformula().isPathFormula();
}
} else if (f.isReachabilityRewardFormula()) {
result = result && inherited.getSpecification().areReachabilityRewardFormulasAllowed();
result = result && f.getSubformula().isStateFormula();
- } else if (f.isReachbilityExpectedTimeFormula()) {
- result = result && inherited.getSpecification().areReachbilityExpectedTimeFormulasAllowed();
+ } else if (f.isReachabilityTimeFormula()) {
+ result = result && inherited.getSpecification().areReachbilityTimeFormulasAllowed();
result = result && f.getSubformula().isStateFormula();
}
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
return result;
}
- boost::any FragmentChecker::visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const {
+ boost::any FragmentChecker::visit(TimeOperatorFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
- bool result = inherited.getSpecification().areExpectedTimeOperatorsAllowed();
- result = result && f.getSubformula().isExpectedTimePathFormula();
+ bool result = inherited.getSpecification().areTimeOperatorsAllowed();
+ result = result && (!f.hasQualitativeResult() || inherited.getSpecification().areQualitativeOperatorResultsAllowed());
+ result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed());
+ result = result && f.getSubformula().isTimePathFormula();
+ result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == RewardMeasureType::Expectation);
if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
} else {
@@ -164,6 +167,8 @@ namespace storm {
boost::any FragmentChecker::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areProbabilityOperatorsAllowed();
+ result = result && (!f.hasQualitativeResult() || inherited.getSpecification().areQualitativeOperatorResultsAllowed());
+ result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed());
result = result && (f.getSubformula().isProbabilityPathFormula() || f.getSubformula().isConditionalProbabilityFormula());
if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
@@ -176,7 +181,10 @@ namespace storm {
boost::any FragmentChecker::visit(RewardOperatorFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areRewardOperatorsAllowed();
+ result = result && (!f.hasQualitativeResult() || inherited.getSpecification().areQualitativeOperatorResultsAllowed());
+ result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed());
result = result && (f.getSubformula().isRewardPathFormula() || f.getSubformula().isConditionalRewardFormula());
+ result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == RewardMeasureType::Expectation);
if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
} else {
diff --git a/src/logic/FragmentChecker.h b/src/logic/FragmentChecker.h
index 3d22390e6..9b0377aba 100644
--- a/src/logic/FragmentChecker.h
+++ b/src/logic/FragmentChecker.h
@@ -20,7 +20,7 @@ namespace storm {
virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override;
virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
- virtual boost::any visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp
index 378fe3a88..31f2eeee2 100644
--- a/src/logic/FragmentSpecification.cpp
+++ b/src/logic/FragmentSpecification.cpp
@@ -22,7 +22,7 @@ namespace storm {
pctl.setProbabilityOperatorsAllowed(true);
pctl.setGloballyFormulasAllowed(true);
- pctl.setEventuallyFormulasAllowed(true);
+ pctl.setReachabilityProbabilityFormulasAllowed(true);
pctl.setNextFormulasAllowed(true);
pctl.setUntilFormulasAllowed(true);
pctl.setBoundedUntilFormulasAllowed(true);
@@ -70,7 +70,7 @@ namespace storm {
longRunAverageOperator = false;
globallyFormula = false;
- eventuallyFormula = false;
+ reachabilityProbabilityFormula = false;
nextFormula = false;
untilFormula = false;
boundedUntilFormula = false;
@@ -89,13 +89,17 @@ namespace storm {
conditionalProbabilityFormula = false;
conditionalRewardFormula = false;
- reachabilityExpectedTimeFormula = false;
+ reachabilityTimeFormula = false;
nestedOperators = true;
nestedPathFormulas = false;
onlyEventuallyFormuluasInConditionalFormulas = true;
stepBoundedUntilFormulas = false;
timeBoundedUntilFormulas = false;
+ varianceAsMeasureType = false;
+
+ qualitativeOperatorResults = true;
+ quantitativeOperatorResults = true;
}
FragmentSpecification FragmentSpecification::copy() const {
@@ -120,11 +124,11 @@ namespace storm {
return *this;
}
- bool FragmentSpecification::areExpectedTimeOperatorsAllowed() const {
+ bool FragmentSpecification::areTimeOperatorsAllowed() const {
return expectedTimeOperator;
}
- FragmentSpecification& FragmentSpecification::setExpectedTimeOperatorsAllowed(bool newValue) {
+ FragmentSpecification& FragmentSpecification::setTimeOperatorsAllowed(bool newValue) {
this->expectedTimeOperator = newValue;
return *this;
}
@@ -147,12 +151,12 @@ namespace storm {
return *this;
}
- bool FragmentSpecification::areEventuallyFormulasAllowed() const {
- return eventuallyFormula;
+ bool FragmentSpecification::areReachabilityProbabilityFormulasAllowed() const {
+ return reachabilityProbabilityFormula;
}
- FragmentSpecification& FragmentSpecification::setEventuallyFormulasAllowed(bool newValue) {
- this->eventuallyFormula = newValue;
+ FragmentSpecification& FragmentSpecification::setReachabilityProbabilityFormulasAllowed(bool newValue) {
+ this->reachabilityProbabilityFormula = newValue;
return *this;
}
@@ -282,12 +286,12 @@ namespace storm {
return *this;
}
- bool FragmentSpecification::areReachbilityExpectedTimeFormulasAllowed() const {
- return reachabilityExpectedTimeFormula;
+ bool FragmentSpecification::areReachbilityTimeFormulasAllowed() const {
+ return reachabilityTimeFormula;
}
- FragmentSpecification& FragmentSpecification::setReachbilityExpectedTimeFormulasAllowed(bool newValue) {
- this->reachabilityExpectedTimeFormula = newValue;
+ FragmentSpecification& FragmentSpecification::setReachbilityTimeFormulasAllowed(bool newValue) {
+ this->reachabilityTimeFormula = newValue;
return *this;
}
@@ -340,13 +344,13 @@ namespace storm {
this->setProbabilityOperatorsAllowed(newValue);
this->setRewardOperatorsAllowed(newValue);
this->setLongRunAverageOperatorsAllowed(newValue);
- this->setExpectedTimeOperatorsAllowed(newValue);
+ this->setTimeOperatorsAllowed(newValue);
return *this;
}
- FragmentSpecification& FragmentSpecification::setExpectedTimeAllowed(bool newValue) {
- this->setExpectedTimeOperatorsAllowed(newValue);
- this->setReachbilityExpectedTimeFormulasAllowed(newValue);
+ FragmentSpecification& FragmentSpecification::setTimeAllowed(bool newValue) {
+ this->setTimeOperatorsAllowed(newValue);
+ this->setReachbilityTimeFormulasAllowed(newValue);
return *this;
}
@@ -355,5 +359,33 @@ namespace storm {
return *this;
}
+ bool FragmentSpecification::isVarianceMeasureTypeAllowed() const {
+ return varianceAsMeasureType;
+ }
+
+ FragmentSpecification& FragmentSpecification::setVarianceMeasureTypeAllowed(bool newValue) {
+ this->varianceAsMeasureType = newValue;
+ return *this;
+ }
+
+ bool FragmentSpecification::areQuantitativeOperatorResultsAllowed() const {
+ return this->quantitativeOperatorResults;
+ }
+
+ FragmentSpecification& FragmentSpecification::setQuantitativeOperatorResultsAllowed(bool newValue) {
+ this->quantitativeOperatorResults = newValue;
+ return *this;
+ }
+
+ bool FragmentSpecification::areQualitativeOperatorResultsAllowed() const {
+ return this->qualitativeOperatorResults;
+ }
+
+ FragmentSpecification& FragmentSpecification::setQualitativeOperatorResultsAllowed(bool newValue) {
+ this->qualitativeOperatorResults = newValue;
+ return *this;
+ }
+
+
}
}
\ No newline at end of file
diff --git a/src/logic/FragmentSpecification.h b/src/logic/FragmentSpecification.h
index 1bd46f4f7..5074187b8 100644
--- a/src/logic/FragmentSpecification.h
+++ b/src/logic/FragmentSpecification.h
@@ -19,8 +19,8 @@ namespace storm {
bool areRewardOperatorsAllowed() const;
FragmentSpecification& setRewardOperatorsAllowed(bool newValue);
- bool areExpectedTimeOperatorsAllowed() const;
- FragmentSpecification& setExpectedTimeOperatorsAllowed(bool newValue);
+ bool areTimeOperatorsAllowed() const;
+ FragmentSpecification& setTimeOperatorsAllowed(bool newValue);
bool areLongRunAverageOperatorsAllowed() const;
FragmentSpecification& setLongRunAverageOperatorsAllowed(bool newValue);
@@ -28,8 +28,8 @@ namespace storm {
bool areGloballyFormulasAllowed() const;
FragmentSpecification& setGloballyFormulasAllowed(bool newValue);
- bool areEventuallyFormulasAllowed() const;
- FragmentSpecification& setEventuallyFormulasAllowed(bool newValue);
+ bool areReachabilityProbabilityFormulasAllowed() const;
+ FragmentSpecification& setReachabilityProbabilityFormulasAllowed(bool newValue);
bool areNextFormulasAllowed() const;
FragmentSpecification& setNextFormulasAllowed(bool newValue);
@@ -73,8 +73,8 @@ namespace storm {
bool areConditionalRewardFormulasFormulasAllowed() const;
FragmentSpecification& setConditionalRewardFormulasAllowed(bool newValue);
- bool areReachbilityExpectedTimeFormulasAllowed() const;
- FragmentSpecification& setReachbilityExpectedTimeFormulasAllowed(bool newValue);
+ bool areReachbilityTimeFormulasAllowed() const;
+ FragmentSpecification& setReachbilityTimeFormulasAllowed(bool newValue);
bool areNestedOperatorsAllowed() const;
FragmentSpecification& setNestedOperatorsAllowed(bool newValue);
@@ -91,8 +91,17 @@ namespace storm {
bool areTimeBoundedUntilFormulasAllowed() const;
FragmentSpecification& setTimeBoundedUntilFormulasAllowed(bool newValue);
+ bool isVarianceMeasureTypeAllowed() const;
+ FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue);
+
+ bool areQuantitativeOperatorResultsAllowed() const;
+ FragmentSpecification& setQuantitativeOperatorResultsAllowed(bool newValue);
+
+ bool areQualitativeOperatorResultsAllowed() const;
+ FragmentSpecification& setQualitativeOperatorResultsAllowed(bool newValue);
+
FragmentSpecification& setOperatorsAllowed(bool newValue);
- FragmentSpecification& setExpectedTimeAllowed(bool newValue);
+ FragmentSpecification& setTimeAllowed(bool newValue);
FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue);
private:
@@ -103,7 +112,7 @@ namespace storm {
bool longRunAverageOperator;
bool globallyFormula;
- bool eventuallyFormula;
+ bool reachabilityProbabilityFormula;
bool nextFormula;
bool untilFormula;
bool boundedUntilFormula;
@@ -122,7 +131,7 @@ namespace storm {
bool conditionalProbabilityFormula;
bool conditionalRewardFormula;
- bool reachabilityExpectedTimeFormula;
+ bool reachabilityTimeFormula;
// Members that indicate certain restrictions.
bool nestedOperators;
@@ -130,6 +139,9 @@ namespace storm {
bool onlyEventuallyFormuluasInConditionalFormulas;
bool stepBoundedUntilFormulas;
bool timeBoundedUntilFormulas;
+ bool varianceAsMeasureType;
+ bool quantitativeOperatorResults;
+ bool qualitativeOperatorResults;
};
// Propositional.
diff --git a/src/logic/LongRunAverageOperatorFormula.cpp b/src/logic/LongRunAverageOperatorFormula.cpp
index c9d781905..f2e253ead 100644
--- a/src/logic/LongRunAverageOperatorFormula.cpp
+++ b/src/logic/LongRunAverageOperatorFormula.cpp
@@ -2,24 +2,15 @@
#include "src/logic/FormulaVisitor.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
namespace storm {
namespace logic {
- LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::none, boost::none, subformula) {
- // Intentionally left empty.
- }
-
- LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::none, bound, subformula) {
- // Intentionally left empty.
- }
-
- LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), bound, subformula) {
+ LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation) : OperatorFormula(subformula, operatorInformation) {
// Intentionally left empty.
}
- LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), boost::none, subformula) {
- // Intentionally left empty.
- }
-
bool LongRunAverageOperatorFormula::isLongRunAverageOperatorFormula() const {
return true;
}
@@ -28,12 +19,8 @@ namespace storm {
return visitor.visit(*this, data);
}
- LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula) {
- // Intentionally left empty.
- }
-
std::shared_ptr<Formula> LongRunAverageOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
- return std::make_shared<LongRunAverageOperatorFormula>(this->optimalityType, this->bound, this->getSubformula().substitute(substitution));
+ return std::make_shared<LongRunAverageOperatorFormula>(this->getSubformula().substitute(substitution), this->operatorInformation);
}
std::ostream& LongRunAverageOperatorFormula::writeToStream(std::ostream& out) const {
diff --git a/src/logic/LongRunAverageOperatorFormula.h b/src/logic/LongRunAverageOperatorFormula.h
index d4a785b80..394188b67 100644
--- a/src/logic/LongRunAverageOperatorFormula.h
+++ b/src/logic/LongRunAverageOperatorFormula.h
@@ -7,11 +7,7 @@ namespace storm {
namespace logic {
class LongRunAverageOperatorFormula : public OperatorFormula {
public:
- LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula);
- LongRunAverageOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
- LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
- LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula);
- LongRunAverageOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
+ LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation());
virtual ~LongRunAverageOperatorFormula() {
// Intentionally left empty.
diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp
index a9cdc09ae..4a8e2e215 100644
--- a/src/logic/OperatorFormula.cpp
+++ b/src/logic/OperatorFormula.cpp
@@ -2,50 +2,62 @@
namespace storm {
namespace logic {
- OperatorFormula::OperatorFormula(boost::optional<storm::solver::OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : UnaryStateFormula(subformula), bound(bound), optimalityType(optimalityType) {
+ OperatorInformation::OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection, boost::optional<Bound<double>> const& bound) : optimalityType(optimizationDirection), bound(bound) {
+ // Intentionally left empty.
+ }
+
+ OperatorFormula::OperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation) : UnaryStateFormula(subformula), operatorInformation(operatorInformation) {
// Intentionally left empty.
}
bool OperatorFormula::hasBound() const {
- return static_cast<bool>(bound);
+ return static_cast<bool>(operatorInformation.bound);
}
ComparisonType OperatorFormula::getComparisonType() const {
- return bound.get().comparisonType;
+ return operatorInformation.bound.get().comparisonType;
}
void OperatorFormula::setComparisonType(ComparisonType newComparisonType) {
- bound.get().comparisonType = newComparisonType;
+ operatorInformation.bound.get().comparisonType = newComparisonType;
}
double OperatorFormula::getThreshold() const {
- return bound.get().threshold;
+ return operatorInformation.bound.get().threshold;
}
void OperatorFormula::setThreshold(double newThreshold) {
- bound.get().threshold = newThreshold;
+ operatorInformation.bound.get().threshold = newThreshold;
}
Bound<double> const& OperatorFormula::getBound() const {
- return bound.get();
+ return operatorInformation.bound.get();
}
void OperatorFormula::setBound(Bound<double> const& newBound) {
- bound = newBound;
+ operatorInformation.bound = newBound;
}
bool OperatorFormula::hasOptimalityType() const {
- return static_cast<bool>(optimalityType);
+ return static_cast<bool>(operatorInformation.optimalityType);
}
OptimizationDirection const& OperatorFormula::getOptimalityType() const {
- return optimalityType.get();
+ return operatorInformation.optimalityType.get();
}
bool OperatorFormula::isOperatorFormula() const {
return true;
}
+ bool OperatorFormula::hasQualitativeResult() const {
+ return this->hasBound();
+ }
+
+ bool OperatorFormula::hasQuantitativeResult() const {
+ return !this->hasBound();
+ }
+
std::ostream& OperatorFormula::writeToStream(std::ostream& out) const {
if (hasOptimalityType()) {
out << (getOptimalityType() == OptimizationDirection::Minimize ? "min" : "max");
diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h
index 7660799a4..447647b99 100644
--- a/src/logic/OperatorFormula.h
+++ b/src/logic/OperatorFormula.h
@@ -8,15 +8,23 @@
#include "src/solver/OptimizationDirection.h"
namespace storm {
- namespace logic {
+ namespace logic {
+ struct OperatorInformation {
+ OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection = boost::none, boost::optional<Bound<double>> const& bound = boost::none);
+
+ boost::optional<storm::solver::OptimizationDirection> optimalityType;
+ boost::optional<Bound<double>> bound;
+ };
+
class OperatorFormula : public UnaryStateFormula {
public:
- OperatorFormula(boost::optional<storm::solver::OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
+ OperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation());
virtual ~OperatorFormula() {
// Intentionally left empty.
}
-
+
+ // Bound-related accessors.
bool hasBound() const;
ComparisonType getComparisonType() const;
void setComparisonType(ComparisonType newComparisonType);
@@ -24,16 +32,19 @@ namespace storm {
void setThreshold(double newThreshold);
Bound<double> const& getBound() const;
void setBound(Bound<double> const& newBound);
+
+ // Optimality-type-related accessors.
bool hasOptimalityType() const;
storm::solver::OptimizationDirection const& getOptimalityType() const;
virtual bool isOperatorFormula() const override;
+
+ virtual bool hasQualitativeResult() const override;
+ virtual bool hasQuantitativeResult() const override;
virtual std::ostream& writeToStream(std::ostream& out) const override;
protected:
- std::string operatorSymbol;
- boost::optional<Bound<double>> bound;
- boost::optional<storm::solver::OptimizationDirection> optimalityType;
+ OperatorInformation operatorInformation;
};
}
}
diff --git a/src/logic/ProbabilityOperatorFormula.cpp b/src/logic/ProbabilityOperatorFormula.cpp
index 09680cbc5..84d6c55d8 100644
--- a/src/logic/ProbabilityOperatorFormula.cpp
+++ b/src/logic/ProbabilityOperatorFormula.cpp
@@ -2,21 +2,12 @@
#include "src/logic/FormulaVisitor.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
namespace storm {
namespace logic {
- ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr<Formula const> const& subformula) : ProbabilityOperatorFormula(boost::none, boost::none, subformula) {
- // Intentionally left empty.
- }
-
- ProbabilityOperatorFormula::ProbabilityOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : ProbabilityOperatorFormula(boost::none, bound, subformula) {
- // Intentionally left empty.
- }
-
- ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : ProbabilityOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), bound, subformula) {
- // Intentionally left empty.
- }
-
- ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula) : ProbabilityOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), boost::none, subformula) {
+ ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation) : OperatorFormula(subformula, operatorInformation) {
// Intentionally left empty.
}
@@ -27,13 +18,9 @@ namespace storm {
boost::any ProbabilityOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
return visitor.visit(*this, data);
}
-
- ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula) {
- // Intentionally left empty.
- }
std::shared_ptr<Formula> ProbabilityOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
- return std::make_shared<ProbabilityOperatorFormula>(this->optimalityType, this->bound, this->getSubformula().substitute(substitution));
+ return std::make_shared<ProbabilityOperatorFormula>(this->getSubformula().substitute(substitution), this->operatorInformation);
}
std::ostream& ProbabilityOperatorFormula::writeToStream(std::ostream& out) const {
diff --git a/src/logic/ProbabilityOperatorFormula.h b/src/logic/ProbabilityOperatorFormula.h
index 1172247d0..786d58b44 100644
--- a/src/logic/ProbabilityOperatorFormula.h
+++ b/src/logic/ProbabilityOperatorFormula.h
@@ -7,11 +7,7 @@ namespace storm {
namespace logic {
class ProbabilityOperatorFormula : public OperatorFormula {
public:
- ProbabilityOperatorFormula(std::shared_ptr<Formula const> const& subformula);
- ProbabilityOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
- ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
- ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula);
- ProbabilityOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
+ ProbabilityOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation());
virtual ~ProbabilityOperatorFormula() {
// Intentionally left empty.
diff --git a/src/logic/RewardMeasureType.cpp b/src/logic/RewardMeasureType.cpp
new file mode 100644
index 000000000..37098d550
--- /dev/null
+++ b/src/logic/RewardMeasureType.cpp
@@ -0,0 +1,19 @@
+#include "src/logic/RewardMeasureType.h"
+
+namespace storm {
+ namespace logic {
+
+ std::ostream& operator<<(std::ostream& out, RewardMeasureType const& type) {
+ switch (type) {
+ case RewardMeasureType::Expectation:
+ out << "exp";
+ break;
+ case RewardMeasureType::Variance:
+ out << "var";
+ break;
+ }
+ return out;
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/logic/RewardMeasureType.h b/src/logic/RewardMeasureType.h
new file mode 100644
index 000000000..a48697855
--- /dev/null
+++ b/src/logic/RewardMeasureType.h
@@ -0,0 +1,16 @@
+#ifndef STORM_LOGIC_REWARDMEASURETYPE_H_
+#define STORM_LOGIC_REWARDMEASURETYPE_H_
+
+#include <iostream>
+
+namespace storm {
+ namespace logic {
+
+ enum class RewardMeasureType { Expectation, Variance };
+
+ std::ostream& operator<<(std::ostream& out, RewardMeasureType const& type);
+
+ }
+}
+
+#endif /* STORM_LOGIC_REWARDMEASURETYPE_H_ */
\ No newline at end of file
diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp
index 711f78789..5daea4b59 100644
--- a/src/logic/RewardOperatorFormula.cpp
+++ b/src/logic/RewardOperatorFormula.cpp
@@ -2,21 +2,12 @@
#include "src/logic/FormulaVisitor.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
namespace storm {
namespace logic {
- RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::shared_ptr<Formula const> const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, boost::none, subformula) {
- // Intentionally left empty.
- }
-
- RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, bound, subformula) {
- // Intentionally left empty.
- }
-
- RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional<OptimizationDirection>(optimalityType), bound, subformula) {
- // Intentionally left empty.
- }
-
- RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional<OptimizationDirection>(optimalityType), boost::none, subformula) {
+ RewardOperatorFormula::RewardOperatorFormula(std::shared_ptr<Formula const> const& subformula, boost::optional<std::string> const& rewardModelName, OperatorInformation const& operatorInformation, RewardMeasureType rewardMeasureType) : OperatorFormula(subformula, operatorInformation), rewardModelName(rewardModelName), rewardMeasureType(rewardMeasureType) {
// Intentionally left empty.
}
@@ -49,16 +40,17 @@ namespace storm {
this->getSubformula().gatherReferencedRewardModels(referencedRewardModels);
}
- RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula), rewardModelName(rewardModelName) {
- // Intentionally left empty.
+ std::shared_ptr<Formula> RewardOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<RewardOperatorFormula>(this->getSubformula().substitute(substitution), this->rewardModelName, this->operatorInformation, this->rewardMeasureType);
}
- std::shared_ptr<Formula> RewardOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
- return std::make_shared<RewardOperatorFormula>(this->rewardModelName, this->optimalityType, this->bound, this->getSubformula().substitute(substitution));
+ RewardMeasureType RewardOperatorFormula::getMeasureType() const {
+ return rewardMeasureType;
}
std::ostream& RewardOperatorFormula::writeToStream(std::ostream& out) const {
out << "R";
+ out << "[" << rewardMeasureType << "]";
if (this->hasRewardModelName()) {
out << "{\"" << this->getRewardModelName() << "\"}";
}
diff --git a/src/logic/RewardOperatorFormula.h b/src/logic/RewardOperatorFormula.h
index 6bcf015d8..300a82e37 100644
--- a/src/logic/RewardOperatorFormula.h
+++ b/src/logic/RewardOperatorFormula.h
@@ -1,18 +1,14 @@
#ifndef STORM_LOGIC_REWARDOPERATORFORMULA_H_
#define STORM_LOGIC_REWARDOPERATORFORMULA_H_
-#include <set>
#include "src/logic/OperatorFormula.h"
+#include "src/logic/RewardMeasureType.h"
namespace storm {
namespace logic {
class RewardOperatorFormula : public OperatorFormula {
public:
- RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::shared_ptr<Formula const> const& subformula);
- RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
- RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
- RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula);
- RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
+ RewardOperatorFormula(std::shared_ptr<Formula const> const& subformula, boost::optional<std::string> const& rewardModelName = boost::none, OperatorInformation const& operatorInformation = OperatorInformation(), RewardMeasureType rewardMeasureType = RewardMeasureType::Expectation);
virtual ~RewardOperatorFormula() {
// Intentionally left empty.
@@ -48,11 +44,21 @@ namespace storm {
*/
std::string const& getRewardModelName() const;
+ /*!
+ * Retrieves the measure type of the operator.
+ *
+ * @return The measure type.
+ */
+ RewardMeasureType getMeasureType() const;
+
virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
private:
// The (optional) name of the reward model this property refers to.
boost::optional<std::string> rewardModelName;
+
+ // The measure type of the operator.
+ RewardMeasureType rewardMeasureType;
};
}
}
diff --git a/src/logic/TimeOperatorFormula.cpp b/src/logic/TimeOperatorFormula.cpp
new file mode 100644
index 000000000..6a421a1a5
--- /dev/null
+++ b/src/logic/TimeOperatorFormula.cpp
@@ -0,0 +1,37 @@
+#include "src/logic/TimeOperatorFormula.h"
+
+#include "src/logic/FormulaVisitor.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+ namespace logic {
+ TimeOperatorFormula::TimeOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation, RewardMeasureType rewardMeasureType) : OperatorFormula(subformula, operatorInformation), rewardMeasureType(rewardMeasureType) {
+ // Intentionally left empty.
+ }
+
+ bool TimeOperatorFormula::isTimeOperatorFormula() const {
+ return true;
+ }
+
+ boost::any TimeOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+ return visitor.visit(*this, data);
+ }
+
+ std::shared_ptr<Formula> TimeOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<TimeOperatorFormula>(this->getSubformula().substitute(substitution), this->operatorInformation, this->rewardMeasureType);
+ }
+
+ RewardMeasureType TimeOperatorFormula::getMeasureType() const {
+ return rewardMeasureType;
+ }
+
+ std::ostream& TimeOperatorFormula::writeToStream(std::ostream& out) const {
+ out << "T";
+ out << "[" << rewardMeasureType << "]";
+ OperatorFormula::writeToStream(out);
+ return out;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/logic/TimeOperatorFormula.h b/src/logic/TimeOperatorFormula.h
new file mode 100644
index 000000000..b9f243a4c
--- /dev/null
+++ b/src/logic/TimeOperatorFormula.h
@@ -0,0 +1,40 @@
+#ifndef STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_
+#define STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_
+
+#include "src/logic/OperatorFormula.h"
+#include "src/logic/FormulaVisitor.h"
+#include "src/logic/RewardMeasureType.h"
+
+namespace storm {
+ namespace logic {
+ class TimeOperatorFormula : public OperatorFormula {
+ public:
+ TimeOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation(), RewardMeasureType rewardMeasureType = RewardMeasureType::Expectation);
+
+ virtual ~TimeOperatorFormula() {
+ // Intentionally left empty.
+ }
+
+ virtual bool isTimeOperatorFormula() const override;
+
+ virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
+ virtual std::ostream& writeToStream(std::ostream& out) const override;
+
+ /*!
+ * Retrieves the measure type of the operator.
+ *
+ * @return The measure type of the operator.
+ */
+ RewardMeasureType getMeasureType() const;
+
+ private:
+ // The measure type of the operator.
+ RewardMeasureType rewardMeasureType;
+ };
+ }
+}
+
+#endif /* STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_ */
\ No newline at end of file
diff --git a/src/logic/UnaryBooleanStateFormula.cpp b/src/logic/UnaryBooleanStateFormula.cpp
index 6d4f9ecdd..3983e5b27 100644
--- a/src/logic/UnaryBooleanStateFormula.cpp
+++ b/src/logic/UnaryBooleanStateFormula.cpp
@@ -2,10 +2,13 @@
#include "src/logic/FormulaVisitor.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
namespace storm {
namespace logic {
UnaryBooleanStateFormula::UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& subformula) : UnaryStateFormula(subformula), operatorType(operatorType) {
- // Intentionally left empty.
+ STORM_LOG_THROW(this->getSubformula().hasQualitativeResult(), storm::exceptions::InvalidPropertyException, "Boolean formula must have subformulas with qualitative result.");
}
bool UnaryBooleanStateFormula::isUnaryBooleanStateFormula() const {
diff --git a/src/logic/UnaryPathFormula.cpp b/src/logic/UnaryPathFormula.cpp
index 3e0cdaebc..415fb4d4c 100644
--- a/src/logic/UnaryPathFormula.cpp
+++ b/src/logic/UnaryPathFormula.cpp
@@ -25,5 +25,14 @@ namespace storm {
void UnaryPathFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
this->getSubformula().gatherReferencedRewardModels(referencedRewardModels);
}
+
+ bool UnaryPathFormula::hasQualitativeResult() const {
+ return false;
+ }
+
+ bool UnaryPathFormula::hasQuantitativeResult() const {
+ return true;
+ }
+
}
}
\ No newline at end of file
diff --git a/src/logic/UnaryPathFormula.h b/src/logic/UnaryPathFormula.h
index 3ea27d8f5..bc698338c 100644
--- a/src/logic/UnaryPathFormula.h
+++ b/src/logic/UnaryPathFormula.h
@@ -23,6 +23,9 @@ namespace storm {
virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+ virtual bool hasQualitativeResult() const override;
+ virtual bool hasQuantitativeResult() const override;
+
private:
std::shared_ptr<Formula const> subformula;
};
diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp
index ebd760d2e..0ad70fd4b 100644
--- a/src/modelchecker/AbstractModelChecker.cpp
+++ b/src/modelchecker/AbstractModelChecker.cpp
@@ -16,16 +16,6 @@ namespace storm {
STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'.");
if (formula.isStateFormula()) {
return this->checkStateFormula(checkTask.substituteFormula(formula.asStateFormula()));
- } else if (formula.isPathFormula()) {
- if (formula.isProbabilityPathFormula()) {
- return this->computeProbabilities(checkTask);
- } else if (formula.isRewardPathFormula()) {
- return this->computeRewards(checkTask);
- }
- } else if (formula.isConditionalProbabilityFormula()) {
- return this->computeConditionalProbabilities(checkTask.substituteFormula(formula.asConditionalFormula()));
- } else if (formula.isConditionalRewardFormula()) {
- return this->computeConditionalRewards(checkTask.substituteFormula(formula.asConditionalFormula()));
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
}
@@ -34,8 +24,8 @@ namespace storm {
storm::logic::Formula const& formula = checkTask.getFormula();
if (formula.isBoundedUntilFormula()) {
return this->computeBoundedUntilProbabilities(checkTask.substituteFormula(formula.asBoundedUntilFormula()));
- } else if (formula.isEventuallyFormula()) {
- return this->computeEventuallyProbabilities(checkTask.substituteFormula(formula.asEventuallyFormula()));
+ } else if (formula.isReachabilityProbabilityFormula()) {
+ return this->computeReachabilityProbabilities(checkTask.substituteFormula(formula.asReachabilityProbabilityFormula()));
} else if (formula.isGloballyFormula()) {
return this->computeGloballyProbabilities(checkTask.substituteFormula(formula.asGloballyFormula()));
} else if (formula.isUntilFormula()) {
@@ -56,7 +46,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
- std::unique_ptr<CheckResult> AbstractModelChecker::computeEventuallyProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula();
storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer());
return this->computeUntilProbabilities(checkTask.substituteFormula(newFormula));
@@ -74,39 +64,39 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
- std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(CheckTask<storm::logic::Formula> const& checkTask) {
+ std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula> const& checkTask) {
storm::logic::Formula const& rewardFormula = checkTask.getFormula();
if (rewardFormula.isCumulativeRewardFormula()) {
- return this->computeCumulativeRewards(checkTask.substituteFormula(rewardFormula.asCumulativeRewardFormula()));
+ return this->computeCumulativeRewards(rewardMeasureType, checkTask.substituteFormula(rewardFormula.asCumulativeRewardFormula()));
} else if (rewardFormula.isInstantaneousRewardFormula()) {
- return this->computeInstantaneousRewards(checkTask.substituteFormula(rewardFormula.asInstantaneousRewardFormula()));
+ return this->computeInstantaneousRewards(rewardMeasureType, checkTask.substituteFormula(rewardFormula.asInstantaneousRewardFormula()));
} else if (rewardFormula.isReachabilityRewardFormula()) {
- return this->computeReachabilityRewards(checkTask.substituteFormula(rewardFormula.asEventuallyFormula()));
+ return this->computeReachabilityRewards(rewardMeasureType, checkTask.substituteFormula(rewardFormula.asReachabilityRewardFormula()));
} else if (rewardFormula.isLongRunAverageRewardFormula()) {
- return this->computeLongRunAverageRewards(checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula()));
+ return this->computeLongRunAverageRewards(rewardMeasureType, checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula()));
} else if (rewardFormula.isConditionalRewardFormula()) {
- return this->computeConditionalRewards(checkTask.substituteFormula(rewardFormula.asConditionalFormula()));
+ return this->computeConditionalRewards(rewardMeasureType, checkTask.substituteFormula(rewardFormula.asConditionalFormula()));
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardFormula << "' is invalid.");
}
- std::unique_ptr<CheckResult> AbstractModelChecker::computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> AbstractModelChecker::computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
- std::unique_ptr<CheckResult> AbstractModelChecker::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> AbstractModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
- std::unique_ptr<CheckResult> AbstractModelChecker::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> AbstractModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
- std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
- std::unique_ptr<CheckResult> AbstractModelChecker::computeLongRunAverageRewards(CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> AbstractModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
@@ -114,7 +104,15 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
- std::unique_ptr<CheckResult> AbstractModelChecker::computeExpectedTimes(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> AbstractModelChecker::computeTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula> const& checkTask) {
+ storm::logic::Formula const& timeFormula = checkTask.getFormula();
+ if (timeFormula.isReachabilityTimeFormula()) {
+ return this->computeReachabilityTimes(rewardMeasureType, checkTask.substituteFormula(timeFormula.asReachabilityTimeFormula()));
+ }
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
+ }
+
+ std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
@@ -130,8 +128,8 @@ namespace storm {
return this->checkProbabilityOperatorFormula(checkTask.substituteFormula(stateFormula.asProbabilityOperatorFormula()));
} else if (stateFormula.isRewardOperatorFormula()) {
return this->checkRewardOperatorFormula(checkTask.substituteFormula(stateFormula.asRewardOperatorFormula()));
- } else if (stateFormula.isExpectedTimeOperatorFormula()) {
- return this->checkExpectedTimeOperatorFormula(checkTask.substituteFormula(stateFormula.asExpectedTimeOperatorFormula()));
+ } else if (stateFormula.isTimeOperatorFormula()) {
+ return this->checkTimeOperatorFormula(checkTask.substituteFormula(stateFormula.asTimeOperatorFormula()));
} else if (stateFormula.isLongRunAverageOperatorFormula()) {
return this->checkLongRunAverageOperatorFormula(checkTask.substituteFormula(stateFormula.asLongRunAverageOperatorFormula()));
} else if (stateFormula.isAtomicExpressionFormula()) {
@@ -193,7 +191,7 @@ namespace storm {
std::unique_ptr<CheckResult> AbstractModelChecker::checkRewardOperatorFormula(CheckTask<storm::logic::RewardOperatorFormula> const& checkTask) {
storm::logic::RewardOperatorFormula const& stateFormula = checkTask.getFormula();
- std::unique_ptr<CheckResult> result = this->computeRewards(checkTask.substituteFormula(stateFormula.getSubformula()));
+ std::unique_ptr<CheckResult> result = this->computeRewards(stateFormula.getMeasureType(), checkTask.substituteFormula(stateFormula.getSubformula()));
if (checkTask.isBoundSet()) {
STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
@@ -203,11 +201,11 @@ namespace storm {
}
}
- std::unique_ptr<CheckResult> AbstractModelChecker::checkExpectedTimeOperatorFormula(CheckTask<storm::logic::ExpectedTimeOperatorFormula> const& checkTask) {
- storm::logic::ExpectedTimeOperatorFormula const& stateFormula = checkTask.getFormula();
- STORM_LOG_THROW(stateFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
+ std::unique_ptr<CheckResult> AbstractModelChecker::checkTimeOperatorFormula(CheckTask<storm::logic::TimeOperatorFormula> const& checkTask) {
+ storm::logic::TimeOperatorFormula const& stateFormula = checkTask.getFormula();
+ STORM_LOG_THROW(stateFormula.getSubformula().isReachabilityTimeFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
- std::unique_ptr<CheckResult> result = this->computeExpectedTimes(checkTask.substituteFormula(stateFormula.getSubformula().asEventuallyFormula()));
+ std::unique_ptr<CheckResult> result = this->computeTimes(stateFormula.getMeasureType(), checkTask.substituteFormula(stateFormula.getSubformula()));
if (checkTask.isBoundSet()) {
STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h
index 90562659b..b6f009197 100644
--- a/src/modelchecker/AbstractModelChecker.h
+++ b/src/modelchecker/AbstractModelChecker.h
@@ -11,6 +11,8 @@ namespace storm {
namespace modelchecker {
class CheckResult;
+ enum class RewardType { Expectation, Variance };
+
class AbstractModelChecker {
public:
virtual ~AbstractModelChecker() {
@@ -38,22 +40,23 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeProbabilities(CheckTask<storm::logic::Formula> const& checkTask);
virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask);
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask);
- virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
+ virtual std::unique_ptr<CheckResult> computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask);
virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask);
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask);
// The methods to compute the rewards for path formulas.
- virtual std::unique_ptr<CheckResult> computeRewards(CheckTask<storm::logic::Formula> const& checkTask);
- virtual std::unique_ptr<CheckResult> computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask);
- virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask);
- virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask);
- virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
- virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask);
+ virtual std::unique_ptr<CheckResult> computeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula> const& checkTask);
+ virtual std::unique_ptr<CheckResult> computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula> const& checkTask);
+ virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask);
+ virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask);
+ virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask);
+ virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask);
- // The methods to compute the long-run average and expected time.
+ // The methods to compute the long-run average probabilities and timing measures.
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask);
- virtual std::unique_ptr<CheckResult> computeExpectedTimes(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
+ virtual std::unique_ptr<CheckResult> computeTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula> const& checkTask);
+ virtual std::unique_ptr<CheckResult> computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask);
// The methods to check state formulas.
virtual std::unique_ptr<CheckResult> checkStateFormula(CheckTask<storm::logic::StateFormula> const& stateFormula);
@@ -63,7 +66,7 @@ namespace storm {
virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(CheckTask<storm::logic::BooleanLiteralFormula> const& checkTask);
virtual std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(CheckTask<storm::logic::ProbabilityOperatorFormula> const& checkTask);
virtual std::unique_ptr<CheckResult> checkRewardOperatorFormula(CheckTask<storm::logic::RewardOperatorFormula> const& checkTask);
- virtual std::unique_ptr<CheckResult> checkExpectedTimeOperatorFormula(CheckTask<storm::logic::ExpectedTimeOperatorFormula> const& checkTask);
+ virtual std::unique_ptr<CheckResult> checkTimeOperatorFormula(CheckTask<storm::logic::TimeOperatorFormula> const& checkTask);
virtual std::unique_ptr<CheckResult> checkLongRunAverageOperatorFormula(CheckTask<storm::logic::LongRunAverageOperatorFormula> const& checkTask);
virtual std::unique_ptr<CheckResult> checkUnaryBooleanStateFormula(CheckTask<storm::logic::UnaryBooleanStateFormula> const& checkTask);
};
diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
index a08d7a6b1..81bbbd00e 100644
--- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
+++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
@@ -56,7 +56,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, class ValueType>
- std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
@@ -85,13 +85,13 @@ namespace storm {
}
template<storm::dd::DdType DdType, class ValueType>
- std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
return storm::modelchecker::helper::HybridCtmcCslHelper<DdType, ValueType>::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory);
}
template<storm::dd::DdType DdType, class ValueType>
- std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
return storm::modelchecker::helper::HybridCtmcCslHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory);
}
diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/modelchecker/csl/HybridCtmcCslModelChecker.h
index d1e26bcb2..5bfe49405 100644
--- a/src/modelchecker/csl/HybridCtmcCslModelChecker.h
+++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.h
@@ -21,9 +21,9 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
protected:
diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
index ee545cb27..7a85682df 100644
--- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
+++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
@@ -79,21 +79,21 @@ namespace storm {
}
template <typename SparseCtmcModelType>
- std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper<ValueType>::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template <typename SparseCtmcModelType>
- std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper<ValueType>::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template <typename SparseCtmcModelType>
- std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h
index 8def83dc7..f6cee6ae4 100644
--- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h
+++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h
@@ -24,9 +24,9 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
private:
diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
index 9892eb530..77535cdbe 100644
--- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
+++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
@@ -33,7 +33,7 @@ namespace storm {
bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula();
storm::logic::FragmentSpecification fragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setReachabilityRewardFormulasAllowed(true);
- fragment.setExpectedTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true);
+ fragment.setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true);
return formula.isInFragment(fragment);
}
@@ -63,7 +63,7 @@ namespace storm {
}
template<typename SparseMarkovAutomatonModelType>
- std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton.");
@@ -88,14 +88,14 @@ namespace storm {
}
template<typename SparseMarkovAutomatonModelType>
- std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeExpectedTimes(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute expected times in non-closed Markov automaton.");
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult();
- std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeExpectedTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory);
+ std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(result)));
}
diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
index 4e4f60850..8509d5f17 100644
--- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
+++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
@@ -23,9 +23,9 @@ namespace storm {
virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeExpectedTimes(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
private:
// An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices.
diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index d926917a5..c03b01871 100644
--- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -349,7 +349,7 @@ namespace storm {
}
template <typename ValueType>
- std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeExpectedTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
+ std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount();
std::vector<ValueType> rewardValues(numberOfStates, storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues(rewardValues, markovianStates, storm::utility::one<ValueType>());
diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h
index 5b24fe569..534f1d272 100644
--- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h
+++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h
@@ -24,7 +24,7 @@ namespace storm {
static std::vector<ValueType> computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
- static std::vector<ValueType> computeExpectedTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
+ static std::vector<ValueType> computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
private:
static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
index 31628f4ed..4f8c38285 100644
--- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
@@ -79,21 +79,21 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound.");
return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory);
}
template<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound.");
return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory);
}
template<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
index b723ea699..3489e74e8 100644
--- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
+++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
@@ -22,9 +22,9 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
protected:
diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
index f79bbb933..4d4d8f400 100644
--- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
@@ -77,7 +77,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
@@ -85,7 +85,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
@@ -93,7 +93,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h
index ec3ef2955..3fa7f3d13 100644
--- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h
@@ -29,9 +29,9 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
protected:
storm::models::symbolic::Mdp<DdType, ValueType> const& getModel() const override;
diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
index b21d509ec..d110f067d 100644
--- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
@@ -82,7 +82,7 @@ namespace storm {
}
template<typename SparseDtmcModelType>
- std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory);
@@ -90,7 +90,7 @@ namespace storm {
}
template<typename SparseDtmcModelType>
- std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory);
@@ -98,7 +98,7 @@ namespace storm {
}
template<typename SparseDtmcModelType>
- std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
@@ -131,7 +131,7 @@ namespace storm {
}
template<typename SparseDtmcModelType>
- std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();
STORM_LOG_THROW(conditionalFormula.getSubformula().isReachabilityRewardFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
index bdfbe5509..6b94f6642 100644
--- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
@@ -27,10 +27,10 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
private:
// An object that is used for retrieving linear equation solvers.
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
index 614522e01..44a0223a0 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
@@ -109,7 +109,7 @@ namespace storm {
}
template<typename SparseMdpModelType>
- std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound.");
@@ -118,7 +118,7 @@ namespace storm {
}
template<typename SparseMdpModelType>
- std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound.");
@@ -127,7 +127,7 @@ namespace storm {
}
template<typename SparseMdpModelType>
- std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
index b08c9abc5..2f862d631 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
@@ -23,9 +23,9 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
private:
diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
index 311ef7590..9612608df 100644
--- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
@@ -80,7 +80,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory);
@@ -88,7 +88,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory);
@@ -96,7 +96,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h
index 3472ee1b0..883af5ba5 100644
--- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h
@@ -19,9 +19,9 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
protected:
storm::models::symbolic::Dtmc<DdType, ValueType> const& getModel() const override;
diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
index d6a3554e3..f9f2ca37b 100644
--- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
@@ -79,7 +79,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
@@ -87,7 +87,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
@@ -95,7 +95,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h
index 488971353..83cb17244 100644
--- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h
@@ -21,9 +21,9 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
protected:
storm::models::symbolic::Mdp<DdType, ValueType> const& getModel() const override;
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index 7022b92c8..dcde3c480 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -149,7 +149,7 @@ namespace storm {
}
template<typename SparseDtmcModelType>
- std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeLongRunAverageRewards(CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) {
// Do some sanity checks to establish some required properties.
RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : "");
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model.");
@@ -540,7 +540,7 @@ namespace storm {
}
template<typename SparseDtmcModelType>
- std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
// Retrieve the appropriate bitvectors by model checking the subformulas.
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
index 8b86e1dd9..25b4c12d4 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
@@ -26,8 +26,8 @@ namespace storm {
virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
- virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp
index 56a6400d1..983bda12e 100644
--- a/src/models/sparse/MarkovAutomaton.cpp
+++ b/src/models/sparse/MarkovAutomaton.cpp
@@ -55,6 +55,11 @@ namespace storm {
return this->exitRates;
}
+ template <typename ValueType, typename RewardModelType>
+ std::vector<ValueType>& MarkovAutomaton<ValueType, RewardModelType>::getExitRates() {
+ return this->exitRates;
+ }
+
template <typename ValueType, typename RewardModelType>
ValueType const& MarkovAutomaton<ValueType, RewardModelType>::getExitRate(storm::storage::sparse::state_type state) const {
return this->exitRates[state];
diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h
index 731b845f3..0556ffa9b 100644
--- a/src/models/sparse/MarkovAutomaton.h
+++ b/src/models/sparse/MarkovAutomaton.h
@@ -94,6 +94,13 @@ namespace storm {
*/
std::vector<ValueType> const& getExitRates() const;
+ /*!
+ * Retrieves the vector representing the exit rates of the states.
+ *
+ * @return The exit rate vector of the model.
+ */
+ std::vector<ValueType>& getExitRates();
+
/*!
* Retrieves the exit rate of the given state.
*
diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h
index dc0378348..a458bdff7 100644
--- a/src/models/sparse/Model.h
+++ b/src/models/sparse/Model.h
@@ -140,6 +140,21 @@ namespace storm {
*/
storm::storage::SparseMatrix<ValueType>& getTransitionMatrix();
+
+ /*!
+ * Retrieves the reward models.
+ *
+ * @return A mapping from reward model names to the reward models.
+ */
+ std::unordered_map<std::string, RewardModelType> const& getRewardModels() const;
+
+ /*!
+ * Retrieves the reward models.
+ *
+ * @return A mapping from reward model names to the reward models.
+ */
+ std::unordered_map<std::string, RewardModelType>& getRewardModels();
+
/*!
* Retrieves whether the model has a reward model with the given name.
*
@@ -318,20 +333,6 @@ namespace storm {
*/
void printRewardModelsInformationToStream(std::ostream& out) const;
- /*!
- * Retrieves the reward models.
- *
- * @return A mapping from reward model names to the reward models.
- */
- std::unordered_map<std::string, RewardModelType> const& getRewardModels() const;
-
- /*!
- * Retrieves the reward models.
- *
- * @return A mapping from reward model names to the reward models.
- */
- std::unordered_map<std::string, RewardModelType>& getRewardModels();
-
private:
// A matrix representing transition relation.
storm::storage::SparseMatrix<ValueType> transitionMatrix;
diff --git a/src/models/sparse/StochasticTwoPlayerGame.cpp b/src/models/sparse/StochasticTwoPlayerGame.cpp
index c8ce13bec..7a6ea02a1 100644
--- a/src/models/sparse/StochasticTwoPlayerGame.cpp
+++ b/src/models/sparse/StochasticTwoPlayerGame.cpp
@@ -65,7 +65,7 @@ namespace storm {
// template class StochasticTwoPlayerGame<float>;
#ifdef STORM_HAVE_CARL
-// template class StochasticTwoPlayerGame<storm::RationalFunction>;
+ template class StochasticTwoPlayerGame<storm::RationalFunction>;
#endif
} // namespace sparse
diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp
index d8fa100c8..dd0137d9a 100644
--- a/src/parser/FormulaParser.cpp
+++ b/src/parser/FormulaParser.cpp
@@ -88,6 +88,17 @@ namespace storm {
// A parser used for recognizing the optimality operators.
optimalityOperatorStruct optimalityOperator_;
+ struct rewardMeasureTypeStruct : qi::symbols<char, storm::logic::RewardMeasureType> {
+ rewardMeasureTypeStruct() {
+ add
+ ("exp", storm::logic::RewardMeasureType::Expectation)
+ ("var", storm::logic::RewardMeasureType::Variance);
+ }
+ };
+
+ // A parser used for recognizing the reward measure types.
+ rewardMeasureTypeStruct rewardMeasureType_;
+
// Parser and manager used for recognizing expressions.
storm::parser::ExpressionParser expressionParser;
@@ -97,10 +108,11 @@ namespace storm {
qi::rule<Iterator, std::vector<std::shared_ptr<storm::logic::Formula>>(), Skipper> start;
- qi::rule<Iterator, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>>(), qi::locals<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
+ qi::rule<Iterator, storm::logic::OperatorInformation(), qi::locals<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
+ qi::rule<Iterator, storm::logic::RewardMeasureType(), Skipper> rewardMeasureType;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> probabilityOperator;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> rewardOperator;
- qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> expectedTimeOperator;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> timeOperator;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> longRunAverageOperator;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> simpleFormula;
@@ -147,11 +159,11 @@ namespace storm {
std::shared_ptr<storm::logic::Formula> createNextFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const;
std::shared_ptr<storm::logic::Formula> createUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula> const& rightSubformula);
std::shared_ptr<storm::logic::Formula> createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::FormulaContext context) const;
- std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const;
- std::shared_ptr<storm::logic::Formula> createLongRunAverageOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
- std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
- std::shared_ptr<storm::logic::Formula> createExpectedTimeOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
- std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula);
+ storm::logic::OperatorInformation createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const;
+ std::shared_ptr<storm::logic::Formula> createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+ std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, boost::optional<std::string> const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+ std::shared_ptr<storm::logic::Formula> createTimeOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+ std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula);
std::shared_ptr<storm::logic::Formula> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
std::shared_ptr<storm::logic::Formula> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
@@ -301,6 +313,9 @@ namespace storm {
pathFormula = conditionalFormula(qi::_r1);
pathFormula.name("path formula");
+ rewardMeasureType = qi::lit("[") >> rewardMeasureType_ >> qi::lit("]");
+ rewardMeasureType.name("reward measure type");
+
operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
operatorInformation.name("operator information");
@@ -310,11 +325,11 @@ namespace storm {
rewardModelName = qi::lit("{\"") > label > qi::lit("\"}");
rewardModelName.name("reward model name");
- rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
+ rewardOperator = (qi::lit("R") > -rewardMeasureType > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)];
rewardOperator.name("reward operator");
- expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::ExpectedTime) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
- expectedTimeOperator.name("expected time operator");
+ timeOperator = (qi::lit("T") > -rewardMeasureType > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::Time) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
+ timeOperator.name("time operator");
probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
probabilityOperator.name("probability operator");
@@ -459,28 +474,36 @@ namespace storm {
return std::shared_ptr<storm::logic::Formula>(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context));
}
- std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const {
+ storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const {
if (comparisonType && threshold) {
- return std::make_pair(optimizationDirection, storm::logic::Bound<double>(comparisonType.get(), threshold.get()));
+ return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound<double>(comparisonType.get(), threshold.get()));
} else {
- return std::make_pair(optimizationDirection, boost::none);
+ return storm::logic::OperatorInformation(optimizationDirection, boost::none);
}
}
- std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createLongRunAverageOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
- return std::shared_ptr<storm::logic::Formula>(new storm::logic::LongRunAverageOperatorFormula(operatorInformation.first, operatorInformation.second, subformula));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation));
}
- std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
- return std::shared_ptr<storm::logic::Formula>(new storm::logic::RewardOperatorFormula(rewardModelName, operatorInformation.first, operatorInformation.second, subformula));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, boost::optional<std::string> const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+ storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation;
+ if (rewardMeasureType) {
+ measureType = rewardMeasureType.get();
+ }
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation, measureType));
}
- std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createExpectedTimeOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
- return std::shared_ptr<storm::logic::Formula>(new storm::logic::ExpectedTimeOperatorFormula(operatorInformation.first, operatorInformation.second, subformula));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createTimeOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+ storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation;
+ if (rewardMeasureType) {
+ measureType = rewardMeasureType.get();
+ }
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::TimeOperatorFormula(subformula, operatorInformation, measureType));
}
- std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createProbabilityOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) {
- return std::shared_ptr<storm::logic::Formula>(new storm::logic::ProbabilityOperatorFormula(operatorInformation.first, operatorInformation.second, subformula));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation));
}
std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) {
diff --git a/src/settings/Option.cpp b/src/settings/Option.cpp
index b5cba7759..cba074b58 100644
--- a/src/settings/Option.cpp
+++ b/src/settings/Option.cpp
@@ -2,6 +2,7 @@
#include <iomanip>
#include <string>
+#include <algorithm>
#include "ArgumentBase.h"
#include "Argument.h"
@@ -211,4 +212,4 @@ namespace storm {
return out;
}
}
-}
\ No newline at end of file
+}
diff --git a/src/solver/AbstractEquationSolver.h b/src/solver/AbstractEquationSolver.h
index 904e459bd..a8f94dc69 100644
--- a/src/solver/AbstractEquationSolver.h
+++ b/src/solver/AbstractEquationSolver.h
@@ -1,6 +1,7 @@
#ifndef STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_
#define STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_
+#include <memory>
#include "src/solver/TerminationCondition.h"
namespace storm {
@@ -50,4 +51,4 @@ namespace storm {
}
}
-#endif /* STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ */
\ No newline at end of file
+#endif /* STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ */
diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp
index 66ff43f96..c52519d7f 100644
--- a/src/storage/BitVectorHashMap.cpp
+++ b/src/storage/BitVectorHashMap.cpp
@@ -1,5 +1,6 @@
#include "src/storage/BitVectorHashMap.h"
+#include <algorithm>
#include <iostream>
#include "src/utility/macros.h"
diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
index 4ef7d93b3..e968c98cd 100644
--- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
@@ -203,6 +203,7 @@ namespace storm {
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::increaseProbabilityToSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType> const& predecessorBlock, ValueType const& value) {
+ STORM_LOG_TRACE("Increasing probability of " << predecessor << " to splitter by " << value << ".");
storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor);
// If the position of the state is to the right of marker1, we have not seen it before.
@@ -269,6 +270,12 @@ namespace storm {
continue;
}
+ // If we are computing a weak bisimulation on CTMCs and the predecessor block is the splitter, we
+ // need to ignore it and proceed to the next predecessor.
+ if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Ctmc && predecessorBlock == splitter) {
+ continue;
+ }
+
// We keep track of the probability of the predecessor moving to the splitter.
increaseProbabilityToSplitter(predecessor, predecessorBlock, predecessorEntry.getValue());
@@ -278,7 +285,10 @@ namespace storm {
moveStateToMarker1(predecessor, predecessorBlock);
}
- insertIntoPredecessorList(predecessorBlock, predecessorBlocks);
+ // We must not insert the the splitter itself if we are not computing a weak bisimulation on CTMCs.
+ if (this->options.getType() != BisimulationType::Weak || this->model.getType() != storm::models::ModelType::Ctmc || predecessorBlock != splitter) {
+ insertIntoPredecessorList(predecessorBlock, predecessorBlocks);
+ }
}
}
@@ -431,7 +441,7 @@ namespace storm {
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) {
STORM_LOG_TRACE("Refining partition based on splitter " << splitter.getId());
-
+
// The outline of the refinement is as follows.
//
// We iterate over all states of the splitter and determine for each predecessor the state the probability
@@ -464,6 +474,12 @@ namespace storm {
continue;
}
+ // If we are computing a weak bisimulation on CTMCs and the predecessor block is the splitter, we
+ // need to ignore it and proceed to the next predecessor.
+ if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Ctmc && predecessorBlock == splitter) {
+ continue;
+ }
+
// We keep track of the probability of the predecessor moving to the splitter.
increaseProbabilityToSplitter(predecessor, predecessorBlock, predecessorEntry.getValue());
@@ -495,6 +511,8 @@ namespace storm {
// Finally, we split the block based on the precomputed probabilities and the chosen bisimulation type.
if (this->options.getType() == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) {
+ // In the case of CTMCs and weak bisimulation, we still call the "splitStrong" method, but we already have
+ // taken care of not adding the splitter to the predecessor blocks, so this is safe.
refinePredecessorBlocksOfSplitterStrong(predecessorBlocks, splitterQueue);
} else {
// If the splitter is a predecessor of we can use the computed probabilities to update the silent
diff --git a/src/storage/bisimulation/Partition.cpp b/src/storage/bisimulation/Partition.cpp
index 698eb5cd7..b433b70d0 100644
--- a/src/storage/bisimulation/Partition.cpp
+++ b/src/storage/bisimulation/Partition.cpp
@@ -211,7 +211,7 @@ namespace storm {
template<typename DataType>
std::pair<typename std::vector<std::unique_ptr<Block<DataType>>>::iterator, bool> Partition<DataType>::splitBlock(Block<DataType>& block, storm::storage::sparse::state_type position) {
STORM_LOG_THROW(position >= block.getBeginIndex() && position <= block.getEndIndex(), storm::exceptions::InvalidArgumentException, "Cannot split block at illegal position.");
- STORM_LOG_TRACE("Splitting " << block.getId() << " at position " << position << " (begin was " << block.getBeginIndex() << ".");
+ STORM_LOG_TRACE("Splitting " << block.getId() << " at position " << position << " (begin was " << block.getBeginIndex() << ").");
// In case one of the resulting blocks would be empty, we simply return the current block and do not create
// a new one.
@@ -230,7 +230,7 @@ namespace storm {
// Update the mapping of the states in the newly created block.
this->mapStatesToBlock(**newBlockIt, this->begin(**newBlockIt), this->end(**newBlockIt));
-
+
return std::make_pair(newBlockIt, true);
}
diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp
index 8f176048e..f8bf6b368 100644
--- a/src/storage/dd/Bdd.cpp
+++ b/src/storage/dd/Bdd.cpp
@@ -1,3 +1,5 @@
+#include <algorithm>
+
#include "src/storage/dd/Bdd.h"
#include "src/storage/dd/Add.h"
#include "src/storage/dd/Odd.h"
@@ -360,4 +362,4 @@ namespace storm {
template Add<DdType::Sylvan, double> Bdd<DdType::Sylvan>::ite(Add<DdType::Sylvan, double> const& thenAdd, Add<DdType::Sylvan, double> const& elseAdd) const;
template Add<DdType::Sylvan, uint_fast64_t> Bdd<DdType::Sylvan>::ite(Add<DdType::Sylvan, uint_fast64_t> const& thenAdd, Add<DdType::Sylvan, uint_fast64_t> const& elseAdd) const;
}
-}
\ No newline at end of file
+}
diff --git a/src/utility/ModelInstantiator.cpp b/src/utility/ModelInstantiator.cpp
new file mode 100644
index 000000000..cb8c62535
--- /dev/null
+++ b/src/utility/ModelInstantiator.cpp
@@ -0,0 +1,161 @@
+/*
+ * File: ModelInstantiator.cpp
+ * Author: Tim Quatmann
+ *
+ * Created on February 23, 2016
+ */
+
+#include "src/utility/ModelInstantiator.h"
+#include "src/models/sparse/StandardRewardModel.h"
+
+namespace storm {
+ namespace utility {
+
+ template<typename ParametricSparseModelType, typename ConstantSparseModelType>
+ ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::ModelInstantiator(ParametricSparseModelType const& parametricModel){
+ //Now pre-compute the information for the equation system.
+ initializeModelSpecificData(parametricModel);
+ initializeMatrixMapping(this->instantiatedModel->getTransitionMatrix(), this->functions, this->matrixMapping, parametricModel.getTransitionMatrix());
+
+ for(auto& rewModel : this->instantiatedModel->getRewardModels()) {
+ if(rewModel.second.hasStateRewards()){
+ initializeVectorMapping(rewModel.second.getStateRewardVector(), this->functions, this->vectorMapping, parametricModel.getRewardModel(rewModel.first).getStateRewardVector());
+ }
+ if(rewModel.second.hasStateActionRewards()){
+ initializeVectorMapping(rewModel.second.getStateActionRewardVector(), this->functions, this->vectorMapping, parametricModel.getRewardModel(rewModel.first).getStateActionRewardVector());
+ }
+ if(rewModel.second.hasTransitionRewards()){
+ initializeMatrixMapping(rewModel.second.getTransitionRewardMatrix(), this->functions, this->matrixMapping, parametricModel.getRewardModel(rewModel.first).getTransitionRewardMatrix());
+ }
+ }
+ }
+
+ template<typename ParametricSparseModelType, typename ConstantType>
+ ModelInstantiator<ParametricSparseModelType, ConstantType>::~ModelInstantiator() {
+ //Intentionally left empty
+ }
+
+ template<typename ParametricSparseModelType, typename ConstantSparseModelType>
+ storm::storage::SparseMatrix<typename ConstantSparseModelType::ValueType> ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::buildDummyMatrix(storm::storage::SparseMatrix<ParametricType> const& parametricMatrix) const{
+ storm::storage::SparseMatrixBuilder<ConstantType> matrixBuilder(parametricMatrix.getRowCount(),
+ parametricMatrix.getColumnCount(),
+ parametricMatrix.getEntryCount(),
+ true, // no force dimensions
+ true, //Custom row grouping
+ parametricMatrix.getRowGroupCount());
+ for(std::size_t rowGroup = 0; rowGroup < parametricMatrix.getRowGroupCount(); ++rowGroup){
+ matrixBuilder.newRowGroup(parametricMatrix.getRowGroupIndices()[rowGroup]);
+ for(std::size_t row = parametricMatrix.getRowGroupIndices()[rowGroup]; row < parametricMatrix.getRowGroupIndices()[rowGroup+1]; ++row){
+ ConstantType dummyValue = storm::utility::one<ConstantType>();
+ for(auto const& paramEntry : parametricMatrix.getRow(row)){
+ matrixBuilder.addNextValue(row, paramEntry.getColumn(), dummyValue);
+ dummyValue = storm::utility::zero<ConstantType>();
+ }
+ }
+ }
+ return matrixBuilder.build();
+ }
+
+ template<typename ParametricSparseModelType, typename ConstantSparseModelType>
+ std::unordered_map<std::string, typename ConstantSparseModelType::RewardModelType> ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::buildDummyRewardModels(std::unordered_map<std::string, typename ParametricSparseModelType::RewardModelType> const& parametricRewardModel) const {
+ std::unordered_map<std::string, typename ConstantSparseModelType::RewardModelType> result;
+ for(auto const& paramRewardModel : parametricRewardModel){
+ auto const& rewModel = paramRewardModel.second;
+ boost::optional<std::vector<ConstantType>> optionalStateRewardVector;
+ if(rewModel.hasStateRewards()) {
+ optionalStateRewardVector = std::vector<ConstantType>(rewModel.getStateRewardVector().size());
+ }
+ boost::optional<std::vector<ConstantType>> optionalStateActionRewardVector;
+ if(rewModel.hasStateActionRewards()) {
+ optionalStateActionRewardVector = std::vector<ConstantType>(rewModel.getStateActionRewardVector().size());
+ }
+ boost::optional<storm::storage::SparseMatrix<ConstantType>> optionalTransitionRewardMatrix;
+ if(rewModel.hasTransitionRewards()) {
+ optionalTransitionRewardMatrix = buildDummyMatrix(rewModel.getTransitionRewardMatrix());
+ }
+ result.insert(std::make_pair(paramRewardModel.first,
+ storm::models::sparse::StandardRewardModel<ConstantType>(std::move(optionalStateRewardVector), std::move(optionalStateActionRewardVector), std::move(optionalTransitionRewardMatrix))
+ ));
+ }
+ return result;
+ }
+
+ template<typename ParametricSparseModelType, typename ConstantSparseModelType>
+ void ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::initializeMatrixMapping(storm::storage::SparseMatrix<ConstantType>& constantMatrix,
+ std::unordered_map<ParametricType, ConstantType>& functions,
+ std::vector<std::pair<typename storm::storage::SparseMatrix<ConstantType>::iterator, ConstantType*>>& mapping,
+ storm::storage::SparseMatrix<ParametricType> const& parametricMatrix) const{
+ ConstantType dummyValue = storm::utility::one<ConstantType>();
+ auto constantEntryIt = constantMatrix.begin();
+ auto parametricEntryIt = parametricMatrix.begin();
+ while(parametricEntryIt != parametricMatrix.end()){
+ STORM_LOG_ASSERT(parametricEntryIt->getColumn() == constantEntryIt->getColumn(), "Entries of parametric and constant matrix are not at the same position");
+ if(storm::utility::isConstant(parametricEntryIt->getValue())){
+ //Constant entries can be inserted directly
+ constantEntryIt->setValue(storm::utility::convertNumber<ConstantType>(storm::utility::parametric::getConstantPart(parametricEntryIt->getValue())));
+ } else {
+ //insert the new function and store that the current constantMatrix entry needs to be set to the value of this function
+ auto functionsIt = functions.insert(std::make_pair(parametricEntryIt->getValue(), dummyValue)).first;
+ mapping.emplace_back(std::make_pair(constantEntryIt, &(functionsIt->second)));
+ //Note that references to elements of an unordered map remain valid after calling unordered_map::insert.
+ }
+ ++constantEntryIt;
+ ++parametricEntryIt;
+ }
+ STORM_LOG_ASSERT(constantEntryIt == constantMatrix.end(), "Parametric matrix seems to have more or less entries then the constant matrix");
+ //TODO: is this necessary?
+ constantMatrix.updateNonzeroEntryCount();
+ }
+
+ template<typename ParametricSparseModelType, typename ConstantSparseModelType>
+ void ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::initializeVectorMapping(std::vector<ConstantType>& constantVector,
+ std::unordered_map<ParametricType, ConstantType>& functions,
+ std::vector<std::pair<typename std::vector<ConstantType>::iterator, ConstantType*>>& mapping,
+ std::vector<ParametricType> const& parametricVector) const{
+ ConstantType dummyValue = storm::utility::one<ConstantType>();
+ auto constantEntryIt = constantVector.begin();
+ auto parametricEntryIt = parametricVector.begin();
+ while(parametricEntryIt != parametricVector.end()){
+ if(storm::utility::isConstant(storm::utility::simplify(*parametricEntryIt))){
+ //Constant entries can be inserted directly
+ *constantEntryIt = storm::utility::convertNumber<ConstantType>(storm::utility::parametric::getConstantPart(*parametricEntryIt));
+ } else {
+ //insert the new function and store that the current constantVector entry needs to be set to the value of this function
+ auto functionsIt = functions.insert(std::make_pair(*parametricEntryIt, dummyValue)).first;
+ mapping.emplace_back(std::make_pair(constantEntryIt, &(functionsIt->second)));
+ //Note that references to elements of an unordered map remain valid after calling unordered_map::insert.
+ }
+ ++constantEntryIt;
+ ++parametricEntryIt;
+ }
+ STORM_LOG_ASSERT(constantEntryIt == constantVector.end(), "Parametric vector seems to have more or less entries then the constant vector");
+ }
+
+ template<typename ParametricSparseModelType, typename ConstantSparseModelType>
+ ConstantSparseModelType const& ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::instantiate(std::map<VariableType, CoefficientType>const& valuation){
+ //Write results into the placeholders
+ for(auto& functionResult : this->functions){
+ functionResult.second=storm::utility::convertNumber<ConstantType>(
+ storm::utility::parametric::evaluate(functionResult.first, valuation));
+ }
+
+ //Write the instantiated values to the matrices and vectors according to the stored mappings
+ for(auto& entryValuePair : this->matrixMapping){
+ entryValuePair.first->setValue(*(entryValuePair.second));
+ }
+ for(auto& entryValuePair : this->vectorMapping){
+ *(entryValuePair.first)=*(entryValuePair.second);
+ }
+
+ return *this->instantiatedModel;
+ }
+
+#ifdef STORM_HAVE_CARL
+ template class ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>>;
+ template class ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>>;
+ template class ModelInstantiator<storm::models::sparse::Ctmc<storm::RationalFunction>, storm::models::sparse::Ctmc<double>>;
+ template class ModelInstantiator<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>, storm::models::sparse::MarkovAutomaton<double>>;
+ template class ModelInstantiator<storm::models::sparse::StochasticTwoPlayerGame<storm::RationalFunction>, storm::models::sparse::StochasticTwoPlayerGame<double>>;
+#endif
+ } //namespace utility
+} //namespace storm
\ No newline at end of file
diff --git a/src/utility/ModelInstantiator.h b/src/utility/ModelInstantiator.h
new file mode 100644
index 000000000..939e71e2d
--- /dev/null
+++ b/src/utility/ModelInstantiator.h
@@ -0,0 +1,158 @@
+/*
+ * File: ModelInstantiator.h
+ * Author: Tim Quatmann
+ *
+ * Created on February 23, 2016
+ */
+
+#ifndef STORM_UTILITY_MODELINSTANTIATOR_H
+#define STORM_UTILITY_MODELINSTANTIATOR_H
+
+#include <unordered_map>
+#include <memory>
+#include <type_traits>
+
+#include "src/models/sparse/Dtmc.h"
+#include "src/models/sparse/Mdp.h"
+#include "src/models/sparse/Ctmc.h"
+#include "src/models/sparse/MarkovAutomaton.h"
+#include "src/models/sparse/StochasticTwoPlayerGame.h"
+#include "src/utility/parametric.h"
+#include "src/utility/constants.h"
+
+namespace storm {
+ namespace utility{
+
+
+ /*!
+ * This class allows efficient instantiation of the given parametric model.
+ * The key to efficiency is to evaluate every distinct transition- (or reward-) function only once
+ * instead of evaluating the same function for each occurrence in the model.
+ */
+ template<typename ParametricSparseModelType, typename ConstantSparseModelType>
+ class ModelInstantiator {
+ public:
+ typedef typename ParametricSparseModelType::ValueType ParametricType;
+ typedef typename storm::utility::parametric::VariableType<ParametricType>::type VariableType;
+ typedef typename storm::utility::parametric::CoefficientType<ParametricType>::type CoefficientType;
+ typedef typename ConstantSparseModelType::ValueType ConstantType;
+
+ /*!
+ * Constructs a ModelInstantiator
+ * @param parametricModel The model that is to be instantiated
+ */
+ ModelInstantiator(ParametricSparseModelType const& parametricModel);
+
+ /*!
+ * Destructs the ModelInstantiator
+ */
+ virtual ~ModelInstantiator();
+
+ /*!
+ * Evaluates the occurring parametric functions and retrieves the instantiated model
+ * @param valuation Maps each occurring variables to the value with which it should be substituted
+ * @return The instantiated model
+ */
+ ConstantSparseModelType const& instantiate(std::map<VariableType, CoefficientType>const& valuation);
+
+
+ private:
+ /*!
+ * Initializes the instantiatedModel with dummy data by considering the model-specific ingredients.
+ * Also initializes other model-specific data, e.g., the exitRate vector of a markov automaton
+ */
+ template<typename PMT = ParametricSparseModelType>
+ typename std::enable_if<
+ std::is_same<PMT,storm::models::sparse::Dtmc<typename ParametricSparseModelType::ValueType>>::value ||
+ std::is_same<PMT,storm::models::sparse::Mdp<typename ParametricSparseModelType::ValueType>>::value ||
+ std::is_same<PMT,storm::models::sparse::Ctmc<typename ParametricSparseModelType::ValueType>>::value
+ >::type
+ initializeModelSpecificData(PMT const& parametricModel) {
+ auto stateLabelingCopy = parametricModel.getStateLabeling();
+ auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling();
+ this->instantiatedModel = std::make_shared<ConstantSparseModelType>(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy));
+ }
+
+ template<typename PMT = ParametricSparseModelType>
+ typename std::enable_if<
+ std::is_same<PMT,storm::models::sparse::MarkovAutomaton<typename ParametricSparseModelType::ValueType>>::value
+ >::type
+ initializeModelSpecificData(PMT const& parametricModel) {
+ auto stateLabelingCopy = parametricModel.getStateLabeling();
+ auto markovianStatesCopy = parametricModel.getMarkovianStates();
+ auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling();
+ std::vector<ConstantType> exitRates(parametricModel.getExitRates().size(), storm::utility::one<ConstantType>());
+ this->instantiatedModel = std::make_shared<ConstantSparseModelType>(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), std::move(markovianStatesCopy), std::move(exitRates), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy));
+
+ initializeVectorMapping(this->instantiatedModel->getExitRates(), this->functions, this->vectorMapping, parametricModel.getExitRates());
+ }
+
+ template<typename PMT = ParametricSparseModelType>
+ typename std::enable_if<
+ std::is_same<PMT,storm::models::sparse::StochasticTwoPlayerGame<typename ParametricSparseModelType::ValueType>>::value
+ >::type
+ initializeModelSpecificData(PMT const& parametricModel) {
+ auto player1MatrixCopy = parametricModel.getPlayer1Matrix();
+ auto stateLabelingCopy = parametricModel.getStateLabeling();
+ boost::optional<std::vector<typename storm::models::sparse::LabelSet>> player1ChoiceLabeling, player2ChoiceLabeling;
+ if(parametricModel.hasPlayer1ChoiceLabeling()) player1ChoiceLabeling = parametricModel.getPlayer1ChoiceLabeling();
+ if(parametricModel.hasPlayer2ChoiceLabeling()) player2ChoiceLabeling = parametricModel.getPlayer2ChoiceLabeling();
+ this->instantiatedModel = std::make_shared<ConstantSparseModelType>(std::move(player1MatrixCopy), buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(player1ChoiceLabeling), std::move(player2ChoiceLabeling));
+ }
+
+ /*!
+ * Creates a matrix that has entries at the same position as the given matrix.
+ * The returned matrix is a stochastic matrix, i.e., the rows sum up to one.
+ */
+ storm::storage::SparseMatrix<ConstantType> buildDummyMatrix(storm::storage::SparseMatrix<ParametricType> const& parametricMatrix) const;
+
+ /*!
+ * Creates a copy of the given reward models with the same names and with state(action)rewards / transitionrewards having the same entry-count and entry-positions.
+ */
+ std::unordered_map<std::string, typename ConstantSparseModelType::RewardModelType> buildDummyRewardModels(std::unordered_map<std::string, typename ParametricSparseModelType::RewardModelType> const& parametricRewardModel) const;
+
+ /*!
+ * Connects the occurring functions with the corresponding matrix entries
+ *
+ * @note constantMatrix and parametricMatrix should have entries at the same positions
+ *
+ * @param constantMatrix The matrix to which the evaluation results are written
+ * @param functions Occurring functions are inserted in this map
+ * @param mapping The connections of functions to matrix entries are push_backed into this
+ * @param parametricMatrix the source matrix with the functions to consider.
+ */
+ void initializeMatrixMapping(storm::storage::SparseMatrix<ConstantType>& constantMatrix,
+ std::unordered_map<ParametricType, ConstantType>& functions,
+ std::vector<std::pair<typename storm::storage::SparseMatrix<ConstantType>::iterator, ConstantType*>>& mapping,
+ storm::storage::SparseMatrix<ParametricType> const& parametricMatrix) const;
+
+ /*!
+ * Connects the occurring functions with the corresponding vector entries
+ *
+ * @note constantVector and parametricVector should have the same size
+ *
+ * @param constantVector The vector to which the evaluation results are written
+ * @param functions Occurring functions with their placeholders are inserted in this map
+ * @param mapping The connections of functions to vector entries are push_backed into this
+ * @param parametricVector the source vector with the functions to consider.
+ */
+ void initializeVectorMapping(std::vector<ConstantType>& constantVector,
+ std::unordered_map<ParametricType, ConstantType>& functions,
+ std::vector<std::pair<typename std::vector<ConstantType>::iterator, ConstantType*>>& mapping,
+ std::vector<ParametricType> const& parametricVector) const;
+
+ /// The resulting model
+ std::shared_ptr<ConstantSparseModelType> instantiatedModel;
+ /// the occurring functions together with the corresponding placeholders for their evaluated result
+ std::unordered_map<ParametricType, ConstantType> functions;
+ /// Connection of matrix entries with placeholders
+ std::vector<std::pair<typename storm::storage::SparseMatrix<ConstantType>::iterator, ConstantType*>> matrixMapping;
+ /// Connection of Vector entries with placeholders
+ std::vector<std::pair<typename std::vector<ConstantType>::iterator, ConstantType*>> vectorMapping;
+
+
+ };
+ }//Namespace utility
+} //namespace storm
+#endif /* STORM_UTILITY_MODELINSTANTIATOR_H */
+
diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index 941f07f7e..7fe39b963 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -39,6 +39,7 @@ namespace storm {
bool isConstant(ValueType const& a) {
return true;
}
+
#ifdef STORM_HAVE_CARL
template<>
@@ -85,11 +86,11 @@ namespace storm {
template<typename ValueType>
ValueType simplify(ValueType value) {
- // In the general case, we don't to anything here, but merely return the value. If something else is
+ // In the general case, we don't do anything here, but merely return the value. If something else is
// supposed to happen here, the templated function can be specialized for this particular type.
return value;
}
-
+
#ifdef STORM_HAVE_CARL
template<>
RationalFunction& simplify(RationalFunction& value);
@@ -119,6 +120,17 @@ namespace storm {
value.simplify();
return std::move(value);
}
+
+ template<>
+ double convertNumber(RationalNumber const& number){
+ return carl::toDouble(number);
+ }
+
+ template<>
+ RationalNumber convertNumber(double const& number){
+ return carl::rationalize<RationalNumber>(number);
+ }
+
#endif
template<typename IndexType, typename ValueType>
@@ -225,6 +237,9 @@ namespace storm {
template RationalFunction& simplify(RationalFunction& value);
template RationalFunction&& simplify(RationalFunction&& value);
+ template double convertNumber(RationalNumber const& number);
+ template RationalNumber convertNumber(double const& number);
+
template bool isOne(Interval const& value);
template bool isZero(Interval const& value);
template bool isConstant(Interval const& value);
diff --git a/src/utility/constants.h b/src/utility/constants.h
index 8f6d8149e..80222b74f 100644
--- a/src/utility/constants.h
+++ b/src/utility/constants.h
@@ -50,6 +50,9 @@ namespace storm {
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry);
+
+ template<typename TargetType, typename SourceType>
+ TargetType convertNumber(SourceType const& number);
}
}
diff --git a/src/utility/macros.h b/src/utility/macros.h
index 4f70b1691..8d7048fdb 100644
--- a/src/utility/macros.h
+++ b/src/utility/macros.h
@@ -2,6 +2,8 @@
#define STORM_UTILITY_MACROS_H_
#include <cassert>
+#include <string.h>
+
#include "storm-config.h"
#ifndef STORM_LOGGING_FRAMEWORK
@@ -272,4 +274,4 @@ LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console."
STORM_PRINT(message); \
}
-#endif /* STORM_UTILITY_MACROS_H_ */
\ No newline at end of file
+#endif /* STORM_UTILITY_MACROS_H_ */
diff --git a/src/utility/parametric.cpp b/src/utility/parametric.cpp
new file mode 100644
index 000000000..c45882c42
--- /dev/null
+++ b/src/utility/parametric.cpp
@@ -0,0 +1,39 @@
+/*
+ * File: parametric.cpp
+ * Author: Tim Quatmann
+ *
+ * Created by Tim Quatmann on 08/03/16.
+ */
+
+#include <string>
+
+#include "src/utility/parametric.h"
+#include "src/utility/constants.h"
+#include "src/utility/macros.h"
+#include "src/settings/SettingsManager.h"
+#include "src/exceptions/IllegalArgumentException.h"
+#include "src/exceptions/NotImplementedException.h"
+
+#ifdef STORM_HAVE_CARL
+#include<carl/numbers/numbers.h>
+#include<carl/core/VariablePool.h>
+#endif
+
+namespace storm {
+ namespace utility{
+ namespace parametric {
+
+#ifdef STORM_HAVE_CARL
+ template<>
+ typename CoefficientType<storm::RationalFunction>::type evaluate<storm::RationalFunction>(storm::RationalFunction const& function, std::map<typename VariableType<storm::RationalFunction>::type, typename CoefficientType<storm::RationalFunction>::type> const& valuation){
+ return function.evaluate(valuation);
+ }
+
+ template<>
+ typename CoefficientType<storm::RationalFunction>::type getConstantPart<storm::RationalFunction>(storm::RationalFunction const& function){
+ return function.constantPart();
+ }
+#endif
+ }
+ }
+}
diff --git a/src/utility/parametric.h b/src/utility/parametric.h
new file mode 100644
index 000000000..2ebf1e18c
--- /dev/null
+++ b/src/utility/parametric.h
@@ -0,0 +1,54 @@
+//
+// parametric.h
+//
+// Created by Tim Quatmann on 08/03/16.
+//
+//
+
+#ifndef STORM_UTILITY_PARAMETRIC_H
+#define STORM_UTILITY_PARAMETRIC_H
+
+#include "src/adapters/CarlAdapter.h"
+
+
+namespace storm {
+ namespace utility {
+ namespace parametric {
+
+ /*!
+ * Access the type of variables from a given function type
+ */
+ template<typename FunctionType>
+ struct VariableType { typedef void type; };
+ /*!
+ * Acess the type of coefficients from a given function type
+ */
+ template<typename FunctionType>
+ struct CoefficientType { typedef void type; };
+
+#ifdef STORM_HAVE_CARL
+ template<>
+ struct VariableType<storm::RationalFunction> { typedef storm::Variable type; };
+ template<>
+ struct CoefficientType<storm::RationalFunction> { typedef storm::RationalNumber type; };
+#endif
+
+ /*!
+ * Evaluates the given function wrt. the given valuation
+ */
+ template<typename FunctionType>
+ typename CoefficientType<FunctionType>::type evaluate(FunctionType const& function, std::map<typename VariableType<FunctionType>::type, typename CoefficientType<FunctionType>::type> const& valuation);
+
+ /*!
+ * Retrieves the constant part of the given function.
+ */
+ template<typename FunctionType>
+ typename CoefficientType<FunctionType>::type getConstantPart(FunctionType const& function);
+
+ }
+
+ }
+}
+
+
+#endif /* STORM_UTILITY_PARAMETRIC_H */
diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp
new file mode 100644
index 000000000..af8f5b8d2
--- /dev/null
+++ b/test/functional/utility/ModelInstantiatorTest.cpp
@@ -0,0 +1,266 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#ifdef STORM_HAVE_CARL
+
+#include "src/adapters/CarlAdapter.h"
+#include<carl/numbers/numbers.h>
+#include<carl/core/VariablePool.h>
+
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/GeneralSettings.h"
+
+#include "utility/storm.h"
+#include "utility/ModelInstantiator.h"
+#include "src/models/sparse/Model.h"
+#include "src/models/sparse/Dtmc.h"
+#include "src/models/sparse/Mdp.h"
+
+TEST(ModelInstantiatorTest, Brp_Prob) {
+ carl::VariablePool::getInstance().clear();
+
+ std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm";
+ std::string const& formulaAsString = "P=? [F s=5 ]";
+ std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
+
+ // Program and formula
+ storm::prism::Program program = storm::parseProgram(programFile);
+ program.checkValidity();
+ std::vector<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
+ ASSERT_TRUE(formulas.size()==1);
+ // Parametric model
+ typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formulas[0]);
+ options.addConstantDefinitionsFromString(program, constantsAsString);
+ options.preserveFormula(*formulas[0]);
+ std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>().translateProgram(program, options)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+
+ storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
+ EXPECT_FALSE(dtmc->hasRewardModel());
+
+ {
+ std::map<storm::Variable, storm::RationalNumber> valuation;
+ storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
+ ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
+ storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
+ ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
+ valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(0.8)));
+ valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
+
+ storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
+
+ ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices());
+ for(std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup){
+ for(std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){
+ auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin();
+ for(auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)){
+ EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn());
+ double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation));
+ EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue());
+ ++instantiatedEntry;
+ }
+ EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry);
+ }
+ }
+ EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling());
+ EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling());
+
+ storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> modelchecker(instantiated);
+ std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
+ storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
+ EXPECT_NEAR(0.2989278941, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision());
+ }
+
+ {
+ std::map<storm::Variable, storm::RationalNumber> valuation;
+ storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
+ ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
+ storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
+ ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
+ valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1)));
+ valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(1)));
+
+ storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
+
+ ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices());
+ for(std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup){
+ for(std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){
+ auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin();
+ for(auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)){
+ EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn());
+ double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation));
+ EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue());
+ ++instantiatedEntry;
+ }
+ EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry);
+ }
+ }
+ EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling());
+ EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling());
+
+ storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> modelchecker(instantiated);
+ std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
+ storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
+ EXPECT_EQ(0.0 , quantitativeChkResult[*instantiated.getInitialStates().begin()]);
+ }
+
+ {
+ std::map<storm::Variable, storm::RationalNumber> valuation;
+ storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
+ ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
+ storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
+ ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
+ valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1)));
+ valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
+
+ storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
+
+ ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices());
+ for(std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup){
+ for(std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){
+ auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin();
+ for(auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)){
+ EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn());
+ double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation));
+ EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue());
+ ++instantiatedEntry;
+ }
+ EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry);
+ }
+ }
+ EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling());
+ EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling());
+
+ storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> modelchecker(instantiated);
+ std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
+ storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
+ EXPECT_NEAR(0.01588055832, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision());
+ }
+}
+
+TEST(ModelInstantiatorTest, Brp_Rew) {
+ carl::VariablePool::getInstance().clear();
+
+ std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm";
+ std::string const& formulaAsString = "R=? [F ((s=5) | (s=0&srep=3)) ]";
+ std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
+
+ // Program and formula
+ storm::prism::Program program = storm::parseProgram(programFile);
+ program.checkValidity();
+ std::vector<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
+ ASSERT_TRUE(formulas.size()==1);
+ // Parametric model
+ typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formulas[0]);
+ options.addConstantDefinitionsFromString(program, constantsAsString);
+ options.preserveFormula(*formulas[0]);
+ std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>().translateProgram(program, options)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+
+ storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
+
+ {
+ std::map<storm::Variable, storm::RationalNumber> valuation;
+ storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
+ ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
+ storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
+ ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
+ storm::Variable const& TOMsg = carl::VariablePool::getInstance().findVariableWithName("TOMsg");
+ ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
+ storm::Variable const& TOAck = carl::VariablePool::getInstance().findVariableWithName("TOAck");
+ ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
+ valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(0.9)));
+ valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.3)));
+ valuation.insert(std::make_pair(TOMsg,carl::rationalize<storm::RationalNumber>(0.3)));
+ valuation.insert(std::make_pair(TOAck,carl::rationalize<storm::RationalNumber>(0.5)));
+
+ storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
+
+ ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices());
+ for(std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup){
+ for(std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){
+ auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin();
+ for(auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)){
+ EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn());
+ double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation));
+ EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue());
+ ++instantiatedEntry;
+ }
+ EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry);
+ }
+ }
+ ASSERT_TRUE(instantiated.hasUniqueRewardModel());
+ EXPECT_FALSE(instantiated.getUniqueRewardModel()->second.hasStateRewards());
+ EXPECT_FALSE(instantiated.getUniqueRewardModel()->second.hasTransitionRewards());
+ EXPECT_TRUE(instantiated.getUniqueRewardModel()->second.hasStateActionRewards());
+ ASSERT_TRUE(dtmc->getUniqueRewardModel()->second.hasStateActionRewards());
+ std::size_t stateActionEntries = dtmc->getUniqueRewardModel()->second.getStateActionRewardVector().size();
+ ASSERT_EQ(stateActionEntries, instantiated.getUniqueRewardModel()->second.getStateActionRewardVector().size());
+ for(std::size_t i =0; i<stateActionEntries; ++i){
+ double evaluatedValue = carl::toDouble(dtmc->getUniqueRewardModel()->second.getStateActionRewardVector()[i].evaluate(valuation));
+ EXPECT_EQ(evaluatedValue, instantiated.getUniqueRewardModel()->second.getStateActionRewardVector()[i]);
+ }
+ EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling());
+ EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling());
+
+ storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> modelchecker(instantiated);
+ std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
+ storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
+ EXPECT_NEAR(1.308324495, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision());
+ }
+
+}
+
+
+TEST(ModelInstantiatorTest, consensus) {
+ carl::VariablePool::getInstance().clear();
+
+ std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/coin2_2.pm";
+ std::string const& formulaAsString = "Pmin=? [F \"finished\"&\"all_coins_equal_1\" ]";
+ std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
+
+ // Program and formula
+ storm::prism::Program program = storm::parseProgram(programFile);
+ program.checkValidity();
+ std::vector<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
+ ASSERT_TRUE(formulas.size()==1);
+ // Parametric model
+ typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formulas[0]);
+ options.addConstantDefinitionsFromString(program, constantsAsString);
+ options.preserveFormula(*formulas[0]);
+ std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> mdp = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>().translateProgram(program, options)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+
+ storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>> modelInstantiator(*mdp);
+
+ std::map<storm::Variable, storm::RationalNumber> valuation;
+ storm::Variable const& p1 = carl::VariablePool::getInstance().findVariableWithName("p1");
+ ASSERT_NE(p1, carl::Variable::NO_VARIABLE);
+ storm::Variable const& p2 = carl::VariablePool::getInstance().findVariableWithName("p2");
+ ASSERT_NE(p2, carl::Variable::NO_VARIABLE);
+ valuation.insert(std::make_pair(p1,carl::rationalize<storm::RationalNumber>(0.51)));
+ valuation.insert(std::make_pair(p2,carl::rationalize<storm::RationalNumber>(0.49)));
+ storm::models::sparse::Mdp<double> const& instantiated(modelInstantiator.instantiate(valuation));
+
+ ASSERT_EQ(mdp->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices());
+ for(std::size_t rowGroup = 0; rowGroup < mdp->getTransitionMatrix().getRowGroupCount(); ++rowGroup){
+ for(std::size_t row = mdp->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < mdp->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){
+ auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin();
+ for(auto const& paramEntry : mdp->getTransitionMatrix().getRow(row)){
+ EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn());
+ double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation));
+ EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue());
+ ++instantiatedEntry;
+ }
+ EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry);
+ }
+ }
+ EXPECT_EQ(mdp->getStateLabeling(), instantiated.getStateLabeling());
+ EXPECT_EQ(mdp->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling());
+
+ storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> modelchecker(instantiated);
+ std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
+ storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
+ EXPECT_NEAR(0.3526577219, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision());
+
+}
+
+#endif
\ No newline at end of file
diff --git a/test/functional/utility/brp16_2.pm b/test/functional/utility/brp16_2.pm
new file mode 100644
index 000000000..d756a90ec
--- /dev/null
+++ b/test/functional/utility/brp16_2.pm
@@ -0,0 +1,146 @@
+// bounded retransmission protocol [D'AJJL01]
+// gxn/dxp 23/05/2001
+
+dtmc
+
+// number of chunks
+const int N = 16;
+// maximum number of retransmissions
+const int MAX = 2;
+
+// reliability of channels
+const double pL;
+const double pK;
+
+// timeouts
+const double TOMsg;
+const double TOAck;
+
+module sender
+
+ s : [0..6];
+ // 0 idle
+ // 1 next_frame
+ // 2 wait_ack
+ // 3 retransmit
+ // 4 success
+ // 5 error
+ // 6 wait sync
+ srep : [0..3];
+ // 0 bottom
+ // 1 not ok (nok)
+ // 2 do not know (dk)
+ // 3 ok (ok)
+ nrtr : [0..MAX];
+ i : [0..N];
+ bs : bool;
+ s_ab : bool;
+ fs : bool;
+ ls : bool;
+
+ // idle
+ [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
+ // next_frame
+ [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
+ // wait_ack
+ [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
+ [TO_Msg] (s=2) -> (s'=3);
+ [TO_Ack] (s=2) -> (s'=3);
+ // retransmit
+ [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
+ [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
+ [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
+ // success
+ [] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
+ [] (s=4) & (i=N) -> (s'=0) & (srep'=3);
+ // error
+ [SyncWait] (s=5) -> (s'=6);
+ // wait sync
+ [SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
+
+endmodule
+
+module receiver
+
+ r : [0..5];
+ // 0 new_file
+ // 1 fst_safe
+ // 2 frame_received
+ // 3 frame_reported
+ // 4 idle
+ // 5 resync
+ rrep : [0..4];
+ // 0 bottom
+ // 1 fst
+ // 2 inc
+ // 3 ok
+ // 4 nok
+ fr : bool;
+ lr : bool;
+ br : bool;
+ r_ab : bool;
+ recv : bool;
+
+
+ // new_file
+ [SyncWait] (r=0) -> (r'=0);
+ [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+ // fst_safe_frame
+ [] (r=1) -> (r'=2) & (r_ab'=br);
+ // frame_received
+ [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
+ [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
+ [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
+ [aA] (r=2) & !(r_ab=br) -> (r'=4);
+ // frame_reported
+ [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
+ // idle
+ [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+ [SyncWait] (r=4) & (ls=true) -> (r'=5);
+ [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
+ // resync
+ [SyncWait] (r=5) -> (r'=0) & (rrep'=0);
+
+endmodule
+
+// prevents more than one file being sent
+module tester
+
+ T : bool;
+
+ [NewFile] (T=false) -> (T'=true);
+
+endmodule
+
+module channelK
+
+ k : [0..2];
+
+ // idle
+ [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2);
+ // sending
+ [aG] (k=1) -> (k'=0);
+ // lost
+ [TO_Msg] (k=2) -> (k'=0);
+
+endmodule
+
+module channelL
+
+ l : [0..2];
+
+ // idle
+ [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2);
+ // sending
+ [aB] (l=1) -> (l'=0);
+ // lost
+ [TO_Ack] (l=2) -> (l'=0);
+
+endmodule
+
+rewards
+ [TO_Msg] true : TOMsg;
+ [TO_Ack] true : TOAck;
+endrewards
+
+
diff --git a/test/functional/utility/coin2_2.pm b/test/functional/utility/coin2_2.pm
new file mode 100644
index 000000000..3f5358cdd
--- /dev/null
+++ b/test/functional/utility/coin2_2.pm
@@ -0,0 +1,56 @@
+//Randomised Consensus Protocol
+
+mdp
+const double p1; // in [0.2 , 0.8]
+const double p2; // in [0.2 , 0.8]
+
+
+const int N=2;
+const int K=2;
+const int range = 2*(K+1)*N;
+const int counter_init = (K+1)*N;
+const int left = N;
+const int right = 2*(K+1)*N - N;
+
+// shared coin
+global counter : [0..range] init counter_init;
+
+module process1
+
+ // program counter
+ pc1 : [0..3];
+ // 0 - flip
+ // 1 - write
+ // 2 - check
+ // 3 - finished
+
+ // local coin
+ coin1 : [0..1];
+
+ // flip coin
+ [] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1 - p1 : (coin1'=1) & (pc1'=1);
+ // write tails -1 (reset coin to add regularity)
+ [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0);
+ // write heads +1 (reset coin to add regularity)
+ [] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0);
+ // check
+ // decide tails
+ [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0);
+ // decide heads
+ [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1);
+ // flip again
+ [] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0);
+ // loop (all loop together when done)
+ [done] (pc1=3) -> (pc1'=3);
+
+endmodule
+
+module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule
+label "finished" = pc1=3 &pc2=3 ;
+label "all_coins_equal_1" = coin1=1 &coin2=1 ;
+rewards "steps"
+ true : 1;
+endrewards
+
+
+