Browse Source
refactoring early termination and solve goals and bounds
refactoring early termination and solve goals and bounds
Former-commit-id: 123835f655
tempestpy_adaptions
dehnert
9 years ago
25 changed files with 346 additions and 282 deletions
-
32src/logic/Bound.h
-
19src/logic/BoundInfo.h
-
12src/logic/ExpectedTimeOperatorFormula.cpp
-
6src/logic/ExpectedTimeOperatorFormula.h
-
12src/logic/LongRunAverageOperatorFormula.cpp
-
6src/logic/LongRunAverageOperatorFormula.h
-
24src/logic/OperatorFormula.cpp
-
19src/logic/OperatorFormula.h
-
12src/logic/ProbabilityOperatorFormula.cpp
-
6src/logic/ProbabilityOperatorFormula.h
-
12src/logic/RewardOperatorFormula.cpp
-
6src/logic/RewardOperatorFormula.h
-
8src/modelchecker/AbstractModelChecker.cpp
-
25src/modelchecker/CheckTask.h
-
2src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
-
53src/solver/AbstractEquationSolver.h
-
48src/solver/AllowEarlyTerminationCondition.cpp
-
52src/solver/AllowEarlyTerminationCondition.h
-
18src/solver/LinearEquationSolver.h
-
48src/solver/MinMaxLinearEquationSolver.h
-
24src/solver/SolveGoal.cpp
-
19src/solver/SolveGoal.h
-
41src/solver/TerminationCondition.cpp
-
53src/solver/TerminationCondition.h
-
71src/utility/vector.h
@ -0,0 +1,32 @@ |
|||
#ifndef STORM_LOGIC_BOUND_H_ |
|||
#define STORM_LOGIC_BOUND_H_ |
|||
|
|||
#include "src/logic/ComparisonType.h" |
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
template<typename ValueType> |
|||
struct Bound { |
|||
Bound(ComparisonType comparisonType, ValueType const& threshold) : comparisonType(comparisonType), threshold(threshold) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
ComparisonType comparisonType; |
|||
ValueType threshold; |
|||
|
|||
friend std::ostream& operator<<(std::ostream& out, Bound<ValueType> const& bound); |
|||
}; |
|||
|
|||
template<typename ValueType> |
|||
std::ostream& operator<<(std::ostream& out, Bound<ValueType> const& bound) { |
|||
out << bound.comparisonType << bound.threshold; |
|||
return out; |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
using Bound = typename logic::Bound<ValueType>; |
|||
} |
|||
|
|||
#endif /* STORM_LOGIC_BOUND_H_ */ |
|||
|
|||
@ -1,19 +0,0 @@ |
|||
|
|||
#ifndef BOUNDINFO_H |
|||
#define BOUNDINFO_H |
|||
|
|||
#include "ComparisonType.h" |
|||
|
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
template<typename BT> |
|||
struct BoundInfo { |
|||
BT bound; |
|||
ComparisonType boundType; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* BOUNDINFO_H */ |
|||
|
|||
@ -0,0 +1,53 @@ |
|||
#ifndef STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ |
|||
#define STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ |
|||
|
|||
#include "src/solver/TerminationCondition.h" |
|||
|
|||
namespace storm { |
|||
namespace solver { |
|||
|
|||
template<typename ValueType> |
|||
class AbstractEquationSolver { |
|||
public: |
|||
/*! |
|||
* Sets a custom termination condition that is used together with the regular termination condition of the |
|||
* solver. |
|||
* |
|||
* @param terminationCondition An object that can be queried whether to terminate early or not. |
|||
*/ |
|||
void setTerminationCondition(std::unique_ptr<TerminationCondition<ValueType>> terminationCondition) { |
|||
this->terminationCondition = std::move(terminationCondition); |
|||
} |
|||
|
|||
/*! |
|||
* Removes a previously set custom termination condition. |
|||
*/ |
|||
void resetTerminationCondition() { |
|||
this->terminationCondition = nullptr; |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves whether a custom termination condition has been set. |
|||
*/ |
|||
bool hasCustomTerminationCondition() { |
|||
return static_cast<bool>(this->terminationCondition); |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves the custom termination condition (if any was set). |
|||
* |
|||
* @return The custom termination condition. |
|||
*/ |
|||
TerminationCondition<ValueType> const& getTerminationCondition() const { |
|||
return *terminationCondition; |
|||
} |
|||
|
|||
protected: |
|||
// A termination condition to be used (can be unset). |
|||
std::unique_ptr<TerminationCondition<ValueType>> terminationCondition; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ */ |
|||
@ -1,48 +0,0 @@ |
|||
#include "AllowEarlyTerminationCondition.h"
|
|||
#include "src/utility/vector.h"
|
|||
|
|||
namespace storm { |
|||
namespace solver { |
|||
|
|||
template<typename ValueType> |
|||
TerminateAfterFilteredSumPassesThresholdValue<ValueType>::TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold) : |
|||
terminationThreshold(threshold), filter(filter) |
|||
{ |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool TerminateAfterFilteredSumPassesThresholdValue<ValueType>::terminateNow(const std::vector<ValueType>& currentValues) const { |
|||
assert(currentValues.size() >= filter.size()); |
|||
ValueType currentThreshold = storm::utility::vector::sum_if(currentValues, filter); |
|||
|
|||
return currentThreshold >= this->terminationThreshold; |
|||
|
|||
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
TerminateAfterFilteredExtremumPassesThresholdValue<ValueType>::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool useMinimum) : |
|||
terminationThreshold(threshold), filter(filter), useMinimumAsExtremum(useMinimum) |
|||
{ |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool TerminateAfterFilteredExtremumPassesThresholdValue<ValueType>::terminateNow(const std::vector<ValueType>& currentValues) const { |
|||
assert(currentValues.size() >= filter.size()); |
|||
|
|||
ValueType initVal = terminationThreshold - 1; |
|||
ValueType currentThreshold = useMinimumAsExtremum ? storm::utility::vector::max_if(currentValues, filter, initVal) : storm::utility::vector::max_if(currentValues, filter, initVal); |
|||
|
|||
return currentThreshold >= this->terminationThreshold; |
|||
|
|||
|
|||
} |
|||
|
|||
|
|||
template class TerminateAfterFilteredExtremumPassesThresholdValue<double>; |
|||
template class TerminateAfterFilteredSumPassesThresholdValue<double>; |
|||
|
|||
} |
|||
} |
|||
@ -1,52 +0,0 @@ |
|||
#ifndef ALLOWEARLYTERMINATIONCONDITION_H |
|||
#define ALLOWEARLYTERMINATIONCONDITION_H |
|||
|
|||
#include <vector> |
|||
#include "src/storage/BitVector.h" |
|||
|
|||
|
|||
namespace storm { |
|||
namespace solver { |
|||
template<typename ValueType> |
|||
class AllowEarlyTerminationCondition { |
|||
public: |
|||
virtual bool terminateNow(std::vector<ValueType> const& currentValues) const = 0; |
|||
}; |
|||
|
|||
template<typename ValueType> |
|||
class NoEarlyTerminationCondition : public AllowEarlyTerminationCondition<ValueType> { |
|||
public: |
|||
bool terminateNow(std::vector<ValueType> const& currentValues) const { return false; } |
|||
}; |
|||
|
|||
template<typename ValueType> |
|||
class TerminateAfterFilteredSumPassesThresholdValue : public AllowEarlyTerminationCondition<ValueType> { |
|||
public: |
|||
TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold); |
|||
bool terminateNow(std::vector<ValueType> const& currentValues) const; |
|||
|
|||
protected: |
|||
ValueType terminationThreshold; |
|||
storm::storage::BitVector filter; |
|||
}; |
|||
|
|||
template<typename ValueType> |
|||
class TerminateAfterFilteredExtremumPassesThresholdValue : public AllowEarlyTerminationCondition<ValueType>{ |
|||
public: |
|||
TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool useMinimum); |
|||
bool terminateNow(std::vector<ValueType> const& currentValue) const; |
|||
|
|||
protected: |
|||
ValueType terminationThreshold; |
|||
storm::storage::BitVector filter; |
|||
bool useMinimumAsExtremum; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
|
|||
|
|||
|
|||
|
|||
#endif /* ALLOWEARLYTERMINATIONCONDITION_H */ |
|||
|
|||
@ -0,0 +1,41 @@ |
|||
#include "src/solver/TerminationCondition.h"
|
|||
#include "src/utility/vector.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
|
|||
namespace storm { |
|||
namespace solver { |
|||
|
|||
template<typename ValueType> |
|||
bool NoTerminationCondition<ValueType>::terminateNow(std::vector<ValueType> const& currentValues) const { |
|||
return false; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
TerminateIfFilteredSumExceedsThreshold<ValueType>::TerminateIfFilteredSumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict) : threshold(threshold), filter(filter), strict(strict) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool TerminateIfFilteredSumExceedsThreshold<ValueType>::terminateNow(std::vector<ValueType> const& currentValues) const { |
|||
STORM_LOG_ASSERT(currentValues.size() == filter.size(), "Vectors sizes mismatch."); |
|||
ValueType currentThreshold = storm::utility::vector::sum_if(currentValues, filter); |
|||
return strict ? currentThreshold > this->threshold : currentThreshold >= this->threshold; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
TerminateIfFilteredExtremumExceedsThreshold<ValueType>::TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum) : TerminateIfFilteredSumExceedsThreshold<ValueType>(filter, threshold, strict), useMinimum(useMinimum) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool TerminateIfFilteredExtremumExceedsThreshold<ValueType>::terminateNow(const std::vector<ValueType>& currentValues) const { |
|||
STORM_LOG_ASSERT(currentValues.size() == filter.size(), "Vectors sizes mismatch."); |
|||
ValueType currentValue = useMinimum ? storm::utility::vector::min_if(currentValues, filter) : storm::utility::vector::max_if(currentValues, filter); |
|||
return this->strict ? currentValue > this->threshold : currentValue >= this->threshold; |
|||
} |
|||
|
|||
template class TerminateIfFilteredSumExceedsThreshold<double>; |
|||
template class TerminateIfFilteredExtremumExceedsThreshold<double>; |
|||
} |
|||
} |
|||
@ -0,0 +1,53 @@ |
|||
#ifndef ALLOWEARLYTERMINATIONCONDITION_H |
|||
#define ALLOWEARLYTERMINATIONCONDITION_H |
|||
|
|||
#include <vector> |
|||
#include "src/storage/BitVector.h" |
|||
|
|||
|
|||
namespace storm { |
|||
namespace solver { |
|||
template<typename ValueType> |
|||
class TerminationCondition { |
|||
public: |
|||
virtual bool terminateNow(std::vector<ValueType> const& currentValues) const = 0; |
|||
}; |
|||
|
|||
template<typename ValueType> |
|||
class NoTerminationCondition : public TerminationCondition<ValueType> { |
|||
public: |
|||
bool terminateNow(std::vector<ValueType> const& currentValues) const; |
|||
}; |
|||
|
|||
template<typename ValueType> |
|||
class TerminateIfFilteredSumExceedsThreshold : public TerminationCondition<ValueType> { |
|||
public: |
|||
TerminateIfFilteredSumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict); |
|||
bool terminateNow(std::vector<ValueType> const& currentValues) const; |
|||
|
|||
protected: |
|||
ValueType threshold; |
|||
storm::storage::BitVector filter; |
|||
bool strict; |
|||
}; |
|||
|
|||
template<typename ValueType> |
|||
class TerminateIfFilteredExtremumExceedsThreshold : public TerminateIfFilteredSumExceedsThreshold<ValueType>{ |
|||
public: |
|||
TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum); |
|||
bool terminateNow(std::vector<ValueType> const& currentValue) const; |
|||
|
|||
protected: |
|||
ValueType threshold; |
|||
storm::storage::BitVector filter; |
|||
bool useMinimum; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
|
|||
|
|||
|
|||
|
|||
#endif /* ALLOWEARLYTERMINATIONCONDITION_H */ |
|||
|
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue