Browse Source

added parser for IMCAs explicit Markov automaton format

tempestpy_adaptions
TimQu 8 years ago
parent
commit
07259e8f0d
  1. 1
      CHANGELOG.md
  2. 11
      src/storm/api/builder.h
  3. 7
      src/storm/cli/cli.cpp
  4. 276
      src/storm/parser/ImcaMarkovAutomatonParser.cpp
  5. 76
      src/storm/parser/ImcaMarkovAutomatonParser.h
  6. 13
      src/storm/settings/modules/IOSettings.cpp
  7. 16
      src/storm/settings/modules/IOSettings.h

1
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)

11
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"
@ -136,6 +137,16 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact models with direct encoding are not supported.");
}
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitIMCAModel(std::string const&) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact models with direct encoding are not supported.");
}
template<>
inline std::shared_ptr<storm::models::sparse::Model<double>> buildExplicitIMCAModel(std::string const& imcaFile) {
return storm::parser::ImcaMarkovAutomatonParser<double>::parseImcaFile(imcaFile);
}
}
}

7
src/storm/cli/cli.cpp

@ -380,8 +380,11 @@ namespace storm {
std::shared_ptr<storm::models::ModelBase> result;
if (ioSettings.isExplicitSet()) {
result = storm::api::buildExplicitModel<ValueType>(ioSettings.getTransitionFilename(), ioSettings.getLabelingFilename(), ioSettings.isStateRewardsSet() ? boost::optional<std::string>(ioSettings.getStateRewardsFilename()) : boost::none, ioSettings.isTransitionRewardsSet() ? boost::optional<std::string>(ioSettings.getTransitionRewardsFilename()) : boost::none, ioSettings.isChoiceLabelingSet() ? boost::optional<std::string>(ioSettings.getChoiceLabelingFilename()) : boost::none);
} else {
} else if (ioSettings.isExplicitDRNSet()) {
result = storm::api::buildExplicitDRNModel<ValueType>(ioSettings.getExplicitDRNFilename());
} else {
STORM_LOG_THROW(ioSettings.isExplicitIMCASet(), storm::exceptions::InvalidSettingsException, "Unexpected explicit model input type.");
result = storm::api::buildExplicitIMCAModel<ValueType>(ioSettings.getExplicitIMCAFilename());
}
return result;
}
@ -397,7 +400,7 @@ namespace storm {
} else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
result = buildModelSparse<ValueType>(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<ValueType>(ioSettings);
}

276
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 <typename ValueType, typename StateType>
ImcaParserGrammar<ValueType, StateType>::ImcaParserGrammar() : ImcaParserGrammar<ValueType, StateType>::base_type(start), numStates(0), numChoices(0), numTransitions(0), hasStateReward(false), hasActionReward(false) {
buildChoiceLabels = storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildChoiceLabelsSet();
initialize();
}
template <typename ValueType, typename StateType>
void ImcaParserGrammar<ValueType, StateType>::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<ValueType, StateType>::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<ValueType, StateType>::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<ValueType, StateType>::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<ValueType, StateType>::addInitialState, phoenix::ref(*this), qi::_1)]);
initials.name("INITIALS");
goals = qi::lit("#GOALS") >> *((state >> qi::eps)[phoenix::bind(&ImcaParserGrammar<ValueType, StateType>::addGoalState, phoenix::ref(*this), qi::_1)]);
goals.name("GOALS");
start = (initials >> goals >> transitions)[qi::_val = phoenix::bind(&ImcaParserGrammar<ValueType, StateType>::createModelComponents, phoenix::ref(*this))];
start.name("start");
}
template <typename ValueType, typename StateType>
StateType ImcaParserGrammar<ValueType, StateType>::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 <typename ValueType, typename StateType>
std::pair<StateType, ValueType> ImcaParserGrammar<ValueType, StateType>::createStateValuePair(StateType const& state, ValueType const& value) {
return std::pair<StateType, ValueType>(state, value);
}
template <typename ValueType, typename StateType>
void ImcaParserGrammar<ValueType, StateType>::addInitialState(StateType const& state) {
initialStates.set(state);
}
template <typename ValueType, typename StateType>
void ImcaParserGrammar<ValueType, StateType>::addGoalState(StateType const& state) {
goalStates.set(state);
}
template <typename ValueType, typename StateType>
void ImcaParserGrammar<ValueType, StateType>::addChoiceToStateBehavior(StateType const& state, std::string const& label, std::vector<std::pair<StateType, ValueType>> const& transitions, boost::optional<ValueType> const& reward) {
bool isMarkovian = label == "!";
storm::generator::Choice<ValueType, StateType> 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<ValueType>(), 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 <typename ValueType, typename StateType>
storm::storage::sparse::ModelComponents<ValueType> ImcaParserGrammar<ValueType, StateType>::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<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet()) {
StateType state = 0;
for (auto& behavior : stateBehaviors) {
if (!behavior.wasExpanded()) {
storm::generator::Choice<ValueType, StateType> choice(0, true);
choice.addProbability(state, storm::utility::one<ValueType>());
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<ValueType> matrixBuilder(numChoices, numStates, numTransitions, true, true, numStates);
std::vector<ValueType> exitRates;
exitRates.reserve(numStates);
boost::optional<std::vector<ValueType>> stateRewards, actionRewards;
if (hasStateReward) {
stateRewards = std::vector<ValueType>(numStates, storm::utility::zero<ValueType>());
}
if (hasActionReward) {
actionRewards = std::vector<ValueType>(numChoices, storm::utility::zero<ValueType>());
}
boost::optional<storm::models::sparse::ChoiceLabeling> 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<ValueType>(transition.second / exitRates.back()));
}
++row;
}
}
} else {
exitRates.push_back(storm::utility::zero<ValueType>());
}
// 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<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModel;
if (hasStateReward || hasActionReward) {
rewardModel.insert(std::make_pair("", storm::models::sparse::StandardRewardModel<ValueType>(stateRewards, actionRewards)));
}
storm::storage::sparse::ModelComponents<ValueType> 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<typename ValueType>
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ImcaMarkovAutomatonParser<ValueType>::parseImcaFile(std::string const& filename) {
// Open file and initialize result.
std::ifstream inputFileStream;
storm::utility::openFile(filename, inputFileStream);
storm::storage::sparse::ModelComponents<ValueType> components;
// Now try to parse the contents of the file.
std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
PositionIteratorType first(fileContent.begin());
PositionIteratorType iter = first;
PositionIteratorType last(fileContent.end());
try {
// Start parsing.
ImcaParserGrammar<ValueType> 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<PositionIteratorType> 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<storm::models::sparse::MarkovAutomaton<ValueType>>();
}
template class ImcaParserGrammar<double>;
template class ImcaMarkovAutomatonParser<double>;
} // namespace parser
} // namespace storm

76
src/storm/parser/ImcaMarkovAutomatonParser.h

@ -0,0 +1,76 @@
#pragma once
#include <memory>
#include <fstream>
#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 <typename ValueType, typename StateType = uint32_t>
class ImcaParserGrammar : public qi::grammar<Iterator, storm::storage::sparse::ModelComponents<ValueType>(), Skipper> {
public:
ImcaParserGrammar();
private:
void initialize();
std::pair<StateType, ValueType> 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<std::pair<StateType, ValueType>> const& transitions, boost::optional<ValueType> const& reward);
storm::storage::sparse::ModelComponents<ValueType> createModelComponents();
qi::rule<Iterator, storm::storage::sparse::ModelComponents<ValueType>(), Skipper> start;
qi::rule<Iterator, qi::unused_type(), Skipper> initials;
qi::rule<Iterator, qi::unused_type(), Skipper> goals;
qi::rule<Iterator, qi::unused_type(), Skipper> transitions;
qi::rule<Iterator, qi::unused_type(), Skipper> choice;
qi::rule<Iterator, std::pair<StateType, ValueType>(), Skipper> transition;
qi::rule<Iterator, std::string(), Skipper> choicelabel;
qi::rule<Iterator, ValueType(), Skipper> reward;
qi::rule<Iterator, StateType(), Skipper> state;
qi::rule<Iterator, ValueType(), Skipper> value;
bool buildChoiceLabels;
StateType numStates;
StateType numChoices;
StateType numTransitions;
bool hasStateReward;
bool hasActionReward;
std::vector<storm::generator::StateBehavior<ValueType, StateType>> stateBehaviors;
storm::storage::BitVector initialStates, goalStates, markovianStates;
std::map<std::string, StateType> stateIndices;
};
template <typename ValueType = double>
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<storm::models::sparse::MarkovAutomaton<ValueType>> parseImcaFile(std::string const& filename);
};
} // namespace parser
} // namespace storm

13
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();
}

16
src/storm/settings/modules/IOSettings.h

@ -100,6 +100,20 @@ namespace storm {
*/
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;

Loading…
Cancel
Save