Matthias Volk
8 years ago
16 changed files with 450 additions and 19 deletions
-
2CHANGELOG.md
-
7src/storm-pars-cli/storm-pars.cpp
-
2src/storm/adapters/GmmxxAdapter.h
-
11src/storm/api/builder.h
-
7src/storm/cli/cli.cpp
-
14src/storm/logic/BoundedUntilFormula.cpp
-
2src/storm/logic/BoundedUntilFormula.h
-
9src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
-
276src/storm/parser/ImcaMarkovAutomatonParser.cpp
-
76src/storm/parser/ImcaMarkovAutomatonParser.h
-
13src/storm/settings/modules/IOSettings.cpp
-
16src/storm/settings/modules/IOSettings.h
-
5src/storm/solver/SmtSolver.cpp
-
18src/storm/solver/SmtSolver.h
-
9src/storm/solver/Z3SmtSolver.cpp
-
2src/storm/solver/Z3SmtSolver.h
@ -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
|
|||
|
|||
@ -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 |
|||
|
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue