Browse Source
Improved storage::Scheduler. We can now consider arbitrary finite memory schedulers, potentially employing randomization.
main
Improved storage::Scheduler. We can now consider arbitrary finite memory schedulers, potentially employing randomization.
main
TimQu
8 years ago
38 changed files with 873 additions and 533 deletions
-
8src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp
-
12src/storm/modelchecker/hints/ExplicitModelCheckerHint.h
-
8src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
-
33src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
-
9src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h
-
42src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
-
8src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h
-
8src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp
-
17src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
-
1src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h
-
59src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
-
12src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h
-
12src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp
-
4src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h
-
165src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
-
4src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
-
6src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
-
8src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h
-
50src/storm/solver/GameSolver.cpp
-
32src/storm/solver/GameSolver.h
-
28src/storm/solver/MinMaxLinearEquationSolver.cpp
-
22src/storm/solver/MinMaxLinearEquationSolver.h
-
18src/storm/solver/StandardGameSolver.cpp
-
2src/storm/solver/StandardGameSolver.h
-
17src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
-
8src/storm/storage/Distribution.cpp
-
48src/storm/storage/PartialScheduler.cpp
-
34src/storm/storage/PartialScheduler.h
-
166src/storm/storage/Scheduler.cpp
-
93src/storm/storage/Scheduler.h
-
82src/storm/storage/SchedulerChoice.cpp
-
79src/storm/storage/SchedulerChoice.h
-
68src/storm/storage/TotalScheduler.cpp
-
78src/storm/storage/TotalScheduler.h
-
59src/storm/utility/graph.cpp
-
19src/storm/utility/graph.h
-
20src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
-
67src/test/storage/SchedulerTest.cpp
@ -1,48 +0,0 @@ |
|||
#include "storm/storage/PartialScheduler.h"
|
|||
#include "storm/exceptions/InvalidArgumentException.h"
|
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
void PartialScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) { |
|||
stateToChoiceMapping[state] = choice; |
|||
} |
|||
|
|||
bool PartialScheduler::isChoiceDefined(uint_fast64_t state) const { |
|||
return stateToChoiceMapping.find(state) != stateToChoiceMapping.end(); |
|||
} |
|||
|
|||
uint_fast64_t PartialScheduler::getChoice(uint_fast64_t state) const { |
|||
auto stateChoicePair = stateToChoiceMapping.find(state); |
|||
|
|||
if (stateChoicePair == stateToChoiceMapping.end()) { |
|||
throw storm::exceptions::InvalidArgumentException() << "Invalid call to PartialScheduler::getChoice: scheduler does not define a choice for state " << state << "."; |
|||
} |
|||
|
|||
return stateChoicePair->second; |
|||
} |
|||
|
|||
PartialScheduler::map_type::const_iterator PartialScheduler::begin() const { |
|||
return stateToChoiceMapping.begin(); |
|||
} |
|||
|
|||
PartialScheduler::map_type::const_iterator PartialScheduler::end() const { |
|||
return stateToChoiceMapping.end(); |
|||
} |
|||
|
|||
std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler) { |
|||
out << "partial scheduler (defined on " << scheduler.stateToChoiceMapping.size() << " states) [ "; |
|||
uint_fast64_t remainingEntries = scheduler.stateToChoiceMapping.size(); |
|||
for (auto const& stateChoicePair : scheduler.stateToChoiceMapping) { |
|||
out << stateChoicePair.first << " -> " << stateChoicePair.second; |
|||
--remainingEntries; |
|||
if (remainingEntries > 0) { |
|||
out << ", "; |
|||
} |
|||
} |
|||
out << "]"; |
|||
return out; |
|||
} |
|||
|
|||
} // namespace storage
|
|||
} // namespace storm
|
|||
@ -1,34 +0,0 @@ |
|||
#ifndef STORM_STORAGE_PARTIALSCHEDULER_H_ |
|||
#define STORM_STORAGE_PARTIALSCHEDULER_H_ |
|||
|
|||
#include <unordered_map> |
|||
#include <ostream> |
|||
|
|||
#include "storm/storage/Scheduler.h" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
class PartialScheduler : public Scheduler { |
|||
public: |
|||
typedef std::unordered_map<uint_fast64_t, uint_fast64_t> map_type; |
|||
|
|||
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; |
|||
|
|||
map_type::const_iterator begin() const; |
|||
map_type::const_iterator end() const; |
|||
|
|||
friend std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler); |
|||
|
|||
private: |
|||
// A mapping from all states that have defined choices to their respective choices. |
|||
map_type stateToChoiceMapping; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_PARTIALSCHEDULER_H_ */ |
|||
@ -0,0 +1,166 @@ |
|||
#include <storm/utility/vector.h>
|
|||
#include "storm/storage/Scheduler.h"
|
|||
|
|||
#include "storm/utility/macros.h"
|
|||
#include "storm/exceptions/NotImplementedException.h"
|
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
template <typename ValueType> |
|||
Scheduler<ValueType>::Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure> const& memoryStructure) : memoryStructure(memoryStructure) { |
|||
uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; |
|||
schedulerChoices = std::vector<std::vector<SchedulerChoice<ValueType>>>(numOfMemoryStates, std::vector<SchedulerChoice<ValueType>>(numberOfModelStates)); |
|||
numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; |
|||
numOfDeterministicChoices = 0; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
Scheduler<ValueType>::Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure>&& memoryStructure) : memoryStructure(std::move(memoryStructure)) { |
|||
uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; |
|||
schedulerChoices = std::vector<std::vector<SchedulerChoice<ValueType>>>(numOfMemoryStates, std::vector<SchedulerChoice<ValueType>>(numberOfModelStates)); |
|||
numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; |
|||
numOfDeterministicChoices = 0; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void Scheduler<ValueType>::setChoice(SchedulerChoice<ValueType> const& choice, uint_fast64_t modelState, uint_fast64_t memoryState) { |
|||
STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index"); |
|||
STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index"); |
|||
auto& schedulerChoice = schedulerChoices[memoryState][modelState]; |
|||
if (schedulerChoice.isDefined()) { |
|||
if (!choice.isDefined()) { |
|||
++numOfUndefinedChoices; |
|||
} |
|||
} else { |
|||
if (choice.isDefined()) { |
|||
assert(numOfUndefinedChoices > 0); |
|||
--numOfUndefinedChoices; |
|||
} |
|||
} |
|||
if (schedulerChoice.isDeterministic()) { |
|||
if (!choice.isDeterministic()) { |
|||
assert(numOfDeterministicChoices > 0); |
|||
--numOfDeterministicChoices; |
|||
} |
|||
} else { |
|||
if (choice.isDeterministic()) { |
|||
++numOfDeterministicChoices; |
|||
} |
|||
} |
|||
|
|||
schedulerChoice = choice; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void Scheduler<ValueType>::clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState) { |
|||
STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index"); |
|||
STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index"); |
|||
setChoice(SchedulerChoice<ValueType>(), modelState, memoryState); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
SchedulerChoice<ValueType> const& Scheduler<ValueType>::getChoice(uint_fast64_t modelState, uint_fast64_t memoryState) const { |
|||
STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index"); |
|||
STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index"); |
|||
return schedulerChoices[memoryState][modelState]; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
bool Scheduler<ValueType>::isPartialScheduler() const { |
|||
return numOfUndefinedChoices != 0; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
bool Scheduler<ValueType>::isDeterministicScheduler() const { |
|||
return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
bool Scheduler<ValueType>::isMemorylessScheduler() const { |
|||
return getNumberOfMemoryStates() == 1; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
uint_fast64_t Scheduler<ValueType>::getNumberOfMemoryStates() const { |
|||
return memoryStructure ? memoryStructure->getNumberOfStates() : 1; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void Scheduler<ValueType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, bool skipUniqueChoices) const { |
|||
out << "___________________________________________________________________" << std::endl; |
|||
out << (isPartialScheduler() ? "Partially" : "Fully") << " defined "; |
|||
out << (isMemorylessScheduler() ? "memoryless " : ""); |
|||
out << (isDeterministicScheduler() ? "deterministic" : "randomized") << " scheduler"; |
|||
if (!isMemorylessScheduler()) { |
|||
out << " with " << getNumberOfMemoryStates() << " memory states"; |
|||
} |
|||
out << "." << std::endl; |
|||
out << "___________________________________________________________________" << std::endl; |
|||
out << "Choices on " << schedulerChoices.front().size() << " model states:" << std::endl; |
|||
STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); |
|||
out << " model state: " << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << std::endl; |
|||
for (uint_fast64_t state = 0; state < schedulerChoices.front().size(); ++state) { |
|||
// Check whether the state is skipped
|
|||
if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) { |
|||
continue; |
|||
} |
|||
if (model != nullptr && model->hasStateValuations()) { |
|||
out << std::setw(20) << model->getStateValuations().getStateInfo(state); |
|||
} else { |
|||
out << std::setw(20) << state; |
|||
} |
|||
out << " "; |
|||
bool firstMemoryState = true; |
|||
for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { |
|||
if (firstMemoryState) { |
|||
firstMemoryState = false; |
|||
} else { |
|||
out << std::setw(20) << ""; |
|||
out << " "; |
|||
} |
|||
if (!isMemorylessScheduler()) { |
|||
out << "m" << std::setw(8) << memoryState; |
|||
} |
|||
|
|||
SchedulerChoice<ValueType> const& choice = schedulerChoices[memoryState][state]; |
|||
if (choice.isDefined()) { |
|||
if (choice.isDeterministic()) { |
|||
if (model != nullptr && model->hasChoiceOrigins()) { |
|||
out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); |
|||
} else { |
|||
out << choice.getDeterministicChoice(); |
|||
} |
|||
} else { |
|||
bool firstChoice = true; |
|||
for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { |
|||
if (firstChoice) { |
|||
firstChoice = false; |
|||
} else { |
|||
out << " + "; |
|||
} |
|||
out << choiceProbPair.second << ": ("; |
|||
if (model != nullptr && model->hasChoiceOrigins()) { |
|||
out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); |
|||
} else { |
|||
out << choiceProbPair.first; |
|||
} |
|||
out << ")"; |
|||
} |
|||
} |
|||
} else { |
|||
out << "undefined."; |
|||
} |
|||
out << std::endl; |
|||
} |
|||
} |
|||
out << "___________________________________________________________________" << std::endl; |
|||
} |
|||
|
|||
template class Scheduler<double>; |
|||
template class Scheduler<float>; |
|||
template class Scheduler<storm::RationalNumber>; |
|||
template class Scheduler<storm::RationalFunction>; |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,82 @@ |
|||
#include "storm/storage/SchedulerChoice.h"
|
|||
|
|||
#include "storm/utility/constants.h"
|
|||
#include "storm/utility/macros.h"
|
|||
|
|||
#include "storm/exceptions/InvalidOperationException.h"
|
|||
#include "storm/adapters/RationalFunctionAdapter.h"
|
|||
#include "storm/adapters/RationalNumberAdapter.h"
|
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
|
|||
|
|||
template <typename ValueType> |
|||
SchedulerChoice<ValueType>::SchedulerChoice() { |
|||
// Intentionally left empty
|
|||
} |
|||
|
|||
template <typename ValueType> |
|||
SchedulerChoice<ValueType>::SchedulerChoice(uint_fast64_t deterministicChoice) { |
|||
distribution.addProbability(deterministicChoice, storm::utility::one<ValueType>()); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
SchedulerChoice<ValueType>::SchedulerChoice(storm::storage::Distribution<ValueType, uint_fast64_t> const& randomizedChoice) : distribution(randomizedChoice) { |
|||
// Intentionally left empty
|
|||
} |
|||
|
|||
template <typename ValueType> |
|||
SchedulerChoice<ValueType>::SchedulerChoice(storm::storage::Distribution<ValueType, uint_fast64_t>&& randomizedChoice) : distribution(std::move(randomizedChoice)) { |
|||
// Intentionally left empty
|
|||
} |
|||
|
|||
template <typename ValueType> |
|||
bool SchedulerChoice<ValueType>::isDefined() const { |
|||
return distribution.size() != 0; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
bool SchedulerChoice<ValueType>::isDeterministic() const { |
|||
return distribution.size() == 1; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
uint_fast64_t SchedulerChoice<ValueType>::getDeterministicChoice() const { |
|||
STORM_LOG_THROW(isDeterministic(), storm::exceptions::InvalidOperationException, "Tried to obtain the deterministic choice of a scheduler, but the choice is not deterministic"); |
|||
return distribution.begin()->first; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
storm::storage::Distribution<ValueType, uint_fast64_t> const& SchedulerChoice<ValueType>::getChoiceAsDistribution() const { |
|||
return distribution; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::ostream& operator<<(std::ostream& out, SchedulerChoice<ValueType> const& schedulerChoice) { |
|||
if (schedulerChoice.isDefined()) { |
|||
if (schedulerChoice.isDeterministic()) { |
|||
out << schedulerChoice.getDeterministicChoice(); |
|||
} else { |
|||
out << schedulerChoice.getChoiceAsDistribution(); |
|||
} |
|||
} else { |
|||
out << "undefined"; |
|||
} |
|||
return out; |
|||
} |
|||
|
|||
template class SchedulerChoice<double>; |
|||
template std::ostream& operator<<(std::ostream& out, SchedulerChoice<double> const& schedulerChoice); |
|||
template class SchedulerChoice<float>; |
|||
template std::ostream& operator<<(std::ostream& out, SchedulerChoice<float> const& schedulerChoice); |
|||
template class SchedulerChoice<storm::RationalNumber>; |
|||
template std::ostream& operator<<(std::ostream& out, SchedulerChoice<storm::RationalNumber> const& schedulerChoice); |
|||
template class SchedulerChoice<storm::RationalFunction>; |
|||
template std::ostream& operator<<(std::ostream& out, SchedulerChoice<storm::RationalFunction> const& schedulerChoice); |
|||
|
|||
} |
|||
} |
|||
|
|||
|
|||
@ -0,0 +1,79 @@ |
|||
#pragma once |
|||
|
|||
#include "storm/utility/constants.h" |
|||
#include "storm/storage/Distribution.h" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
template <typename ValueType> |
|||
class SchedulerChoice { |
|||
|
|||
public: |
|||
|
|||
/*! |
|||
* Creates an undefined scheduler choice |
|||
*/ |
|||
SchedulerChoice(); |
|||
|
|||
/*! |
|||
* Creates a deterministic scheduler choice |
|||
* @param deterministicChoice the (local) choice index |
|||
*/ |
|||
SchedulerChoice(uint_fast64_t deterministicChoice); |
|||
|
|||
/*! |
|||
* Creates a scheduler choice that potentially considers randomization |
|||
* @param randomizedChoice a distribution over the (local) choice indices |
|||
*/ |
|||
SchedulerChoice(storm::storage::Distribution<ValueType, uint_fast64_t> const& randomizedChoice); |
|||
|
|||
/*! |
|||
* Creates a scheduler choice that potentially considers randomization |
|||
* @param randomizedChoice a distribution over the (local) choice indices |
|||
*/ |
|||
SchedulerChoice(storm::storage::Distribution<ValueType, uint_fast64_t>&& randomizedChoice); |
|||
|
|||
/*! |
|||
* Returns true iff this scheduler choice is defined |
|||
*/ |
|||
bool isDefined() const; |
|||
|
|||
/*! |
|||
* Returns true iff this scheduler choice is deterministic (i.e., not randomized) |
|||
*/ |
|||
bool isDeterministic() const; |
|||
|
|||
/*! |
|||
* If this choice is deterministic, this function returns the selected (local) choice index. |
|||
* Otherwise, an exception is thrown. |
|||
*/ |
|||
uint_fast64_t getDeterministicChoice() const; |
|||
|
|||
/*! |
|||
* Retrieves this choice in the form of a probability distribution. |
|||
*/ |
|||
storm::storage::Distribution<ValueType, uint_fast64_t> const& getChoiceAsDistribution() const; |
|||
|
|||
/*! |
|||
* Changes the value type of this scheduler choice to the given one. |
|||
*/ |
|||
template<typename NewValueType> |
|||
SchedulerChoice<NewValueType> toValueType() const { |
|||
storm::storage::Distribution<NewValueType, uint_fast64_t> newDistribution; |
|||
for (auto const& stateValuePair : distribution) { |
|||
newDistribution.addProbability(stateValuePair.first, storm::utility::convertNumber<NewValueType>(stateValuePair.second)); |
|||
} |
|||
return SchedulerChoice<NewValueType>(std::move(newDistribution)); |
|||
} |
|||
|
|||
private: |
|||
storm::storage::Distribution<ValueType, uint_fast64_t> distribution; |
|||
}; |
|||
|
|||
template<typename ValueType> |
|||
std::ostream& operator<<(std::ostream& out, SchedulerChoice<ValueType> const& schedulerChoice); |
|||
} |
|||
} |
|||
|
|||
|
|||
@ -1,68 +0,0 @@ |
|||
#include "storm/storage/TotalScheduler.h"
|
|||
#include "storm/exceptions/InvalidArgumentException.h"
|
|||
#include "storm/utility/Hash.h"
|
|||
#include "storm/utility/vector.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.
|
|||
} |
|||
|
|||
TotalScheduler::TotalScheduler(std::vector<uint_fast64_t>&& choices) : choices(std::move(choices)) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
bool TotalScheduler::operator==(storm::storage::TotalScheduler const& other) const { |
|||
return this->choices == other.choices; |
|||
} |
|||
|
|||
void TotalScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) { |
|||
if (state > choices.size()) { |
|||
throw storm::exceptions::InvalidArgumentException() << "Invalid call to TotalScheduler::setChoice: scheduler cannot not define a choice for state " << state << "."; |
|||
} |
|||
choices[state] = choice; |
|||
} |
|||
|
|||
bool TotalScheduler::isChoiceDefined(uint_fast64_t state) const { |
|||
return state < choices.size(); |
|||
} |
|||
|
|||
uint_fast64_t TotalScheduler::getChoice(uint_fast64_t state) const { |
|||
if (state >= choices.size()) { |
|||
throw storm::exceptions::InvalidArgumentException() << "Invalid call to TotalScheduler::getChoice: scheduler does not define a choice for state " << state << "."; |
|||
} |
|||
|
|||
return choices[state]; |
|||
} |
|||
|
|||
std::vector<uint_fast64_t> const& TotalScheduler::getChoices() const { |
|||
return choices; |
|||
} |
|||
|
|||
TotalScheduler TotalScheduler::getSchedulerForSubsystem(storm::storage::BitVector const& subsystem) const { |
|||
return TotalScheduler(storm::utility::vector::filterVector(choices, subsystem)); |
|||
} |
|||
|
|||
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; |
|||
} |
|||
} |
|||
} |
|||
|
|||
namespace std { |
|||
std::size_t hash<storm::storage::TotalScheduler>::operator()(storm::storage::TotalScheduler const& totalScheduler) const { |
|||
return storm::utility::Hash<uint_fast64_t>::getHash(totalScheduler.choices); |
|||
} |
|||
} |
|||
@ -1,78 +0,0 @@ |
|||
#ifndef STORM_STORAGE_TOTALSCHEDULER_H_ |
|||
#define STORM_STORAGE_TOTALSCHEDULER_H_ |
|||
|
|||
#include <vector> |
|||
#include <ostream> |
|||
|
|||
#include "storm/storage/Scheduler.h" |
|||
#include "storm/storage/BitVector.h" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
class TotalScheduler : public Scheduler { |
|||
public: |
|||
|
|||
TotalScheduler(TotalScheduler const& other) = default; |
|||
TotalScheduler(TotalScheduler&& other) = default; |
|||
TotalScheduler& operator=(TotalScheduler const& other) = default; |
|||
TotalScheduler& operator=(TotalScheduler&& other) = default; |
|||
|
|||
/*! |
|||
* Creates a total scheduler that defines a choice for the given number of states. By default, all choices |
|||
* are initialized to zero. |
|||
* |
|||
* @param numberOfStates The number of states for which the scheduler defines a choice. |
|||
*/ |
|||
TotalScheduler(uint_fast64_t numberOfStates = 0); |
|||
|
|||
/*! |
|||
* Creates a total scheduler that defines the choices for states according to the given vector. |
|||
* |
|||
* @param choices A vector whose i-th entry defines the choice of state i. |
|||
*/ |
|||
TotalScheduler(std::vector<uint_fast64_t> const& choices); |
|||
|
|||
/*! |
|||
* Creates a total scheduler that defines the choices for states according to the given vector. |
|||
* |
|||
* @param choices A vector whose i-th entry defines the choice of state i. |
|||
*/ |
|||
TotalScheduler(std::vector<uint_fast64_t>&& choices); |
|||
|
|||
bool operator==(TotalScheduler const& other) const; |
|||
|
|||
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; |
|||
|
|||
std::vector<uint_fast64_t> const& getChoices() const; |
|||
|
|||
/*! |
|||
* Constructs the scheduler for the subsystem indicated by the given BitVector |
|||
* |
|||
* @param subsystem A BitVector whose i-th entry is true iff state i is part of the subsystem |
|||
*/ |
|||
TotalScheduler getSchedulerForSubsystem(storm::storage::BitVector const& subsystem) const; |
|||
|
|||
friend std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler); |
|||
friend struct std::hash<storm::storage::TotalScheduler>; |
|||
|
|||
private: |
|||
// A vector that stores the choice for each state. |
|||
std::vector<uint_fast64_t> choices; |
|||
}; |
|||
} // namespace storage |
|||
} // namespace storm |
|||
|
|||
|
|||
namespace std { |
|||
template <> |
|||
struct hash<storm::storage::TotalScheduler> { |
|||
std::size_t operator()(storm::storage::TotalScheduler const& totalScheduler) const; |
|||
}; |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_TOTALSCHEDULER_H_ */ |
|||
@ -1,42 +1,53 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
#include "storm/exceptions/InvalidArgumentException.h"
|
|||
#include "storm/storage/PartialScheduler.h"
|
|||
#include "storm/storage/TotalScheduler.h"
|
|||
#include "storm/exceptions/InvalidOperationException.h"
|
|||
#include "storm/storage/Scheduler.h"
|
|||
|
|||
TEST(SchedulerTest, PartialScheduler) { |
|||
storm::storage::PartialScheduler scheduler; |
|||
TEST(SchedulerTest, TotalDeterministicMemorylessScheduler) { |
|||
storm::storage::Scheduler<double> scheduler(4); |
|||
|
|||
ASSERT_NO_THROW(scheduler.setChoice(0, 1)); |
|||
ASSERT_NO_THROW(scheduler.setChoice(0, 3)); |
|||
ASSERT_NO_THROW(scheduler.setChoice(3, 4)); |
|||
ASSERT_NO_THROW(scheduler.setChoice(1, 0)); |
|||
ASSERT_NO_THROW(scheduler.setChoice(3, 1)); |
|||
ASSERT_NO_THROW(scheduler.setChoice(5, 2)); |
|||
ASSERT_NO_THROW(scheduler.setChoice(4, 3)); |
|||
|
|||
ASSERT_TRUE(scheduler.isChoiceDefined(0)); |
|||
ASSERT_EQ(3ul, scheduler.getChoice(0)); |
|||
ASSERT_FALSE(scheduler.isPartialScheduler()); |
|||
ASSERT_TRUE(scheduler.isMemorylessScheduler()); |
|||
ASSERT_TRUE(scheduler.isDeterministicScheduler()); |
|||
|
|||
ASSERT_TRUE(scheduler.isChoiceDefined(3)); |
|||
ASSERT_EQ(4ul, scheduler.getChoice(3)); |
|||
ASSERT_TRUE(scheduler.getChoice(0).isDefined()); |
|||
ASSERT_EQ(1ul, scheduler.getChoice(0).getDeterministicChoice()); |
|||
|
|||
ASSERT_TRUE(scheduler.getChoice(1).isDefined()); |
|||
ASSERT_EQ(3ul, scheduler.getChoice(1).getDeterministicChoice()); |
|||
|
|||
ASSERT_TRUE(scheduler.getChoice(2).isDefined()); |
|||
ASSERT_EQ(5ul, scheduler.getChoice(2).getDeterministicChoice()); |
|||
|
|||
ASSERT_TRUE(scheduler.getChoice(3).isDefined()); |
|||
ASSERT_EQ(4ul, scheduler.getChoice(3).getDeterministicChoice()); |
|||
|
|||
ASSERT_FALSE(scheduler.isChoiceDefined(1)); |
|||
ASSERT_THROW(scheduler.getChoice(1), storm::exceptions::InvalidArgumentException); |
|||
} |
|||
|
|||
TEST(SchedulerTest, TotalScheduler) { |
|||
storm::storage::TotalScheduler scheduler(4); |
|||
TEST(SchedulerTest, PartialDeterministicMemorylessScheduler) { |
|||
storm::storage::Scheduler<double> scheduler(4); |
|||
|
|||
ASSERT_NO_THROW(scheduler.setChoice(1, 0)); |
|||
ASSERT_NO_THROW(scheduler.setChoice(3, 0)); |
|||
ASSERT_NO_THROW(scheduler.setChoice(5, 2)); |
|||
ASSERT_NO_THROW(scheduler.setChoice(4, 3)); |
|||
ASSERT_NO_THROW(scheduler.clearChoice(2)); |
|||
|
|||
ASSERT_NO_THROW(scheduler.setChoice(0, 1)); |
|||
ASSERT_NO_THROW(scheduler.setChoice(0, 3)); |
|||
ASSERT_NO_THROW(scheduler.setChoice(3, 4)); |
|||
ASSERT_TRUE(scheduler.isPartialScheduler()); |
|||
ASSERT_TRUE(scheduler.isMemorylessScheduler()); |
|||
ASSERT_TRUE(scheduler.isDeterministicScheduler()); |
|||
|
|||
ASSERT_TRUE(scheduler.isChoiceDefined(0)); |
|||
ASSERT_EQ(3ul, scheduler.getChoice(0)); |
|||
ASSERT_TRUE(scheduler.getChoice(0).isDefined()); |
|||
ASSERT_EQ(3ul, scheduler.getChoice(0).getDeterministicChoice()); |
|||
|
|||
ASSERT_TRUE(scheduler.isChoiceDefined(3)); |
|||
ASSERT_EQ(4ul, scheduler.getChoice(3)); |
|||
ASSERT_TRUE(scheduler.getChoice(3).isDefined()); |
|||
ASSERT_EQ(4ul, scheduler.getChoice(3).getDeterministicChoice()); |
|||
|
|||
ASSERT_TRUE(scheduler.isChoiceDefined(1)); |
|||
ASSERT_EQ(0ul, scheduler.getChoice(1)); |
|||
|
|||
ASSERT_THROW(scheduler.getChoice(4), storm::exceptions::InvalidArgumentException); |
|||
ASSERT_THROW(scheduler.setChoice(5, 2), storm::exceptions::InvalidArgumentException); |
|||
ASSERT_FALSE(scheduler.getChoice(1).isDefined()); |
|||
ASSERT_FALSE(scheduler.getChoice(2).isDefined()); |
|||
} |
|||
Reference in new issue
xxxxxxxxxx