Further work on reintegrating parametric model checking into main executable.

Former-commit-id: be95ce2722

CMakeLists.txt

@@ -33,7 +33,6 @@ set(MSAT_ROOT "" CACHE STRING "The root directory of MathSAT (if available).")
 set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.")
 set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.")
 set(CUSTOM_BOOST_ROOT "" CACHE STRING "A custom path to the Boost root directory.")
-option(PARAMETRIC_SYSTEMS "Sets whether models with parameters are supported." ON)
 #############################################################
 ##
 ##	Inclusion of required libraries
@@ -89,17 +88,15 @@ else()
     set(ENABLE_MSAT ON)
 endif()
 
-if(${PARAMETRIC_SYSTEMS})
-    find_package(carl REQUIRED)
+find_package(carl QUIET)
+if(carl_FOUND)
+    message(STATUS "StoRM - Activating CArL.")
     set(STORM_HAVE_CARL ON)
 endif()
 
 message(STATUS "StoRM - CMAKE_BUILD_TYPE: ${CMAKE_BUILD_TYPE}")
 message(STATUS "StoRM - CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}")
 
-
-
-
 #############################################################
 ##
 ##	Compiler specific settings and definitions
@@ -258,8 +255,7 @@ include_directories("${PROJECT_BINARY_DIR}/include")
 file(GLOB_RECURSE STORM_HEADERS ${PROJECT_SOURCE_DIR}/src/*.h)
 file(GLOB_RECURSE STORM_SOURCES_WITHOUT_MAIN ${PROJECT_SOURCE_DIR}/src/*/*.cpp)
 file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp)
-file(GLOB_RECURSE STORM_PARAMETRIC_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/stormParametric.cpp)
-set(STORM_SOURCES "${STORM_SOURCES_WITHOUT_MAIN};${STORM_MAIN_FILE};${STORM_PARAMETRIC_MAIN_FILE};")
+set(STORM_SOURCES "${STORM_SOURCES_WITHOUT_MAIN};${STORM_MAIN_FILE};")
 file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp)
 file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp)
 file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp)
@@ -379,11 +375,6 @@ add_library(storm ${STORM_SOURCES_WITHOUT_MAIN} ${STORM_HEADERS})
 add_executable(storm-main ${STORM_MAIN_FILE})
 target_link_libraries(storm-main storm)
 set_target_properties(storm-main PROPERTIES OUTPUT_NAME "storm")
-if(PARAMETRIC_SYSTEMS)
-	add_executable(storm-main-param ${STORM_PARAMETRIC_MAIN_FILE})
-	target_link_libraries(storm-main-param storm)
-	set_target_properties(storm-main-param PROPERTIES OUTPUT_NAME "pstorm")
-endif()
 add_executable(storm-functional-tests ${STORM_FUNCTIONAL_TEST_MAIN_FILE} ${STORM_FUNCTIONAL_TEST_FILES})
 target_link_libraries(storm-functional-tests storm)
 add_executable(storm-performance-tests ${STORM_PERFORMANCE_TEST_MAIN_FILE} ${STORM_PERFORMANCE_TEST_FILES})
@@ -471,8 +462,8 @@ endif(ENABLE_Z3)
 ##
 #############################################################
 
-if(PARAMETRIC_SYSTEMS)
-    message(STATUS "StoRM - Linking with carl")
+if(STORM_HAVE_CARL)
+    message(STATUS "StoRM - Linking with carl.")
     include_directories("${carl_INCLUDE_DIR}")
     target_link_libraries(storm lib_carl)
     target_link_libraries(storm-functional-tests lib_carl)

src/builder/ExplicitPrismModelBuilder.cpp

@@ -103,7 +103,11 @@ namespace storm {
             }
             
             // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
-            if (!std::is_same<ValueType, RationalFunction>::value && preparedProgram.hasUndefinedConstants()) {
+#ifdef STORM_HAVE_CARL
+            if (!std::is_same<ValueType, storm::RationalFunction>::value && preparedProgram.hasUndefinedConstants()) {
+#else
+            if (preparedProgram.hasUndefinedConstants()) {
+#endif
                 std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram.getUndefinedConstants();
                 std::stringstream stream;
                 bool printComma = false;
@@ -788,6 +792,9 @@ namespace storm {
         
         // Explicitly instantiate the class.
         template class ExplicitPrismModelBuilder<double, uint32_t>;
+        
+#ifdef STORM_HAVE_CARL
         template class ExplicitPrismModelBuilder<RationalFunction, uint32_t>;
+#endif
     }
 }

src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp

@@ -184,11 +184,13 @@ namespace storm {
             }
         }
         
+#ifdef STORM_HAVE_CARL
         template<>
         std::unique_ptr<CheckResult> ExplicitQuantitativeCheckResult<storm::RationalFunction>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const {
             // Since it is not possible to compare rational functions against bounds, we simply call the base class method.
             return QuantitativeCheckResult::compareAgainstBound(comparisonType, bound);
         }
+#endif
         
         template<typename ValueType>
         ValueType& ExplicitQuantitativeCheckResult<ValueType>::operator[](storm::storage::sparse::state_type state) {

src/settings/modules/GeneralSettings.cpp

@@ -41,7 +41,10 @@ namespace storm {
             const std::string GeneralSettings::statisticsOptionShortName = "stats";
             const std::string GeneralSettings::bisimulationOptionName = "bisimulation";
             const std::string GeneralSettings::bisimulationOptionShortName = "bisim";
+            
+#ifdef STORM_HAVE_CARL
             const std::string GeneralSettings::parametricOptionName = "parametric";
+#endif
 
             GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
@@ -85,7 +88,10 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build());
+
+#ifdef STORM_HAVE_CARL
                 this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to use the parametric engine.").build());
+#endif
             }
             
             bool GeneralSettings::isHelpSet() const {
@@ -245,10 +251,12 @@ namespace storm {
                 return this->getOption(bisimulationOptionName).getHasOptionBeenSet();
             }
             
+#ifdef STORM_HAVE_CARL
             bool GeneralSettings::isParametricSet() const {
                 return this->getOption(parametricOptionName).getHasOptionBeenSet();
             }
-
+#endif
+            
             bool GeneralSettings::check() const {
                 // Ensure that the model was given either symbolically or explicitly.
                 STORM_LOG_THROW(!isSymbolicSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format, but not both.");

src/settings/modules/GeneralSettings.h

@@ -1,6 +1,7 @@
 #ifndef STORM_SETTINGS_MODULES_GENERALSETTINGS_H_
 #define STORM_SETTINGS_MODULES_GENERALSETTINGS_H_
 
+#include "storm-config.h"
 #include "src/settings/modules/ModuleSettings.h"
 
 namespace storm {
@@ -286,12 +287,14 @@ namespace storm {
                  */
                 bool isBisimulationSet() const;
                 
+#ifdef STORM_HAVE_CARL
                 /*!
                  * Retrieves whether the option enabling parametric model checking is set.
                  *
                  * @return True iff the option was set.
                  */
                 bool isParametricSet() const;
+#endif
                 
                 bool check() const override;
 
@@ -332,7 +335,10 @@ namespace storm {
                 static const std::string statisticsOptionShortName;
                 static const std::string bisimulationOptionName;
                 static const std::string bisimulationOptionShortName;
+                
+#ifdef STORM_HAVE_CARL
                 static const std::string parametricOptionName;
+#endif
             };
             
         } // namespace modules

src/storage/SparseMatrix.cpp

@@ -720,14 +720,7 @@ namespace storm {
             return std::make_pair(std::move(resultLU), dInvBuilder.build());
         }
         
-#ifdef PARAMETRIC_SYSTEMS
-        template<>
-        typename std::pair<storm::storage::SparseMatrix<Polynomial>, storm::storage::SparseMatrix<Polynomial>> SparseMatrix<Polynomial>::getJacobiDecomposition() const {
-            // NOT SUPPORTED
-            // TODO do whatever storm does in such cases.
-            assert(false);
-        }
-        
+#ifdef STORM_HAVE_CARL
         template<>
         typename std::pair<storm::storage::SparseMatrix<RationalFunction>, storm::storage::SparseMatrix<RationalFunction>> SparseMatrix<RationalFunction>::getJacobiDecomposition() const {
             // NOT SUPPORTED
@@ -992,12 +985,6 @@ namespace storm {
         template class SparseMatrixBuilder<RationalFunction>;
         template class SparseMatrix<RationalFunction>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<RationalFunction> const& matrix);
-        
-        template class MatrixEntry<typename SparseMatrix<Polynomial>::index_type, Polynomial>;
-        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, Polynomial> const& entry);
-        template class SparseMatrixBuilder<Polynomial>;
-        template class SparseMatrix<Polynomial>;
-        template std::ostream& operator<<(std::ostream& out, SparseMatrix<Polynomial> const& matrix);
 #endif
         
         

src/storage/StronglyConnectedComponentDecomposition.cpp

@@ -212,7 +212,6 @@ namespace storm {
         // Explicitly instantiate the SCC decomposition.
         template class StronglyConnectedComponentDecomposition<double>;
 #ifdef STORM_HAVE_CARL
-        template class StronglyConnectedComponentDecomposition<storm::Polynomial>;
         template class StronglyConnectedComponentDecomposition<storm::RationalFunction>;
 #endif
     } // namespace storage

src/storage/expressions/ExpressionEvaluator.cpp

@@ -7,7 +7,7 @@ namespace storm {
             // Intentionally left empty.
         }
         
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
         ExpressionEvaluator<RationalFunction>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalFunction>(manager) {
             // Intentionally left empty.
         }

src/utility/ConstantsComparator.h

@@ -41,7 +41,7 @@ namespace storm {
         template<typename ValueType>
         ValueType pow(ValueType const& value, uint_fast64_t exponent);
         
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
         template<>
         RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
 #endif

src/utility/cli.h

@@ -332,10 +332,12 @@ namespace storm {
                 }
             }
             
+#ifdef STORM_HAVE_CARL
             template<>
             void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::AbstractModel<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> formula) {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
             }
+#endif
             
             template<typename ValueType>
             void verifyModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::AbstractModel<ValueType>> model, std::shared_ptr<storm::logic::Formula> formula) {
@@ -376,6 +378,7 @@ namespace storm {
                 }
             }
             
+#ifdef STORM_HAVE_CARL
             template<>
             void verifyModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::AbstractModel<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> formula) {
                 storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
@@ -402,6 +405,7 @@ namespace storm {
                     std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
                 }
             }
+#endif
             
             template<typename ValueType>
             void buildAndCheckSymbolicModel(boost::optional<storm::prism::Program> const& program, boost::optional<std::shared_ptr<storm::logic::Formula>> formula) {
@@ -467,11 +471,15 @@ namespace storm {
                 }
                 
                 if (settings.isSymbolicSet()) {
+#ifdef STORM_HAVE_CARL
                     if (settings.isParametricSet()) {
                         buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formula);
                     } else {
+#endif
                         buildAndCheckSymbolicModel<double>(program.get(), formula);
+#ifdef STORM_HAVE_CARL
                     }
+#endif
                 } else if (settings.isExplicitSet()) {
                     buildAndCheckExplicitModel<double>(formula);
                 } else {