diff --git a/src/adapters/extendedCarl.h b/src/adapters/extendedCarl.h index e72d88a55..90c1cef4d 100644 --- a/src/adapters/extendedCarl.h +++ b/src/adapters/extendedCarl.h @@ -12,8 +12,8 @@ #include #include #include +#include -#undef LOG_ASSERT namespace carl { template @@ -31,6 +31,5 @@ inline size_t hash_value(carl::RationalFunction const& f) } -#include "src/exceptions/ExceptionMacros.h" #endif \ No newline at end of file diff --git a/src/modelchecker/reachability/CollectConstraints.h b/src/modelchecker/reachability/CollectConstraints.h new file mode 100644 index 000000000..cd7fa90f3 --- /dev/null +++ b/src/modelchecker/reachability/CollectConstraints.h @@ -0,0 +1,63 @@ +/** + * @file: CollectConstraints.h + * @author: Sebastian Junges + * + * @since October 8, 2014 + */ + +#pragma once +#include "src/models/Dtmc.h" + + +namespace storm { +namespace modelchecker { + namespace reachability { + template + class CollectConstraints + { + private: + std::unordered_set> wellformedConstraintSet; + std::unordered_set> graphPreservingConstraintSet; + + public: + std::unordered_set> const& wellformedConstraints() const { + return this->wellformedConstraintSet; + } + + std::unordered_set> const& graphPreservingConstraints() const { + return this->graphPreservingConstraintSet; + } + + void process(storm::models::Dtmc const& dtmc) + { + for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) + { + ValueType sum; + assert(storm::utility::isZero(sum)); + for(auto const& transition : dtmc.getRows(state)) + { + sum += transition.getValue(); + if(!transition.getValue().isConstant()) + { + wellformedConstraintSet.emplace(transition.getValue() - 1, storm::CompareRelation::LEQ); + wellformedConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GEQ); + graphPreservingConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GT); + } + } + assert(!sum.isConstant() || storm::utility::isOne(sum)); + if(!sum.isConstant()) { + wellformedConstraintSet.emplace(sum - 1, storm::CompareRelation::EQ); + } + + } + } + + void operator()(storm::models::Dtmc const& dtmc) + { + process(dtmc); + } + + }; + } +} +} diff --git a/src/modelchecker/reachability/DirectEncoding.h b/src/modelchecker/reachability/DirectEncoding.h index 6bc2506e7..2c9f43e7c 100644 --- a/src/modelchecker/reachability/DirectEncoding.h +++ b/src/modelchecker/reachability/DirectEncoding.h @@ -90,7 +90,7 @@ namespace storm smt2 << ("reachability"); - carl::CompareRelation thresholdRelation = lessequal ? carl::CompareRelation::LE : carl::CompareRelation::GE; + carl::CompareRelation thresholdRelation = lessequal ? carl::CompareRelation::LEQ : carl::CompareRelation::GEQ; smt2 << carl::Constraint(initStateReachSum - threshold, thresholdRelation); smt2 << carl::io::smt2flag::CHECKSAT; smt2 << carl::io::smt2flag::MODEL; diff --git a/src/settings/Option.h b/src/settings/Option.h index d8a1d9d02..84fe10bca 100644 --- a/src/settings/Option.h +++ b/src/settings/Option.h @@ -284,11 +284,11 @@ namespace storm { STORM_LOG_THROW(!longName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty name."); STORM_LOG_THROW(!moduleName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty module name."); - bool longNameContainsNonAlpha = std::find_if(longName.begin(), longName.end(), [](char c) { return !std::isalpha(c); }) != longName.end(); - STORM_LOG_THROW(!longNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal name."); + bool longNameContainsNonAlpha = std::find_if(longName.begin(), longName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c)); }) != longName.end(); + STORM_LOG_THROW(!longNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal long name '" << longName << "'."); - bool shortNameContainsNonAlpha = std::find_if(shortName.begin(), shortName.end(), [](char c) { return !std::isalpha(c); }) != shortName.end(); - STORM_LOG_THROW(!shortNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal name."); + bool shortNameContainsNonAlpha = std::find_if(shortName.begin(), shortName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c)); }) != shortName.end(); + STORM_LOG_THROW(!shortNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal short name '" << shortName << "'."); // Then index all arguments. for (auto const& argument : arguments) { diff --git a/src/settings/modules/ParametricSettings.cpp b/src/settings/modules/ParametricSettings.cpp index 50e7dfa47..7b9cecbc4 100644 --- a/src/settings/modules/ParametricSettings.cpp +++ b/src/settings/modules/ParametricSettings.cpp @@ -10,12 +10,21 @@ namespace storm { const std::string ParametricSettings::entryStatesLastOptionName = "entrylast"; const std::string ParametricSettings::maximalSccSizeOptionName = "sccsize"; const std::string ParametricSettings::sortTrivialSccOptionName = "sorttrivial"; + const std::string ParametricSettings::encodeSmt2StrategyOptionName = "smt2strategy"; + const std::string ParametricSettings::exportSmt2DestinationPathOptionName = "smt2path"; + const std::string ParametricSettings::exportResultDestinationPathOptionName = "resultfile"; ParametricSettings::ParametricSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, sortTrivialSccOptionName, true, "Sets whether the trivial SCCs are to be eliminated in descending order with respect to their distances from the initial state.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.") .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxsize", "The maximal size of an SCC on which state elimination is applied.").setDefaultValueUnsignedInteger(20).setIsOptional(true).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, encodeSmt2StrategyOptionName, true, "Set the smt2 encoding strategy.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("strategy", "the used strategy").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportSmt2DestinationPathOptionName, true, "A path to a file where the result should be saved.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportResultDestinationPathOptionName, true, "A path to a file where the smt2 encoding should be saved.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build()); } bool ParametricSettings::isEliminateEntryStatesLastSet() const { @@ -30,6 +39,40 @@ namespace storm { return this->getOption(sortTrivialSccOptionName).getHasOptionBeenSet(); } + bool ParametricSettings::exportResultToFile() const { + return this->getOption(exportResultDestinationPathOptionName).getHasOptionBeenSet(); + } + + std::string ParametricSettings::exportResultPath() const { + return this->getOption(exportResultDestinationPathOptionName).getArgumentByName("path").getValueAsString(); + } + + bool ParametricSettings::exportToSmt2File() const { + return this->getOption(exportSmt2DestinationPathOptionName).getHasOptionBeenSet(); + } + + std::string ParametricSettings::exportSmt2Path() const { + return this->getOption(exportSmt2DestinationPathOptionName).getArgumentByName("path").getValueAsString(); + } + + ParametricSettings::Smt2EncodingStrategy ParametricSettings::smt2EncodingStrategy() const { + std::string strategy = this->getOption(encodeSmt2StrategyOptionName).getArgumentByName("strategy").getValueAsString(); + + if(strategy == "fts") { + return Smt2EncodingStrategy::FULL_TRANSITION_SYSTEM; + } else if(strategy == "rf") { + return Smt2EncodingStrategy::RATIONAL_FUNCTION; + } else { + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown smt2encoding strategy '" << strategy << "'."); + } + + + + } + + + + } // namespace modules } // namespace settings } // namespace storm \ No newline at end of file diff --git a/src/settings/modules/ParametricSettings.h b/src/settings/modules/ParametricSettings.h index 14a436efa..7bc5e2e29 100644 --- a/src/settings/modules/ParametricSettings.h +++ b/src/settings/modules/ParametricSettings.h @@ -12,6 +12,17 @@ namespace storm { */ class ParametricSettings : public ModuleSettings { public: + /** + * A type for saving the Smt2EncondingStrategy. + * + * FULL_TRANSITION_SYSTEM: The transition system should be reduced only with very basic operations. + * ONLY_SCC_ENTRY_STATES: Scc elimination should be performed, but no further reduction. + * HIGH_INDEGREE: State elimination but for states with a high indegree. + * RATIONAL_FUNCTION: The smt file should contain only the rational function. + */ + enum class Smt2EncodingStrategy {FULL_TRANSITION_SYSTEM, ONLY_SCC_ENTRY_STATES, HIGH_INDEGREE, RATIONAL_FUNCTION}; + + /*! * Creates a new set of parametric model checking settings that is managed by the given manager. * @@ -40,13 +51,47 @@ namespace storm { * @return True iff the trivial SCCs are to be sorted. */ bool isSortTrivialSccsSet() const; - + + /** + * Retrieves whether the model checking result should be exported to a file. + * @return True iff the result should be exported to a file. + */ + bool exportResultToFile() const; + + /** + * The path to a file location which should contain the model checking result. + * @return A path to a file location. + */ + std::string exportResultPath() const; + + /** + * Retrieves whether the encoding of the transition system should be exported to a file. + * @return True iff the smt file should be encoded. + */ + bool exportToSmt2File() const; + + /** + * The path to a file location which should contain the smt2 encoding. + * @return A path to a file location. + */ + std::string exportSmt2Path() const; + + /** + * Retrieves which encoding strategy should be used for generating the smt2 file. + * @return The encoding strategy to be used. + */ + Smt2EncodingStrategy smt2EncodingStrategy() const; + + const static std::string moduleName; private: const static std::string entryStatesLastOptionName; const static std::string maximalSccSizeOptionName; const static std::string sortTrivialSccOptionName; + const static std::string encodeSmt2StrategyOptionName; + const static std::string exportSmt2DestinationPathOptionName; + const static std::string exportResultDestinationPathOptionName; }; } // namespace modules diff --git a/src/storage/parameters.h b/src/storage/parameters.h index d718d9c64..923ef5fc9 100644 --- a/src/storage/parameters.h +++ b/src/storage/parameters.h @@ -11,7 +11,10 @@ namespace storm { typedef carl::MultivariatePolynomial Polynomial; - //typedef Parameter carl::Variable ; + typedef carl::Variable Variable; + + + typedef carl::CompareRelation CompareRelation; typedef carl::RationalFunction RationalFunction; } #endif diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 092378256..f5f0271a0 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -6,7 +6,10 @@ #include "src/exceptions/BaseException.h" #include "src/utility/macros.h" #include "src/utility/cli.h" +#include "src/utility/export.h" +#include "src/modelchecker/reachability/CollectConstraints.h" +#include "src/modelchecker/reachability/DirectEncoding.h" #include "src/modelchecker/reachability/SparseSccModelChecker.h" #include "src/storage/parameters.h" /*! @@ -31,19 +34,51 @@ int main(const int argc, const char** argv) { storm::prism::Program program = storm::parser::PrismParser::parse(programFile); std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(program, constants); + + 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; + std::shared_ptr> dtmc = model->as>(); + assert(dtmc); + storm::modelchecker::reachability::CollectConstraints constraintCollector; + constraintCollector(*dtmc); + + storm::modelchecker::reachability::SparseSccModelChecker modelChecker; STORM_LOG_THROW(storm::settings::generalSettings().isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to perform model checking without a property."); std::shared_ptr> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty()); - storm::RationalFunction value = modelChecker.computeReachabilityProbability(*model->as>(), filterFormula); + storm::RationalFunction value = modelChecker.computeReachabilityProbability(*dtmc, filterFormula); STORM_PRINT_AND_LOG(std::endl << "computed value " << value << std::endl); + + // Get variables from parameter definitions in prism program. + std::set parameters; + for(auto constant : program.getConstants()) + { + if(!constant.isDefined()) + { + carl::Variable p = carl::VariablePool::getInstance().findVariableWithName(constant.getName()); + assert(p != storm::Variable::NO_VARIABLE); + parameters.insert(p); + } + } + // + STORM_LOG_ASSERT(parameters == value.gatherVariables(), "Parameters in result and program definition do not coincide."); + + if(storm::settings::parametricSettings().exportResultToFile()) { + storm::utility::exportParametricMcResult(value, constraintCollector); + } + + if(storm::settings::parametricSettings().exportToSmt2File()) { + storm::modelchecker::reachability::DirectEncoding dec; + //storm::utility::exportStreamToFile(dec.encodeAsSmt2(modelChecker.getMatrix(), parameters,)); + } + // All operations have now been performed, so we clean up everything and terminate. storm::utility::cli::cleanUp(); @@ -172,16 +207,7 @@ int main(const int argc, const char** argv) { // // modelchecker::reachability::DirectEncoding dec; // std::vector parameters; -// for(auto constant : mProgram.getConstants()) -// { -// if(!constant.isDefined()) -// { -// std::cout << constant.getName() << std::endl; -// carl::Variable p = carl::VariablePool::getInstance().findVariableWithName(constant.getName()); -// assert(p != carl::Variable::NO_VARIABLE); -// parameters.push_back(p); -// } -// } + // return dec.encodeAsSmt2(subdtmc, parameters, subdtmc.getLabeledStates("init"), subdtmc.getLabeledStates("__targets__"), mpq_class(1,2)); // //} diff --git a/src/utility/cli.h b/src/utility/cli.h index 3ed39734c..fd1c2a496 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -62,13 +62,15 @@ namespace storm { */ void initializeLogger() { logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); - auto loglevel = storm::settings::debugSettings().isTraceSet() ? log4cplus::TRACE_LOG_LEVEL : storm::settings::debugSettings().isDebugSet() ? log4cplus::DEBUG_LOG_LEVEL : log4cplus::WARN_LOG_LEVEL; - logger.setLogLevel(loglevel); log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender()); consoleLogAppender->setName("mainConsoleAppender"); - consoleLogAppender->setThreshold(loglevel); consoleLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n"))); logger.addAppender(consoleLogAppender); + auto loglevel = storm::settings::debugSettings().isTraceSet() ? log4cplus::TRACE_LOG_LEVEL : storm::settings::debugSettings().isDebugSet() ? log4cplus::DEBUG_LOG_LEVEL : log4cplus::WARN_LOG_LEVEL; + logger.setLogLevel(loglevel); + consoleLogAppender->setThreshold(loglevel); + + } /*! diff --git a/src/utility/constants.h b/src/utility/constants.h index 2a5b8ba86..699ee7368 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -204,6 +204,58 @@ inline storm::storage::LabeledValues constantInfinity() { /*! @endcond */ +template +inline bool isConstant(T const& v) +{ + return true; +} + + +#ifdef PARAMETRIC_SYSTEMS +template<> +inline bool isConstant(storm::RationalFunction const& r) +{ + return r.isConstant(); +} + +template<> +inline bool isConstant(storm::Polynomial const& p) +{ + return p.isConstant(); +} +#endif + + + +template +inline bool isZero(T const& v) +{ + return v == T(0); +} + +template<> +inline bool isZero(double const& d) +{ + double precision = storm::settings::generalSettings().getPrecision(); + return std::abs(d) < precision; +} + +#ifdef PARAMETRIC_SYSTEMS +template<> +inline bool isZero(storm::RationalFunction const& r) +{ + return r.isZero(); +} + +template<> +inline bool isZero(storm::Polynomial const& p) +{ + return p.isZero(); +} +#endif + + + template inline bool isOne(T const& sum) { diff --git a/src/utility/export.h b/src/utility/export.h new file mode 100644 index 000000000..7d66bd0b3 --- /dev/null +++ b/src/utility/export.h @@ -0,0 +1,51 @@ +/** + * @file: export.h + * @author: Sebastian Junges + * + * @since October 7, 2014 + */ + +#ifndef STORM_UTILITY_EXPORT_H_ +#define STORM_UTILITY_EXPORT_H_ + +#include + +#include "src/storage/parameters.h" +#include "src/settings/modules/ParametricSettings.h" +#include "src/modelchecker/reachability/CollectConstraints.h" + +namespace storm { +namespace utility { + +template +void exportParametricMcResult(const ValueType& mcresult, storm::modelchecker::reachability::CollectConstraints const& constraintCollector) { + std::string path = storm::settings::parametricSettings().exportResultPath(); + std::ofstream filestream; + filestream.open(path); + // todo add checks. + filestream << "!Parameters: "; + std::set vars = mcresult.gatherVariables(); + std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, " ")); + filestream << std::endl; + filestream << "!Result: " << mcresult << std::endl; + filestream << "!Well-formed Constraints: " << std::endl; + std::copy(constraintCollector.wellformedConstraints().begin(), constraintCollector.wellformedConstraints().end(), std::ostream_iterator>(filestream, "\n")); + filestream << "!Graph-preserving Constraints: " << std::endl; + std::copy(constraintCollector.graphPreservingConstraints().begin(), constraintCollector.graphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); + filestream.close(); +} + +void exportStringStreamToFile(std::stringstream& stream, std::string filepath) { + // todo add checks. + std::ofstream filestream; + filestream.open(filepath); + filestream << stream.str(); + filestream.close(); +} + +} +} + + + +#endif \ No newline at end of file