From 3f44b1295f844289d1ce5442fb8a93c4acc273e5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 9 Feb 2015 17:07:51 +0100 Subject: [PATCH] started polishing pstorm a bit Former-commit-id: bd9c2a42a7f9e01cdd81d7c5b15c08c03373e88a --- src/stormParametric.cpp | 378 +++++----------------------------------- src/utility/cli.h | 8 +- 2 files changed, 51 insertions(+), 335 deletions(-) diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 09cfa47d5..1346a8431 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -17,112 +17,6 @@ #include "src/storage/parameters.h" #include "src/models/Dtmc.h" -//std::tuple>, boost::optional>, boost::optional, boost::optional, boost::optional> computeReachabilityProbability(storm::models::Dtmc const& dtmc, std::shared_ptr> const& filterFormula) { -// // The first thing we need to do is to make sure the formula is of the correct form and - if so - extract -// // the bitvector representation of the atomic propositions. -// -// std::shared_ptr> stateFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); -// std::shared_ptr> pathFormula; -// boost::optional threshold; -// boost::optional strict; -// if (stateFormula != nullptr) { -// std::shared_ptr> probabilisticBoundFormula = std::dynamic_pointer_cast>(stateFormula); -// STORM_LOG_THROW(probabilisticBoundFormula != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties are permitted."); -// STORM_LOG_THROW(probabilisticBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS_EQUAL || probabilisticBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties with upper probability bounds are permitted."); -// -// threshold = probabilisticBoundFormula->getBound(); -// strict = probabilisticBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS; -// pathFormula = probabilisticBoundFormula->getChild(); -// } else { -// pathFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); -// } -// -// STORM_LOG_THROW(pathFormula != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties are permitted."); -// -// std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(pathFormula); -// std::shared_ptr> phiStateFormula; -// std::shared_ptr> psiStateFormula; -// if (untilFormula != nullptr) { -// phiStateFormula = untilFormula->getLeft(); -// psiStateFormula = untilFormula->getRight(); -// } else { -// std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(pathFormula); -// STORM_LOG_THROW(eventuallyFormula != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties are permitted."); -// phiStateFormula = std::shared_ptr>(new storm::properties::prctl::Ap("true")); -// psiStateFormula = eventuallyFormula->getChild(); -// } -// -// // Now we need to make sure the formulas defining the phi and psi states are just labels. -// std::shared_ptr> phiStateFormulaApFormula = std::dynamic_pointer_cast>(phiStateFormula); -// std::shared_ptr> psiStateFormulaApFormula = std::dynamic_pointer_cast>(psiStateFormula); -// STORM_LOG_THROW(phiStateFormulaApFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *phiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); -// STORM_LOG_THROW(psiStateFormulaApFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *psiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); -// -// // Now retrieve the appropriate bitvectors from the atomic propositions. -// storm::storage::BitVector phiStates = phiStateFormulaApFormula->getAp() != "true" ? dtmc.getLabeledStates(phiStateFormulaApFormula->getAp()) : storm::storage::BitVector(dtmc.getNumberOfStates(), true); -// storm::storage::BitVector psiStates = dtmc.getLabeledStates(psiStateFormulaApFormula->getAp()); -// -// // Do some sanity checks to establish some required properties. -// STORM_LOG_THROW(dtmc.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); -// -// // Then, compute the subset of states that has a probability of 0 or 1, respectively. -// std::pair statesWithProbability01 = storm::utility::graph::performProb01(dtmc, phiStates, psiStates); -// storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; -// storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; -// storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); -// -// // If the initial state is known to have either probability 0 or 1, we can directly return the result. -// if (dtmc.getInitialStates().isDisjointFrom(maybeStates)) { -// STORM_LOG_DEBUG("The probability of all initial states was found in a preprocessing step."); -// return statesWithProbability0.get(*dtmc.getInitialStates().begin()) ? storm::utility::constantZero() : storm::utility::constantOne(); -// } -// -// // Determine the set of states that is reachable from the initial state without jumping over a target state. -// storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(dtmc.getTransitionMatrix(), dtmc.getInitialStates(), maybeStates, statesWithProbability1); -// -// // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). -// maybeStates &= reachableStates; -// -// // Create a vector for the probabilities to go to a state with probability 1 in one step. -// std::vector oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); -// -// // Determine the set of initial states of the sub-DTMC. -// storm::storage::BitVector newInitialStates = dtmc.getInitialStates() % maybeStates; -// -// // We then build the submatrix that only has the transitions of the maybe states. -// storm::storage::SparseMatrix submatrix = dtmc.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); -// -// // To be able to apply heuristics later, we now determine the distance of each state to the initial state. -// std::vector> stateQueue; -// stateQueue.reserve(submatrix.getRowCount()); -// storm::storage::BitVector statesInQueue(submatrix.getRowCount()); -// std::vector distances(submatrix.getRowCount()); -// -// storm::storage::sparse::state_type currentPosition = 0; -// for (auto const& initialState : newInitialStates) { -// stateQueue.emplace_back(initialState, 0); -// statesInQueue.set(initialState); -// } -// -// // Perform a BFS. -// while (currentPosition < stateQueue.size()) { -// std::pair const& stateDistancePair = stateQueue[currentPosition]; -// distances[stateDistancePair.first] = stateDistancePair.second; -// -// for (auto const& successorEntry : submatrix.getRow(stateDistancePair.first)) { -// if (!statesInQueue.get(successorEntry.getColumn())) { -// stateQueue.emplace_back(successorEntry.getColumn(), stateDistancePair.second + 1); -// statesInQueue.set(successorEntry.getColumn()); -// } -// } -// ++currentPosition; -// } -// -// storm::modelchecker::reachability::SparseSccModelChecker modelchecker; -// -// return std::make_tuple(modelchecker.computeReachabilityProbability(submatrix, oneStepProbabilities, submatrix.transpose(), newInitialStates, phiStates, psiStates, distances),submatrix, oneStepProbabilities, newInitialStates, threshold, strict); -//} - template void printApproximateResult(ValueType const& value) { // Intentionally left empty. @@ -146,10 +40,15 @@ void check() { std::string const& constants = storm::settings::generalSettings().getConstantDefinitionString(); storm::prism::Program program = storm::parser::PrismParser::parse(programFile); - STORM_LOG_THROW(storm::settings::generalSettings().isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to perform model checking without a property."); - std::shared_ptr formula = storm::parser::FormulaParser(program.getManager().getSharedPointer()).parseFromString(storm::settings::generalSettings().getProperty()); + boost::optional> formula; + if (storm::settings::generalSettings().isPropertySet()) { + formula = storm::parser::FormulaParser(program.getManager().getSharedPointer()).parseFromString(storm::settings::generalSettings().getProperty()); + } - typename storm::builder::ExplicitPrismModelBuilder::Options options(*formula); + typename storm::builder::ExplicitPrismModelBuilder::Options options; + if (formula) { + options = typename storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); + } options.addConstantDefinitionsFromString(program, storm::settings::generalSettings().getConstantDefinitionString()); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); @@ -158,60 +57,57 @@ void check() { if (model->hasTransitionRewards()) { model->convertTransitionRewardsToStateRewards(); } - - model->printModelInformationToStream(std::cout); - + // Program Translation Time Measurement, End std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now(); std::cout << "Parsing and translating the model took " << std::chrono::duration_cast(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl; - if (model->hasTransitionRewards()) { - model->convertTransitionRewardsToStateRewards(); - } - - std::shared_ptr> dtmc = model->template as>(); - - storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); - STORM_LOG_THROW(modelchecker.canHandle(*formula), storm::exceptions::InvalidPropertyException, "Model checker cannot handle the property: '" << *formula << "'."); + model->printModelInformationToStream(std::cout); - std::cout << "Checking formula " << *formula << std::endl; + if (formula) { + STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidArgumentException, "The given model is not a DTMC and, hence, not currently supported."); + std::shared_ptr> dtmc = model->template as>(); - bool checkRewards = formula->isRewardOperatorFormula(); + storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); + STORM_LOG_THROW(modelchecker.canHandle(*formula.get()), storm::exceptions::InvalidPropertyException, "Model checker cannot handle the property: '" << *formula.get() << "'."); - // Perform bisimulation minimization if requested. - if (storm::settings::generalSettings().isBisimulationSet()) { - typename storm::storage::DeterministicModelBisimulationDecomposition::Options options(*dtmc, *formula); - options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet(); + std::cout << "Checking formula " << *formula.get() << std::endl; - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, options); - *dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as>()); - - dtmc->printModelInformationToStream(std::cout); - } - - assert(dtmc); - - storm::modelchecker::reachability::CollectConstraints constraintCollector; - constraintCollector(*dtmc); - - std::unique_ptr result = modelchecker.check(*formula); - ValueType valueFunction = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; - - if (storm::settings::parametricSettings().exportResultToFile()) { - storm::utility::exportParametricMcResult(valueFunction, constraintCollector); - } - - // Report the result. - STORM_PRINT_AND_LOG(std::endl << "Result (initial state): "); - result->writeToStream(std::cout, model->getInitialStates()); - if (std::is_same::value) { - printApproximateResult(valueFunction); + // Perform bisimulation minimization if requested. + if (storm::settings::generalSettings().isBisimulationSet()) { + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options(*dtmc, *formula.get()); + options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet(); + + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, options); + *dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as>()); + + dtmc->printModelInformationToStream(std::cout); + } + + STORM_LOG_THROW(dtmc, storm::exceptions::InvalidStateException, "Preprocessing went wrong."); + + storm::modelchecker::reachability::CollectConstraints constraintCollector; + constraintCollector(*dtmc); + + std::unique_ptr result = modelchecker.check(*formula.get()); + ValueType valueFunction = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; + + if (storm::settings::parametricSettings().exportResultToFile()) { + storm::utility::exportParametricMcResult(valueFunction, constraintCollector); + } + + // Report the result. + STORM_PRINT_AND_LOG(std::endl << "Result (initial state): "); + result->writeToStream(std::cout, model->getInitialStates()); + if (std::is_same::value) { + printApproximateResult(valueFunction); + } + std::cout << std::endl; } - std::cout << std::endl; } /*! - * Main entry point of the executable storm. + * Main entry point of the executable pstorm. */ int main(const int argc, const char** argv) { try { @@ -227,44 +123,6 @@ int main(const int argc, const char** argv) { std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Total time: " << std::chrono::duration_cast(totalTimeEnd - totalTimeStart).count() << "ms." << std::endl << std::endl; -// // Perform bisimulation minimization if requested. -// if (storm::settings::generalSettings().isBisimulationSet()) { -// storm::storage::DeterministicModelStrongBisimulationDecomposition bisimulationDecomposition(*dtmc, true); -// dtmc = bisimulationDecomposition.getQuotient()->as>(); -// -// dtmc->printModelInformationToStream(std::cout); -// } - -// storm::RationalFunction valueFunction2 = modelchecker.computeReachabilityProbability(*dtmc, filterFormula); -// STORM_PRINT_AND_LOG(std::endl << "computed value2 " << valueFunction2 << std::endl); -// -// storm::RationalFunction diff = storm::utility::simplify(valueFunction - valueFunction2); -// STORM_PRINT_AND_LOG(std::endl << "difference: " << diff << std::endl); - - // Get variables from parameter definitions in prism program. -// std::set parameters; -// for(auto constant : program.getConstants()) -// { -// if(!constant.isDefined()) -// { -// std::cout << "got undef constant " << constant.getName() << std::endl; -// carl::Variable p = carl::VariablePool::getInstance().findVariableWithName(constant.getName()); -// assert(p != storm::Variable::NO_VARIABLE); -// parameters.insert(p); -// } -// } - -// STORM_LOG_ASSERT(parameters == valueFunction.gatherVariables(), "Parameters in result and program definition do not coincide."); - -// if(storm::settings::parametricSettings().exportResultToFile()) { -// storm::utility::exportParametricMcResult(valueFunction, constraintCollector); -// } - -// if (storm::settings::parametricSettings().exportToSmt2File() && std::get<1>(result) && std::get<2>(result) && std::get<3>(result) && std::get<4>(result) && std::get<5>(result)) { -// storm::modelchecker::reachability::DirectEncoding dec; -// storm::utility::exportStringStreamToFile(dec.encodeAsSmt2(std::get<1>(result).get(), std::get<2>(result).get(), parameters, std::get<3>(result).get(), carl::rationalize(std::get<4>(result).get()), std::get<5>(result).get()), "out.smt"); -// } - // All operations have now been performed, so we clean up everything and terminate. storm::utility::cli::cleanUp(); return 0; @@ -273,144 +131,4 @@ int main(const int argc, const char** argv) { } catch (std::exception const& exception) { STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM to terminate. The message of this exception is: " << exception.what()); } -} - -//#include -//#include -// -//#include "stormParametric.h" -//#include "adapters/ExplicitModelAdapter.h" -//#include "utility/graph.h" -//#include "modelchecker/reachability/DirectEncoding.h" -//#include "storage/BitVector.h" -//#include "storage/DeterministicTransition.h" -// -//using storm::storage::StateId; -// -//namespace storm -//{ -// -// -//void ParametricStormEntryPoint::createModel() -//{ -// mModel = storm::adapters::ExplicitModelAdapter::translateProgram(mProgram, mConstants); -// mModel->printModelInformationToStream(std::cout); -//} -// -//std::string ParametricStormEntryPoint::reachabilityToSmt2(std::string const& label) -//{ -// -// storm::storage::BitVector phiStates(mModel->getNumberOfStates(), true); -// storm::storage::BitVector initStates = mModel->getInitialStates(); -// storm::storage::BitVector targetStates = mModel->getLabeledStates(label); -// -// std::shared_ptr> dtmc = mModel->as>(); -// // 1. make target states absorbing. -// dtmc->makeAbsorbing(targetStates); -// // 2. throw away anything which does not add to the reachability probability. -// // 2a. remove non productive states -// storm::storage::BitVector productiveStates = utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, targetStates); -// // 2b. calculate set of states wich -// storm::storage::BitVector almostSurelyReachingTargetStates = ~utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, ~productiveStates); -// // 2c. Make such states also target states. -// dtmc->makeAbsorbing(almostSurelyReachingTargetStates); -// // 2d. throw away non reachable states -// storm::storage::BitVector reachableStates = utility::graph::performProbGreater0(*dtmc, dtmc->getTransitionMatrix(), phiStates, initStates); -// storm::storage::BitVector bv = productiveStates & reachableStates; -// dtmc->getStateLabeling().addAtomicProposition("__targets__", targetStates | almostSurelyReachingTargetStates); -// models::Dtmc subdtmc = dtmc->getSubDtmc(bv); -// -// phiStates = storm::storage::BitVector(subdtmc.getNumberOfStates(), true); -// initStates = subdtmc.getInitialStates(); -// targetStates = subdtmc.getLabeledStates("__targets__"); -// storm::storage::BitVector deadlockStates(phiStates); -// deadlockStates.set(subdtmc.getNumberOfStates()-1,false); -// -// // Search for states with only one non-deadlock successor. -// std::map> chainedStates; -// StateId nrStates = subdtmc.getNumberOfStates(); -// StateId deadlockState = nrStates - 1; -// for(StateId source = 0; source < nrStates - 1; ++source) -// { -// if(targetStates[source]) -// { -// continue; -// } -// storage::DeterministicTransition productiveTransition(nrStates); -// for(auto const& transition : subdtmc.getRows(source)) -// { -// if(productiveTransition.targetState() == nrStates) -// { -// // first transition. -// productiveTransition = transition; -// } -// else -// { -// // second transition -// if(transition.first != deadlockState) -// { -// productiveTransition.targetState() = nrStates; -// break; -// } -// } -// } -// if(productiveTransition.targetState() != nrStates) -// { -// chainedStates.emplace(source, productiveTransition); -// } -// } -// storage::BitVector eliminatedStates(nrStates, false); -// for(auto & chainedState : chainedStates) -// { -// assert(chainedState.first != chainedState.second.targetState()); -// auto it = chainedStates.find(chainedState.second.targetState()); -// if(it != chainedStates.end()) -// { -// //std::cout << "----------------------------" << std::endl; -// //std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl; -// //std::cout << it->first << " -- " << it->second.probability() << " --> " << it->second.targetState() << std::endl; -// chainedState.second.targetState() = it->second.targetState(); -// chainedState.second.probability() *= it->second.probability(); -// //std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl; -// //std::cout << "----------------------------" << std::endl; -// chainedStates.erase(it); -// eliminatedStates.set(it->first, true); -// } -// } -// -// -// for(auto chainedState : chainedStates) -// { -// if(!eliminatedStates[chainedState.first]) -// { -// std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl; -// } -// } -// -// storage::StronglyConnectedComponentDecomposition sccs(subdtmc); -// std::cout << sccs << std::endl; -// -// modelchecker::reachability::DirectEncoding dec; -// std::vector parameters; - -// return dec.encodeAsSmt2(subdtmc, parameters, subdtmc.getLabeledStates("init"), subdtmc.getLabeledStates("__targets__"), mpq_class(1,2)); -// -//} -// -// -//void storm_parametric(const std::string& constants, const storm::prism::Program& program) -//{ -// ParametricStormEntryPoint entry(constants, program); -// entry.createModel(); -// storm::settings::Settings* s = storm::settings::Settings::getInstance(); -// if(s->isSet("reachability")) -// { -// std::ofstream fstream("test.smt2"); -// fstream << entry.reachabilityToSmt2(s->getOptionByLongName("reachability").getArgument(0).getValueAsString()); -// fstream.close(); -// } -// -// -//} -// -//} +} \ No newline at end of file diff --git a/src/utility/cli.h b/src/utility/cli.h index 6319144d5..32539dade 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -129,7 +129,7 @@ namespace storm { * Prints the header including information about the linked libraries. */ void printHeader(const int argc, const char* argv[]) { - std::cout << "PROPhESY" << std::endl; + std::cout << "StoRM" << std::endl; std::cout << "--------" << std::endl << std::endl; @@ -138,7 +138,7 @@ namespace storm { std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; #endif #ifdef STORM_HAVE_GLPK -// std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl; + std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl; #endif #ifdef STORM_HAVE_GUROBI std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl; @@ -160,7 +160,7 @@ namespace storm { commandStream << argv[i] << " "; } std::cout << "Command line arguments: " << commandStream.str() << std::endl; -// std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl; + std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl; } @@ -218,8 +218,6 @@ namespace storm { storm::settings::SettingsManager& manager = storm::settings::mutableManager(); try { manager.setFromCommandLine(argc, argv); -// std::vector arguments = {"--symbolic", "/Users/chris/work/prism-trunk/prism-examples/self-stabilisation/herman/herman7.mod", "--prop", "R=? [F \"stable\"]"}; -// manager.setFromExplodedString(arguments); } catch (storm::exceptions::OptionParserException& e) { manager.printHelp(); throw e;