Merge remote-tracking branch 'origin/future' into TimParamSysAndSMT

Former-commit-id: ac3b6383ee

CMakeLists.txt

@@ -85,7 +85,7 @@ if(CMAKE_COMPILER_IS_GNUCC)
     set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops")
     set(CMAKE_C_FLAGS_RELEASE "${CMAKE_C_FLAGS_RELEASE} -funroll-loops")
     add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE)
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -Wall -pedantic -Wno-deprecated-declarations -Wno-unused-local-typedefs")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -Wall -pedantic -Wno-deprecated-declarations -Wno-unused-local-typedefs -Wno-unknown-pragmas")
     set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic -Wno-deprecated-declarations")
 
     # Turn on popcnt instruction if desired (yes by default)

src/cli/entrypoints.h

@@ -3,6 +3,8 @@
 
 #include "src/utility/storm.h"
 
+#include "src/exceptions/NotImplementedException.h"
+
 namespace storm {
     namespace cli {
 
@@ -74,6 +76,11 @@ namespace storm {
         }
 #endif
 
+        template<storm::dd::DdType DdType>
+        void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented.");
+        }
+
         template<storm::dd::DdType DdType>
         void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
             for (auto const& formula : formulas) {
@@ -135,65 +142,71 @@ namespace storm {
     
         template<typename ValueType, storm::dd::DdType LibraryType>
         void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
-            storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
-            STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
+            storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
             
-            std::cout << "PrintingInfo;Filename;Constants;NumStates;NumTransitions" << std::endl;
-            std::cout << "INPUTMODEL_INFO;" << 
+            if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) {
+                verifySymbolicModelWithAbstractionRefinementEngine(program, formulas);
+            } else {
+                storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
+                STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
+                
+                std::cout << "PrintingInfo;Filename;Constants;NumStates;NumTransitions" << std::endl;
+                std::cout << "INPUTMODEL_INFO;" << 
                     storm::settings::generalSettings().getSymbolicModelFilename() << ";" <<
                     storm::settings::generalSettings().getConstantDefinitionString() << ";" <<
                     modelProgramPair.model->getNumberOfStates() << ";" <<
                     modelProgramPair.model->getNumberOfTransitions() << ";" << std::endl;
-            
-            // Preprocess the model if needed.
-            BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas);
-            
-            // Print some information about the model.
-            modelProgramPair.model->printModelInformationToStream(std::cout);
-            
-            // Verify the model, if a formula was given.
-            if (!formulas.empty()) {
-                // There may be constants of the model appearing in the formulas, so we replace all their occurrences
-                // by their definitions in the translated program.
                 
-                // Start by building a mapping from constants of the (translated) model to their defining expressions.
-                std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
-                for (auto const& constant : modelProgramPair.program.getConstants()) {
-                    if (constant.isDefined()) {
-                        constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
-                    }
-                }
+                // Preprocess the model if needed.
+                BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas);
                 
-                std::vector<std::shared_ptr<storm::logic::Formula>> preparedFormulas;
-                for (auto const& formula : formulas) {
-                    preparedFormulas.emplace_back(formula->substitute(constantSubstitution));
-                }
+                // Print some information about the model.
+                modelProgramPair.model->printModelInformationToStream(std::cout);
                 
-                if (modelProgramPair.model->isSparseModel()) {
-                    if(storm::settings::generalSettings().isCounterexampleSet()) {
-                        // If we were requested to generate a counterexample, we now do so for each formula.
-                        for(auto const& formula : preparedFormulas) {
-                            generateCounterexample<ValueType>(program, modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
+                // Verify the model, if a formula was given.
+                if (!formulas.empty()) {
+                    // There may be constants of the model appearing in the formulas, so we replace all their occurrences
+                    // by their definitions in the translated program.
+                    
+                    // Start by building a mapping from constants of the (translated) model to their defining expressions.
+                    std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
+                    for (auto const& constant : modelProgramPair.program.getConstants()) {
+                        if (constant.isDefined()) {
+                            constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
                         }
-                    } else {
-                        verifySparseModel<ValueType>(modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), preparedFormulas);
                     }
-                } else if (modelProgramPair.model->isSymbolicModel()) {
-                    if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
-                        verifySymbolicModelWithHybridEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
+                    
+                    std::vector<std::shared_ptr<storm::logic::Formula>> preparedFormulas;
+                    for (auto const& formula : formulas) {
+                        preparedFormulas.emplace_back(formula->substitute(constantSubstitution));
+                    }
+                    
+                    if (modelProgramPair.model->isSparseModel()) {
+                        if(settings.isCounterexampleSet()) {
+                            // If we were requested to generate a counterexample, we now do so for each formula.
+                            for(auto const& formula : preparedFormulas) {
+                                generateCounterexample<ValueType>(program, modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
+                            }
+                        } else {
+                            verifySparseModel<ValueType>(modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), preparedFormulas);
+                        }
+                    } else if (modelProgramPair.model->isSymbolicModel()) {
+                        if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
+                            verifySymbolicModelWithHybridEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
+                        } else {
+                            verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
+                        }
                     } else {
-                        verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
                     }
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
                 }
+                std::cout << "PrintingInfo;Filename;Constants;NumStates;NumTransitions" << std::endl;
+                std::cout << "DONE_MODEL_INFO;" << 
+                        storm::settings::generalSettings().getSymbolicModelFilename() << ";" <<
+                        storm::settings::generalSettings().getConstantDefinitionString() << ";" <<
+                        modelProgramPair.model->getNumberOfStates() << ";" <<
+                        modelProgramPair.model->getNumberOfTransitions() << ";" << std::endl;
             }
-            std::cout << "PrintingInfo;Filename;Constants;NumStates;NumTransitions" << std::endl;
-            std::cout << "DONE_MODEL_INFO;" << 
-                    storm::settings::generalSettings().getSymbolicModelFilename() << ";" <<
-                    storm::settings::generalSettings().getConstantDefinitionString() << ";" <<
-                    modelProgramPair.model->getNumberOfStates() << ";" <<
-                    modelProgramPair.model->getNumberOfTransitions() << ";" << std::endl;
         }
         
         template<typename ValueType>

src/parser/SpiritParserDefinitions.h

@@ -1,6 +1,9 @@
 #ifndef STORM_PARSER_SPIRITPARSERDEFINITIONS_H_
 #define	STORM_PARSER_SPIRITPARSERDEFINITIONS_H_
 
+#pragma clang diagnostic push
+#pragma clang diagnostic ignored "-W#pragma-messages"
+
 // Include boost spirit.
 #define BOOST_SPIRIT_USE_PHOENIX_V3
 #include <boost/typeof/typeof.hpp>
@@ -9,6 +12,8 @@
 #include <boost/spirit/include/support_line_pos_iterator.hpp>
 #include <boost/spirit/home/classic/iterator/position_iterator.hpp>
 
+#pragma clang diagnostic pop
+
 namespace qi = boost::spirit::qi;
 namespace phoenix = boost::phoenix;
 

src/settings/modules/GeneralSettings.cpp

@@ -97,9 +97,9 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build());
                 
-                std::vector<std::string> engines = {"sparse", "hybrid", "dd"};
+                std::vector<std::string> engines = {"sparse", "hybrid", "dd", "abs"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName)
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd, ar}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build());
                 
                 std::vector<std::string> linearEquationSolver = {"gmm++", "native"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
@@ -351,10 +351,11 @@ namespace storm {
                     engine = GeneralSettings::Engine::Hybrid;
                 } else if (engineStr == "dd") {
                     engine = GeneralSettings::Engine::Dd;
+                } else if (engineStr == "abs") {
+                    engine = GeneralSettings::Engine::AbstractionRefinement;
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engineStr << "'.");
                 }
-
             }
 
             bool GeneralSettings::check() const {

src/settings/modules/GeneralSettings.h

@@ -27,7 +27,7 @@ namespace storm {
                 // An enumeration of all engines.
 
                 enum class Engine {
-                    Sparse, Hybrid, Dd
+                    Sparse, Hybrid, Dd, AbstractionRefinement
                 };
 
                 /*!

src/storage/BitVectorHashMap.cpp

@@ -7,7 +7,7 @@
 namespace storm {
     namespace storage {
         template<class ValueType, class Hash1, class Hash2>
-        const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191};
+        const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 102863003};
         
         template<class ValueType, class Hash1, class Hash2>
         BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) {

src/utility/storm.h

@@ -236,6 +236,9 @@ namespace storm {
                 STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model");
                 return verifySymbolicModelWithDdEngine(ddModel, formula);
             }
+            case storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement: {
+                STORM_LOG_ASSERT(false, "This position should not be reached, as at this point no model has been built.");
+            }
         }
     }