diff --git a/.gitignore b/.gitignore
index 71a15cc93..48ebde709 100644
--- a/.gitignore
+++ b/.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
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2c11fea31..51a33bc11 100644
--- a/CHANGELOG.md
+++ b/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.
diff --git a/CMakeLists.txt b/CMakeLists.txt
index d1b58879e..134b6577a 100644
--- a/CMakeLists.txt
+++ b/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")
diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp
index 12d5771bd..9105bc9a2 100644
--- a/src/storm-cli-utilities/cli.cpp
+++ b/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
diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
index 58f13ae10..4d4dd9629 100644
--- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
+++ b/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);
diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp
index 87338ff30..f7a5093a7 100644
--- a/src/storm-dft-cli/storm-dft.cpp
+++ b/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
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 00fe1d0d9..241027e8f 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/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;
diff --git a/src/storm-dft/settings/modules/DftIOSettings.cpp b/src/storm-dft/settings/modules/DftIOSettings.cpp
index 662fd0f34..fca700e5a 100644
--- a/src/storm-dft/settings/modules/DftIOSettings.cpp
+++ b/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() {
diff --git a/src/storm-dft/settings/modules/DftIOSettings.h b/src/storm-dft/settings/modules/DftIOSettings.h
index 60369b36e..37a5fb464 100644
--- a/src/storm-dft/settings/modules/DftIOSettings.h
+++ b/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;
};
diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp
index bac028c27..c9d1ff7cd 100644
--- a/src/storm-gspn/storage/gspn/GSPN.cpp
+++ b/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) {
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp
index 002a43692..4065f236b 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp
+++ b/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) {
diff --git a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp
index 320dda2e8..7c2a5e18c 100644
--- a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp
+++ b/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.");
}
diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp
index 683a87d77..1dd6322d9 100644
--- a/src/storm-parsers/parser/DirectEncodingParser.cpp
+++ b/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
diff --git a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp b/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp
index 783a4782a..3cd17c25d 100644
--- a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp
+++ b/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) {
diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
index 6c260746b..87baa0b98 100644
--- a/src/storm/generator/JaniNextStateGenerator.cpp
+++ b/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>
diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp
index a0fb216e5..6bec68bed 100644
--- a/src/storm/generator/PrismNextStateGenerator.cpp
+++ b/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>
diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp
index 7abcdc7e4..33633b319 100644
--- a/src/storm/logic/CumulativeRewardFormula.cpp
+++ b/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;
}
diff --git a/src/storm/logic/InstantaneousRewardFormula.cpp b/src/storm/logic/InstantaneousRewardFormula.cpp
index 37bdee1c9..1ed2c1f66 100644
--- a/src/storm/logic/InstantaneousRewardFormula.cpp
+++ b/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;
}
diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
index 307d91c3f..db0fa99f1 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
+++ b/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;
}
}
}
diff --git a/src/storm/models/sparse/Pomdp.cpp b/src/storm/models/sparse/Pomdp.cpp
index 5b2e2a8a6..135b74f48 100644
--- a/src/storm/models/sparse/Pomdp.cpp
+++ b/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;
- };
+ }
diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp
index a4ad5fca9..6edf61f1b 100644
--- a/src/storm/storage/BitVector.cpp
+++ b/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);
diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h
index 64b823652..323020b48 100644
--- a/src/storm/storage/BitVector.h
+++ b/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;
diff --git a/src/storm/utility/resources.h b/src/storm/utility/resources.h
index eb84d73c0..349796acd 100644
--- a/src/storm/utility/resources.h
+++ b/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.