Merge branch 'master' into multi-objective-lra

src/storm-parsers/parser/ExpressionCreator.cpp

@@ -141,18 +141,18 @@ namespace storm {
             return manager.boolean(false);
         }
         
-        storm::expressions::Expression ExpressionCreator::createUnaryExpression(boost::optional<storm::expressions::OperatorType> const& operatorType, storm::expressions::Expression const& e1, bool& pass) const {
+        storm::expressions::Expression ExpressionCreator::createUnaryExpression(std::vector<storm::expressions::OperatorType> const& operatorTypes, storm::expressions::Expression const& e1, bool& pass) const {
             if (this->createExpressions) {
                 try {
-                    if (operatorType) {
-                        switch (operatorType.get()) {
-                            case storm::expressions::OperatorType::Not: return !e1; break;
-                            case storm::expressions::OperatorType::Minus: return -e1; break;
+                    storm::expressions::Expression result = e1;
+                    for (auto const& op : operatorTypes) {
+                        switch (op) {
+                            case storm::expressions::OperatorType::Not: result = !result; break;
+                            case storm::expressions::OperatorType::Minus: result = -result; break;
                             default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
                         }
-                    } else {
-                        return e1;
                     }
+                    return result;
                 } catch (storm::exceptions::InvalidTypeException const& e) {
                     pass = false;
                 }

src/storm-parsers/parser/ExpressionCreator.h

@@ -64,7 +64,7 @@ namespace storm {
             storm::expressions::Expression createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
             storm::expressions::Expression createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
             storm::expressions::Expression createPowerModuloExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
-            storm::expressions::Expression createUnaryExpression(boost::optional<storm::expressions::OperatorType> const& operatorType, storm::expressions::Expression const& e1, bool& pass) const;
+            storm::expressions::Expression createUnaryExpression(std::vector<storm::expressions::OperatorType> const& operatorType, storm::expressions::Expression const& e1, bool& pass) const;
             storm::expressions::Expression createRationalLiteralExpression(storm::RationalNumber const& value, bool& pass) const;
             storm::expressions::Expression createIntegerLiteralExpression(int value, bool& pass) const;
             storm::expressions::Expression createBooleanLiteralExpression(bool value, bool& pass) const;

src/storm-parsers/parser/ExpressionParser.cpp

@@ -87,7 +87,7 @@ namespace storm {
             atomicExpression = floorCeilExpression | roundExpression | prefixPowerModuloExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | identifierExpression | literalExpression;
             atomicExpression.name("atomic expression");
             
-            unaryExpression = (-unaryOperator_ >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createUnaryExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)];
+            unaryExpression = (*unaryOperator_ >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createUnaryExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)];
             unaryExpression.name("unary expression");
             
             if (allowBacktracking) {

src/storm/solver/helper/OptimisticValueIterationHelper.cpp

@@ -3,6 +3,7 @@
 #include "storm/utility/vector.h"
 #include "storm/utility/SignalHandler.h"
 #include "storm/environment/solver/OviSolverEnvironment.h"
+#include "storm/utility/ProgressMeasurement.h"
 
 #include "storm/exceptions/NotSupportedException.h"
 
@@ -260,6 +261,8 @@ namespace storm {
     
                 SolverStatus status = SolverStatus::InProgress;
     
+                storm::utility::ProgressMeasurement progress("iterations.");
+                progress.startNewMeasurement(0);
                 while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) {
                     // Perform value iteration until convergence
                     lastValueIterationIterations = dir ? iterationHelper.repeatedIterate(dir.get(), *lowerX, b, iterationPrecision, relative) : iterationHelper.repeatedIterate(*lowerX, b, iterationPrecision, relative);
@@ -348,8 +351,8 @@ namespace storm {
                     if (storm::utility::resources::isTerminate()) {
                         status = SolverStatus::Aborted;
                     }
+                    progress.updateProgress(overallIterations);
                 } // end while
-                
                 // Swap the results into the output vectors (if necessary).
                 assert(initLowerX != lowerX || (initLowerX == lowerX && initUpperX == upperX));
                 if (initLowerX != lowerX) {