Browse Source

Fixed memory bug in Markov automaton parser.

Former-commit-id: 444b834b91
tempestpy_adaptions
dehnert 11 years ago
parent
commit
66f15efbc6
  1. 3
      src/models/AbstractModel.h
  2. 2
      src/parser/MarkovAutomatonSparseTransitionParser.cpp
  3. 22
      src/storm.cpp

3
src/models/AbstractModel.h

@ -459,7 +459,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
* @return void * @return void
*/ */
virtual void setStateIdBasedChoiceLabeling() = 0; virtual void setStateIdBasedChoiceLabeling() = 0;
protected:
/*! /*!
* Exports the model to the dot-format and prints the result to the given stream. * Exports the model to the dot-format and prints the result to the given stream.
* *
@ -536,6 +536,7 @@ protected:
} }
} }
protected:
/*! A matrix representing the likelihoods of moving between states. */ /*! A matrix representing the likelihoods of moving between states. */
storm::storage::SparseMatrix<T> transitionMatrix; storm::storage::SparseMatrix<T> transitionMatrix;

2
src/parser/MarkovAutomatonSparseTransitionParser.cpp

@ -245,7 +245,7 @@ namespace storm {
// Record the value as well as the exit rate in case of a Markovian choice. // Record the value as well as the exit rate in case of a Markovian choice.
result.transitionMatrix.addNextValue(currentChoice, target, val); result.transitionMatrix.addNextValue(currentChoice, target, val);
if (isMarkovianChoice) { if (isMarkovianChoice) {
result.exitRates[currentChoice] += val;
result.exitRates[source] += val;
} }
buf = forwardToNextLine(buf, lineEndings); buf = forwardToNextLine(buf, lineEndings);

22
src/storm.cpp

@ -430,27 +430,7 @@ int main(const int argc, const char* argv[]) {
if (s->isSet("exportdot")) { if (s->isSet("exportdot")) {
std::ofstream outputFileStream; std::ofstream outputFileStream;
outputFileStream.open(s->getOptionByLongName("exportdot").getArgument(0).getValueAsString(), std::ofstream::out); outputFileStream.open(s->getOptionByLongName("exportdot").getArgument(0).getValueAsString(), std::ofstream::out);
switch (parser.getType()) {
case storm::models::DTMC:
parser.getModel<storm::models::Dtmc<double>>()->writeDotToStream(outputFileStream);
break;
case storm::models::CTMC:
parser.getModel<storm::models::Ctmc<double>>()->writeDotToStream(outputFileStream);
break;
case storm::models::MDP:
parser.getModel<storm::models::Mdp<double>>()->writeDotToStream(outputFileStream);
break;
case storm::models::CTMDP:
parser.getModel<storm::models::Ctmdp<double>>()->writeDotToStream(outputFileStream);
break;
case storm::models::MA:
parser.getModel<storm::models::MarkovAutomaton<double>>()->writeDotToStream(outputFileStream);
break;
default:
LOG4CPLUS_ERROR(logger, "Illegal model type.");
break;
}
parser.getModel<storm::models::AbstractModel<double>>()->writeDotToStream(outputFileStream);
outputFileStream.close(); outputFileStream.close();
} }

Loading…
Cancel
Save