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

Merge pull request '[STORM PR] Fixes after LTL merge' (#47) from merge_pr_137 into main 

Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/47
tempestpy_adaptions
Stefan Pranger 3 years ago
parent
814f7b036d 90dba4cd5d
commit
6c6f501900
7 changed files with 33 additions and 86 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. 3
      src/storm/logic/Formula.h
  2. 29
      src/storm/logic/FragmentSpecification.cpp
  3. 5
      src/storm/logic/ToPrefixStringVisitor.cpp
  4. 44
      src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
  5. 31
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  6. 4
      src/storm/storage/Scheduler.cpp
  7. 3
      src/storm/storage/Scheduler.h

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

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

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

@ -114,35 +114,6 @@ namespace storm {
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 = pctl();

5
src/storm/logic/ToPrefixStringVisitor.cpp
View File

@ -59,6 +59,11 @@ namespace storm {
return result;
}
boost::any ToPrefixStringVisitor::visit(BoundedGloballyFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(BoundedUntilFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}

44
src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
View File

@ -29,7 +29,7 @@ namespace storm {
SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::SparseMarkovAutomatonCslModelChecker(SparseMarkovAutomatonModelType const& model) : SparsePropositionalModelChecker<SparseMarkovAutomatonModelType>(model) {
// Intentionally left empty.
}
template <typename ModelType>
bool SparseMarkovAutomatonCslModelChecker<ModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) {
auto singleObjectiveFragment = storm::logic::csrlstar().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false);
@ -48,7 +48,7 @@ namespace storm {
}
return false;
}
template<typename SparseMarkovAutomatonModelType>
bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
bool requiresSingleInitialState = false;
@ -58,7 +58,7 @@ namespace storm {
return false;
}
}
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
@ -85,18 +85,18 @@ namespace storm {
std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), std::make_pair(lowerBound, upperBound));
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(result)));
}
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::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();
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeNextProbabilities(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeNextProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
}
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeGloballyProbabilities(Environment const& env, CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) {
storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula();
@ -110,7 +110,7 @@ namespace storm {
}
return result;
}
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
@ -131,14 +131,14 @@ namespace storm {
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeHOAPathProbabilities(Environment const& env, CheckTask<storm::logic::HOAPathFormula, ValueType> const& checkTask) {
storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula();
storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(this->getModel().getTransitionMatrix());
storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(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);
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
if (checkTask.isProduceSchedulersSet()) {
result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(helper.extractScheduler(this->getModel())));
@ -146,7 +146,7 @@ namespace storm {
return result;
}
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeLTLProbabilities(Environment const& env, CheckTask<storm::logic::PathFormula, ValueType> const& checkTask) {
storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
@ -155,7 +155,7 @@ namespace storm {
storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(this->getModel().getTransitionMatrix());
storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(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);
@ -166,7 +166,7 @@ namespace storm {
return result;
}
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
@ -183,7 +183,7 @@ namespace storm {
}
return result;
}
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask<storm::logic::TotalRewardFormula, ValueType> const& checkTask) {
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
@ -197,7 +197,7 @@ namespace storm {
}
return result;
}
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) {
storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
@ -216,13 +216,13 @@ namespace storm {
}
return result;
}
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) {
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute long run average rewards in non-closed Markov automaton.");
auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);
storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper<ValueType> helper(this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRates());
storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel());
auto values = helper.computeLongRunAverageRewards(env, rewardModel.get());
@ -233,7 +233,7 @@ namespace storm {
}
return result;
}
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
@ -249,12 +249,12 @@ namespace storm {
}
return result;
}
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::checkMultiObjectiveFormula(Environment const& env, CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) {
return multiobjective::performMultiObjectiveModelChecking(env, this->getModel(), checkTask.getFormula());
}
template class SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<double>>;
template class SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
}

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

@ -117,41 +117,14 @@ namespace storm {
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 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::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 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)));
}
@ -161,7 +134,7 @@ namespace storm {
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(); };
std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker);

4
src/storm/storage/Scheduler.cpp
View File

@ -323,9 +323,9 @@ namespace storm {
}
}
if (numOfSkippedStatesWithUniqueChoice > 0) {
stateString << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl;
out << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl;
}
stateString << "___________________________________________________________________" << std::endl;
out << "___________________________________________________________________" << std::endl;
}

3
src/storm/storage/Scheduler.h
View File

@ -143,8 +143,9 @@ namespace storm {
* Prints the scheduler in json format to the given output stream.
*/
void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false, bool skipDontCareStates = false) const;
void setPrintUndefinedChoices(bool value);
private:
protected:
boost::optional<storm::storage::MemoryStructure> memoryStructure;
std::vector<std::vector<SchedulerChoice<ValueType>>> schedulerChoices;

Write Preview
Loading…
Cancel
Save