From 86ff07ec0d9a37064764ee5837c5801589f8ab8d Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 21 Jul 2015 09:32:36 +0200 Subject: [PATCH] take sampling point before approximation to know whether to minimize or maximize. only compute the rational function when it is needed. Former-commit-id: 0000360472fd8b6784b9a04c45bbb948ca91faa6 --- .../SparseDtmcRegionModelChecker.cpp | 117 +++++++++--------- .../SparseDtmcRegionModelChecker.h | 9 +- src/storage/SparseMatrix.cpp | 4 + src/utility/cli.h | 5 + 4 files changed, 74 insertions(+), 61 deletions(-) diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp index 2e2dbbef3..9619f4c6d 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp @@ -178,8 +178,15 @@ namespace storm { template - SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc const& model) : model(model), eliminationModelChecker(model), smtSolver(nullptr), probabilityOperatorFormula(nullptr), sampleDtmc(nullptr), approxMdp(nullptr) { - // Intentionally left empty. + SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc const& model) : + model(model), + eliminationModelChecker(model), + smtSolver(nullptr), + probabilityOperatorFormula(nullptr), + sampleDtmc(nullptr), + approxMdp(nullptr), + isReachProbFunctionComputed(false) { + //intentionally left empty } template @@ -229,8 +236,9 @@ namespace storm { // If the initial state is known to have either probability 0 or 1, we can directly set the reachProbFunction. if (model.getInitialStates().isDisjointFrom(maybeStates)) { - STORM_LOG_DEBUG("The probability of the initial state is constant (0 or 1)"); + STORM_LOG_WARN("The probability of the initial state is constant (0 or 1)"); this->reachProbFunction = statesWithProbability0.get(*model.getInitialStates().begin()) ? storm::utility::zero() : storm::utility::one(); + this->isReachProbFunctionComputed=true; } // Determine the set of states that is reachable from the initial state without jumping over a target state. @@ -262,28 +270,17 @@ namespace storm { //eliminate the remaining states to get the reachability probability function - this->sparseTransitions = flexibleTransitions.getSparseMatrix(); + this->sparseTransitions = this->flexibleTransitions.getSparseMatrix(); this->sparseBackwardTransitions = this->sparseTransitions.transpose(); - std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionStart = std::chrono::high_resolution_clock::now(); - this->reachProbFunction = computeReachProbFunction(this->subsystem, this->flexibleTransitions, this->flexibleBackwardTransitions, this->sparseTransitions, this->sparseBackwardTransitions, this->oneStepProbabilities, this->initialState); - std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionEnd = std::chrono::high_resolution_clock::now(); - - //std::string funcStr = " (/ " + - // this->reachProbFunction.nominator().toString(false, true) + " " + - // this->reachProbFunction.denominator().toString(false, true) + - // " )"; - // std::cout << std::endl <<"the resulting reach prob function is " << std::endl << funcStr << std::endl << std::endl; std::chrono::high_resolution_clock::time_point timeInitialStateEliminationEnd = std::chrono::high_resolution_clock::now(); initializeSampleDtmcAndApproxMdp(this->sampleDtmc,this->sampleDtmcMapping,this->approxMdp,this->approxMdpMapping,this->approxMdpSubstitutions,this->subsystem, this->sparseTransitions,this->oneStepProbabilities, this->initialState); - initializeSMTSolver(this->smtSolver, this->reachProbFunction,*this->probabilityOperatorFormula); //some information for statistics... std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now(); this->timePreprocessing= timePreprocessingEnd - timePreprocessingStart; this->timeInitialStateElimination = timeInitialStateEliminationEnd-timeInitialStateEliminationStart; - this->timeComputeReachProbFunction = timeComputeReachProbFunctionEnd-timeComputeReachProbFunctionStart; this->numOfCheckedRegions=0; this->numOfRegionsSolvedThroughSampling=0; this->numOfRegionsSolvedThroughApproximation=0; @@ -347,6 +344,8 @@ namespace storm { std::vector const& oneStepProbs, storm::storage::sparse::state_type const& initState) { + std::set functionSet; + //the matrix "transitions" might have empty rows where states have been eliminated. //The DTMC/ MDP matrices should not have such rows. We therefore leave them out, but we have to change the indices of the states accordingly. std::vector newStateIndexMap(transitions.getRowCount(), transitions.getRowCount()); //initialize with some illegal index to easily check if a transition leads to an unselected state @@ -379,6 +378,7 @@ namespace storm { for(auto const& entry: transitions.getRow(oldStateIndex)){ valueToSinkState-=entry.getValue(); storm::utility::regions::gatherOccurringVariables(entry.getValue(), occurringParameters); + functionSet.insert(entry.getValue()); dtmcMatrixBuilder.addNextValue(newStateIndexMap[oldStateIndex],newStateIndexMap[entry.getColumn()],dummyEntry); mdpMatrixBuilder.addNextValue(currentMdpRow, newStateIndexMap[entry.getColumn()], dummyEntry); rowInformation.emplace_back(std::make_pair(newStateIndexMap[entry.getColumn()], dummyEntry)); @@ -389,7 +389,7 @@ namespace storm { if(!this->parametricTypeComparator.isZero(oneStepProbs[oldStateIndex])){ valueToSinkState-=oneStepProbs[oldStateIndex]; storm::utility::regions::gatherOccurringVariables(oneStepProbs[oldStateIndex], occurringParameters); - + functionSet.insert(oneStepProbs[oldStateIndex]); dtmcMatrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], targetState, dummyEntry); mdpMatrixBuilder.addNextValue(currentMdpRow, targetState, dummyEntry); rowInformation.emplace_back(std::make_pair(targetState, dummyEntry)); @@ -401,6 +401,7 @@ namespace storm { mdpMatrixBuilder.addNextValue(currentMdpRow, sinkState, dummyEntry); rowInformation.emplace_back(std::make_pair(sinkState, dummyEntry)); oneStepToSink[oldStateIndex]=valueToSinkState; + functionSet.insert(valueToSinkState); } // Find the different combinations of occuring variables and lower/upper bounds (mathematically speaking we want to have the set 'occuringVariables times {u,l}' ) std::size_t numOfSubstitutions=std::pow(2,occurringParameters.size()); //1 substitution = 1 combination of lower and upper bounds @@ -456,7 +457,7 @@ namespace storm { // the final dtmc and mdp sampleDtmc=std::make_shared>(dtmcMatrixBuilder.build(), std::move(dtmcStateLabeling), std::move(dtmcNoStateRewards), std::move(dtmcNoTransitionRewards), std::move(dtmcNoChoiceLabeling)); approxMdp=std::make_shared>(mdpMatrixBuilder.build(), std::move(mdpStateLabeling), std::move(mdpNoStateRewards), std::move(mdpNoTransitionRewards), std::move(mdpNoChoiceLabeling)); - + std::cout << "THERE ARE " << functionSet.size() << " DIFFERENT RATIONAL FUNCTIONS" << std::endl; //build mapping vectors and the substitution vector. sampleDtmcMapping=std::vector&>>(); sampleDtmcMapping.reserve(sampleDtmc->getTransitionMatrix().getEntryCount()); @@ -531,8 +532,25 @@ namespace storm { } } } - + template + ParametricType SparseDtmcRegionModelChecker::getReachProbFunction() { + if(!this->isReachProbFunctionComputed){ + std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionStart = std::chrono::high_resolution_clock::now(); + this->reachProbFunction = computeReachProbFunction(this->subsystem, this->flexibleTransitions, this->flexibleBackwardTransitions, this->sparseTransitions, this->sparseBackwardTransitions, this->oneStepProbabilities, this->initialState); + std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionEnd = std::chrono::high_resolution_clock::now(); + std::string funcStr = " (/ " + + this->reachProbFunction.nominator().toString(false, true) + " " + + this->reachProbFunction.denominator().toString(false, true) + + " )"; + std::cout << std::endl <<"the resulting reach prob function is " << std::endl << funcStr << std::endl << std::endl; + STORM_LOG_DEBUG("Computed reachProbFunction"); + this->isReachProbFunctionComputed=true; + this->timeComputeReachProbFunction = timeComputeReachProbFunctionEnd-timeComputeReachProbFunctionStart; + } + return this->reachProbFunction; + } + template ParametricType SparseDtmcRegionModelChecker::computeReachProbFunction( storm::storage::BitVector const& subsys, @@ -593,7 +611,7 @@ namespace storm { } template - void SparseDtmcRegionModelChecker::initializeSMTSolver(std::shared_ptr& solver, const ParametricType& reachProbFunction, const storm::logic::ProbabilityOperatorFormula& formula) { + void SparseDtmcRegionModelChecker::initializeSMTSolver(std::shared_ptr& solver, const ParametricType& reachProbFunc, const storm::logic::ProbabilityOperatorFormula& formula) { storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions.. solver = std::shared_ptr(new storm::solver::Smt2SmtSolver(manager, true)); @@ -603,7 +621,7 @@ namespace storm { // To prove that the property is satisfied in the initial state for all parameters, // we ask the solver whether the negation of the property is satisfiable and invert the answer. // In this case, assert that this variable is true: - VariableType proveAllSatVar=storm::utility::regions::getNewVariable("proveAllSat", storm::utility::regions::VariableSort::VS_BOOL); + VariableType proveAllSatVar=storm::utility::regions::getNewVariable("storm_proveAllSat", storm::utility::regions::VariableSort::VS_BOOL); //Example: //Property: P<=p [ F 'target' ] holds iff... @@ -627,19 +645,19 @@ namespace storm { default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported"); } - storm::utility::regions::addGuardedConstraintToSmtSolver(solver, proveAllSatVar, this->reachProbFunction, proveAllSatRel, bound); + storm::utility::regions::addGuardedConstraintToSmtSolver(solver, proveAllSatVar, reachProbFunc, proveAllSatRel, bound); // To prove that the property is violated in the initial state for all parameters, // we ask the solver whether the the property is satisfiable and invert the answer. // In this case, assert that this variable is true: - VariableType proveAllViolatedVar=storm::utility::regions::getNewVariable("proveAllViolated", storm::utility::regions::VariableSort::VS_BOOL); + VariableType proveAllViolatedVar=storm::utility::regions::getNewVariable("storm_proveAllViolated", storm::utility::regions::VariableSort::VS_BOOL); //Example: //Property: P<=p [ F 'target' ] holds iff... // f(x) <= p // Hence: If f(x) <= p is unsat, the property is violated for all parameters. storm::logic::ComparisonType proveAllViolatedRel = this->probabilityOperatorFormula->getComparisonType(); - storm::utility::regions::addGuardedConstraintToSmtSolver(solver, proveAllViolatedVar, this->reachProbFunction, proveAllViolatedRel, bound); + storm::utility::regions::addGuardedConstraintToSmtSolver(solver, proveAllViolatedVar, reachProbFunc, proveAllViolatedRel, bound); } @@ -657,7 +675,7 @@ namespace storm { bool doApproximation=this->hasOnlyLinearFunctions; // this approach is only correct if the model has only linear functions bool doSampling=true; bool doSubsystemSmt=false; //this->hasOnlyLinearFunctions; // this approach is only correct if the model has only linear functions - bool doFullSmt=true; + bool doFullSmt=false; std::chrono::high_resolution_clock::time_point timeApproximationStart = std::chrono::high_resolution_clock::now(); std::vector lowerBounds; @@ -765,10 +783,9 @@ namespace storm { template bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool viaReachProbFunction) { - // check whether the property is satisfied or not at the given point bool valueInBoundOfFormula; if(viaReachProbFunction){ - valueInBoundOfFormula = this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction(this->reachProbFunction, point)); + valueInBoundOfFormula = this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction(getReachProbFunction(), point)); } else{ //put the values into the dtmc matrix @@ -783,14 +800,6 @@ namespace storm { storm::modelchecker::SparseDtmcPrctlModelChecker modelChecker(*this->sampleDtmc); std::unique_ptr resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula,false); valueInBoundOfFormula=this->valueIsInBoundOfFormula(resultPtr->asExplicitQuantitativeCheckResult().getValueVector()[*this->sampleDtmc->getInitialStates().begin()]); - - //Delete from here - // ConstantType result=resultPtr->asExplicitQuantitativeCheckResult().getValueVector()[*this->sampleDtmc->getInitialStates().begin()]; - // ConstantType otherresult=storm::utility::regions::convertNumber(storm::utility::regions::evaluateFunction(this->reachProbFunction, point)); - - // STORM_LOG_THROW((std::abs(result - otherresult) <= 0.01),storm::exceptions::UnexpectedException, "The results of new DTMC algorithm does not match: " << result << " vs. " << otherresult); - //To here - } if(valueInBoundOfFormula){ @@ -818,7 +827,7 @@ namespace storm { template bool SparseDtmcRegionModelChecker::checkApproximativeProbabilities(ParameterRegion& region, std::vector& lowerBounds, std::vector& upperBounds) { - STORM_LOG_THROW(this->hasOnlyLinearFunctions, storm::exceptions::UnexpectedException, "Tried to generate bounds on the probability (only applicable if all functions are linear), but there are nonlinear functions."); + STORM_LOG_THROW(this->hasOnlyLinearFunctions, storm::exceptions::UnexpectedException, "Tried to perform approximative method (only applicable if all functions are linear), but there are nonlinear functions."); //build the mdp and a reachability formula and create a modelchecker std::chrono::high_resolution_clock::time_point timeMDPBuildStart = std::chrono::high_resolution_clock::now(); buildMdpForApproximation(region); @@ -828,10 +837,12 @@ namespace storm { storm::logic::EventuallyFormula eventuallyFormula(targetFormulaPtr); storm::modelchecker::SparseMdpPrctlModelChecker modelChecker(*this->approxMdp); + if (region.getCheckResult()==RegionCheckResult::UNKNOWN){ + //Sampling to get a hint of whether we should try to prove ALLSAT or ALLVIOLATED + checkPoint(region,region.getLowerBounds(), false); + } - - //Decide whether we should compute lower or upper bounds first. - //This does not matter if the current result is unknown. However, let us assume that it is more likely that the final result will be ALLSAT. So we test this first. + // Decide whether we should compute lower or upper bounds first. storm::logic::OptimalityType firstOpType; switch (this->probabilityOperatorFormula->getComparisonType()) { case storm::logic::ComparisonType::Greater: @@ -867,20 +878,12 @@ namespace storm { } //one iteration for each opType \in {Maximize, Minimize} + //However, the second iteration might not be performed if the first one proved ALLSAT or ALLVIOLATED storm::logic::OptimalityType opType=firstOpType; for(int i=1; i<=2; ++i){ //perform model checking on the mdp std::unique_ptr resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula,false,opType); - //DELETE FROM HERE - // storm::models::sparse::Mdp othermdp = buildMdpForApproximation2(region); - // storm::modelchecker::SparseMdpPrctlModelChecker othermodelChecker(othermdp); - // std::unique_ptr otherresultPtr = othermodelChecker.computeEventuallyProbabilities(eventuallyFormula,false,opType); - // ConstantType origResult=resultPtr->asExplicitQuantitativeCheckResult().getValueVector()[*this->approxMdp->getInitialStates().begin()]; - // ConstantType otherResult=otherresultPtr->asExplicitQuantitativeCheckResult().getValueVector()[*othermdp.getInitialStates().begin()]; - // STORM_LOG_THROW(this->constantTypeComparator.isEqual(origResult,otherResult),storm::exceptions::UnexpectedException, "The results of new mdp algorithm does not match: " << origResult << " vs. " << otherResult); - //TO HERE - //check if the approximation yielded a conclusive result if(opType==storm::logic::OptimalityType::Maximize){ upperBounds = resultPtr->asExplicitQuantitativeCheckResult().getValueVector(); @@ -900,7 +903,6 @@ namespace storm { } //flip the optype for the next iteration opType=storm::logic::OptimalityType::Minimize; - // if(i==1) std::cout << " Requiring a second model checker run (with Minimize)" << std::endl; } else if(opType==storm::logic::OptimalityType::Minimize){ lowerBounds = resultPtr->asExplicitQuantitativeCheckResult().getValueVector(); @@ -920,7 +922,6 @@ namespace storm { } //flip the optype for the next iteration opType=storm::logic::OptimalityType::Maximize; - // if(i==1) std::cout << " Requiring a second model checker run (with Maximize)" << std::endl; } } @@ -1084,6 +1085,10 @@ namespace storm { checkPoint(region,region.getLowerBounds(), true); } + if(this->smtSolver==nullptr){ + initializeSMTSolver(this->smtSolver, getReachProbFunction(),*this->probabilityOperatorFormula); + } + this->smtSolver->push(); //add constraints for the region @@ -1093,8 +1098,8 @@ namespace storm { } //add constraint that states what we want to prove - VariableType proveAllSatVar=storm::utility::regions::getVariableFromString("proveAllSat"); - VariableType proveAllViolatedVar=storm::utility::regions::getVariableFromString("proveAllViolated"); + VariableType proveAllSatVar=storm::utility::regions::getVariableFromString("storm_proveAllSat"); + VariableType proveAllViolatedVar=storm::utility::regions::getVariableFromString("storm_proveAllViolated"); switch(region.getCheckResult()){ case RegionCheckResult::EXISTSBOTH: STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::EXISTSBOTH), "checkFullSmt invoked although the result is already clear (EXISTSBOTH). Will validate this now..."); @@ -1162,7 +1167,7 @@ namespace storm { default: STORM_LOG_WARN("The SMT solver was not able to compute a result for this region. (Timeout? Memout?)"); if(this->smtSolver->isNeedsRestart()){ - initializeSMTSolver(this->smtSolver,this->reachProbFunction, *this->probabilityOperatorFormula); + initializeSMTSolver(this->smtSolver,getReachProbFunction(), *this->probabilityOperatorFormula); } return false; } @@ -1221,7 +1226,7 @@ namespace storm { outstream << std::endl << "Statistics Region Model Checker Statistics:" << std::endl; outstream << "-----------------------------------------------" << std::endl; outstream << "Model: " << this->model.getNumberOfStates() << " states, " << this->model.getNumberOfTransitions() << " transitions." << std::endl; - outstream << "Reduced model: " << this->subsystem.getNumberOfSetBits() << " states, " << subsystemTransitions << "transitions" << std::endl; + outstream << "Reduced model: " << this->subsystem.getNumberOfSetBits() << " states, " << subsystemTransitions << " transitions" << std::endl; outstream << "Formula: " << *this->probabilityOperatorFormula << std::endl; outstream << (this->hasOnlyLinearFunctions ? "A" : "Not a") << "ll occuring functions in the model are linear" << std::endl; outstream << "Number of checked regions: " << this->numOfCheckedRegions << std::endl; @@ -1230,7 +1235,7 @@ namespace storm { outstream << " AllViolated: " << this->numOfRegionsAllViolated << "(" << this->numOfRegionsAllViolated*100/this->numOfCheckedRegions << "%)" << std::endl; outstream << " ExistsBoth: " << this->numOfRegionsExistsBoth << "(" << this->numOfRegionsExistsBoth*100/this->numOfCheckedRegions << "%)" << std::endl; outstream << " Unsolved: " << this->numOfCheckedRegions - numOfSolvedRegions << "(" << (this->numOfCheckedRegions - numOfSolvedRegions)*100/this->numOfCheckedRegions << "%)" << std::endl; - outstream << " -- " << std::endl; + outstream << " -- Note: %-numbers are relative to the NUMBER of regions, not the size of their area --" << std::endl; outstream << " " << this->numOfRegionsSolvedThroughSampling << " regions solved through Sampling" << std::endl; outstream << " " << this->numOfRegionsSolvedThroughApproximation << " regions solved through Approximation" << std::endl; outstream << " " << this->numOfRegionsSolvedThroughSubsystemSmt << " regions solved through SubsystemSmt" << std::endl; @@ -1239,8 +1244,8 @@ namespace storm { outstream << "Running times:" << std::endl; outstream << " " << timeOverallInMilliseconds.count() << "ms overall" << std::endl; outstream << " " << timePreprocessingInMilliseconds.count() << "ms Preprocessing including... " << std::endl; - outstream << " " << timeInitialStateEliminationInMilliseconds.count() << "ms Initial state elimination including..." << std::endl; - outstream << " " << timeComputeReachProbFunctionInMilliseconds.count() << "ms to compute the reachability probability function" << std::endl; + outstream << " " << timeInitialStateEliminationInMilliseconds.count() << "ms Initial state elimination of const transitions" << std::endl; + outstream << " " << timeComputeReachProbFunctionInMilliseconds.count() << "ms to compute the reachability probability function" << std::endl; outstream << " " << timeCheckRegionInMilliseconds.count() << "ms Region Check including... " << std::endl; outstream << " " << timeSammplingInMilliseconds.count() << "ms Sampling " << std::endl; outstream << " " << timeApproximationInMilliseconds.count() << "ms Approximation including... " << std::endl; diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h index c3fcedfee..f2ed8f521 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h @@ -249,6 +249,8 @@ namespace storm { storm::storage::sparse::state_type const& initState ); + ParametricType getReachProbFunction(); + //Computes the reachability probability function by performing state elimination ParametricType computeReachProbFunction( storm::storage::BitVector const& subsys, @@ -289,7 +291,7 @@ namespace storm { * If this approximation already yields that the property is satisfied/violated in the whole region, * true is returned and the regioncheckresult of the region is changed accordingly. * The computed bounds are stored in the given vectors. - * However, it only the lowerBounds (or upperBounds) need to be computed in order to get a conclusive result, + * However, if only the lowerBounds (or upperBounds) need to be computed in order to prove ALLSAT or ALLVIOLATED, * the upperBounds (or lowerBounds) vector remains untouched. */ bool checkApproximativeProbabilities(ParameterRegion& region, std::vector& lowerBounds, std::vector& upperBounds); @@ -363,12 +365,9 @@ namespace storm { // stores the different substitutions of the variables std::vector> approxMdpSubstitutions; - - - - // The function for the reachability probability in the initial state ParametricType reachProbFunction; + bool isReachProbFunctionComputed; // runtimes and other information for statistics. diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 3dd8910dc..7372580e4 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -251,6 +251,7 @@ namespace storm { template SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), nontrivialRowGrouping(other.nontrivialRowGrouping), rowGroupIndices(other.rowGroupIndices) { // Intentionally left empty. + std::cout << "!!!! copying matrix (constructor)" << std::endl; } template @@ -258,6 +259,7 @@ namespace storm { storm::storage::BitVector rowConstraint(other.getRowCount(), true); storm::storage::BitVector columnConstraint(other.getColumnCount(), true); *this = other.getSubmatrix(false, rowConstraint, columnConstraint, insertDiagonalElements); + std::cout << "!!!! copying matrix (insertingDiagElements)" << std::endl; } template @@ -271,6 +273,7 @@ namespace storm { template SparseMatrix::SparseMatrix(index_type columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices, bool nontrivialRowGrouping) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), nontrivialRowGrouping(nontrivialRowGrouping), rowGroupIndices(rowGroupIndices) { this->updateNonzeroEntryCount(); + std::cout << "!!!! copying matrix (copying Ingredients)" << std::endl; } template @@ -280,6 +283,7 @@ namespace storm { template SparseMatrix& SparseMatrix::operator=(SparseMatrix const& other) { + std::cout << "!!!! copying matrix (operator=)" << std::endl; // Only perform assignment if source and target are not the same. if (this != &other) { rowCount = other.rowCount; diff --git a/src/utility/cli.h b/src/utility/cli.h index b466ba5a5..ebeb28dd2 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -223,7 +223,11 @@ namespace storm { getrusage(RUSAGE_SELF, &ru); std::cout << "===== Statistics ==============================" << std::endl; +#ifndef LINUX std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl; +#else + std::cout << "peak memory usage: " << ru.ru_maxrss/1024 << "MB" << std::endl; +#endif std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; std::cout << "===============================================" << std::endl; #else @@ -704,6 +708,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } } + printUsage(); } } }