some more work on games

Former-commit-id: 6741b1f0bc

CMakeLists.txt

@@ -456,7 +456,6 @@ endif()
 
 if(STORM_HAVE_CARL)
     message(STATUS "StoRM - Linking with carl.")
-	message("${carl_INCLUDE_DIR}")
     include_directories("${carl_INCLUDE_DIR}")
     list(APPEND STORM_LINK_LIBRARIES ${carl_LIBRARIES})
 endif()

src/CMakeLists.txt

@@ -21,6 +21,7 @@ file(GLOB STORM_MODELCHECKER_CSL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/cs
 file(GLOB_RECURSE STORM_MODELCHECKER_CSL_HELPER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/helper/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/helper/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_REACHABILITY_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_PROPOSITIONAL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.cpp)
+file(GLOB_RECURSE STORM_MODELCHECKER_ABSTRACTION_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/abstraction/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/abstraction/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_RESULTS_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.cpp)
 file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp)
 file(GLOB_RECURSE STORM_PERMISSIVESCHEDULER_FILES ${PROJECT_SOURCE_DIR}/src/permissivesched/*.h ${PROJECT_SOURCE_DIR}/src/permissivesched/*.cpp)
@@ -69,6 +70,7 @@ source_group(modelchecker\\csl FILES ${STORM_MODELCHECKER_CSL_FILES})
 source_group(modelchecker\\csl\\helper FILES ${STORM_MODELCHECKER_CSL_HELPER_FILES})
 source_group(modelchecker\\reachability FILES ${STORM_MODELCHECKER_REACHABILITY_FILES})
 source_group(modelchecker\\propositional FILES ${STORM_MODELCHECKER_PROPOSITIONAL_FILES})
+source_group(modelchecker\\abstraction FILES ${STORM_MODELCHECKER_ABSTRACTION_FILES})
 source_group(modelchecker\\results FILES ${STORM_MODELCHECKER_RESULTS_FILES})
 source_group(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES})
 source_group(permissiveschedulers FILES ${STORM_PERMISSIVESCHEDULER_FILES})

src/cli/cli.cpp

@@ -7,7 +7,7 @@
 #include "src/exceptions/OptionParserException.h"
 
 #include "src/utility/storm-version.h"
-
+#include "src/utility/resources.h"
 
 // Includes for the linked libraries and versions header.
 #ifdef STORM_HAVE_INTELTBB
@@ -212,6 +212,12 @@ namespace storm {
 
                 storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
 
+                // If we were given a time or memory limit, we put it in place now.
+                // FIXME: insert actual option.
+                if (false) {
+                    
+                }
+                
                 // If we have to build the model from a symbolic representation, we need to parse the representation first.
                 boost::optional<storm::prism::Program> program;
                 if (settings.isSymbolicSet()) {

src/cli/entrypoints.h

@@ -3,8 +3,6 @@
 
 #include "src/utility/storm.h"
 
-#include "src/exceptions/NotImplementedException.h"
-
 namespace storm {
     namespace cli {
 
@@ -49,9 +47,19 @@ namespace storm {
         }
 #endif
 
-        template<storm::dd::DdType DdType>
+        template<typename ValueType, 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.");
+            for (auto const& formula : formulas) {
+                std::cout << std::endl << "Model checking property: " << *formula << " ...";
+                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifyProgramWithAbstractionRefinementEngine<DdType, ValueType>(program, formula));
+                if (result) {
+                    std::cout << " done." << std::endl;
+                    std::cout << "Result (initial states): ";
+                    std::cout << *result << std::endl;
+                } else {
+                    std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+                }
+            }
         }
 
         template<storm::dd::DdType DdType>
@@ -118,7 +126,7 @@ namespace storm {
             storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
             
             if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) {
-                verifySymbolicModelWithAbstractionRefinementEngine<LibraryType>(program, formulas);
+                verifySymbolicModelWithAbstractionRefinementEngine<ValueType, LibraryType>(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.");

src/modelchecker/reachability/MenuGameMdpModelChecker.cpp → src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -1,4 +1,4 @@
-#include "src/modelchecker/reachability/MenuGameMdpModelChecker.h"
+#include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h"
 
 #include "src/utility/macros.h"
 
@@ -8,18 +8,25 @@
 
 namespace storm {
     namespace modelchecker {
-        MenuGameMdpModelChecker::MenuGameMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : originalProgram(program), smtSolverFactory(std::move(smtSolverFactory)) {
+        template<storm::dd::DdType Type, typename ValueType>
+        GameBasedMdpModelChecker<Type, ValueType>::GameBasedMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : originalProgram(program), smtSolverFactory(std::move(smtSolverFactory)) {
             STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only MDPs are supported by the game-based model checker.");
                         
             // Start by preparing the program. That is, we flatten the modules if there is more than one.
             if (originalProgram.getNumberOfModules() > 1) {
-                preprocessedProgram = originalProgram.flattenModules(smtSolverFactory);
+                preprocessedProgram = originalProgram.flattenModules(this->smtSolverFactory);
             } else {
                 preprocessedProgram = originalProgram;
             }
         }
 
-        bool MenuGameMdpModelChecker::canHandle(storm::logic::Formula const& formula) const {
+        template<storm::dd::DdType Type, typename ValueType>
+        GameBasedMdpModelChecker<Type, ValueType>::~GameBasedMdpModelChecker() {
+            // Intentionally left empty.
+        }
+
+        template<storm::dd::DdType Type, typename ValueType>
+        bool GameBasedMdpModelChecker<Type, ValueType>::canHandle(storm::logic::Formula const& formula) const {
             if (formula.isProbabilityOperatorFormula()) {
                 storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
                 return this->canHandle(probabilityOperatorFormula.getSubformula());
@@ -39,23 +46,24 @@ namespace storm {
             return false;
         }
         
-        std::unique_ptr<CheckResult> MenuGameMdpModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) {
+        template<storm::dd::DdType Type, typename ValueType>
+        std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) {
             // Depending on whether or not there is a bound, we do something slightly different here.
-            
             return nullptr;
         }
         
-        std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
+        template<storm::dd::DdType Type, typename ValueType>
+        std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
             // TODO
-            
             return nullptr;
         }
         
-        std::unique_ptr<CheckResult> computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
+        template<storm::dd::DdType Type, typename ValueType>
+        std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
             // TODO
-
             return nullptr;
         }
         
+        template class GameBasedMdpModelChecker<storm::dd::DdType::CUDD, double>;
     }
 }

src/modelchecker/reachability/MenuGameMdpModelChecker.h → src/modelchecker/abstraction/GameBasedMdpModelChecker.h

@@ -1,15 +1,18 @@
-#ifndef STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_
-#define STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_
+#ifndef STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_
+#define STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_
 
 #include "src/modelchecker/AbstractModelChecker.h"
 
+#include "src/utility/solver.h"
+
 #include "src/storage/prism/Program.h"
 
-#include "src/utility/solver.h"
+#include "src/storage/dd/DdType.h"
 
 namespace storm {
     namespace modelchecker {
-        class MenuGameMdpModelChecker : public AbstractModelChecker {
+        template<storm::dd::DdType Type, typename ValueType>
+        class GameBasedMdpModelChecker : public AbstractModelChecker {
         public:
             /*!
              * Constructs a model checker whose underlying model is implicitly given by the provided program. All
@@ -18,7 +21,9 @@ namespace storm {
              * @param program The program that implicitly specifies the model to check.
              * @param smtSolverFactory A factory used to create SMT solver when necessary.
              */
-            explicit MenuGameMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory);
+            explicit GameBasedMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory = std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+            
+            virtual ~GameBasedMdpModelChecker() override;
                         
             virtual bool canHandle(storm::logic::Formula const& formula) const override;
             
@@ -28,21 +33,6 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
             
         private:
-            /*!
-             * Performs game-based abstraction refinement on the model until either the precision is met or the provided
-             * proof goal was successfully proven.
-             *
-             * @param filterPredicate A predicate that needs to hold until the target predicate holds.
-             * @param targetPredicate A predicate characterizing the target states.
-             * @param precision The precision to use. This governs what difference between lower and upper bounds is
-             * acceptable.
-             * @param proofGoal A proof goal that says the probability must only be established to be above/below a given
-             * threshold. If the proof goal is met before the precision is achieved, the refinement procedure will abort
-             * and return the current result.
-             * @return A pair of values, that are under- and over-approximations of the actual probability, respectively.
-             */
-            std::pair<double, double> performGameBasedRefinement(storm::expressions::Expression const& filterPredicate, storm::expressions::Expression const& targetPredicate, double precision, boost::optional<std::pair<double, storm::logic::ComparisonType>> const& proofGoal);
-            
             // The original program that was used to create this model checker.
             storm::prism::Program originalProgram;
             
@@ -56,4 +46,4 @@ namespace storm {
     }
 }
 
-#endif /* STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_ */
+#endif /* STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_ */

src/utility/resources.h

@@ -0,0 +1,84 @@
+#ifndef STORM_UTILITY_RESOURCES_H_
+#define STORM_UTILITY_RESOURCES_H_
+
+#include <cstdlib>
+#include <csignal>
+#include <sys/time.h>
+#include <sys/times.h>
+#include <sys/resource.h>
+
+#include "storm-config.h"
+
+#include "src/utility/OsDetection.h"
+
+namespace storm {
+    namespace utility {
+        namespace resources {
+            
+            static const int STORM_EXIT_GENERALERROR = -1;
+            static const int STORM_EXIT_TIMEOUT = -2;
+            static const int STORM_EXIT_MEMOUT = -3;
+            
+            inline void setCPULimit(std::size_t seconds) {
+                rlimit rl;
+                getrlimit(RLIMIT_CPU, &rl);
+                rl.rlim_cur = seconds;
+                setrlimit(RLIMIT_CPU, &rl);
+            }
+            
+            inline std::size_t getCPULimit() {
+                rlimit rl;
+                getrlimit(RLIMIT_CPU, &rl);
+                return rl.rlim_cur;
+            }
+            
+            inline std::size_t usedCPU() {
+                return std::size_t(clock()) / CLOCKS_PER_SEC;
+            }
+            
+            inline void setMemoryLimit(std::size_t megabytes) {
+                rlimit rl;
+                getrlimit(RLIMIT_AS, &rl);
+                rl.rlim_cur = megabytes * 1024 * 1024;
+                setrlimit(RLIMIT_AS, &rl);
+            }
+            
+            inline std::size_t getMemoryLimit() {
+                rlimit rl;
+                getrlimit(RLIMIT_AS, &rl);
+                return rl.rlim_cur;
+            }
+            
+            inline void quick_exit_if_available(int errorCode) {
+#ifdef LINUX
+                std::quick_exit(errorCode);
+#elseif MACOS
+                std::_Exit(errorCode);
+#else
+                std::abort();
+#endif
+            }
+            
+            inline void signalHandler(int signal) {
+                if (signal == SIGXCPU) {
+                    std::cerr << "Timeout." << std::endl;
+                    quick_exit_if_available(STORM_EXIT_TIMEOUT);
+                } else if (signal == ENOMEM) {
+                    std::cerr << "Out of memory" << std::endl;
+                    quick_exit_if_available(STORM_EXIT_MEMOUT);
+                } else {
+                    std::cerr << "Unknown abort in resource limitation module." << std::endl;
+                    quick_exit_if_available(STORM_EXIT_GENERALERROR);
+                }
+            }
+            
+            inline void installSignalHandler() {
+                std::signal(SIGXCPU, signalHandler);
+                std::signal(ENOMEM, signalHandler);
+            }
+            
+        }
+    }
+}
+
+#endif /* STORM_UTILITY_RESOURCES_H_ */

src/utility/solver.h

@@ -1,6 +1,8 @@
 #ifndef STORM_UTILITY_SOLVER_H_
 #define STORM_UTILITY_SOLVER_H_
 
+#include <iostream>
+
 #include <set>
 #include <vector>
 #include <memory>

src/utility/storm.h

@@ -56,6 +56,7 @@
 #include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
 #include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
 #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
+#include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h"
 #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h"
 #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h"
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
@@ -337,7 +338,6 @@ namespace storm {
         return result;
     }
 
-
     template<storm::dd::DdType DdType>
     std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
         std::unique_ptr<storm::modelchecker::CheckResult> result;
@@ -359,6 +359,15 @@ namespace storm {
         return result;
     }
     
+    template<storm::dd::DdType DdType, typename ValueType>
+    std::unique_ptr<storm::modelchecker::CheckResult> verifyProgramWithAbstractionRefinementEngine(storm::prism::Program const& program, std::shared_ptr<storm::logic::Formula> const& formula) {
+        STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Cannot treat non-MDP model using the abstraction refinement engine.");
+        
+        // FIXME: Cudd -> ValueType, double -> ValueType
+        storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::CUDD, double> modelchecker(program);
+        return modelchecker.check(*formula);
+    }
+
     template<typename ValueType>
     void exportMatrixToFile(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::string const& filepath) {
         STORM_LOG_THROW(model->getType() != storm::models::ModelType::Ctmc, storm::exceptions::NotImplementedException, "This functionality is not yet implemented." );