Browse Source

updated canHandle

Conflicts:
	src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
tempestpy_adaptions
hannah 3 years ago
committed by Stefan Pranger
parent
commit
1332e39b8c
  1. 2
      src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  2. 2
      src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

2
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp

@ -40,7 +40,7 @@ namespace storm {
template <typename ModelType>
bool SparseCtmcCslModelChecker<ModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
auto fragment = storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setTotalRewardFormulasAllowed(true).setRewardAccumulationAllowed(true);
auto fragment = storm::logic::csrlstar().setGloballyFormulasAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setTotalRewardFormulasAllowed(true).setRewardAccumulationAllowed(true);
if (!storm::NumberTraits<ValueType>::SupportsExponential) {
fragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false);
}

2
src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@ -40,7 +40,7 @@ namespace storm {
template <typename ModelType>
bool SparseMarkovAutomatonCslModelChecker<ModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) {
auto singleObjectiveFragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false).setNestedPathFormulasAllowed(true); //TODO (hannah) correct?
auto singleObjectiveFragment = storm::logic::csl().setGloballyFormulasAllowed(true).setNextFormulasAllowed(true).setNestedPathFormulasAllowed(true).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false);
auto multiObjectiveFragment = storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setRewardAccumulationAllowed(true);
if (!storm::NumberTraits<ValueType>::SupportsExponential) {
singleObjectiveFragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false);

Loading…
Cancel
Save