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

Removed bit vector for storing markovian choices of MA. From now on, the first choice of a hybrid/Markovian state is the Markovian one. 

Former-commit-id: 6b646597dc
tempestpy_adaptions
dehnert 11 years ago
parent
cebda374d1
commit
d725a3f898
3 changed files with 11 additions and 12 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. 18
      src/models/MarkovAutomaton.h
  2. 2
      src/parser/MarkovAutomatonParser.cpp
  3. 3
      src/parser/MarkovAutomatonSparseTransitionParser.cpp

18
src/models/MarkovAutomaton.h
View File

@ -23,12 +23,11 @@ namespace storm {
public:
MarkovAutomaton(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
std::vector<uint_fast64_t>&& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates,
storm::storage::BitVector const& markovianChoices, std::vector<T> const& exitRates,
std::vector<uint_fast64_t>&& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector<T> const& exitRates,
boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> const& optionalChoiceLabeling)
: AbstractNondeterministicModel<T>(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling),
markovianStates(markovianStates), markovianChoices(markovianChoices), exitRates(exitRates) {
markovianStates(markovianStates), exitRates(exitRates) {
if (this->hasTransitionRewards()) {
if (!this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix())) {
LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
@ -40,13 +39,12 @@ namespace storm {
MarkovAutomaton(storm::storage::SparseMatrix<T>&& transitionMatrix,
storm::models::AtomicPropositionsLabeling&& stateLabeling,
std::vector<uint_fast64_t>&& nondeterministicChoiceIndices,
storm::storage::BitVector const& markovianStates,
storm::storage::BitVector const& markovianChoices, std::vector<T> const& exitRates,
storm::storage::BitVector const& markovianStates, std::vector<T> const& exitRates,
boost::optional<std::vector<T>>&& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>&& optionalChoiceLabeling)
: AbstractNondeterministicModel<T>(std::move(transitionMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
std::move(optionalChoiceLabeling)), markovianStates(markovianStates), markovianChoices(std::move(markovianChoices)), exitRates(std::move(exitRates)) {
std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)) {
if (this->hasTransitionRewards()) {
if (!this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix())) {
LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
@ -55,11 +53,11 @@ namespace storm {
}
}
MarkovAutomaton(MarkovAutomaton<T> const& markovAutomaton) : AbstractNondeterministicModel<T>(markovAutomaton), exitRates(markovAutomaton.exitRates), markovianStates(markovAutomaton.markovianStates), markovianChoices(markovAutomaton.markovianChoices) {
MarkovAutomaton(MarkovAutomaton<T> const& markovAutomaton) : AbstractNondeterministicModel<T>(markovAutomaton), exitRates(markovAutomaton.exitRates), markovianStates(markovAutomaton.markovianStates) {
// Intentionally left empty.
}
MarkovAutomaton(MarkovAutomaton<T>&& markovAutomaton) : AbstractNondeterministicModel<T>(std::move(markovAutomaton)), markovianStates(std::move(markovAutomaton.markovianStates)), markovianChoices(std::move(markovAutomaton.markovianChoices)), exitRates(std::move(markovAutomaton.exitRates)) {
MarkovAutomaton(MarkovAutomaton<T>&& markovAutomaton) : AbstractNondeterministicModel<T>(std::move(markovAutomaton)), markovianStates(std::move(markovAutomaton.markovianStates)), exitRates(std::move(markovAutomaton.exitRates)) {
// Intentionally left empty.
}
@ -91,7 +89,9 @@ namespace storm {
}
}
if (!markovianChoices.get(this->getNondeterministicChoiceIndices()[state] + row)) {
// If it's not a Markovian state or the current row is the first choice for this state, then we
// are dealing with a probabilitic choice.
if (!markovianStates.get(state) || row != 0) {
// For each nondeterministic choice, we draw an arrow to an intermediate node to better display
// the grouping of transitions.
outStream << "\t\"" << state << "c" << row << "\" [shape = \"point\"";

2
src/parser/MarkovAutomatonParser.cpp
View File

@ -19,7 +19,7 @@ namespace storm {
throw storm::exceptions::WrongFormatException() << "Transition rewards are unsupported for Markov automata.";
}
storm::models::MarkovAutomaton<double> resultingAutomaton(std::move(transitionResult.transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.markovianChoices), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional<storm::storage::SparseMatrix<double>>(), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>());
storm::models::MarkovAutomaton<double> resultingAutomaton(std::move(transitionResult.transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional<storm::storage::SparseMatrix<double>>(), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>());
return resultingAutomaton;
}

3
src/parser/MarkovAutomatonSparseTransitionParser.cpp
View File

@ -194,8 +194,7 @@ namespace storm {
if (strcmp(actionNameBuffer, "!") == 0) {
isMarkovianChoice = true;
// Mark the current choice and state as a Markovian one.
result.markovianChoices.set(currentChoice, true);
// Mark the current state as a Markovian one.
result.markovianStates.set(source, true);
} else {
isMarkovianChoice = false;

Write Preview
Loading…
Cancel
Save