Browse Source

preparations for scheduler extraction support

tempestpy_adaptions
Sebastian Junges 7 years ago
parent
commit
0534216a85
  1. 4
      src/storm/modelchecker/results/CheckResult.cpp
  2. 4
      src/storm/modelchecker/results/CheckResult.h
  3. 2
      src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h
  4. 6
      src/storm/storage/Scheduler.h

4
src/storm/modelchecker/results/CheckResult.cpp

@ -162,6 +162,10 @@ namespace storm {
SymbolicParetoCurveCheckResult<Type, ValueType> const& CheckResult::asSymbolicParetoCurveCheckResult() const {
return dynamic_cast<SymbolicParetoCurveCheckResult<Type, ValueType> const&>(*this);
}
bool CheckResult::hasScheduler() const {
return false;
}
// Explicitly instantiate the template functions.
template QuantitativeCheckResult<double>& CheckResult::asQuantitativeCheckResult();

4
src/storm/modelchecker/results/CheckResult.h

@ -111,7 +111,9 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
SymbolicParetoCurveCheckResult<Type, ValueType> const& asSymbolicParetoCurveCheckResult() const;
virtual bool hasScheduler() const;
virtual std::ostream& writeToStream(std::ostream& out) const = 0;
};

2
src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h

@ -65,7 +65,7 @@ namespace storm {
virtual ValueType average() const override;
virtual ValueType sum() const override;
bool hasScheduler() const;
virtual bool hasScheduler() const override;
void setScheduler(std::unique_ptr<storm::storage::Scheduler<ValueType>>&& scheduler);
storm::storage::Scheduler<ValueType> const& getScheduler() const;
storm::storage::Scheduler<ValueType>& getScheduler();

6
src/storm/storage/Scheduler.h

@ -44,10 +44,10 @@ namespace storm {
void clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0);
/*!
* Sets the choice defined by the scheduler for the given model and memory state.
* Gets the choice defined by the scheduler for the given model and memory state.
*
* @param state The state for which to set the choice.
* @param choice The choice to set for the given state.
* @param state The state for which to get the choice.
* @param memoryState the memory state which we consider.
*/
SchedulerChoice<ValueType> const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const;

Loading…
Cancel
Save