sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge pull request 'next formulae' (#18) from next_formulae into main 

Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/18
tempestpy_adaptions
Stefan Pranger 4 years ago
parent
2a86bfa14c a86426211c
commit
3437d76a55
6 changed files with 41 additions and 2 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 1
      src/storm/logic/FragmentSpecification.cpp
  2. 17
      src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
  3. 2
      src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h
  4. 21
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
  5. 1
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h
  6. 1
      src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h

1
src/storm/logic/FragmentSpecification.cpp
View File

@ -67,6 +67,7 @@ namespace storm {
rpatl.setReachabilityProbabilityFormulasAllowed(true);
rpatl.setUntilFormulasAllowed(true);
rpatl.setGloballyFormulasAllowed(true);
rpatl.setNextFormulasAllowed(true);
return rpatl;
}

17
src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
View File

@ -114,6 +114,8 @@ namespace storm {
return this->computeUntilProbabilities(env, checkTask.substituteFormula(formula.asUntilFormula()));
} else if (formula.isGloballyFormula()) {
return this->computeGloballyProbabilities(env, checkTask.substituteFormula(formula.asGloballyFormula()));
} else if (formula.isNextFormula()) {
return this->computeNextProbabilities(env, checkTask.substituteFormula(formula.asNextFormula()));
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
}
@ -136,7 +138,6 @@ namespace storm {
std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
storm::solver::SolveGoal<ValueType> foo(this->getModel(), checkTask);
auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint());
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
@ -160,7 +161,19 @@ namespace storm {
return result;
}
template<typename SparseSmgModelType>
template<typename ModelType>
std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::computeNextProbabilities(Environment const& env, CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) {
storm::logic::NextFormula const& pathFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeNextProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint());
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
return result;
}
template<typename SparseSmgModelType>
std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<SparseSmgModelType>::computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI");
}

2
src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h
View File

@ -38,6 +38,8 @@ namespace storm {
std::unique_ptr<CheckResult> computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) override;
std::unique_ptr<CheckResult> computeGloballyProbabilities(Environment const& env, CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) override;
std::unique_ptr<CheckResult> computeNextProbabilities(Environment const& env, CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) override;
std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;

21
src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
View File

@ -85,6 +85,27 @@ namespace storm {
return result;
}
template<typename ValueType>
MDPSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeNextProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
// create vector x for result, bitvector allStates with a true for each state and a vector b for the probability to get to state psi
std::vector<ValueType> x = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
storm::storage::BitVector allStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true);
std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(allStates, psiStates);
statesOfCoalition.complement();
if (produceScheduler) {
STORM_LOG_WARN("Next formula does not expect that produceScheduler is set to true.");
}
// create multiplier and execute the calculation for 1 step
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
multiplier->multiplyAndReduce(env, goal.direction(), x, &b, x, nullptr, &statesOfCoalition);
STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x));
return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x));
}
template class SparseSmgRpatlHelper<double>;
#ifdef STORM_HAVE_CARL
template class SparseSmgRpatlHelper<storm::RationalNumber>;

1
src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h
View File

@ -38,6 +38,7 @@ namespace storm {
static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
static MDPSparseModelCheckingHelperReturnType<ValueType> computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
static MDPSparseModelCheckingHelperReturnType<ValueType> computeNextProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint);
private:
static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates);

1
src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h
View File

@ -41,6 +41,7 @@ namespace storm {
bool isProduceSchedulerSet() const;
storm::storage::Scheduler<ValueType> extractScheduler() const;
private:
void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);

Write Preview
Loading…
Cancel
Save