Browse Source
Merge branch 'master' into imca
Merge branch 'master' into imca
Conflicts:
src/models/AbstractModel.h
Former-commit-id: f94c912331
tempestpy_adaptions
dehnert
11 years ago
19 changed files with 332 additions and 33 deletions
-
11CMakeLists.txt
-
2examples/mdp/tiny/tiny.pctl
-
4src/counterexamples/MILPMinimalLabelSetGenerator.h
-
6src/counterexamples/SMTMinimalCommandSetGenerator.h
-
1src/ir/expressions/BinaryNumericalFunctionExpression.cpp
-
38src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
-
13src/models/AbstractModel.h
-
7src/models/AbstractNondeterministicModel.h
-
11src/models/Ctmc.h
-
12src/models/Ctmdp.h
-
14src/models/Dtmc.h
-
15src/models/Mdp.h
-
40src/storage/PartialScheduler.cpp
-
29src/storage/PartialScheduler.h
-
39src/storage/Scheduler.h
-
37src/storage/TotalScheduler.cpp
-
33src/storage/TotalScheduler.h
-
1src/storage/VectorSet.h
-
52src/utility/matrix.h
@ -0,0 +1,2 @@ |
|||
Pmin=? [ F a ] |
|||
Pmax=? [ F a ] |
|||
@ -0,0 +1,40 @@ |
|||
#include "src/storage/PartialScheduler.h"
|
|||
#include "src/exceptions/InvalidArgumentException.h"
|
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
void PartialScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) { |
|||
choices[state] = choice; |
|||
} |
|||
|
|||
bool PartialScheduler::isChoiceDefined(uint_fast64_t state) const { |
|||
return choices.find(state) != choices.end(); |
|||
} |
|||
|
|||
uint_fast64_t PartialScheduler::getChoice(uint_fast64_t state) const { |
|||
auto stateChoicePair = choices.find(state); |
|||
|
|||
if (stateChoicePair == choices.end()) { |
|||
throw storm::exceptions::InvalidArgumentException() << "Scheduler does not define a choice for state " << state; |
|||
} |
|||
|
|||
return stateChoicePair->second; |
|||
} |
|||
|
|||
std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler) { |
|||
out << "partial scheduler (defined on " << scheduler.choices.size() << " states) [ "; |
|||
uint_fast64_t remainingEntries = scheduler.choices.size(); |
|||
for (auto stateChoicePair : scheduler.choices) { |
|||
out << stateChoicePair.first << " -> " << stateChoicePair.second; |
|||
--remainingEntries; |
|||
if (remainingEntries > 0) { |
|||
out << ", "; |
|||
} |
|||
} |
|||
out << "]"; |
|||
return out; |
|||
} |
|||
|
|||
} // namespace storage
|
|||
} // namespace storm
|
|||
@ -0,0 +1,29 @@ |
|||
#ifndef STORM_STORAGE_PARTIALSCHEDULER_H_ |
|||
#define STORM_STORAGE_PARTIALSCHEDULER_H_ |
|||
|
|||
#include <unordered_map> |
|||
#include <ostream> |
|||
|
|||
#include "src/storage/Scheduler.h" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
class PartialScheduler : public Scheduler { |
|||
public: |
|||
void setChoice(uint_fast64_t state, uint_fast64_t choice) override; |
|||
|
|||
bool isChoiceDefined(uint_fast64_t state) const override; |
|||
|
|||
uint_fast64_t getChoice(uint_fast64_t state) const override; |
|||
|
|||
friend std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler); |
|||
|
|||
private: |
|||
// A mapping from all states that have defined choices to their respective choices. |
|||
std::unordered_map<uint_fast64_t, uint_fast64_t> choices; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_PARTIALSCHEDULER_H_ */ |
|||
@ -0,0 +1,39 @@ |
|||
#ifndef STORM_STORAGE_SCHEDULER_H_ |
|||
#define STORM_STORAGE_SCHEDULER_H_ |
|||
|
|||
#include <cstdint> |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
/* |
|||
* This class is the abstract base class of all scheduler classes. Scheduler classes define which action is chosen in a particular state of a non-deterministic model. |
|||
* More concretely, a scheduler maps a state s to i if the scheduler takes the i-th action available in s (i.e. the choices are relative to the states). |
|||
*/ |
|||
class Scheduler { |
|||
public: |
|||
/* |
|||
* Sets the choice defined by the scheduler for the given state. |
|||
* |
|||
* @param state The state for which to set the choice. |
|||
* @param choice The choice to set for the given state. |
|||
*/ |
|||
virtual void setChoice(uint_fast64_t state, uint_fast64_t choice) = 0; |
|||
|
|||
/* |
|||
* Retrieves whether this scheduler defines a choice for the given state. |
|||
* |
|||
* @param state The state for which to check whether the scheduler defines a choice. |
|||
* @return True if the scheduler defines a choice for the given state. |
|||
*/ |
|||
virtual bool isChoiceDefined(uint_fast64_t state) const = 0; |
|||
|
|||
/*! |
|||
* Retrieves the choice for the given state under the assumption that the scheduler defines a proper choice for the state. |
|||
*/ |
|||
virtual uint_fast64_t getChoice(uint_fast64_t state) const = 0; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_SCHEDULER_H_ */ |
|||
@ -0,0 +1,37 @@ |
|||
#include "src/storage/TotalScheduler.h"
|
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
TotalScheduler::TotalScheduler(uint_fast64_t numberOfStates) : choices(numberOfStates) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
TotalScheduler::TotalScheduler(std::vector<uint_fast64_t> const& choices) : choices(choices) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
void TotalScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) { |
|||
choices[state] = choice; |
|||
} |
|||
|
|||
bool TotalScheduler::isChoiceDefined(uint_fast64_t state) const { |
|||
return true; |
|||
} |
|||
|
|||
uint_fast64_t TotalScheduler::getChoice(uint_fast64_t state) const { |
|||
return choices[state]; |
|||
} |
|||
|
|||
std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler) { |
|||
out << "total scheduler (defined on " << scheduler.choices.size() << " states) [ "; |
|||
for (uint_fast64_t state = 0; state < scheduler.choices.size() - 1; ++state) { |
|||
out << state << " -> " << scheduler.choices[state] << ", "; |
|||
} |
|||
if (scheduler.choices.size() > 0) { |
|||
out << (scheduler.choices.size() - 1) << " -> " << scheduler.choices[scheduler.choices.size() - 1] << " ]"; |
|||
} |
|||
return out; |
|||
} |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,33 @@ |
|||
#ifndef STORM_STORAGE_TOTALSCHEDULER_H_ |
|||
#define STORM_STORAGE_TOTALSCHEDULER_H_ |
|||
|
|||
#include <vector> |
|||
#include <ostream> |
|||
|
|||
#include "src/storage/Scheduler.h" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
class TotalScheduler : public Scheduler { |
|||
public: |
|||
TotalScheduler(uint_fast64_t numberOfStates); |
|||
|
|||
TotalScheduler(std::vector<uint_fast64_t> const& choices); |
|||
|
|||
void setChoice(uint_fast64_t state, uint_fast64_t choice) override; |
|||
|
|||
bool isChoiceDefined(uint_fast64_t state) const override; |
|||
|
|||
uint_fast64_t getChoice(uint_fast64_t state) const override; |
|||
|
|||
friend std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler); |
|||
|
|||
private: |
|||
// A vector that stores the choice for each state. |
|||
std::vector<uint_fast64_t> choices; |
|||
}; |
|||
} // namespace storage |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_STORAGE_TOTALSCHEDULER_H_ */ |
|||
@ -0,0 +1,52 @@ |
|||
#ifndef STORM_UTILITY_MATRIX_H_ |
|||
#define STORM_UTILITY_MATRIX_H_ |
|||
|
|||
#include "src/storage/SparseMatrix.h" |
|||
#include "src/storage/Scheduler.h" |
|||
#include "src/exceptions/InvalidStateException.h" |
|||
|
|||
namespace storm { |
|||
namespace utility { |
|||
namespace matrix { |
|||
|
|||
/*! |
|||
* Applies the given scheduler to the given transition matrix. This means that all choices that are not taken by the scheduler are |
|||
* dropped from the transition matrix. If a state has no choice enabled, it is equipped with a self-loop instead. |
|||
* |
|||
* @param transitionMatrix The transition matrix of the original system. |
|||
* @param nondeterministicChoiceIndices A vector indicating at which rows the choices for the states begin. |
|||
* @param scheduler The scheduler to apply to the system. |
|||
* @return A transition matrix that corresponds to all transitions of the given system that are selected by the given scheduler. |
|||
*/ |
|||
template <typename T> |
|||
storm::storage::SparseMatrix<T> applyScheduler(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::Scheduler const& scheduler) { |
|||
storm::storage::SparseMatrix<T> result(nondeterministicChoiceIndices.size() - 1, transitionMatrix.getColumnCount()); |
|||
|
|||
for (uint_fast64_t state = 0; state < nondeterministicChoiceIndices.size() - 1; ++state) { |
|||
if (scheduler.isChoiceDefined(state)) { |
|||
// Check whether the choice is valid for this state. |
|||
uint_fast64_t choice = nondeterministicChoiceIndices[state] + scheduler.getChoice(state); |
|||
if (choice >= nondeterministicChoiceIndices[state + 1]) { |
|||
throw storm::exceptions::InvalidStateException() << "Scheduler defines illegal choice " << choice << " for state " << state << "."; |
|||
} |
|||
|
|||
// If a valid choice for this state is defined, we copy over the corresponding entries. |
|||
typename storm::storage::SparseMatrix<T>::Rows selectedRow = transitionMatrix.getRow(choice); |
|||
for (auto entry : selectedRow) { |
|||
result.insertNextValue(state, entry.column(), entry.value()); |
|||
} |
|||
} else { |
|||
// If no valid choice for the state is defined, we insert a self-loop. |
|||
result.insertNextValue(state, state, storm::utility::constGetOne<T>()); |
|||
} |
|||
} |
|||
|
|||
// Finalize the matrix creation and return result. |
|||
result.finalize(); |
|||
return result; |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_UTILITY_MATRIX_H_ */ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue