Browse Source

Merge branch 'master' into pomdp_datastructures

tempestpy_adaptions
Sebastian Junges 6 years ago
parent
commit
2e7569eea4
  1. 64
      .travis.yml
  2. 5
      src/storm/adapters/Z3ExpressionAdapter.cpp
  3. 2
      src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp
  4. 2
      src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  5. 21
      src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
  6. 6
      src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
  7. 2
      src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp
  8. 2
      src/storm/storage/expressions/ToRationalNumberVisitor.cpp
  9. 6
      src/storm/storage/prism/ToJaniConverter.cpp
  10. 6
      travis/generate_travis.py

64
.travis.yml

@ -47,6 +47,8 @@ jobs:
env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build_carl.sh - travis/build_carl.sh
after_success: after_success:
@ -60,6 +62,8 @@ jobs:
env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build_carl.sh - travis/build_carl.sh
after_success: after_success:
@ -79,6 +83,8 @@ jobs:
install: install:
- rm -rf build - rm -rf build
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build1 - travis/build.sh Build1
before_cache: before_cache:
@ -93,6 +99,8 @@ jobs:
install: install:
- rm -rf build - rm -rf build
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build1 - travis/build.sh Build1
before_cache: before_cache:
@ -107,6 +115,8 @@ jobs:
install: install:
- rm -rf build - rm -rf build
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build1 - travis/build.sh Build1
before_cache: before_cache:
@ -121,6 +131,8 @@ jobs:
install: install:
- rm -rf build - rm -rf build
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build1 - travis/build.sh Build1
before_cache: before_cache:
@ -135,6 +147,8 @@ jobs:
install: install:
- rm -rf build - rm -rf build
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build1 - travis/build.sh Build1
before_cache: before_cache:
@ -149,6 +163,8 @@ jobs:
install: install:
- rm -rf build - rm -rf build
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build1 - travis/build.sh Build1
before_cache: before_cache:
@ -167,6 +183,8 @@ jobs:
env: CONFIG=DefaultDebug LINUX=debian-9 COMPILER=gcc env: CONFIG=DefaultDebug LINUX=debian-9 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build2 - travis/build.sh Build2
before_cache: before_cache:
@ -180,6 +198,8 @@ jobs:
env: CONFIG=DefaultRelease LINUX=debian-9 COMPILER=gcc env: CONFIG=DefaultRelease LINUX=debian-9 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build2 - travis/build.sh Build2
before_cache: before_cache:
@ -193,6 +213,8 @@ jobs:
env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build2 - travis/build.sh Build2
before_cache: before_cache:
@ -206,6 +228,8 @@ jobs:
env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build2 - travis/build.sh Build2
before_cache: before_cache:
@ -219,6 +243,8 @@ jobs:
env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build2 - travis/build.sh Build2
before_cache: before_cache:
@ -232,6 +258,8 @@ jobs:
env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build2 - travis/build.sh Build2
before_cache: before_cache:
@ -250,6 +278,8 @@ jobs:
env: CONFIG=DefaultDebug LINUX=debian-9 COMPILER=gcc env: CONFIG=DefaultDebug LINUX=debian-9 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build3 - travis/build.sh Build3
before_cache: before_cache:
@ -263,6 +293,8 @@ jobs:
env: CONFIG=DefaultRelease LINUX=debian-9 COMPILER=gcc env: CONFIG=DefaultRelease LINUX=debian-9 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build3 - travis/build.sh Build3
before_cache: before_cache:
@ -276,6 +308,8 @@ jobs:
env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build3 - travis/build.sh Build3
before_cache: before_cache:
@ -289,6 +323,8 @@ jobs:
env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build3 - travis/build.sh Build3
before_cache: before_cache:
@ -302,6 +338,8 @@ jobs:
env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build3 - travis/build.sh Build3
before_cache: before_cache:
@ -315,6 +353,8 @@ jobs:
env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh Build3 - travis/build.sh Build3
before_cache: before_cache:
@ -333,6 +373,8 @@ jobs:
env: CONFIG=DefaultDebug LINUX=debian-9 COMPILER=gcc env: CONFIG=DefaultDebug LINUX=debian-9 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh BuildLast - travis/build.sh BuildLast
before_cache: before_cache:
@ -346,6 +388,8 @@ jobs:
env: CONFIG=DefaultRelease LINUX=debian-9 COMPILER=gcc env: CONFIG=DefaultRelease LINUX=debian-9 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh BuildLast - travis/build.sh BuildLast
before_cache: before_cache:
@ -359,6 +403,8 @@ jobs:
env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh BuildLast - travis/build.sh BuildLast
before_cache: before_cache:
@ -372,6 +418,8 @@ jobs:
env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh BuildLast - travis/build.sh BuildLast
before_cache: before_cache:
@ -385,6 +433,8 @@ jobs:
env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh BuildLast - travis/build.sh BuildLast
before_cache: before_cache:
@ -398,6 +448,8 @@ jobs:
env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh BuildLast - travis/build.sh BuildLast
before_cache: before_cache:
@ -416,6 +468,8 @@ jobs:
env: CONFIG=DefaultDebug LINUX=debian-9 COMPILER=gcc env: CONFIG=DefaultDebug LINUX=debian-9 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh TestAll - travis/build.sh TestAll
before_cache: before_cache:
@ -429,6 +483,8 @@ jobs:
env: CONFIG=DefaultRelease LINUX=debian-9 COMPILER=gcc env: CONFIG=DefaultRelease LINUX=debian-9 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh TestAll - travis/build.sh TestAll
before_cache: before_cache:
@ -442,6 +498,8 @@ jobs:
env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultDebugTravis LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh TestAll - travis/build.sh TestAll
before_cache: before_cache:
@ -459,6 +517,8 @@ jobs:
env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultReleaseTravis LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh TestAll - travis/build.sh TestAll
before_cache: before_cache:
@ -476,6 +536,8 @@ jobs:
env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultDebug LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh TestAll - travis/build.sh TestAll
before_cache: before_cache:
@ -489,6 +551,8 @@ jobs:
env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc env: CONFIG=DefaultRelease LINUX=ubuntu-18.04 COMPILER=gcc
install: install:
- travis/install_linux.sh - travis/install_linux.sh
before_script:
- python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode
script: script:
- travis/build.sh TestAll - travis/build.sh TestAll
before_cache: before_cache:

5
src/storm/adapters/Z3ExpressionAdapter.cpp

@ -227,6 +227,9 @@ namespace storm {
result = leftResult * rightResult; result = leftResult * rightResult;
break; break;
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide: case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide:
if (leftResult.is_int() && rightResult.is_int()) {
leftResult = z3::expr(context, Z3_mk_int2real(context, leftResult));
}
result = leftResult / rightResult; result = leftResult / rightResult;
break; break;
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Min: case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Min:
@ -363,7 +366,7 @@ namespace storm {
case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Ceil:{ case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Ceil:{
storm::expressions::Variable freshAuxiliaryVariable = manager.declareFreshVariable(manager.getIntegerType(), true); storm::expressions::Variable freshAuxiliaryVariable = manager.declareFreshVariable(manager.getIntegerType(), true);
z3::expr ceilVariable = context.int_const(freshAuxiliaryVariable.getName().c_str()); z3::expr ceilVariable = context.int_const(freshAuxiliaryVariable.getName().c_str());
additionalAssertions.push_back(z3::expr(context, Z3_mk_int2real(context, ceilVariable)) - 1 <= result && result < z3::expr(context, Z3_mk_int2real(context, ceilVariable)));
additionalAssertions.push_back(z3::expr(context, Z3_mk_int2real(context, ceilVariable)) - 1 < result && result <= z3::expr(context, Z3_mk_int2real(context, ceilVariable)));
result = ceilVariable; result = ceilVariable;
break; break;
} }

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

@ -37,7 +37,7 @@ namespace storm {
template<typename CValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type> template<typename CValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
bool HybridCtmcCslModelChecker<ModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const { bool HybridCtmcCslModelChecker<ModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true));
return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false));
} }
template<typename ModelType> template<typename ModelType>

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

@ -44,7 +44,7 @@ namespace storm {
template<typename CValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type> template<typename CValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const { bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true));
return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false));
} }
template <typename SparseCtmcModelType> template <typename SparseCtmcModelType>

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

@ -28,6 +28,12 @@ namespace storm {
template<typename SparseMarkovAutomatonModelType> template<typename SparseMarkovAutomatonModelType>
bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const { bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
return SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandleImplementation<ValueType>(checkTask);
}
template <typename SparseMarkovAutomatonModelType>
template<typename CValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::Formula const& formula = checkTask.getFormula();
if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true))) { if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true))) {
return true; return true;
@ -40,6 +46,21 @@ namespace storm {
} }
} }
template <typename SparseMarkovAutomatonModelType>
template<typename CValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula();
if(formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false))) {
return true;
} else {
// Check whether we consider a multi-objective formula
// For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude multiple initial states.
if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
if (!checkTask.isOnlyInitialStatesRelevantSet()) return false;
return formula.isInFragment(storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false));
}
}
template<typename SparseMarkovAutomatonModelType> template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();

6
src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h

@ -29,7 +29,13 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override; virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override; virtual std::unique_ptr<CheckResult> computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(Environment const& env, CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) override; virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(Environment const& env, CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) override;
private:
template<typename CValueType = ValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0>
bool canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const;
template<typename CValueType = ValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0>
bool canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const;
}; };
} }
} }

2
src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp

@ -111,7 +111,7 @@ namespace storm {
case OperatorType::Divide: newValue = firstOperandEvaluation / secondOperandEvaluation; break; case OperatorType::Divide: newValue = firstOperandEvaluation / secondOperandEvaluation; break;
case OperatorType::Power: { case OperatorType::Power: {
if (carl::isInteger(secondOperandEvaluation)) { if (carl::isInteger(secondOperandEvaluation)) {
std::size_t exponent = carl::toInt<carl::uint>(secondOperandEvaluation);
std::size_t exponent = carl::toInt<carl::sint>(secondOperandEvaluation);
newValue = carl::pow(firstOperandEvaluation, exponent); newValue = carl::pow(firstOperandEvaluation, exponent);
} }
break; break;

2
src/storm/storage/expressions/ToRationalNumberVisitor.cpp

@ -76,7 +76,7 @@ namespace storm {
break; break;
case BinaryNumericalFunctionExpression::OperatorType::Power: case BinaryNumericalFunctionExpression::OperatorType::Power:
STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalNumber), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer."); STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalNumber), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer.");
exponentAsInteger = storm::utility::convertNumber<carl::uint>(secondOperandAsRationalNumber);
exponentAsInteger = storm::utility::convertNumber<carl::sint>(secondOperandAsRationalNumber);
result = storm::utility::pow(firstOperandAsRationalNumber, exponentAsInteger); result = storm::utility::pow(firstOperandAsRationalNumber, exponentAsInteger);
return result; return result;
break; break;

6
src/storm/storage/prism/ToJaniConverter.cpp

@ -251,6 +251,7 @@ namespace storm {
// Go through the reward models and construct assignments to the transient variables that are to be added to // Go through the reward models and construct assignments to the transient variables that are to be added to
// edges and transient assignments that are added to the locations. // edges and transient assignments that are added to the locations.
std::map<uint_fast64_t, std::vector<storm::jani::Assignment>> transientEdgeAssignments; std::map<uint_fast64_t, std::vector<storm::jani::Assignment>> transientEdgeAssignments;
bool hasStateRewards = false;
for (auto const& rewardModel : program.getRewardModels()) { for (auto const& rewardModel : program.getRewardModels()) {
std::string finalRewardModelName; std::string finalRewardModelName;
if (rewardModel.getName().empty()) { if (rewardModel.getName().empty()) {
@ -270,6 +271,7 @@ namespace storm {
storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(finalRewardModelName, newExpressionVariable, manager->rational(0.0), true)); storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(finalRewardModelName, newExpressionVariable, manager->rational(0.0), true));
if (rewardModel.hasStateRewards()) { if (rewardModel.hasStateRewards()) {
hasStateRewards = true;
storm::expressions::Expression transientLocationExpression; storm::expressions::Expression transientLocationExpression;
for (auto const& stateReward : rewardModel.getStateRewards()) { for (auto const& stateReward : rewardModel.getStateRewards()) {
storm::expressions::Expression rewardTerm = stateReward.getStatePredicateExpression().isTrue() ? stateReward.getRewardValueExpression() : storm::expressions::ite(stateReward.getStatePredicateExpression(), stateReward.getRewardValueExpression(), manager->rational(0)); storm::expressions::Expression rewardTerm = stateReward.getStatePredicateExpression().isTrue() ? stateReward.getRewardValueExpression() : storm::expressions::ite(stateReward.getStatePredicateExpression(), stateReward.getRewardValueExpression(), manager->rational(0));
@ -321,6 +323,10 @@ namespace storm {
STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Transition reward translation currently not implemented."); STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Transition reward translation currently not implemented.");
} }
STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition."); STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition.");
// if there are state rewards and the model is a discrete time model, we add the corresponding model feature
if (janiModel.isDiscreteTimeModel() && hasStateRewards) {
janiModel.getModelFeatures().add(storm::jani::ModelFeature::StateExitRewards);
}
// Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the // Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the
// previously built mapping to make variables global that are read by more than one module. // previously built mapping to make variables global that are read by more than one module.

6
travis/generate_travis.py

@ -91,6 +91,8 @@ if __name__ == "__main__":
buildConfig += " env: CONFIG={} LINUX={} COMPILER={}\n".format(build_type, linux, compiler) buildConfig += " env: CONFIG={} LINUX={} COMPILER={}\n".format(build_type, linux, compiler)
buildConfig += " install:\n" buildConfig += " install:\n"
buildConfig += " - travis/install_linux.sh\n" buildConfig += " - travis/install_linux.sh\n"
buildConfig += " before_script:\n"
buildConfig += ' - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode\n'
buildConfig += " script:\n" buildConfig += " script:\n"
buildConfig += " - travis/build_carl.sh\n" buildConfig += " - travis/build_carl.sh\n"
# Upload to DockerHub # Upload to DockerHub
@ -129,6 +131,8 @@ if __name__ == "__main__":
if stage[1] == "Build1": if stage[1] == "Build1":
buildConfig += " - rm -rf build\n" buildConfig += " - rm -rf build\n"
buildConfig += " - travis/install_osx.sh\n" buildConfig += " - travis/install_osx.sh\n"
buildConfig += " before_script:\n"
buildConfig += ' - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode\n'
buildConfig += " script:\n" buildConfig += " script:\n"
buildConfig += " - travis/build.sh {}\n".format(stage[1]) buildConfig += " - travis/build.sh {}\n".format(stage[1])
buildConfig += " after_failure:\n" buildConfig += " after_failure:\n"
@ -154,6 +158,8 @@ if __name__ == "__main__":
if stage[1] == "Build1": if stage[1] == "Build1":
buildConfig += " - rm -rf build\n" buildConfig += " - rm -rf build\n"
buildConfig += " - travis/install_linux.sh\n" buildConfig += " - travis/install_linux.sh\n"
buildConfig += " before_script:\n"
buildConfig += ' - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)" # Workaround for nonblocking mode\n'
buildConfig += " script:\n" buildConfig += " script:\n"
buildConfig += " - travis/build.sh {}\n".format(stage[1]) buildConfig += " - travis/build.sh {}\n".format(stage[1])
buildConfig += " before_cache:\n" buildConfig += " before_cache:\n"
Loading…
Cancel
Save