From 07259e8f0dde1d4cdd8d048054000e18242de33c Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 5 Jul 2017 17:49:52 +0200 Subject: [PATCH] added parser for IMCAs explicit Markov automaton format --- CHANGELOG.md | 1 + src/storm/api/builder.h | 11 + src/storm/cli/cli.cpp | 7 +- .../parser/ImcaMarkovAutomatonParser.cpp | 276 ++++++++++++++++++ src/storm/parser/ImcaMarkovAutomatonParser.h | 76 +++++ src/storm/settings/modules/IOSettings.cpp | 13 + src/storm/settings/modules/IOSettings.h | 16 + 7 files changed, 398 insertions(+), 2 deletions(-) create mode 100644 src/storm/parser/ImcaMarkovAutomatonParser.cpp create mode 100644 src/storm/parser/ImcaMarkovAutomatonParser.h diff --git a/CHANGELOG.md b/CHANGELOG.md index cb2ccd7d1..94c0c14b9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -21,6 +21,7 @@ Version 1.0.x Then, using FORCE_POPCNT enables the use of the SSE 4.2 instruction - Parametric model checking is now handled in a separated library/executable called storm-pars - Support for long-run average rewwards on Markov automata using the value-iteration based approach by Butkova et al. (TACAS 17) +- Support for parsing/building models given in the explicit input format of IMCA. ### Version 1.0.1 (2017/4) diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index b2ecc2626..868c47bba 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -2,6 +2,7 @@ #include "storm/parser/AutoParser.h" #include "storm/parser/DirectEncodingParser.h" +#include "storm/parser/ImcaMarkovAutomatonParser.h" #include "storm/storage/SymbolicModelDescription.h" @@ -135,6 +136,16 @@ namespace storm { inline std::shared_ptr> buildExplicitDRNModel(std::string const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact models with direct encoding are not supported."); } + + template + std::shared_ptr> buildExplicitIMCAModel(std::string const&) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact models with direct encoding are not supported."); + } + + template<> + inline std::shared_ptr> buildExplicitIMCAModel(std::string const& imcaFile) { + return storm::parser::ImcaMarkovAutomatonParser::parseImcaFile(imcaFile); + } } diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 3284b353c..caf3aa0c3 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -380,8 +380,11 @@ namespace storm { std::shared_ptr result; if (ioSettings.isExplicitSet()) { result = storm::api::buildExplicitModel(ioSettings.getTransitionFilename(), ioSettings.getLabelingFilename(), ioSettings.isStateRewardsSet() ? boost::optional(ioSettings.getStateRewardsFilename()) : boost::none, ioSettings.isTransitionRewardsSet() ? boost::optional(ioSettings.getTransitionRewardsFilename()) : boost::none, ioSettings.isChoiceLabelingSet() ? boost::optional(ioSettings.getChoiceLabelingFilename()) : boost::none); - } else { + } else if (ioSettings.isExplicitDRNSet()) { result = storm::api::buildExplicitDRNModel(ioSettings.getExplicitDRNFilename()); + } else { + STORM_LOG_THROW(ioSettings.isExplicitIMCASet(), storm::exceptions::InvalidSettingsException, "Unexpected explicit model input type."); + result = storm::api::buildExplicitIMCAModel(ioSettings.getExplicitIMCAFilename()); } return result; } @@ -397,7 +400,7 @@ namespace storm { } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) { result = buildModelSparse(input, ioSettings); } - } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet()) { + } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) { STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); result = buildModelExplicit(ioSettings); } diff --git a/src/storm/parser/ImcaMarkovAutomatonParser.cpp b/src/storm/parser/ImcaMarkovAutomatonParser.cpp new file mode 100644 index 000000000..c00b44497 --- /dev/null +++ b/src/storm/parser/ImcaMarkovAutomatonParser.cpp @@ -0,0 +1,276 @@ +#include "storm/parser/ImcaMarkovAutomatonParser.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/utility/file.h" +#include "storm/utility/builder.h" + +namespace storm { + namespace parser { + + template + ImcaParserGrammar::ImcaParserGrammar() : ImcaParserGrammar::base_type(start), numStates(0), numChoices(0), numTransitions(0), hasStateReward(false), hasActionReward(false) { + buildChoiceLabels = storm::settings::getModule().isBuildChoiceLabelsSet(); + initialize(); + } + + template + void ImcaParserGrammar::initialize() { + value = qi::double_[qi::_val = qi::_1]; + value.name("value"); + + // We assume here that imca files are alphanumeric strings, If we restrict ourselves to the 's12345' representation, we could also do: + // state = (qi::lit("s") > qi::ulong_)[qi::_val = qi::_1]; + state = qi::as_string[qi::raw[qi::lexeme[(qi::alnum | qi::char_('_')) % qi::eps]]][qi::_val = phoenix::bind(&ImcaParserGrammar::getStateIndex, phoenix::ref(*this), qi::_1)]; + state.name("state"); + + reward = (-qi::lit("R") >> value)[qi::_val = qi::_1]; + reward.name("reward"); + + transition = (qi::lit("*") >> state >> value)[qi::_val = phoenix::bind(&ImcaParserGrammar::createStateValuePair, phoenix::ref(*this), qi::_1, qi::_2)]; + transition.name("transition"); + + choicelabel = qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')) | qi::lit("!"))]]]; + choicelabel.name("choicelabel"); + + choice = (state >> choicelabel >> -reward >> *(transition >> qi::eps))[phoenix::bind(&ImcaParserGrammar::addChoiceToStateBehavior, phoenix::ref(*this), qi::_1, qi::_2, qi::_4, qi::_3)]; + choice.name("choice"); + + transitions = qi::lit("#TRANSITIONS") >> *(choice); + transitions.name("TRANSITIONS"); + + initials = qi::lit("#INITIALS") >> *((state >> qi::eps)[phoenix::bind(&ImcaParserGrammar::addInitialState, phoenix::ref(*this), qi::_1)]); + initials.name("INITIALS"); + + goals = qi::lit("#GOALS") >> *((state >> qi::eps)[phoenix::bind(&ImcaParserGrammar::addGoalState, phoenix::ref(*this), qi::_1)]); + goals.name("GOALS"); + + start = (initials >> goals >> transitions)[qi::_val = phoenix::bind(&ImcaParserGrammar::createModelComponents, phoenix::ref(*this))]; + start.name("start"); + + } + + template + StateType ImcaParserGrammar::getStateIndex(std::string const& stateString) { + auto it = stateIndices.find(stateString); + if (it == stateIndices.end()) { + this->stateIndices.emplace_hint(it, stateString, numStates); + ++numStates; + initialStates.grow(numStates); + goalStates.grow(numStates); + markovianStates.grow(numStates); + stateBehaviors.resize(numStates); + return numStates - 1; + } else { + return it->second; + } + } + + template + std::pair ImcaParserGrammar::createStateValuePair(StateType const& state, ValueType const& value) { + return std::pair(state, value); + } + + template + void ImcaParserGrammar::addInitialState(StateType const& state) { + initialStates.set(state); + } + + template + void ImcaParserGrammar::addGoalState(StateType const& state) { + goalStates.set(state); + } + + template + void ImcaParserGrammar::addChoiceToStateBehavior(StateType const& state, std::string const& label, std::vector> const& transitions, boost::optional const& reward) { + bool isMarkovian = label == "!"; + storm::generator::Choice choice(0, isMarkovian); + STORM_LOG_THROW(!transitions.empty(), storm::exceptions::WrongFormatException, "Empty choice defined for state s" << state << "."); + if (buildChoiceLabels && !isMarkovian) { + choice.addLabel(label); + } + if (reward && !isMarkovian) { + hasActionReward = true; + choice.addReward(reward.get()); + } + for (auto const& t : transitions) { + STORM_LOG_THROW(t.second > storm::utility::zero(), storm::exceptions::WrongFormatException, "Probabilities and rates have to be positive. got " << t.second << " at state s" << state << "."); + choice.addProbability(t.first, t.second); + } + STORM_LOG_THROW(isMarkovian || storm::utility::isOne(choice.getTotalMass()), storm::exceptions::WrongFormatException, "Probability for choice " << label << " on state s" << state << " does not sum up to one."); + + ++numChoices; + numTransitions += choice.size(); + auto& behavior = stateBehaviors[state]; + behavior.setExpanded(true); + behavior.addChoice(std::move(choice)); + if (isMarkovian) { + markovianStates.set(state); + if (reward) { + hasStateReward = true; + behavior.addStateReward(reward.get()); + } + } + } + + template + storm::storage::sparse::ModelComponents ImcaParserGrammar::createModelComponents() { + + // Prepare the statelabeling + initialStates.resize(numStates); + goalStates.resize(numStates); + markovianStates.resize(numStates); + storm::models::sparse::StateLabeling stateLabeling(numStates); + stateLabeling.addLabel("init", std::move(initialStates)); + stateLabeling.addLabel("goal", std::move(goalStates)); + + // Fix deadlocks (if required) + assert(stateBehaviors.size() == numStates); + if (!storm::settings::getModule().isDontFixDeadlocksSet()) { + StateType state = 0; + for (auto& behavior : stateBehaviors) { + if (!behavior.wasExpanded()) { + storm::generator::Choice choice(0, true); + choice.addProbability(state, storm::utility::one()); + behavior.setExpanded(true); + behavior.addChoice(std::move(choice)); + markovianStates.set(state); + ++numChoices; + ++numTransitions; + } + ++state; + } + } + + // Build the transition matrix together with exit rates, reward models, and choice labeling + storm::storage::SparseMatrixBuilder matrixBuilder(numChoices, numStates, numTransitions, true, true, numStates); + std::vector exitRates; + exitRates.reserve(numStates); + boost::optional> stateRewards, actionRewards; + if (hasStateReward) { + stateRewards = std::vector(numStates, storm::utility::zero()); + } + if (hasActionReward) { + actionRewards = std::vector(numChoices, storm::utility::zero()); + } + boost::optional choiceLabeling; + if (buildChoiceLabels) { + choiceLabeling = storm::models::sparse::ChoiceLabeling(numChoices); + } + StateType state = 0; + StateType row = 0; + for (auto const& behavior : stateBehaviors) { + matrixBuilder.newRowGroup(row); + if (!behavior.getStateRewards().empty()) { + assert(behavior.getStateRewards().size() == 1); + stateRewards.get()[state] = behavior.getStateRewards().front(); + } + if (markovianStates.get(state)) { + //For Markovian states, the Markovian choice has to be the first one in the resulting transition matrix. + bool markovianChoiceFound = false; + for (auto const& choice : behavior) { + if (choice.isMarkovian()) { + STORM_LOG_THROW(!markovianChoiceFound, storm::exceptions::WrongFormatException, "Multiple Markovian choices defined for state " << state << "."); + markovianChoiceFound = true; + if (!choice.getRewards().empty()) { + assert(choice.getRewards().size() == 1); + actionRewards.get()[row] = choice.getRewards().front(); + } + if (buildChoiceLabels && choice.hasLabels()) { + assert(choice.getLabels().size() == 1); + std::string const& label = *choice.getLabels().begin(); + if (!choiceLabeling->containsLabel(label)) { + choiceLabeling->addLabel(label); + } + choiceLabeling->addLabelToChoice(label, row); + } + exitRates.push_back(choice.getTotalMass()); + for (auto const& transition : choice) { + matrixBuilder.addNextValue(row, transition.first, static_cast(transition.second / exitRates.back())); + } + ++row; + } + } + } else { + exitRates.push_back(storm::utility::zero()); + } + // Now add all probabilistic choices. + for (auto const& choice : behavior) { + if (!choice.isMarkovian()) { + if (!choice.getRewards().empty()) { + assert(choice.getRewards().size() == 1); + actionRewards.get()[row] = choice.getRewards().front(); + } + if (buildChoiceLabels && choice.hasLabels()) { + assert(choice.getLabels().size() == 1); + std::string const& label = *choice.getLabels().begin(); + if (!choiceLabeling->containsLabel(label)) { + choiceLabeling->addLabel(label); + } + choiceLabeling->addLabelToChoice(label, row); + } + for (auto const& transition : choice) { + matrixBuilder.addNextValue(row, transition.first, transition.second); + } + ++row; + } + } + ++state; + } + + // Finalize the model components + std::unordered_map> rewardModel; + if (hasStateReward || hasActionReward) { + rewardModel.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(stateRewards, actionRewards))); + } + storm::storage::sparse::ModelComponents components(matrixBuilder.build(), std::move(stateLabeling), std::move(rewardModel), false, std::move(markovianStates)); + components.exitRates = std::move(exitRates); + components.choiceLabeling = std::move(choiceLabeling); + + return components; + } + + template + std::shared_ptr> ImcaMarkovAutomatonParser::parseImcaFile(std::string const& filename) { + // Open file and initialize result. + std::ifstream inputFileStream; + storm::utility::openFile(filename, inputFileStream); + + storm::storage::sparse::ModelComponents components; + + // Now try to parse the contents of the file. + std::string fileContent((std::istreambuf_iterator(inputFileStream)), (std::istreambuf_iterator())); + PositionIteratorType first(fileContent.begin()); + PositionIteratorType iter = first; + PositionIteratorType last(fileContent.end()); + + try { + // Start parsing. + ImcaParserGrammar grammar; + bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), components); + STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse imca file."); + STORM_LOG_DEBUG("Parsed imca file successfully."); + } catch (qi::expectation_failure const& e) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_); + storm::utility::closeFile(inputFileStream); + } catch(std::exception& e) { + // In case of an exception properly close the file before passing exception. + storm::utility::closeFile(inputFileStream); + throw e; + } + + // Close the stream in case everything went smoothly + storm::utility::closeFile(inputFileStream); + + // Build the model from the obtained model components + return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::MarkovAutomaton, std::move(components))->template as>(); + } + + + + template class ImcaParserGrammar; + template class ImcaMarkovAutomatonParser; + } // namespace parser +} // namespace storm + diff --git a/src/storm/parser/ImcaMarkovAutomatonParser.h b/src/storm/parser/ImcaMarkovAutomatonParser.h new file mode 100644 index 000000000..f2820242e --- /dev/null +++ b/src/storm/parser/ImcaMarkovAutomatonParser.h @@ -0,0 +1,76 @@ +#pragma once + +#include +#include + +#include "storm/storage/sparse/ModelComponents.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/generator/StateBehavior.h" + +#include "storm/parser/SpiritErrorHandler.h" + +namespace storm { + namespace parser { + + template + class ImcaParserGrammar : public qi::grammar(), Skipper> { + + public: + ImcaParserGrammar(); + + private: + void initialize(); + + std::pair createStateValuePair(StateType const& state, ValueType const& value); + StateType getStateIndex(std::string const& stateString); + void addInitialState(StateType const& state); + void addGoalState(StateType const& state); + void addChoiceToStateBehavior(StateType const& state, std::string const& label, std::vector> const& transitions, boost::optional const& reward); + storm::storage::sparse::ModelComponents createModelComponents(); + + + qi::rule(), Skipper> start; + + qi::rule initials; + qi::rule goals; + qi::rule transitions; + + qi::rule choice; + qi::rule(), Skipper> transition; + qi::rule choicelabel; + qi::rule reward; + qi::rule state; + qi::rule value; + + bool buildChoiceLabels; + + StateType numStates; + StateType numChoices; + StateType numTransitions; + bool hasStateReward; + bool hasActionReward; + + std::vector> stateBehaviors; + storm::storage::BitVector initialStates, goalStates, markovianStates; + std::map stateIndices; + + }; + + template + class ImcaMarkovAutomatonParser { + public: + + /*! + * Parses the given file under the assumption that it contains a Markov automaton specified in the imca format. + * + * @param filename The name of the file to parse. + * @return The obtained Markov automaton + */ + static std::shared_ptr> parseImcaFile(std::string const& filename); + + }; + + + } // namespace parser +} // namespace storm + diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 51d7fe512..677b78513 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -24,6 +24,8 @@ namespace storm { const std::string IOSettings::explicitOptionShortName = "exp"; const std::string IOSettings::explicitDrnOptionName = "explicit-drn"; const std::string IOSettings::explicitDrnOptionShortName = "drn"; + const std::string IOSettings::explicitImcaOptionName = "explicit-imca"; + const std::string IOSettings::explicitImcaOptionShortName = "imca"; const std::string IOSettings::prismInputOptionName = "prism"; const std::string IOSettings::janiInputOptionName = "jani"; const std::string IOSettings::prismToJaniOptionName = "prism2jani"; @@ -62,6 +64,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, explicitDrnOptionName, false, "Parses the model given in the DRN format.").setShortName(explicitDrnOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("drn filename", "The name of the DRN file containing the model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()) .build()); + this->addOption(storm::settings::OptionBuilder(moduleName, explicitImcaOptionName, false, "Parses the model given in the IMCA format.").setShortName(explicitImcaOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("imca filename", "The name of the imca file containing the model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()) + .build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismInputOptionName, false, "Parses the model given in the PRISM format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the PRISM input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.") @@ -136,6 +141,14 @@ namespace storm { return this->getOption(explicitDrnOptionName).getArgumentByName("drn filename").getValueAsString(); } + bool IOSettings::isExplicitIMCASet() const { + return this->getOption(explicitImcaOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getExplicitIMCAFilename() const { + return this->getOption(explicitImcaOptionName).getArgumentByName("imca filename").getValueAsString(); + } + bool IOSettings::isPrismInputSet() const { return this->getOption(prismInputOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index d7674e9f2..55f777334 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -99,6 +99,20 @@ namespace storm { * @return The name of the DRN file that contains the model. */ std::string getExplicitDRNFilename() const; + + /*! + * Retrieves whether the explicit option with IMCA was set. + * + * @return True if the explicit option with IMCA was set. + */ + bool isExplicitIMCASet() const; + + /*! + * Retrieves the name of the file that contains the model in the IMCA format. + * + * @return The name of the IMCA file that contains the model. + */ + std::string getExplicitIMCAFilename() const; /*! * Retrieves whether the PRISM language option was set. @@ -312,6 +326,8 @@ namespace storm { static const std::string explicitOptionShortName; static const std::string explicitDrnOptionName; static const std::string explicitDrnOptionShortName; + static const std::string explicitImcaOptionName; + static const std::string explicitImcaOptionShortName; static const std::string prismInputOptionName; static const std::string janiInputOptionName; static const std::string prismToJaniOptionName;