Merge branch 'master' into rubicon

CMakeLists.txt

@@ -194,10 +194,11 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang")
 	# using AppleClang
 	if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 7.3)
 		message(FATAL_ERROR "AppleClang version must be at least 7.3.")
-	elseif ((CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 11.0) OR (CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 11.0))
-		message(WARNING "Temporarily disabling stack checks for AppleClang 11.0 or higher.")
-		# TODO: In release mode, stack checks currently fail at runtime. Might be a compiler bug as there does not seem to be faulty behavior.
-		# TODO: This seems to be fixed for clang 11.0.3 (bundled with XCode 11.5). Check again, if the clang version coming with the command line tools is greater than 11.0.0.
+	elseif ((CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 11.0.0) OR (CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 11.0.0))
+		message(WARNING "Disabling stack checks for AppleClang version 11.0.0 or higher.")
+		# Stack checks are known to produce errors with the following Clang versions:
+		# 11.0.0: Runtime errors (stack_not_16_byte_aligned_error) when invoking storm in release mode
+		# 11.0.3: Catching exceptions thrown within PRISM parser does not work (The exception just falls through)
 		set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fno-stack-check")
 	endif()
 
@@ -276,13 +277,17 @@ elseif (STORM_COMPILER_GCC)
 endif ()
 
 if (STORM_USE_THIN_LTO)
-    set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto=thin")
-	message(STATUS "Storm - Enabling link-time optimizations using ThinLTO.")
+    if (STORM_COMPILER_CLANG OR STORM_COMPILER_APPLECLANG)
+        set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto=thin")
+        message(STATUS "Storm - Enabling link-time optimizations using ThinLTO.")
+    else()
+        message(FATAL_ERROR "Storm - ThinLTO only supported for Clang. Use regular LTO instead.")
+    endif()
 elseif (STORM_USE_LTO)
     set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto")
 
     # Fix for problems that occurred when using LTO on gcc. This should be removed when it
-    # is not needed anymore as it makes the the already long link-step potentially longer.
+    # is not needed anymore as it makes the already long link-step potentially longer.
     if (STORM_COMPILER_GCC)
         set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto-partition=none")
     endif()
@@ -440,15 +445,15 @@ set(STORM_VERSION_APPENDIX "${CMAKE_MATCH_5}") # might be empty
 if (STORM_GIT_VERSION_STRING MATCHES "NOTFOUND")
 	set(STORM_VERSION_SOURCE "VersionSource::Static")
 	set(STORM_VERSION_COMMITS_AHEAD 0)
-	set(STORM_VERSION_DIRTY boost::none)
+	set(STORM_VERSION_DIRTY DirtyState:Unknown)
 	include(version.cmake)
 	message(WARNING "Storm - Git version information not available, statically assuming version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.")
 else()
 	set(STORM_VERSION_SOURCE "VersionSource::Git")
 	if ("${STORM_VERSION_APPENDIX}" MATCHES "^.*dirty.*$")
-		set(STORM_VERSION_DIRTY "true")
+		set(STORM_VERSION_DIRTY "DirtyState::Dirty")
 	else()
-		set(STORM_VERSION_DIRTY "false")
+		set(STORM_VERSION_DIRTY "DirtyState::Clean")
 	endif()
 endif()
 

src/storm-gspn/parser/GspnParser.h

@@ -1,3 +1,5 @@
+#pragma once
+
 #include "storm-gspn/storage/gspn/GSPN.h"
 
 namespace storm {

src/storm-pars/utility/ModelInstantiator.cpp

@@ -137,10 +137,7 @@ namespace storm {
             template<typename ParametricSparseModelType, typename ConstantSparseModelType>
             ConstantSparseModelType const& ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::instantiate(storm::utility::parametric::Valuation<ParametricType> 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));
-                }
+                instantiate_helper(valuation);
                 
                 //Write the instantiated values to the matrices and vectors according to the stored mappings
                 for(auto& entryValuePair : this->matrixMapping){
@@ -170,6 +167,12 @@ namespace storm {
             template class ModelInstantiator<storm::models::sparse::Ctmc<storm::RationalFunction>, storm::models::sparse::Ctmc<storm::RationalNumber>>;
             template class ModelInstantiator<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>, storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
             template class ModelInstantiator<storm::models::sparse::StochasticTwoPlayerGame<storm::RationalFunction>, storm::models::sparse::StochasticTwoPlayerGame<storm::RationalNumber>>;
+
+            // For stormpy:
+            template class ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<storm::RationalFunction>>;
+            template class ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<storm::RationalFunction>>;
+            template class ModelInstantiator<storm::models::sparse::Ctmc<storm::RationalFunction>, storm::models::sparse::Ctmc<storm::RationalFunction>>;
+            template class ModelInstantiator<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>, storm::models::sparse::MarkovAutomaton<storm::RationalFunction>>;
 #endif
     } //namespace utility
 } //namespace storm

src/storm-pars/utility/ModelInstantiator.h

@@ -117,7 +117,29 @@ namespace storm {
                     
                     this->instantiatedModel = std::make_shared<ConstantSparseModelType>(std::move(components));
                 }
-                
+
+                template<typename PMT = ParametricSparseModelType>
+                typename std::enable_if<
+                        std::is_same<PMT,ConstantSparseModelType>::value
+                >::type
+                instantiate_helper(storm::utility::parametric::Valuation<ParametricType> const& valuation) {
+                    for(auto& functionResult : this->functions){
+                        functionResult.second=
+                                storm::utility::parametric::substitute(functionResult.first, valuation);
+                    }
+                }
+
+                template<typename PMT = ParametricSparseModelType>
+                typename std::enable_if<
+                        !std::is_same<PMT,ConstantSparseModelType>::value
+                >::type
+                instantiate_helper(storm::utility::parametric::Valuation<ParametricType> const& valuation) {
+                    for(auto& functionResult : this->functions){
+                        functionResult.second=storm::utility::convertNumber<ConstantType>(
+                                storm::utility::parametric::evaluate(functionResult.first, valuation));
+                    }
+                }
+
                 /*!
                  * 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.

src/storm-pars/utility/parametric.cpp

@@ -21,7 +21,13 @@ namespace storm {
             typename CoefficientType<storm::RationalFunction>::type evaluate<storm::RationalFunction>(storm::RationalFunction const& function, Valuation<storm::RationalFunction> const& valuation){
                 return function.evaluate(valuation);
             }
-            
+
+            template<>
+            typename storm::RationalFunction substitute<storm::RationalFunction>(storm::RationalFunction const& function, Valuation<storm::RationalFunction> const& valuation){
+                return function.substitute(valuation);
+            }
+
+
             template<>
             void gatherOccurringVariables<storm::RationalFunction>(storm::RationalFunction const& function, std::set<typename VariableType<storm::RationalFunction>::type>& variableSet){
                 function.gatherVariables(variableSet);

src/storm-pars/utility/parametric.h

@@ -35,7 +35,13 @@ namespace storm {
              */
             template<typename FunctionType>
             typename CoefficientType<FunctionType>::type evaluate(FunctionType const& function, Valuation<FunctionType> const& valuation);
-            
+
+            /*!
+             * Evaluates the given function wrt. the given valuation
+             */
+            template<typename FunctionType>
+            FunctionType substitute(FunctionType const& function, Valuation<FunctionType> const& valuation);
+
             /*!
              *  Add all variables that occur in the given function to the the given set
              */

src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp

@@ -19,7 +19,7 @@ namespace storm {
         }
 
         struct RationalFunctionConstructor {
-            RationalFunctionConstructor() : cache(std::make_shared<RawPolynomialCache>()) {
+            RationalFunctionConstructor(std::shared_ptr<RawPolynomialCache> const& cache) : cache(cache) {
 
             }
 
@@ -31,11 +31,25 @@ namespace storm {
             std::shared_ptr<RawPolynomialCache> cache;
         };
 
+        template<typename ValueType>
+        std::shared_ptr<RawPolynomialCache> getCache(storm::models::sparse::Pomdp<ValueType> const& model) {
+            return std::make_shared<RawPolynomialCache>();
+        }
+
+        template<>
+        std::shared_ptr<RawPolynomialCache> getCache(storm::models::sparse::Pomdp<storm::RationalFunction> const& model) {
+            for (auto const& entry : model.getTransitionMatrix()) {
+                if(!entry.getValue().isConstant()) {
+                    return entry.getValue().nominatorAsPolynomial().pCache();
+                }
+            }
+            return std::make_shared<RawPolynomialCache>();
+        }
 
         template<typename ValueType>
         std::unordered_map<uint32_t, std::vector<storm::RationalFunction>> ApplyFiniteSchedulerToPomdp<ValueType>::getObservationChoiceWeights(PomdpFscApplicationMode applicationMode ) const {
             std::unordered_map<uint32_t, std::vector<storm::RationalFunction>> res;
-            RationalFunctionConstructor ratFuncConstructor;
+            RationalFunctionConstructor ratFuncConstructor(getCache(pomdp));
 
             for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) {
                 auto observation = pomdp.getObservation(state);
@@ -46,7 +60,7 @@ namespace storm {
                     storm::RationalFunction lastWeight = storm::utility::one<storm::RationalFunction>();
                     for (uint64_t a = 0; a < pomdp.getNumberOfChoices(state) - 1; ++a) {
                         std::string varName = "p" + std::to_string(observation) + "_" + std::to_string(a);
-                        storm::RationalFunction var = ratFuncConstructor.translate(carl::freshRealVariable(varName));
+                        storm::RationalFunction var = ratFuncConstructor.translate(storm::createRFVariable(varName));
                         if (applicationMode == PomdpFscApplicationMode::SIMPLE_LINEAR) {
                             weights.push_back(collected * var);
                             collected *= storm::utility::one<storm::RationalFunction>() - var;
@@ -133,5 +147,6 @@ namespace storm {
 
         template
         class ApplyFiniteSchedulerToPomdp<double>;
+        template class ApplyFiniteSchedulerToPomdp<storm::RationalFunction>;
     }
 }

src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp

@@ -141,8 +141,11 @@ namespace storm {
             for (auto const& labelName : pomdp.getStateLabeling().getLabels()) {
                 storm::storage::BitVector newStates = pomdp.getStateLabeling().getStates(labelName);
                 newStates.resize(data.simpleMatrix.getRowGroupCount(), false);
-                for (uint64_t newState = pomdp.getNumberOfStates(); newState < data.simpleMatrix.getRowGroupCount(); ++newState ) {
-                    newStates.set(newState, newStates[data.simpleStateToOriginalState[newState]]);
+                if (labelName != "init") {
+                    for (uint64_t newState = pomdp.getNumberOfStates();
+                         newState < data.simpleMatrix.getRowGroupCount(); ++newState) {
+                        newStates.set(newState, newStates[data.simpleStateToOriginalState[newState]]);
+                    }
                 }
                 labeling.addLabel(labelName, std::move(newStates));
 
@@ -173,5 +176,6 @@ namespace storm {
 
         template
         class BinaryPomdpTransformer<double>;
+        template class BinaryPomdpTransformer<storm::RationalFunction>;
     }
 }

src/storm-pomdp/transformer/MakePOMDPCanonic.cpp

@@ -289,5 +289,6 @@ namespace storm {
 
         template class MakePOMDPCanonic<double>;
         template class MakePOMDPCanonic<storm::RationalNumber>;
+        template class MakePOMDPCanonic<storm::RationalFunction>;
     }
 }

src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp

@@ -187,6 +187,7 @@ namespace storm {
             }
 
             template class PomdpMemoryUnfolder<storm::RationalNumber>;
+        template class PomdpMemoryUnfolder<storm::RationalFunction>;
 
         template
         class PomdpMemoryUnfolder<double>;

src/storm-version-info/storm-version.cpp.in

@@ -11,7 +11,7 @@ namespace storm {
     const StormVersion::VersionSource StormVersion::versionSource = @STORM_VERSION_SOURCE@;
     const std::string StormVersion::gitRevisionHash = "@STORM_VERSION_GIT_HASH@";
     const unsigned StormVersion::commitsAhead = @STORM_VERSION_COMMITS_AHEAD@;
-    const boost::optional<bool> StormVersion::dirty = @STORM_VERSION_DIRTY@;
+    const StormVersion::DirtyState StormVersion::dirty = @STORM_VERSION_DIRTY@;
     const std::string StormVersion::systemName = "@CMAKE_SYSTEM_NAME@";
     const std::string StormVersion::systemVersion = "@CMAKE_SYSTEM_VERSION@";
     const std::string StormVersion::cxxCompiler = "@STORM_COMPILER_ID@ @CMAKE_CXX_COMPILER_VERSION@";

src/storm-version-info/storm-version.h

@@ -3,8 +3,6 @@
 #include <string>
 #include <sstream>
 
-#include <boost/optional.hpp>
-
 namespace storm {
 
     struct StormVersion {
@@ -36,8 +34,14 @@ namespace storm {
         /// How many commits passed since the tag was last set.
         const static unsigned commitsAhead;
 
-        /// 0 iff there no files were modified in the checkout, 1 otherwise. If none, no information about dirtyness is given.
-        const static boost::optional<bool> dirty;
+        enum class DirtyState {
+            Clean, /// no files were modified in the checkout
+            Dirty, /// some files were modified
+            Unknown /// No information about dirtyness is given.
+        };
+        
+        /// Indicates whether files were modified
+        const static DirtyState dirty;
 
         /// The system which has compiled Storm.
         const static std::string systemName;
@@ -77,14 +81,10 @@ namespace storm {
             } else {
                 sstream << " built from archive";
             }
-            if (dirty) {
-                if (dirty.get()) {
-                    sstream << " (dirty)";
-                } else {
-                    sstream << " (clean)";
-                }
-            } else {
-                sstream << " (potentially dirty)";
+            switch (dirty) {
+                case DirtyState::Clean: sstream << " (clean)"; break;
+                case DirtyState::Dirty: sstream << " (dirty)"; break;
+                default: sstream << " (potentially dirty)"; break;
             }
             return sstream.str();
         }

src/storm/CMakeLists.txt

@@ -1,3 +1,15 @@
+# Storm versions before 1.6.0 generated an in-source  .cpp file containing version information.
+# When users upgrade from such a version, the generated file will still be there.
+# We now delete this file to prevent building issues as there is no corresponding .h file (anymore).
+if ((EXISTS "${PROJECT_SOURCE_DIR}/src/storm/utility/storm-version.cpp"))
+	file(READ "${PROJECT_SOURCE_DIR}/src/storm/utility/storm-version.cpp" STORM_OLD_VERSION_FILE)
+	string(FIND "${STORM_OLD_VERSION_FILE}" "// AUTO GENERATED -- DO NOT CHANGE" STORM_OLD_VERSION_FILE_DETECTED)
+	if (STORM_OLD_VERSION_FILE_DETECTED EQUAL 0)
+		message(WARNING "Storm - The file ${PROJECT_SOURCE_DIR}/src/storm/utility/storm-version.cpp was probably generated by an old Storm version and will be deleted now.")
+		file(REMOVE "${PROJECT_SOURCE_DIR}/src/storm/utility/storm-version.cpp")
+	endif(STORM_OLD_VERSION_FILE_DETECTED EQUAL 0)
+endif()
+
 file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm/*.h ${PROJECT_SOURCE_DIR}/src/storm/*.cpp)
 
 register_source_groups_from_filestructure("${ALL_FILES}" storm)

src/storm/adapters/RationalFunctionAdapter.cpp

@@ -0,0 +1,7 @@
+#include "storm/adapters/RationalFunctionAdapter.h"
+
+namespace storm {
+    RationalFunctionVariable createRFVariable(std::string const& name) {
+        return carl::freshRealVariable(name);
+    }
+}

src/storm/adapters/RationalFunctionAdapter.h

@@ -41,6 +41,8 @@ namespace carl {
 namespace storm {
     typedef carl::Variable RationalFunctionVariable;
 
+    RationalFunctionVariable createRFVariable(std::string const& name);
+
 #if defined(STORM_HAVE_CLN) && defined(STORM_USE_CLN_RF)
     typedef cln::cl_RA RationalFunctionCoefficient;
 #elif defined(STORM_HAVE_GMP) && !defined(STORM_USE_CLN_RF)

src/storm/builder/DdPrismModelBuilder.cpp

@@ -56,7 +56,7 @@ namespace storm {
             void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter<Type, storm::RationalFunction>& rowExpressionAdapter) {
                 for (auto const& constant : program.getConstants()) {
                     if (!constant.isDefined()) {
-                        storm::RationalFunctionVariable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName());
+                        storm::RationalFunctionVariable carlVariable = storm::createRFVariable(constant.getExpressionVariable().getName());
                         parameters.insert(carlVariable);
                         auto rf = convertVariableToPolynomial(carlVariable);
                         rowExpressionAdapter.setValue(constant.getExpressionVariable(), rf);

src/storm/storage/expressions/Expression.cpp

@@ -449,6 +449,10 @@ namespace storm {
         Expression sum(std::vector<storm::expressions::Expression> const& expressions) {
             return applyAssociative(expressions, [] (Expression const& e1, Expression const& e2) { return e1 + e2; });
         }
+
+        Expression modulo(Expression const& first, Expression const& second) {
+            return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().minimumMaximum(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Modulo)));
+        }
         
         Expression apply(std::vector<storm::expressions::Expression> const& expressions, std::function<Expression (Expression const&, Expression const&)> const& function) {
             STORM_LOG_THROW(!expressions.empty(), storm::exceptions::InvalidArgumentException, "Cannot build function application of empty expression list.");

src/storm/storage/expressions/Expression.h

@@ -436,6 +436,7 @@ namespace storm {
         Expression floor(Expression const& first);
         Expression ceil(Expression const& first);
         Expression round(Expression const& first);
+        Expression modulo(Expression const& first, Expression const& second);
         Expression minimum(Expression const& first, Expression const& second);
         Expression maximum(Expression const& first, Expression const& second);
         Expression disjunction(std::vector<storm::expressions::Expression> const& expressions);

src/storm/storage/expressions/ToRationalFunctionVisitor.cpp

@@ -82,7 +82,7 @@ namespace storm {
             if (variablePair != variableToVariableMap.end()) {
                 return convertVariableToPolynomial(variablePair->second);
             } else {
-                storm::RationalFunctionVariable carlVariable = carl::freshRealVariable(expression.getVariableName());
+                storm::RationalFunctionVariable carlVariable = storm::createRFVariable(expression.getVariableName());
                 variableToVariableMap.emplace(expression.getVariable(), carlVariable);
                 return convertVariableToPolynomial(carlVariable);
             }

src/test/storm/storage/ExpressionTest.cpp

@@ -257,6 +257,10 @@ TEST(Expression, OperatorTest) {
     EXPECT_TRUE(tempExpression.hasIntegerType());
     ASSERT_NO_THROW(tempExpression = intVarExpression ^ rationalVarExpression);
     EXPECT_TRUE(tempExpression.hasRationalType());
+
+    STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::modulo(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
+    ASSERT_NO_THROW(tempExpression = storm::expressions::maximum(threeExpression, threeExpression));
+    EXPECT_TRUE(tempExpression.hasIntegerType());
 }
 
 TEST(Expression, SubstitutionTest) {