Browse Source
Merge branch 'future' of https://sselab.de/lab9/private/git/storm into future
Merge branch 'future' of https://sselab.de/lab9/private/git/storm into future
Former-commit-id: 8cbeeb315a
main
sjunges
9 years ago
56 changed files with 793 additions and 460 deletions
-
6resources/3rdparty/CMakeLists.txt
-
7src/counterexamples/MILPMinimalLabelSetGenerator.h
-
8src/counterexamples/SMTMinimalCommandSetGenerator.h
-
33src/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
-
48src/modelchecker/CheckTask.h
-
2src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
-
8src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
-
2src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
-
26src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h
-
74src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
-
6src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
-
16src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
-
9src/modelchecker/results/ExplicitQuantitativeCheckResult.h
-
37src/parser/FormulaParser.cpp
-
2src/parser/PrismParser.cpp
-
4src/permissivesched/PermissiveSchedulers.cpp
-
53src/solver/AbstractEquationSolver.h
-
48src/solver/AllowEarlyTerminationCondition.cpp
-
52src/solver/AllowEarlyTerminationCondition.h
-
2src/solver/GmmxxLinearEquationSolver.cpp
-
34src/solver/GmmxxMinMaxLinearEquationSolver.cpp
-
4src/solver/GmmxxMinMaxLinearEquationSolver.h
-
11src/solver/LinearEquationSolver.h
-
47src/solver/MinMaxLinearEquationSolver.cpp
-
72src/solver/MinMaxLinearEquationSolver.h
-
4src/solver/NativeLinearEquationSolver.cpp
-
29src/solver/NativeMinMaxLinearEquationSolver.cpp
-
4src/solver/NativeMinMaxLinearEquationSolver.h
-
43src/solver/SolveGoal.cpp
-
103src/solver/SolveGoal.h
-
41src/solver/TerminationCondition.cpp
-
51src/solver/TerminationCondition.h
-
8src/storage/PartialScheduler.cpp
-
3src/storage/PartialScheduler.h
-
4src/storage/TotalScheduler.cpp
-
7src/storage/TotalScheduler.h
-
6src/utility/graph.cpp
-
14src/utility/solver.cpp
-
6src/utility/solver.h
-
67src/utility/vector.h
-
52test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
-
16test/functional/modelchecker/scheduler_generation.nm
-
6test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp
-
8test/functional/utility/VectorTest.cpp
@ -0,0 +1,33 @@ |
|||
#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; |
|||
|
|||
template<typename ValueTypePrime> |
|||
friend std::ostream& operator<<(std::ostream& out, Bound<ValueTypePrime> 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() const { |
|||
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 */ |
|||
|
|||
@ -1,36 +1,55 @@ |
|||
#include "SolveGoal.h"
|
|||
|
|||
#include <memory>
|
|||
|
|||
#include "src/utility/solver.h"
|
|||
#include "src/solver/LinearEquationSolver.h"
|
|||
#include "src/solver/MinMaxLinearEquationSolver.h"
|
|||
#include <memory>
|
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
template <typename VT> class SparseMatrix; |
|||
template <typename ValueType> class SparseMatrix; |
|||
} |
|||
|
|||
namespace solver { |
|||
|
|||
template<typename VT> |
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<VT>> configureMinMaxLinearEquationSolver(BoundedGoal<VT> const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory<VT> const& factory, storm::storage::SparseMatrix<VT> const& matrix) { |
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<VT>> p = factory.create(matrix); |
|||
template<typename ValueType> |
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> configureMinMaxLinearEquationSolver(BoundedGoal<ValueType> const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& factory, storm::storage::SparseMatrix<ValueType> const& matrix) { |
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> p = factory.create(matrix); |
|||
p->setOptimizationDirection(goal.direction()); |
|||
p->setEarlyTerminationCriterion(std::make_unique<TerminateAfterFilteredExtremumPassesThresholdValue<double>>(goal.relevantColumns(), goal.threshold, goal.minimize())); |
|||
p->setTerminationCondition(std::make_unique<TerminateIfFilteredExtremumExceedsThreshold<double>>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), goal.minimize())); |
|||
return p; |
|||
} |
|||
|
|||
template<typename VT> |
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<VT>> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory<VT> const& factory, storm::storage::SparseMatrix<VT> const& matrix) { |
|||
template<typename ValueType> |
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& factory, storm::storage::SparseMatrix<ValueType> const& matrix) { |
|||
if (goal.isBounded()) { |
|||
return configureMinMaxLinearEquationSolver(static_cast<BoundedGoal<VT> const&>(goal), factory, matrix); |
|||
return configureMinMaxLinearEquationSolver(static_cast<BoundedGoal<ValueType> const&>(goal), factory, matrix); |
|||
} |
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<VT>> p = factory.create(matrix); |
|||
p->setOptimizationDirection(goal.direction()); |
|||
return p; |
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = factory.create(matrix); |
|||
solver->setOptimizationDirection(goal.direction()); |
|||
return solver; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> configureLinearEquationSolver(BoundedGoal<ValueType> const& goal, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& factory, storm::storage::SparseMatrix<ValueType> const& matrix) { |
|||
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = factory.create(matrix); |
|||
solver->setTerminationCondition(std::make_unique<TerminateIfFilteredExtremumExceedsThreshold<double>>(goal.relevantValues(), goal.thresholdValue(), goal.boundIsStrict(), goal.minimize())); |
|||
return solver; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& factory, storm::storage::SparseMatrix<ValueType> const& matrix) { |
|||
if (goal.isBounded()) { |
|||
return configureLinearEquationSolver(static_cast<BoundedGoal<ValueType> const&>(goal), factory, matrix); |
|||
} |
|||
return factory.create(matrix); |
|||
} |
|||
|
|||
template std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<double>> configureMinMaxLinearEquationSolver(BoundedGoal<double> const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory<double> const& factory, storm::storage::SparseMatrix<double> const& matrix); |
|||
template std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<double>> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory<double> const& factory, storm::storage::SparseMatrix<double> const& matrix); |
|||
template std::unique_ptr<storm::solver::LinearEquationSolver<double>> configureLinearEquationSolver(BoundedGoal<double> const& goal, storm::utility::solver::LinearEquationSolverFactory<double> const& factory, storm::storage::SparseMatrix<double> const& matrix); |
|||
template std::unique_ptr<storm::solver::LinearEquationSolver<double>> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory<double> const& factory, storm::storage::SparseMatrix<double> const& matrix); |
|||
|
|||
} |
|||
} |
|||
@ -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(std::vector<ValueType> const& currentValues) const { |
|||
STORM_LOG_ASSERT(currentValues.size() == this->filter.size(), "Vectors sizes mismatch."); |
|||
ValueType currentValue = useMinimum ? storm::utility::vector::min_if(currentValues, this->filter) : storm::utility::vector::max_if(currentValues, this->filter); |
|||
return this->strict ? currentValue > this->threshold : currentValue >= this->threshold; |
|||
} |
|||
|
|||
template class TerminateIfFilteredSumExceedsThreshold<double>; |
|||
template class TerminateIfFilteredExtremumExceedsThreshold<double>; |
|||
} |
|||
} |
|||
@ -0,0 +1,51 @@ |
|||
#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: |
|||
bool useMinimum; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
|
|||
|
|||
|
|||
|
|||
#endif /* ALLOWEARLYTERMINATIONCONDITION_H */ |
|||
|
|||
@ -0,0 +1,16 @@ |
|||
mdp |
|||
|
|||
module one |
|||
|
|||
s : [0 .. 5] init 0; |
|||
|
|||
[] s=0 -> 0.5: (s'=1) + 0.5: (s'=3); |
|||
[] s=1 -> 0.4 : (s'=4) + 0.6: (s'=3); |
|||
[] s=1 -> 1: (s'=4); |
|||
[] s=1 -> 0.8: (s'=3) + 0.2: (s'=4); |
|||
[] s=0 | s = 2 -> 0.9: (s'=s) + 0.1 : (s'=3); |
|||
[] 3 <= s & s <= 4 -> 1: true; |
|||
|
|||
endmodule |
|||
|
|||
label "target" = s=3; |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue