diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index ecf795182..db972f49a 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -1233,6 +1233,8 @@ namespace storm { template class StatePriorityQueue; template class SparseDtmcEliminationModelChecker>; + template uint_fast64_t estimateComplexity(double const& value); + #ifdef STORM_HAVE_CARL template class StatePriorityQueue; diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 242995834..c40fadceb 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -7,6 +7,7 @@ #include "DFTIsomorphism.h" #include "utility/iota_n.h" +#include "utility/vector.h" namespace storm { namespace storage { @@ -233,12 +234,8 @@ namespace storm { template DFT DFT::optimize() const { std::vector modIdea = findModularisationRewrite(); - std::cout << "Modularisation idea: " << std::endl; - - for( auto const& i : modIdea ) { - std::cout << i << ", "; - } - + STORM_LOG_DEBUG("Modularisation idea: " << storm::utility::vector::toString(modIdea)); + if (modIdea.empty()) { // No rewrite needed return *this; @@ -316,6 +313,7 @@ namespace storm { builder.setTopLevel(mElements[mTopLevelIndex]->name()); // TODO use reference? DFT newDft = builder.build(); + STORM_LOG_TRACE(newDft.getElementsString()); return newDft.optimize(); } @@ -487,20 +485,20 @@ namespace storm { std::sort(sortedParent2Ids.begin(), sortedParent2Ids.end()); if(influencedElem1Ids == getSortedParentAndOutDepIds(*it2)) { - std::cout << "Considering ids " << *it1 << ", " << *it2 << " for isomorphism." << std::endl; + STORM_LOG_TRACE("Considering ids " << *it1 << ", " << *it2 << " for isomorphism."); bool isSymmetry = false; std::vector isubdft1 = getGate(*it1)->independentSubDft(false); std::vector isubdft2 = getGate(*it2)->independentSubDft(false); if(isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) { continue; } - std::cout << "Checking subdfts from " << *it1 << ", " << *it2 << " for isomorphism." << std::endl; + STORM_LOG_TRACE("Checking subdfts from " << *it1 << ", " << *it2 << " for isomorphism."); auto LHS = colouring.colourSubdft(isubdft1); auto RHS = colouring.colourSubdft(isubdft2); auto IsoCheck = DFTIsomorphismCheck(LHS, RHS, *this); isSymmetry = IsoCheck.findIsomorphism(); if(isSymmetry) { - std::cout << "subdfts are symmetric" << std::endl; + STORM_LOG_TRACE("Subdfts are symmetric"); foundEqClassFor.insert(*it2); if(symClass.empty()) { for(auto const& i : isubdft1) { @@ -534,20 +532,13 @@ namespace storm { // suitable parent gate! - Lets check the independent submodules of the children auto const& children = std::static_pointer_cast>(e)->children(); for(auto const& child : children) { - //std::cout << "check idea for: " << child->id() << std::endl;; auto ISD = std::static_pointer_cast>(child)->independentSubDft(true); // In the ISD, check for other children: - //std::cout << "** subdft = "; - for(auto const& isdelemid : ISD) { - std::cout << isdelemid << " "; - } - std::cout << std::endl; std::vector rewrite = {e->id(), child->id()}; for(size_t isdElemId : ISD) { if(isdElemId == child->id()) continue; if(std::find_if(children.begin(), children.end(), [&isdElemId](std::shared_ptr> const& e) { return e->id() == isdElemId; } ) != children.end()) { - //std::cout << "** found child in subdft: " << isdElemId << std::endl; rewrite.push_back(isdElemId); } } diff --git a/src/storage/dft/DFTIsomorphism.h b/src/storage/dft/DFTIsomorphism.h index 542fa954a..b1f845b9f 100644 --- a/src/storage/dft/DFTIsomorphism.h +++ b/src/storage/dft/DFTIsomorphism.h @@ -249,7 +249,7 @@ namespace storage { } void colourize(std::shared_ptr> const& gate) { - std::cout << "Colour " << gate->id() << ": " << gate->type() << " " << gate->nrChildren() << " " << gate->rank() << "." << std::endl; + STORM_LOG_TRACE("Colour " << gate->id() << ": " << gate->type() << " " << gate->nrChildren() << " " << gate->rank() << "."); gateColour[gate->id()] = gateColourizer(gate->type(), gate->nrChildren(), gate->nrParents(), 0, gate->rank()); } @@ -336,7 +336,7 @@ namespace storage { initializePermutationsAndTreatTrivialGroups(bleft.gateCandidates, bright.gateCandidates, currentPermutations.gateCandidates); initializePermutationsAndTreatTrivialGroups(bleft.pdepCandidates, bright.pdepCandidates, currentPermutations.pdepCandidates); initializePermutationsAndTreatTrivialGroups(bleft.restrictionCandidates, bright.restrictionCandidates, currentPermutations.restrictionCandidates); - std::cout << bijection.size() << " vs. " << bleft.size() << " vs. " << bright.size() << std::endl; + STORM_LOG_TRACE(bijection.size() << " vs. " << bleft.size() << " vs. " << bright.size()); assert(bijection.size() == bleft.size()); } diff --git a/src/storage/dft/SymmetricUnits.h b/src/storage/dft/SymmetricUnits.h index 6521ee8d2..58a70e492 100644 --- a/src/storage/dft/SymmetricUnits.h +++ b/src/storage/dft/SymmetricUnits.h @@ -12,16 +12,14 @@ namespace storm { inline std::ostream& operator<<(std::ostream& os, DFTIndependentSymmetries const& s) { for(auto const& cl : s.groups) { - std::cout << "SYM GROUP FOR " << cl.first << std::endl; + os << "Symmetry group for " << cl.first << std::endl; for(auto const& eqClass : cl.second) { for(auto const& i : eqClass) { - std::cout << i << " "; + os << i << " "; } - std::cout << std::endl; + os << std::endl; } } - - return os; } } diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 6240bf374..49f97b76b 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -20,53 +20,65 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false) manager.setFromString(""); // Parsing DFT - std::cout << "Parsing DFT file..." << std::endl; + std::chrono::high_resolution_clock::time_point parsingStart = std::chrono::high_resolution_clock::now(); storm::parser::DFTGalileoParser parser; storm::storage::DFT dft = parser.parseDFT(filename); - std::cout << "Built data structure" << std::endl; - std::cout << "Parse formula..." << std::endl; std::vector> parsedFormulas = storm::parseFormulasForExplicit(property); std::vector> formulas(parsedFormulas.begin(), parsedFormulas.end()); assert(formulas.size() == 1); - std::cout << "Parsed formula." << std::endl; + // Optimize DFT dft = dft.optimize(); - std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); if(symred) { auto colouring = dft.colourDFT(); symmetries = dft.findSymmetries(colouring); - std::cout << "Symmetries: " << symmetries << std::endl; + std::cout << "Found " << symmetries.groups.size() << " symmetries." << std::endl; + STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); } - + std::chrono::high_resolution_clock::time_point parsingEnd = std::chrono::high_resolution_clock::now(); + // Building Markov Automaton std::cout << "Building Model..." << std::endl; storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries); typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; // TODO initialize this with the formula std::shared_ptr> model = builder.buildModel(labeloptions); - std::cout << "Built Model" << std::endl; - - - model->printModelInformationToStream(std::cout); + //model->printModelInformationToStream(std::cout); std::cout << "No. states (Explored): " << model->getNumberOfStates() << std::endl; std::cout << "No. transitions (Explored): " << model->getNumberOfTransitions() << std::endl; + std::chrono::high_resolution_clock::time_point explorationEnd = std::chrono::high_resolution_clock::now(); + // Bisimulation if (model->isOfType(storm::models::ModelType::Ctmc)) { std::cout << "Bisimulation..." << std::endl; model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), formulas, storm::storage::BisimulationType::Weak)->template as>(); - model->printModelInformationToStream(std::cout); + //model->printModelInformationToStream(std::cout); } - std::cout << "No. states (Bisimulation): " << model->getNumberOfStates() << std::endl; std::cout << "No. transitions (Bisimulation): " << model->getNumberOfTransitions() << std::endl; + std::chrono::high_resolution_clock::time_point bisimulationEnd = std::chrono::high_resolution_clock::now(); // Model checking std::cout << "Model checking..." << std::endl; std::unique_ptr result(storm::verifySparseModel(model, formulas[0])); assert(result); - std::cout << "Result: "; result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + + // Times + std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now(); + std::chrono::duration parsingTime = parsingEnd - parsingStart; + std::chrono::duration explorationTime = explorationEnd - parsingEnd; + std::chrono::duration bisimulationTime = bisimulationEnd - explorationEnd; + std::chrono::duration modelCheckingTime = modelCheckingEnd - bisimulationEnd; + std::chrono::duration totalTime = modelCheckingEnd - parsingStart; + std::cout << "Times:" << std::endl; + std::cout << "Parsing:\t" << parsingTime.count() << std::endl; + std::cout << "Exploration:\t" << explorationTime.count() << std::endl; + std::cout << "Bisimulaton:\t" << bisimulationTime.count() << std::endl; + std::cout << "Modelchecking:\t" << modelCheckingTime.count() << std::endl; + std::cout << "Total:\t\t" << totalTime.count() << std::endl; + std::cout << "Result: "; std::cout << *result << std::endl; } diff --git a/src/utility/vector.h b/src/utility/vector.h index aa526cf54..b5480de9b 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -705,6 +705,26 @@ namespace storm { assert(result.size() == filter.getNumberOfSetBits()); return result; } + + /*! + * Output vector as string. + * + * @param vector Vector to output. + * @return String containing the representation of the vector. + */ + template + std::string toString(std::vector vector) { + std::stringstream stream; + stream << "vector (" << vector.size() << ") [ "; + for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) { + stream << vector[i] << ", "; + } + if (!vector.empty()) { + stream << vector.back(); + } + stream << " ]"; + return stream.str(); + } } // namespace vector } // namespace utility } // namespace storm