renamed expected time formulas to time formulas

Former-commit-id: 50a11fe446

src/logic/EventuallyFormula.cpp

@@ -7,7 +7,7 @@
 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 {
@@ -22,8 +22,8 @@ namespace storm {
             return context == FormulaContext::Reward;
         }
         
-        bool EventuallyFormula::isReachabilityExpectedTimeFormula() const {
-            return context == FormulaContext::ExpectedTime;
+        bool EventuallyFormula::isReachabilityTimeFormula() const {
+            return context == FormulaContext::Time;
         }
         
         bool EventuallyFormula::isProbabilityPathFormula() const {
@@ -34,8 +34,8 @@ namespace storm {
             return this->isReachabilityRewardFormula();
         }
         
-        bool EventuallyFormula::isExpectedTimePathFormula() const {
-            return this->isReachabilityExpectedTimeFormula();
+        bool EventuallyFormula::isTimePathFormula() const {
+            return this->isReachabilityTimeFormula();
         }
         
         boost::any EventuallyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {

src/logic/EventuallyFormula.h

@@ -17,10 +17,10 @@ namespace storm {
             virtual bool isEventuallyFormula() const override;
             virtual bool isReachabilityProbabilityFormula() const override;
             virtual bool isReachabilityRewardFormula() const override;
-            virtual bool isReachabilityExpectedTimeFormula() 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;
 

src/logic/ExpectedTimeOperatorFormula.cpp

@@ -1,32 +0,0 @@
-#include "src/logic/ExpectedTimeOperatorFormula.h"
-
-#include "src/logic/FormulaVisitor.h"
-
-#include "src/utility/macros.h"
-#include "src/exceptions/InvalidPropertyException.h"
-
-namespace storm {
-    namespace logic {
-        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation) : OperatorFormula(subformula, operatorInformation) {
-            STORM_LOG_THROW(this->getMeasureType() == MeasureType::Expectation || this->getMeasureType() == MeasureType::Variance, storm::exceptions::InvalidPropertyException, "Invalid measure type in ET-operator.");
-        }
-        
-        bool ExpectedTimeOperatorFormula::isExpectedTimeOperatorFormula() const {
-            return true;
-        }
-        
-        boost::any ExpectedTimeOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
-            return visitor.visit(*this, data);
-        }
-        
-        std::shared_ptr<Formula> ExpectedTimeOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<ExpectedTimeOperatorFormula>(this->getSubformula().substitute(substitution), this->operatorInformation);
-        }
-        
-        std::ostream& ExpectedTimeOperatorFormula::writeToStream(std::ostream& out) const {
-            out << "ET";
-            OperatorFormula::writeToStream(out);
-            return out;
-        }
-    }
-}

src/logic/Formula.cpp

@@ -94,7 +94,7 @@ namespace storm {
             return false;
         }
         
-        bool Formula::isExpectedTimePathFormula() const {
+        bool Formula::isTimePathFormula() const {
             return false;
         }
         
@@ -106,7 +106,7 @@ namespace storm {
             return false;
         }
         
-        bool Formula::isExpectedTimeOperatorFormula() const {
+        bool Formula::isTimeOperatorFormula() const {
             return false;
         }
         
@@ -126,7 +126,7 @@ namespace storm {
             return false;
         }
         
-        bool Formula::isReachabilityExpectedTimeFormula() const {
+        bool Formula::isReachabilityTimeFormula() const {
             return false;
         }
         
@@ -276,11 +276,11 @@ namespace storm {
             return dynamic_cast<EventuallyFormula const&>(*this);
         }
         
-        EventuallyFormula& Formula::asReachabilityExpectedTimeFormula() {
+        EventuallyFormula& Formula::asReachabilityTimeFormula() {
             return dynamic_cast<EventuallyFormula&>(*this);
         }
 
-        EventuallyFormula const& Formula::asReachabilityExpectedTimeFormula() const {
+        EventuallyFormula const& Formula::asReachabilityTimeFormula() const {
             return dynamic_cast<EventuallyFormula const&>(*this);
         }
         
@@ -324,12 +324,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() {

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;
 
@@ -76,7 +76,7 @@ namespace storm {
             virtual bool isLongRunAverageRewardFormula() const;
             
             // Expected time formulas.
-            virtual bool isReachabilityExpectedTimeFormula() const;
+            virtual bool isReachabilityTimeFormula() const;
             
             // Type checks for abstract intermediate classes.
             virtual bool isBinaryPathFormula() const;
@@ -133,8 +133,8 @@ namespace storm {
             EventuallyFormula& asReachabilityRewardFormula();
             EventuallyFormula const& asReachabilityRewardFormula() const;
 
-            EventuallyFormula& asReachabilityExpectedTimeFormula();
-            EventuallyFormula const& asReachabilityExpectedTimeFormula() const;
+            EventuallyFormula& asReachabilityTimeFormula();
+            EventuallyFormula const& asReachabilityTimeFormula() const;
             
             GloballyFormula& asGloballyFormula();
             GloballyFormula const& asGloballyFormula() const;
@@ -154,8 +154,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;

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 };
         
     }
 }

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);
         }
         

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;

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;

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"

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;

src/logic/FragmentChecker.cpp

@@ -99,18 +99,18 @@ namespace storm {
             } else if (f.isReachabilityRewardFormula()) {
                 result = result && inherited.getSpecification().areReachabilityRewardFormulasAllowed();
                 result = result && f.getSubformula().isStateFormula();
-            } else if (f.isReachabilityExpectedTimeFormula()) {
-                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.getSubformula().isTimePathFormula();
             result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == MeasureType::Expectation);
             if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
                 result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));

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;

src/logic/FragmentSpecification.cpp

@@ -89,7 +89,7 @@ namespace storm {
             conditionalProbabilityFormula = false;
             conditionalRewardFormula = false;
             
-            reachabilityExpectedTimeFormula = false;
+            reachabilityTimeFormula = false;
             
             nestedOperators = true;
             nestedPathFormulas = false;
@@ -121,11 +121,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;
         }
@@ -283,12 +283,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;
         }
         
@@ -341,13 +341,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;
         }
         

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);
@@ -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);
@@ -95,7 +95,7 @@ namespace storm {
             FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue);
             
             FragmentSpecification& setOperatorsAllowed(bool newValue);
-            FragmentSpecification& setExpectedTimeAllowed(bool newValue);
+            FragmentSpecification& setTimeAllowed(bool newValue);
             FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue);
             
         private:
@@ -125,7 +125,7 @@ namespace storm {
             bool conditionalProbabilityFormula;
             bool conditionalRewardFormula;
             
-            bool reachabilityExpectedTimeFormula;
+            bool reachabilityTimeFormula;
             
             // Members that indicate certain restrictions.
             bool nestedOperators;

src/logic/TimeOperatorFormula.cpp

@@ -0,0 +1,32 @@
+#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) : OperatorFormula(subformula, operatorInformation) {
+            STORM_LOG_THROW(this->getMeasureType() == MeasureType::Expectation || this->getMeasureType() == MeasureType::Variance, storm::exceptions::InvalidPropertyException, "Invalid measure type in ET-operator.");
+        }
+        
+        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);
+        }
+        
+        std::ostream& TimeOperatorFormula::writeToStream(std::ostream& out) const {
+            out << "T";
+            OperatorFormula::writeToStream(out);
+            return out;
+        }
+    }
+}

src/logic/ExpectedTimeOperatorFormula.h → src/logic/TimeOperatorFormula.h

@@ -7,15 +7,15 @@
 
 namespace storm {
     namespace logic {
-        class ExpectedTimeOperatorFormula : public OperatorFormula {
+        class TimeOperatorFormula : public OperatorFormula {
         public:
-            ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation());
+            TimeOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation());
             
-            virtual ~ExpectedTimeOperatorFormula() {
+            virtual ~TimeOperatorFormula() {
                 // Intentionally left empty.
             }
             
-            virtual bool isExpectedTimeOperatorFormula() const override;
+            virtual bool isTimeOperatorFormula() const override;
 
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             

src/modelchecker/AbstractModelChecker.cpp

@@ -21,6 +21,8 @@ namespace storm {
                     return this->computeProbabilities(checkTask);
                 } else if (formula.isRewardPathFormula()) {
                     return this->computeRewards(checkTask);
+                } else if (formula.isTimePathFormula()) {
+                    return this->computeTimes(checkTask);
                 }
             } else if (formula.isConditionalProbabilityFormula()) {
                 return this->computeConditionalProbabilities(checkTask.substituteFormula(formula.asConditionalFormula()));
@@ -114,7 +116,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(CheckTask<storm::logic::Formula> const& checkTask) {
+            storm::logic::Formula const& timeFormula = checkTask.getFormula();
+            if (timeFormula.isReachabilityTimeFormula()) {
+                return this->computeReachabilityTimes(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(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 +140,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()) {
@@ -203,11 +213,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().isReachabilityExpectedTimeFormula(), 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(checkTask.substituteFormula(stateFormula.getSubformula()));
             
             if (checkTask.isBoundSet()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");

src/modelchecker/AbstractModelChecker.h

@@ -51,9 +51,10 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(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(CheckTask<storm::logic::Formula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeReachabilityTimes(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 +64,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);
         };

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);
         }
         
@@ -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(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)));
         }
                 

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h

@@ -25,7 +25,7 @@ namespace storm {
             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> 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(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
             
         private:
             // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices.

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>());

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);

src/parser/FormulaParser.cpp

@@ -113,7 +113,7 @@ namespace storm {
             qi::rule<Iterator, storm::logic::MeasureType(), Skipper> measureType;
             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;
@@ -163,7 +163,7 @@ namespace storm {
             storm::logic::OperatorInformation createOperatorInformation(storm::logic::MeasureType const& measureType, 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<std::string> const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula> createExpectedTimeOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createTimeOperatorFormula(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);
@@ -329,8 +329,8 @@ namespace storm {
             rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation(storm::logic::MeasureType::Expectation) > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
             rewardOperator.name("reward operator");
             
-            expectedTimeOperator = (qi::lit("ET") > operatorInformation(storm::logic::MeasureType::Expectation) > 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") > operatorInformation(storm::logic::MeasureType::Expectation) > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::Time) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            timeOperator.name("time operator");
             
             probabilityOperator = (qi::lit("P") > operatorInformation(storm::logic::MeasureType::Value) > 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");
@@ -491,8 +491,8 @@ namespace storm {
             return std::shared_ptr<storm::logic::Formula>(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createExpectedTimeOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ExpectedTimeOperatorFormula(subformula, operatorInformation));
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createTimeOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::TimeOperatorFormula(subformula, operatorInformation));
         }
         
         std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) {