Merge branch 'master' into almostsurepomdp

.gitignore

@@ -50,6 +50,7 @@ src/storm/utility/storm-version.cpp
 nbproject/
 .DS_Store
 .idea
+.vscode
 *.out
 resources/3rdparty/cudd-3.0.0/Makefile.in
 resources/3rdparty/cudd-3.0.0/aclocal.m4

CHANGELOG.md

@@ -11,6 +11,7 @@ Version 1.5.x
 - Scheduler export: Properly handle models with end components. Added export in .json format.
 - CMake: Search for Gurobi prefers new versions
 - Tests: Enabled tests for permissive schedulers
+- `storm-dft`: Renamed setting `--show-dft-stats` to `dft-statistics` and added approximation information to statistics.
 
 ## Version 1.5.1 (2020/03)
 - Jani models are now parsed using exact arithmetic.

CMakeLists.txt

@@ -263,6 +263,9 @@ if (STORM_COMPILER_CLANG OR STORM_COMPILER_APPLECLANG)
         set (CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-export_dynamic")
     endif()
 elseif (STORM_COMPILER_GCC)
+    if(FORCE_COLOR)
+        set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdiagnostics-color=always")
+    endif()
     set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14")
     set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fprefetch-loop-arrays")
     set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -rdynamic")

src/storm-cli-utilities/cli.cpp

@@ -202,7 +202,7 @@ namespace storm {
             
             // If we were given a time limit, we put it in place now.
             if (resources.isTimeoutSet()) {
-                storm::utility::resources::setCPULimit(resources.getTimeoutInSeconds());
+                storm::utility::resources::setTimeoutAlarm(resources.getTimeoutInSeconds());
             }
 
             // register signal handler to handle aborts

src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h

@@ -1220,10 +1220,6 @@ namespace storm {
                 // try with an increased bound.
                 while (solver.checkWithAssumptions({assumption}) == storm::solver::SmtSolver::CheckResult::Unsat) {
                     STORM_LOG_DEBUG("Constraint system is unsatisfiable with at most " << currentBound << " taken commands; increasing bound.");
-#ifndef NDEBUG
-                    STORM_LOG_DEBUG("Sanity check to see whether constraint system is still satisfiable.");
-                    STORM_LOG_ASSERT(solver.check() == storm::solver::SmtSolver::CheckResult::Sat, "Constraint system is not satisfiable anymore.");
-#endif
                     solver.add(variableInformation.auxiliaryVariables.back());
                     variableInformation.auxiliaryVariables.push_back(assertLessOrEqualKRelaxed(solver, variableInformation, ++currentBound));
                     assumption = !variableInformation.auxiliaryVariables.back();
@@ -1755,6 +1751,10 @@ namespace storm {
                     if (result.size() > 0 && iterations > firstCounterexampleFound + options.maximumExtraIterations) {
                         break;
                     }
+                    if (result.size() == 0) {
+                        STORM_LOG_DEBUG("Sanity check to see whether constraint system is still satisfiable.");
+                        STORM_LOG_ASSERT(solver->check() == storm::solver::SmtSolver::CheckResult::Sat, "Constraint system is not satisfiable anymore.");
+                    }
                     STORM_LOG_DEBUG("Computing minimal command set.");
                     solverClock = std::chrono::high_resolution_clock::now();
                     boost::optional<storm::storage::FlatSet<uint_fast64_t>> smallest = findSmallestCommandSet(*solver, variableInformation, currentBound);

src/storm-dft-cli/storm-dft.cpp

@@ -40,9 +40,10 @@ void processOptions() {
         STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model given.");
     }
 
-    // DFT statistics
-    if (dftIOSettings.isDisplayStatsSet()) {
+    // Show statistics about DFT (number of gates, etc.)
+    if (dftIOSettings.isShowDftStatisticsSet()) {
         dft->writeStatsToStream(std::cout);
+        std::cout << std::endl;
     }
 
     // Export to json

src/storm-dft/modelchecker/dft/DFTModelChecker.cpp

@@ -13,6 +13,7 @@
 #include "storm-dft/api/storm-dft.h"
 #include "storm-dft/builder/ExplicitDFTModelBuilder.h"
 #include "storm-dft/storage/dft/DFTIsomorphism.h"
+#include "storm-dft/settings/modules/DftIOSettings.h"
 #include "storm-dft/settings/modules/FaultTreeSettings.h"
 
 
@@ -305,6 +306,8 @@ namespace storm {
                                              storm::builder::ApproximationHeuristic approximationHeuristic,
                                              bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) {
             explorationTimer.start();
+            auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+            auto dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
 
             // Find symmetries
             std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
@@ -355,12 +358,12 @@ namespace storm {
                     STORM_LOG_DEBUG("Getting model for lower bound...");
                     model = builder.getModelApproximation(true, !probabilityFormula);
                     // We only output the info from the lower bound as the info for the upper bound is the same
-                    if (printInfo) {
+                    if (printInfo && dftIOSettings.isShowDftStatisticsSet()) {
+                        std::cout << "Model in iteration " << (iteration + 1) << ":" << std::endl;
                         model->printModelInformationToStream(std::cout);
                     }
                     buildingTimer.stop();
 
-                    auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
                     if (ioSettings.isExportExplicitSet()) {
                         std::vector<std::string> parameterNames;
                         // TODO fill parameter names
@@ -388,24 +391,33 @@ namespace storm {
                                                                << approxResult.second);
                     approxResult.second = newResult[0];
 
-                    ++iteration;
                     STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) ||
                                      comparator.isEqual(approxResult.first, approxResult.second),
                                      "Under-approximation " << approxResult.first
                                                             << " is greater than over-approximation "
                                                             << approxResult.second);
-                    STORM_LOG_DEBUG("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")");
                     totalTimer.stop();
-                    printTimings();
+                    if (printInfo && dftIOSettings.isShowDftStatisticsSet()) {
+                        std::cout << "Result after iteration " << (iteration + 1) << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")" << std::endl;
+                        printTimings();
+                        std::cout << std::endl;
+                    } else {
+                        STORM_LOG_DEBUG("Result after iteration " << (iteration + 1) << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")");
+                    }
+                    
                     totalTimer.start();
                     STORM_LOG_THROW(!storm::utility::isInfinity<ValueType>(approxResult.first) &&
                                     !storm::utility::isInfinity<ValueType>(approxResult.second),
                                     storm::exceptions::NotSupportedException,
                                     "Approximation does not work if result might be infinity.");
+                    ++iteration;
                 } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError,
                                                     probabilityFormula));
 
                 //STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : "."));
+                if (printInfo) {
+                    model->printModelInformationToStream(std::cout);
+                }
                 dft_results results;
                 results.push_back(approxResult);
                 return results;

src/storm-dft/settings/modules/DftIOSettings.cpp

@@ -26,7 +26,8 @@ namespace storm {
             const std::string DftIOSettings::maxValueOptionName = "max";
             const std::string DftIOSettings::exportToJsonOptionName = "export-json";
             const std::string DftIOSettings::exportToSmtOptionName = "export-smt";
-            const std::string DftIOSettings::displayStatsOptionName = "show-dft-stats";
+            const std::string DftIOSettings::dftStatisticsOptionName = "dft-statistics";
+            const std::string DftIOSettings::dftStatisticsOptionShortName = "dftstats";
 
 
             DftIOSettings::DftIOSettings() : ModuleSettings(moduleName) {
@@ -62,7 +63,7 @@ namespace storm {
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename",
                                                                                                             "The name of the smtlib2 file to export to.").build())
                                         .build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, displayStatsOptionName, false, "Print stats to stdout").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, dftStatisticsOptionName, false, "Sets whether to display DFT statistics if available.").setShortName(dftStatisticsOptionShortName).build());
             }
 
             bool DftIOSettings::isDftFileSet() const {
@@ -136,8 +137,8 @@ namespace storm {
                 return this->getOption(exportToSmtOptionName).getArgumentByName("filename").getValueAsString();
             }
 
-            bool DftIOSettings::isDisplayStatsSet() const {
-                return this->getOption(displayStatsOptionName).getHasOptionBeenSet();
+            bool DftIOSettings::isShowDftStatisticsSet() const {
+                return this->getOption(dftStatisticsOptionName).getHasOptionBeenSet();
             }
 
             void DftIOSettings::finalize() {

src/storm-dft/settings/modules/DftIOSettings.h

@@ -130,11 +130,11 @@ namespace storm {
                 std::string getExportSmtFilename() const;
 
                 /*!
-                 * Retrieves whether statistics for the DFT should be displayed.
+                 * Retrieves whether statistics about the DFT analysis should be displayed.
                  *
                  * @return True if the statistics option was set.
                  */
-                bool isDisplayStatsSet() const;
+                bool isShowDftStatisticsSet() const;
                 
                 bool check() const override;
                 void finalize() override;
@@ -157,7 +157,8 @@ namespace storm {
                 static const std::string maxValueOptionName;
                 static const std::string exportToJsonOptionName;
                 static const std::string exportToSmtOptionName;
-                static const std::string displayStatsOptionName;
+                static const std::string dftStatisticsOptionName;
+                static const std::string dftStatisticsOptionShortName;
 
             };
 

src/storm-gspn/storage/gspn/GSPN.cpp

@@ -94,7 +94,7 @@ namespace storm {
                 }
             }
             return nullptr;
-        };
+        }
         
         storm::gspn::Place* GSPN::getPlace(std::string const& name) {
             for (auto& place : places) {
@@ -103,7 +103,7 @@ namespace storm {
                 }
             }
             return nullptr;
-        };
+        }
 
         storm::gspn::TimedTransition<GSPN::RateType> const* GSPN::getTimedTransition(std::string const& name) const {
             for (auto& trans : timedTransitions) {

src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp

@@ -25,7 +25,7 @@ namespace storm {
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
         bool ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
             return getImpreciseChecker().canHandle(parametricModel, checkTask) && getPreciseChecker().canHandle(parametricModel, checkTask);
-        };
+        }
  
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
         RegionResult ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::analyzeRegion(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis, RegionResult const& initialResult, bool sampleVerticesOfRegion) {

src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp

@@ -48,7 +48,10 @@ namespace storm {
                 
                 out << "Region refinement Check result (visualization):" << std::endl;
                 out << " \t x-axis: " << x << "  \t y-axis: " << y << "  \t S=safe, [ ]=unsafe, -=ambiguous " << std::endl;
-                for (uint_fast64_t i = 0; i < sizeX+2; ++i) out << "#"; out << std::endl;
+                for (uint_fast64_t i = 0; i < sizeX+2; ++i) {
+                    out << "#";
+                }
+                out << std::endl;
                 
                 CoefficientType deltaX = (getParameterSpace().getUpperBoundary(x) - getParameterSpace().getLowerBoundary(x)) / storm::utility::convertNumber<CoefficientType>(sizeX);
                 CoefficientType deltaY = (getParameterSpace().getUpperBoundary(y) - getParameterSpace().getLowerBoundary(y)) / storm::utility::convertNumber<CoefficientType>(sizeY);
@@ -94,7 +97,10 @@ namespace storm {
                     }
                     out << "#" << std::endl;
                 }
-                for (uint_fast64_t i = 0; i < sizeX+2; ++i) out << "#"; out << std::endl;
+                for (uint_fast64_t i = 0; i < sizeX+2; ++i) {
+                    out << "#";
+                }
+                out << std::endl;
             } else {
                 STORM_LOG_WARN("Writing illustration of region check result to a stream is only implemented for two parameters.");
             }

src/storm-parsers/parser/DirectEncodingParser.cpp

@@ -164,7 +164,6 @@ namespace storm {
             // Iterate over all lines
             std::string line;
             size_t row = 0;
-            size_t firstRowOfState = 0;
             size_t state = 0;
             bool firstState = true;
             bool firstActionForState = true;
@@ -197,7 +196,6 @@ namespace storm {
                         STORM_LOG_TRACE("new Row Group starts at " << row << ".");
                         builder.newRowGroup(row);
                     }
-                    firstRowOfState = row;
 
                     if (continuousTime) {
                         // Parse exit rate for CTMC or MA

src/storm-pomdp/transformer/MakePOMDPCanonic.cpp

@@ -47,7 +47,7 @@ namespace storm {
                     ++it2;
                 }
                 return it1 == end1 && it2 == end2;
-            };
+            }
 
 
             bool operator<(ActionIdentifier const& lhs, ActionIdentifier const& rhs) {

src/storm/generator/JaniNextStateGenerator.cpp

@@ -169,7 +169,7 @@ namespace storm {
         template<typename ValueType, typename StateType>
         bool JaniNextStateGenerator<ValueType, StateType>::isPartiallyObservable() const {
             return false;
-        };
+        }
         
         template<typename ValueType, typename StateType>
         uint64_t JaniNextStateGenerator<ValueType, StateType>::getLocation(CompressedState const& state, LocationVariableInformation const& locationVariable) const {
@@ -1201,7 +1201,7 @@ namespace storm {
         storm::storage::BitVector JaniNextStateGenerator<ValueType, StateType>::evaluateObservationLabels(CompressedState const& state) const {
             STORM_LOG_WARN("There are no observation labels in JANI currenty");
             return storm::storage::BitVector(0);
-        };
+        }
 
 
         template<typename ValueType, typename StateType>

src/storm/generator/PrismNextStateGenerator.cpp

@@ -734,7 +734,7 @@ namespace storm {
                 result.setFromInt(64*i,64,this->evaluator->asInt(program.getObservationLabels()[i].getStatePredicateExpression()));
             }
             return result;
-        };
+        }
 
 
         template<typename ValueType, typename StateType>

src/storm/logic/CumulativeRewardFormula.cpp

@@ -99,7 +99,6 @@ namespace storm {
         double CumulativeRewardFormula::getBound(unsigned i) const {
             checkNoVariablesInBound(bounds.at(i).getBound());
             double value = bounds.at(i).getBound().evaluateAsDouble();
-            STORM_LOG_THROW(value >= 0.0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
             return value;
         }
 
@@ -107,7 +106,6 @@ namespace storm {
         storm::RationalNumber CumulativeRewardFormula::getBound(unsigned i) const {
             checkNoVariablesInBound(bounds.at(i).getBound());
             storm::RationalNumber value = bounds.at(i).getBound().evaluateAsRational();
-            STORM_LOG_THROW(value >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
             return value;
         }
 
@@ -115,7 +113,6 @@ namespace storm {
         uint64_t CumulativeRewardFormula::getBound(unsigned i) const {
             checkNoVariablesInBound(bounds.at(i).getBound());
             uint64_t value = bounds.at(i).getBound().evaluateAsInt();
-            STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
             return value;
         }
         

src/storm/logic/InstantaneousRewardFormula.cpp

@@ -55,7 +55,7 @@ namespace storm {
         template <>
         uint64_t InstantaneousRewardFormula::getBound() const {
             checkNoVariablesInBound(bound);
-            uint64_t value = bound.evaluateAsInt();
+            int64_t value = bound.evaluateAsInt();
             STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
             return value;
         }

src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp

@@ -563,6 +563,7 @@ namespace storm {
                             if (rowLeadsToDefinedScheduler && (rowStaysInEC || !statesThatShouldStayInTheirEC.get(state))) {
                                 originalOptimalChoices[state] = row - transitionMatrix.getRowGroupIndices()[state];
                                 statesWithUndefSched.set(state, false);
+                                break;
                             }
                         }
                     }

src/storm/models/sparse/Pomdp.cpp

@@ -97,7 +97,7 @@ namespace storm {
             template<typename ValueType, typename RewardModelType>
             bool Pomdp<ValueType, RewardModelType>::isCanonic() const {
                 return canonicFlag;
-            };
+            }
 
 
 

src/storm/storage/BitVector.cpp

@@ -156,6 +156,7 @@ namespace storm {
             // Only perform the assignment if the source and target are not identical.
             if (this != &other) {
                 bitCount = other.bitCount;
+                other.bitCount = 0;
                 if (this->buckets) {
                     delete[] this->buckets;
                 }
@@ -1239,6 +1240,36 @@ namespace storm {
             
             return h1 ^ h2;
         }
+
+        void BitVector::store(std::ostream& os) const {
+            os << bitCount;
+            for (uint64_t i = 0; i < bucketCount(); ++i) {
+                os << " " << buckets[i];
+            }
+        }
+
+        BitVector BitVector::load(std::string const& description) {
+            std::vector<std::string> splitted;
+            std::stringstream ss(description);
+            ss >> std::noskipws;
+            std::string field;
+            char ws_delim;
+            while(true) {
+                if( ss >> field )
+                    splitted.push_back(field);
+                else if (ss.eof())
+                    break;
+                else
+                    splitted.push_back(std::string());
+                ss.clear();
+                ss >> ws_delim;
+            }
+            BitVector bv(std::stoul(splitted[0]));
+            for(uint64_t i = 0; i < splitted.size()-1; ++i) {
+                bv.buckets[i] = std::stoul(splitted[i+1]);
+            }
+            return bv;
+        }
         
         // All necessary explicit template instantiations.
         template BitVector::BitVector(uint_fast64_t length, std::vector<uint_fast64_t>::iterator begin, std::vector<uint_fast64_t>::iterator end);

src/storm/storage/BitVector.h

@@ -538,6 +538,9 @@ namespace storm {
 
             friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector);
 
+            void store(std::ostream&) const;
+            static BitVector load(std::string const& description);
+
             friend struct std::hash<storm::storage::BitVector>;
             friend struct FNV1aBitVectorHash;
 

src/storm/utility/resources.h

@@ -13,27 +13,6 @@ namespace storm {
     namespace utility {
         namespace resources {
 
-            /*!
-             * Get CPU limit.
-             * @return CPU limit in seconds.
-             */
-            inline std::size_t getCPULimit() {
-                rlimit rl;
-                getrlimit(RLIMIT_CPU, &rl);
-                return rl.rlim_cur;
-            }
-
-            /*!
-             * Set CPU limit.
-             * @param seconds CPU limit in seconds.
-             */
-            inline void setCPULimit(std::size_t seconds) {
-                rlimit rl;
-                getrlimit(RLIMIT_CPU, &rl);
-                rl.rlim_cur = seconds;
-                setrlimit(RLIMIT_CPU, &rl);
-            }
-
             /*!
              * Get used CPU time.
              * @return CPU time in seconds.