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

removed duplicate code after big merge

tempestpy_adaptions
Stefan Pranger 3 years ago
parent
7e7d6defa0
commit
85c5125610
3 changed files with 2 additions and 61 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 3
      src/storm/logic/Formula.h
  2. 29
      src/storm/logic/FragmentSpecification.cpp
  3. 31
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

3
src/storm/logic/Formula.h
View File

@ -149,9 +149,6 @@ namespace storm {
HOAPathFormula& asHOAPathFormula(); HOAPathFormula& asHOAPathFormula();
HOAPathFormula const& asHOAPathFormula() const; HOAPathFormula const& asHOAPathFormula() const;
HOAPathFormula& asHOAPathFormula();
HOAPathFormula const& asHOAPathFormula() const;
BoundedUntilFormula& asBoundedUntilFormula(); BoundedUntilFormula& asBoundedUntilFormula();
BoundedUntilFormula const& asBoundedUntilFormula() const; BoundedUntilFormula const& asBoundedUntilFormula() const;

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

@ -114,35 +114,6 @@ namespace storm {
return rpatl; return rpatl;
} }
FragmentSpecification prctl() {
FragmentSpecification prctl = pctl();
prctl.setRewardOperatorsAllowed(true);
prctl.setCumulativeRewardFormulasAllowed(true);
prctl.setInstantaneousFormulasAllowed(true);
prctl.setReachabilityRewardFormulasAllowed(true);
prctl.setLongRunAverageOperatorsAllowed(true);
prctl.setStepBoundedCumulativeRewardFormulasAllowed(true);
prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true);
return prctl;
}
FragmentSpecification prctlstar() {
FragmentSpecification prctlstar = pctlstar();
prctlstar.setRewardOperatorsAllowed(true);
prctlstar.setCumulativeRewardFormulasAllowed(true);
prctlstar.setInstantaneousFormulasAllowed(true);
prctlstar.setReachabilityRewardFormulasAllowed(true);
prctlstar.setLongRunAverageOperatorsAllowed(true);
prctlstar.setStepBoundedCumulativeRewardFormulasAllowed(true);
prctlstar.setTimeBoundedCumulativeRewardFormulasAllowed(true);
return prctlstar;
}
FragmentSpecification csl() { FragmentSpecification csl() {
FragmentSpecification csl = pctl(); FragmentSpecification csl = pctl();

31
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View File

@ -117,41 +117,14 @@ namespace storm {
template<typename SparseDtmcModelType> template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeHOAPathProbabilities(Environment const& env, CheckTask<storm::logic::HOAPathFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeHOAPathProbabilities(Environment const& env, CheckTask<storm::logic::HOAPathFormula, ValueType> const& checkTask) {
storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula();
storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(this->getModel().getTransitionMatrix());
storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel());
auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); };
auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker);
std::vector<ValueType> numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeLTLProbabilities(Environment const& env, CheckTask<storm::logic::PathFormula, ValueType> const& checkTask) {
storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(this->getModel().getTransitionMatrix()); storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(this->getModel().getTransitionMatrix());
storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel());
auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); };
std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeHOAPathProbabilities(Environment const& env, CheckTask<storm::logic::HOAPathFormula, ValueType> const& checkTask) {
storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula();
storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(this->getModel().getTransitionMatrix());
storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel());
auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); };
auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker);
std::vector<ValueType> numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); std::vector<ValueType> numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult))); return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
} }
@ -161,7 +134,7 @@ namespace storm {
storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(this->getModel().getTransitionMatrix()); storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(this->getModel().getTransitionMatrix());
storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel());
auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); };
std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker);

Write Preview
Loading…
Cancel
Save