sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Fixed DRN exporter/parser: MAs are not supported as there is no indication for Markovian choices

tempestpy_adaptions
TimQu 8 years ago
parent
36b38b10ee
commit
9f894667eb
2 changed files with 26 additions and 33 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 52
      src/storm/parser/DirectEncodingParser.cpp
  2. 5
      src/storm/utility/DirectEncodingExporter.cpp

52
src/storm/parser/DirectEncodingParser.cpp
View File

@ -14,6 +14,7 @@
#include "storm/adapters/CarlAdapter.h"
#include "storm/utility/constants.h"
#include "storm/utility/builder.h"
#include "storm/utility/macros.h"
#include "storm/utility/file.h"
@ -68,6 +69,9 @@ namespace storm {
STORM_LOG_THROW(boost::starts_with(line, "@type: "), storm::exceptions::WrongFormatException, "Expected model type.");
storm::models::ModelType type = storm::models::getModelType(line.substr(7));
STORM_LOG_TRACE("Model type: " << type);
STORM_LOG_THROW(type != storm::models::ModelType::MarkovAutomaton, storm::exceptions::NotSupportedException, "Markov Automata in DRN format are not supported (unclear indication of Markovian Choices in DRN format)");
STORM_LOG_THROW(type != storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Stochastic Two Player Games in DRN format are not supported.");
// Parse parameters
std::getline(file, line);
STORM_LOG_THROW(line == "@parameters", storm::exceptions::WrongFormatException, "Expected parameter declaration.");
@ -91,35 +95,14 @@ namespace storm {
std::getline(file, line);
STORM_LOG_THROW(line == "@model", storm::exceptions::WrongFormatException, "Expected model declaration.");
// Construct transition matrix
// Construct model components
std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> modelComponents = parseStates(file, type, nrStates, valueParser);
// Done parsing
storm::utility::closeFile(file);
// Build model
switch (type) {
case storm::models::ModelType::Dtmc:
{
STORM_LOG_THROW(false, storm::exceptions::FileIoException, "DTMC not supported.");
}
case storm::models::ModelType::Ctmc:
{
modelComponents->rateTransitions = true;
return std::make_shared<storm::models::sparse::Ctmc<ValueType, RewardModelType>>(std::move(*modelComponents));
}
case storm::models::ModelType::Mdp:
{
STORM_LOG_THROW(false, storm::exceptions::FileIoException, "MDP not supported.");
}
case storm::models::ModelType::MarkovAutomaton:
{
modelComponents->rateTransitions = true;
return std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>>(std::move(*modelComponents));
}
default:
STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Unknown/Unhandled model type " << type << " which cannot be parsed.");
}
return storm::utility::builder::buildModelFromComponents(type, std::move(*modelComponents));
}
template<typename ValueType, typename RewardModelType>
@ -130,17 +113,23 @@ namespace storm {
storm::storage::SparseMatrixBuilder<ValueType> builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, nonDeterministic, 0);
modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize);
// We parse rates for continuous time models.
if (type == storm::models::ModelType::Ctmc) {
modelComponents->rateTransitions = true;
}
// Iterate over all lines
std::string line;
size_t row = 0;
size_t state = 0;
bool first = true;
bool firstState = true;
bool firstAction = true;
while (std::getline(file, line)) {
STORM_LOG_TRACE("Parsing: " << line);
if (boost::starts_with(line, "state ")) {
// New state
if (first) {
first = false;
if (firstState) {
firstState = false;
} else {
++state;
}
@ -180,12 +169,13 @@ namespace storm {
STORM_LOG_TRACE("New state " << state);
STORM_LOG_ASSERT(state == parsedId, "State ids do not correspond.");
if (nonDeterministic) {
STORM_LOG_TRACE("new Row Group starts at " << row << ".");
builder.newRowGroup(row);
}
} else if (boost::starts_with(line, "\taction ")) {
// New action
if (first) {
first = false;
if (firstAction) {
firstAction = false;
} else {
++row;
}
@ -210,13 +200,13 @@ namespace storm {
size_t target = boost::lexical_cast<size_t>(line.substr(2, posColon-3));
std::string valueStr = line.substr(posColon+2);
ValueType value = valueParser.parseValue(valueStr);
STORM_LOG_TRACE("Transition " << state << " -> " << target << ": " << value);
builder.addNextValue(state, target, value);
STORM_LOG_TRACE("Transition " << row << " -> " << target << ": " << value);
builder.addNextValue(row, target, value);
}
}
STORM_LOG_TRACE("Finished parsing");
modelComponents->transitionMatrix = builder.build(stateSize, stateSize);
modelComponents->transitionMatrix = builder.build(row + 1, stateSize, nonDeterministic ? stateSize : 0);
STORM_LOG_TRACE("Built matrix");
return modelComponents;
}

5
src/storm/utility/DirectEncodingExporter.cpp
View File

@ -21,17 +21,20 @@ namespace storm {
// Notice that for CTMCs we write the rate matrix instead of probabilities
// Initialize
storm::models::ModelType type = sparseModel->getType();
std::vector<ValueType> exitRates; // Only for CTMCs and MAs.
if(sparseModel->getType() == storm::models::ModelType::Ctmc) {
exitRates = sparseModel->template as<storm::models::sparse::Ctmc<ValueType>>()->getExitRateVector();
} else if(sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) {
type = storm::models::ModelType::Mdp;
STORM_LOG_WARN("Markov automaton is exported as MDP (indication of Markovian choices is not supported in DRN format).");
exitRates = sparseModel->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()->getExitRates();
}
// Write header
os << "// Exported by storm" << std::endl;
os << "// Original model type: " << sparseModel->getType() << std::endl;
os << "@type: " << sparseModel->getType() << std::endl;
os << "@type: " << type << std::endl;
os << "@parameters" << std::endl;
if (parameters.empty()) {
for (std::string const& parameter : getParameters(sparseModel)) {

Write Preview
Loading…
Cancel
Save