diff --git a/CHANGELOG.md b/CHANGELOG.md index 7b13f803b..726449028 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,12 +2,25 @@ Changelog ============== This changelog lists only the most important changes. Smaller (bug)fixes as well as non-mature features are not part of the changelog. -The releases of major and minor versions contain an overview of changes since the last major/minor update. +The releases of major and minor versions contain an overview of changes since the last major/minor update. Version 1.0.x ------------------- +### Version 1.0.2 (2017/5) + +- Fix for nested formulae +- JANI: Explicit engine supports custom model compositions. +- Storm now overwrites files if asked to write files to a specific location +- Changes in build process to accommodate for changes in carl. Also, more robust against issues with carl +- Wellformedness constraints on PMCs: + * include constraints from rewards + * are in smtlib2 +- USE_POPCNT removed in favor of FORCE_POPCNT. The popcnt instruction is used if available due to march=native, unless portable is set. + Then, using FORCE_POPCNT enables the use of the SSE 4.2 instruction +- Parametric model checking is now handled in a separated library/executable called storm-pars + ### Version 1.0.1 (2017/4) - Multi-objective model checking support now fully included diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 4148df10a..3a7a44240 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -199,6 +199,9 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake) ############################################################# set(STORM_HAVE_CARL OFF) +set(CARL_MINYEAR 17) +set(CARL_MINMONTH 06) +set(CARL_MINPATCH 0) if(USE_CARL) if (NOT STORM_FORCE_SHIPPED_CARL) find_package(carl QUIET) @@ -212,6 +215,18 @@ if(USE_CARL) else() message(SEND_ERROR "File ${carlLOCATION} does not exist, did you build carl?") endif() + if(${carl_MINORYEARVERSION} LESS ${CARL_MINYEAR}) + message(SEND_ERROR "Carl outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}") + elseif(${carl_MINORYEARVERSION} EQUAL ${CARL_MINYEAR}) + if(${carl_MINORMONTHVERSION} LESS ${CARL_MINMONTH}) + message(SEND_ERROR "Carl outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}") + elseif(${carl_MINORMONTHVERSION} EQUAL ${CARL_MINMONTH}) + if(${carl_MAINTENANCEVERSION} LESS ${CARL_MINPATCH}) + message(SEND_ERROR "Carl outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}") + endif() + endif() + endif() + set(STORM_SHIPPED_CARL OFF) set(STORM_HAVE_CARL ON) message(STATUS "Storm - Use system version of carl.") diff --git a/resources/3rdparty/cudd-3.0.0/Makefile.in b/resources/3rdparty/cudd-3.0.0/Makefile.in index 75846bc4c..7bfa478ae 100644 --- a/resources/3rdparty/cudd-3.0.0/Makefile.in +++ b/resources/3rdparty/cudd-3.0.0/Makefile.in @@ -1,7 +1,7 @@ -# Makefile.in generated by automake 1.15 from Makefile.am. +# Makefile.in generated by automake 1.15.1 from Makefile.am. # @configure_input@ -# Copyright (C) 1994-2014 Free Software Foundation, Inc. +# Copyright (C) 1994-2017 Free Software Foundation, Inc. # This Makefile.in is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -2850,7 +2850,7 @@ distdir: $(DISTFILES) ! -type d ! -perm -444 -exec $(install_sh) -c -m a+r {} {} \; \ || chmod -R a+r "$(distdir)" dist-gzip: distdir - tardir=$(distdir) && $(am__tar) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).tar.gz + tardir=$(distdir) && $(am__tar) | eval GZIP= gzip $(GZIP_ENV) -c >$(distdir).tar.gz $(am__post_remove_distdir) dist-bzip2: distdir @@ -2876,7 +2876,7 @@ dist-shar: distdir @echo WARNING: "Support for shar distribution archives is" \ "deprecated." >&2 @echo WARNING: "It will be removed altogether in Automake 2.0" >&2 - shar $(distdir) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).shar.gz + shar $(distdir) | eval GZIP= gzip $(GZIP_ENV) -c >$(distdir).shar.gz $(am__post_remove_distdir) dist-zip: distdir @@ -2894,7 +2894,7 @@ dist dist-all: distcheck: dist case '$(DIST_ARCHIVES)' in \ *.tar.gz*) \ - GZIP=$(GZIP_ENV) gzip -dc $(distdir).tar.gz | $(am__untar) ;;\ + eval GZIP= gzip $(GZIP_ENV) -dc $(distdir).tar.gz | $(am__untar) ;;\ *.tar.bz2*) \ bzip2 -dc $(distdir).tar.bz2 | $(am__untar) ;;\ *.tar.lz*) \ @@ -2904,7 +2904,7 @@ distcheck: dist *.tar.Z*) \ uncompress -c $(distdir).tar.Z | $(am__untar) ;;\ *.shar.gz*) \ - GZIP=$(GZIP_ENV) gzip -dc $(distdir).shar.gz | unshar ;;\ + eval GZIP= gzip $(GZIP_ENV) -dc $(distdir).shar.gz | unshar ;;\ *.zip*) \ unzip $(distdir).zip ;;\ esac diff --git a/resources/3rdparty/cudd-3.0.0/aclocal.m4 b/resources/3rdparty/cudd-3.0.0/aclocal.m4 index 0de6688a7..b1d04ee86 100644 --- a/resources/3rdparty/cudd-3.0.0/aclocal.m4 +++ b/resources/3rdparty/cudd-3.0.0/aclocal.m4 @@ -1,6 +1,6 @@ -# generated automatically by aclocal 1.15 -*- Autoconf -*- +# generated automatically by aclocal 1.15.1 -*- Autoconf -*- -# Copyright (C) 1996-2014 Free Software Foundation, Inc. +# Copyright (C) 1996-2017 Free Software Foundation, Inc. # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -20,7 +20,7 @@ You have another version of autoconf. It may work, but is not guaranteed to. If you have problems, you may need to regenerate the build system entirely. To do so, use the procedure documented by the package, typically 'autoreconf'.])]) -# Copyright (C) 2002-2014 Free Software Foundation, Inc. +# Copyright (C) 2002-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -35,7 +35,7 @@ AC_DEFUN([AM_AUTOMAKE_VERSION], [am__api_version='1.15' dnl Some users find AM_AUTOMAKE_VERSION and mistake it for a way to dnl require some minimum version. Point them to the right macro. -m4_if([$1], [1.15], [], +m4_if([$1], [1.15.1], [], [AC_FATAL([Do not call $0, use AM_INIT_AUTOMAKE([$1]).])])dnl ]) @@ -51,12 +51,12 @@ m4_define([_AM_AUTOCONF_VERSION], []) # Call AM_AUTOMAKE_VERSION and AM_AUTOMAKE_VERSION so they can be traced. # This function is AC_REQUIREd by AM_INIT_AUTOMAKE. AC_DEFUN([AM_SET_CURRENT_AUTOMAKE_VERSION], -[AM_AUTOMAKE_VERSION([1.15])dnl +[AM_AUTOMAKE_VERSION([1.15.1])dnl m4_ifndef([AC_AUTOCONF_VERSION], [m4_copy([m4_PACKAGE_VERSION], [AC_AUTOCONF_VERSION])])dnl _AM_AUTOCONF_VERSION(m4_defn([AC_AUTOCONF_VERSION]))]) -# Copyright (C) 2011-2014 Free Software Foundation, Inc. +# Copyright (C) 2011-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -118,7 +118,7 @@ AC_SUBST([AR])dnl # AM_AUX_DIR_EXPAND -*- Autoconf -*- -# Copyright (C) 2001-2014 Free Software Foundation, Inc. +# Copyright (C) 2001-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -170,7 +170,7 @@ am_aux_dir=`cd "$ac_aux_dir" && pwd` # AM_COND_IF -*- Autoconf -*- -# Copyright (C) 2008-2014 Free Software Foundation, Inc. +# Copyright (C) 2008-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -207,7 +207,7 @@ fi[]dnl # AM_CONDITIONAL -*- Autoconf -*- -# Copyright (C) 1997-2014 Free Software Foundation, Inc. +# Copyright (C) 1997-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -238,7 +238,7 @@ AC_CONFIG_COMMANDS_PRE( Usually this means the macro was only invoked conditionally.]]) fi])]) -# Copyright (C) 1999-2014 Free Software Foundation, Inc. +# Copyright (C) 1999-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -429,7 +429,7 @@ _AM_SUBST_NOTMAKE([am__nodep])dnl # Generate code to set up dependency tracking. -*- Autoconf -*- -# Copyright (C) 1999-2014 Free Software Foundation, Inc. +# Copyright (C) 1999-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -505,7 +505,7 @@ AC_DEFUN([AM_OUTPUT_DEPENDENCY_COMMANDS], # Do all the work for Automake. -*- Autoconf -*- -# Copyright (C) 1996-2014 Free Software Foundation, Inc. +# Copyright (C) 1996-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -702,7 +702,7 @@ for _am_header in $config_headers :; do done echo "timestamp for $_am_arg" >`AS_DIRNAME(["$_am_arg"])`/stamp-h[]$_am_stamp_count]) -# Copyright (C) 2001-2014 Free Software Foundation, Inc. +# Copyright (C) 2001-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -723,7 +723,7 @@ if test x"${install_sh+set}" != xset; then fi AC_SUBST([install_sh])]) -# Copyright (C) 2003-2014 Free Software Foundation, Inc. +# Copyright (C) 2003-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -744,7 +744,7 @@ AC_SUBST([am__leading_dot])]) # Check to see how 'make' treats includes. -*- Autoconf -*- -# Copyright (C) 2001-2014 Free Software Foundation, Inc. +# Copyright (C) 2001-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -794,7 +794,7 @@ rm -f confinc confmf # Fake the existence of programs that GNU maintainers use. -*- Autoconf -*- -# Copyright (C) 1997-2014 Free Software Foundation, Inc. +# Copyright (C) 1997-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -833,7 +833,7 @@ fi # Helper functions for option handling. -*- Autoconf -*- -# Copyright (C) 2001-2014 Free Software Foundation, Inc. +# Copyright (C) 2001-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -862,7 +862,7 @@ AC_DEFUN([_AM_SET_OPTIONS], AC_DEFUN([_AM_IF_OPTION], [m4_ifset(_AM_MANGLE_OPTION([$1]), [$2], [$3])]) -# Copyright (C) 1999-2014 Free Software Foundation, Inc. +# Copyright (C) 1999-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -909,7 +909,7 @@ AC_LANG_POP([C])]) # For backward compatibility. AC_DEFUN_ONCE([AM_PROG_CC_C_O], [AC_REQUIRE([AC_PROG_CC])]) -# Copyright (C) 2001-2014 Free Software Foundation, Inc. +# Copyright (C) 2001-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -928,7 +928,7 @@ AC_DEFUN([AM_RUN_LOG], # Check to make sure that the build environment is sane. -*- Autoconf -*- -# Copyright (C) 1996-2014 Free Software Foundation, Inc. +# Copyright (C) 1996-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -1009,7 +1009,7 @@ AC_CONFIG_COMMANDS_PRE( rm -f conftest.file ]) -# Copyright (C) 2009-2014 Free Software Foundation, Inc. +# Copyright (C) 2009-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -1069,7 +1069,7 @@ AC_SUBST([AM_BACKSLASH])dnl _AM_SUBST_NOTMAKE([AM_BACKSLASH])dnl ]) -# Copyright (C) 2001-2014 Free Software Foundation, Inc. +# Copyright (C) 2001-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -1097,7 +1097,7 @@ fi INSTALL_STRIP_PROGRAM="\$(install_sh) -c -s" AC_SUBST([INSTALL_STRIP_PROGRAM])]) -# Copyright (C) 2006-2014 Free Software Foundation, Inc. +# Copyright (C) 2006-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, @@ -1116,7 +1116,7 @@ AC_DEFUN([AM_SUBST_NOTMAKE], [_AM_SUBST_NOTMAKE($@)]) # Check how to create a tarball. -*- Autoconf -*- -# Copyright (C) 2004-2014 Free Software Foundation, Inc. +# Copyright (C) 2004-2017 Free Software Foundation, Inc. # # This file is free software; the Free Software Foundation # gives unlimited permission to copy and/or distribute it, diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp index b042227fd..ae9a91bb9 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp @@ -201,8 +201,8 @@ storm_rational_number_ptr storm_rational_number_pow(storm_rational_number_ptr a, storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; - - uint64_t exponentAsInteger = carl::toInt(srn_b); + + carl::uint exponentAsInteger = carl::toInt(srn_b); storm::RationalNumber* result_srn = new storm::RationalNumber(carl::pow(srn_a, exponentAsInteger)); return (storm_rational_number_ptr)result_srn; } @@ -515,7 +515,7 @@ storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; - uint64_t exponentAsInteger = carl::toInt(srf_b.nominatorAsNumber()); + carl::uint exponentAsInteger = carl::toInt(srf_b.nominatorAsNumber()); storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger)); return (storm_rational_function_ptr)result_srf; } diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 5bb379962..b2dc40006 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -185,7 +185,7 @@ int main(const int argc, const char** argv) { storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); auto evtlFormula = std::make_shared(targetExpression); - auto tbFormula = std::make_shared(std::make_shared(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundType::Time); + auto tbFormula = std::make_shared(std::make_shared(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)); auto tbUntil = std::make_shared(tbFormula); auto evFormula = std::make_shared(evtlFormula, storm::logic::FormulaContext::Time); diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt index 3951551ae..9ec70aed2 100644 --- a/src/storm-dft/CMakeLists.txt +++ b/src/storm-dft/CMakeLists.txt @@ -8,7 +8,7 @@ file(GLOB_RECURSE STORM_DFT_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.cpp) file(GLOB_RECURSE STORM_DFT_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h) -# Create storm-pgcl. +# Create storm-dft. add_library(storm-dft SHARED ${STORM_DFT_SOURCES} ${STORM_DFT_HEADERS}) # Remove define symbol for shared libstorm. diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h index 043f461b0..a8cc6bbe2 100644 --- a/src/storm-pars/api/region.h +++ b/src/storm-pars/api/region.h @@ -78,7 +78,7 @@ namespace storm { } template - std::unique_ptr> initializeParameterLiftingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::shared_ptr> initializeParameterLiftingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually..."); @@ -93,22 +93,22 @@ namespace storm { } // Obtain the region model checker - std::unique_ptr> result; + std::shared_ptr> checker; if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) { - result = std::make_unique, ConstantType>>(); + checker = std::make_shared, ConstantType>>(); } else if (consideredModel->isOfType(storm::models::ModelType::Mdp)) { - result = std::make_unique, ConstantType>>(); + checker = std::make_shared, ConstantType>>(); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); } - result->specify(consideredModel, task); + checker->specify(consideredModel, task); - return result; + return checker; } template - std::unique_ptr> initializeValidatingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::shared_ptr> initializeValidatingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually..."); @@ -123,22 +123,22 @@ namespace storm { } // Obtain the region model checker - std::unique_ptr> result; + std::shared_ptr> checker; if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) { - result = std::make_unique, ImpreciseType, PreciseType>>(); + checker = std::make_shared, ImpreciseType, PreciseType>>(); } else if (consideredModel->isOfType(storm::models::ModelType::Mdp)) { - result = std::make_unique, ImpreciseType, PreciseType>>(); + checker = std::make_shared, ImpreciseType, PreciseType>>(); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); } - result->specify(consideredModel, task); + checker->specify(consideredModel, task); - return result; + return checker; } template - std::unique_ptr> initializeRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::modelchecker::RegionCheckEngine engine) { + std::shared_ptr> initializeRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::modelchecker::RegionCheckEngine engine) { switch (engine) { case storm::modelchecker::RegionCheckEngine::ParameterLifting: return initializeParameterLiftingRegionModelChecker(model, task); diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 5f32c8386..155b13dec 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -75,7 +75,7 @@ namespace storm { // get the step bound STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported."); STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound."); - STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); + STORM_LOG_THROW(checkTask.getFormula().getTimeBoundReference().isStepBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt(); STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive."); if (checkTask.getFormula().isUpperBoundStrict()) { diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index 6169d22bf..65e16d628 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp @@ -76,7 +76,7 @@ namespace storm { // get the step bound STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported."); STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound."); - STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); + STORM_LOG_THROW(checkTask.getFormula().getTimeBoundReference().isStepBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt(); STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive."); if (checkTask.getFormula().isUpperBoundStrict()) { diff --git a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp index ed05131e4..826e141ff 100644 --- a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp @@ -111,7 +111,7 @@ namespace storm { // obtain the simplified formula for the simplified model auto labelFormula = std::make_shared (targetLabel); - auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundType::Steps); + auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)); this->simplifiedFormula = std::make_shared(boundedUntilFormula, formula.getOperatorInformation()); return true; diff --git a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp index 1862936f4..97f93cf03 100644 --- a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp @@ -135,7 +135,7 @@ namespace storm { // obtain the simplified formula for the simplified model auto labelFormula = std::make_shared (targetLabel); - auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundType::Steps); + auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)); this->simplifiedFormula = std::make_shared(boundedUntilFormula, formula.getOperatorInformation()); return true; diff --git a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp index 343fc06e3..1679bdcca 100644 --- a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp @@ -78,21 +78,21 @@ namespace storm { template bool SparseParametricModelSimplifier::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { // If this method was not overriden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } template bool SparseParametricModelSimplifier::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) { // If this method was not overriden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } template bool SparseParametricModelSimplifier::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) { // If this method was not overriden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 4f47f15a7..812429dec 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -50,25 +50,35 @@ namespace storm { for (auto const& transition : dtmc.getRows(state)) { sum += transition.getValue(); if (!storm::utility::isConstant(transition.getValue())) { + // Assert: 0 <= transition <= 1 if (transition.getValue().denominator().isConstant()) { - if (transition.getValue().denominatorAsNumber() > 0) { + if (transition.getValue().denominator().constantPart() > 0) { + // Assert: nom <= denom wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::LEQ); + // Assert: nom >= 0 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ); - } else if (transition.getValue().denominatorAsNumber() < 0) { + } else if (transition.getValue().denominator().constantPart() < 0) { + // Assert nom >= denom wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::GEQ); + // Assert: nom <= 0 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ); } else { - assert(false); // Should fail before. + STORM_LOG_ASSERT(false, "Denominator must not equal 0."); } } else { + // Assert: denom != 0 wellformedConstraintSet.emplace(transition.getValue().denominator().polynomial(), storm::CompareRelation::NEQ); - wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GREATER), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ)); + // Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0 + wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(transition.getValue().denominator().polynomial(), storm::CompareRelation::GREATER), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ)); + // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0 } + // Assert: transition > 0 graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::NEQ); } } STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1."); if(!storm::utility::isConstant(sum)) { + // Assert: sum == 1 wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomial(), storm::CompareRelation::EQ); } diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index 87b95a78c..c6043fd5a 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -35,7 +35,7 @@ namespace storm { void wellformedRequiresNonNegativeEntries(std::vector const&); public: /*! - * Constructs the a constraint collector for the given DTMC. The constraints are built and ready for + * Constructs a constraint collector for the given DTMC. The constraints are built and ready for * retrieval after the construction. * * @param dtmc The DTMC for which to create the constraints. @@ -47,14 +47,14 @@ namespace storm { * * @return The set of wellformed-ness constraints. */ - std::unordered_set::val> const& getWellformedConstraints() const; + std::unordered_set::val> const& getWellformedConstraints() const; /*! * Returns the set of graph-preserving constraints. * * @return The set of graph-preserving constraints. */ - std::unordered_set::val> const& getGraphPreservingConstraints() const; + std::unordered_set::val> const& getGraphPreservingConstraints() const; /*! * Constructs the constraints for the given DTMC. diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index b28f068c3..3284b353c 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -352,15 +352,27 @@ namespace storm { return input; } + std::vector> createFormulasToRespect(std::vector const& properties) { + std::vector> result = storm::api::extractFormulasFromProperties(properties); + + for (auto const& property : properties) { + if (!property.getFilter().getStatesFormula()->isInitialFormula()) { + result.push_back(property.getFilter().getStatesFormula()); + } + } + + return result; + } + template std::shared_ptr buildModelDd(SymbolicInput const& input) { - return storm::api::buildSymbolicModel(input.model.get(), storm::api::extractFormulasFromProperties(input.properties)); + return storm::api::buildSymbolicModel(input.model.get(), createFormulasToRespect(input.properties)); } template std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { auto counterexampleGeneratorSettings = storm::settings::getModule(); - return storm::api::buildSparseModel(input.model.get(), storm::api::extractFormulasFromProperties(input.properties), ioSettings.isBuildChoiceLabelsSet(), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); + return storm::api::buildSparseModel(input.model.get(), createFormulasToRespect(input.properties), ioSettings.isBuildChoiceLabelsSet(), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); } template @@ -416,7 +428,7 @@ namespace storm { } STORM_LOG_INFO("Performing bisimulation minimization..."); - return storm::api::performBisimulationMinimization(model, storm::api::extractFormulasFromProperties(input.properties), bisimType); + return storm::api::performBisimulationMinimization(model, createFormulasToRespect(input.properties), bisimType); } template @@ -602,9 +614,11 @@ namespace storm { } template - void printInitialStatesResult(std::unique_ptr const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) { + void printResult(std::unique_ptr const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) { if (result) { - STORM_PRINT_AND_LOG("Result (initial states): "); + std::stringstream ss; + ss << "'" << *property.getFilter().getStatesFormula() << "'"; + STORM_PRINT_AND_LOG("Result (for " << (property.getFilter().getStatesFormula()->isInitialFormula() ? "initial" : ss.str()) << " states): "); printFilteredResult(result, property.getFilter().getFilterType()); if (watch) { STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl); @@ -621,21 +635,22 @@ namespace storm { }; template - void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula)> const& verificationCallback, std::function const&)> const& postprocessingCallback = PostprocessingIdentity()) { + void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula, std::shared_ptr const& states)> const& verificationCallback, std::function const&)> const& postprocessingCallback = PostprocessingIdentity()) { for (auto const& property : properties) { printModelCheckingProperty(property); storm::utility::Stopwatch watch(true); - std::unique_ptr result = verificationCallback(property.getRawFormula()); + std::unique_ptr result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula()); watch.stop(); - printInitialStatesResult(result, property, &watch); postprocessingCallback(result); + printResult(result, property, &watch); } } template void verifyWithAbstractionRefinementEngine(SymbolicInput const& input) { STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); - verifyProperties(input.properties, [&input] (std::shared_ptr const& formula) { + verifyProperties(input.properties, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { + STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states."); return storm::api::verifyWithAbstractionRefinementEngine(input.model.get(), storm::api::createTask(formula, true)); }); } @@ -644,7 +659,8 @@ namespace storm { void verifyWithExplorationEngine(SymbolicInput const& input) { STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Exploration does not support other data-types than floating points."); - verifyProperties(input.properties, [&input] (std::shared_ptr const& formula) { + verifyProperties(input.properties, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { + STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states."); return storm::api::verifyWithExplorationEngine(input.model.get(), storm::api::createTask(formula, true)); }); } @@ -653,29 +669,60 @@ namespace storm { void verifyWithSparseEngine(std::shared_ptr const& model, SymbolicInput const& input) { auto sparseModel = model->as>(); verifyProperties(input.properties, - [&sparseModel] (std::shared_ptr const& formula) { - std::unique_ptr result = storm::api::verifyWithSparseEngine(sparseModel, storm::api::createTask(formula, true)); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates())); + [&sparseModel] (std::shared_ptr const& formula, std::shared_ptr const& states) { + bool filterForInitialStates = states->isInitialFormula(); + auto task = storm::api::createTask(formula, filterForInitialStates); + std::unique_ptr result = storm::api::verifyWithSparseEngine(sparseModel, task); + + std::unique_ptr filter; + if (filterForInitialStates) { + filter = std::make_unique(sparseModel->getInitialStates()); + } else { + filter = storm::api::verifyWithSparseEngine(sparseModel, storm::api::createTask(states, false)); + } + result->filter(filter->asQualitativeCheckResult()); return result; }); } template void verifyWithHybridEngine(std::shared_ptr const& model, SymbolicInput const& input) { - verifyProperties(input.properties, [&model] (std::shared_ptr const& formula) { + verifyProperties(input.properties, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { + bool filterForInitialStates = states->isInitialFormula(); + auto task = storm::api::createTask(formula, filterForInitialStates); + auto symbolicModel = model->as>(); - std::unique_ptr result = storm::api::verifyWithHybridEngine(symbolicModel, storm::api::createTask(formula, true)); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(symbolicModel->getReachableStates(), symbolicModel->getInitialStates())); + std::unique_ptr result = storm::api::verifyWithHybridEngine(symbolicModel, task); + + std::unique_ptr filter; + if (filterForInitialStates) { + filter = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()); + } else { + filter = storm::api::verifyWithHybridEngine(symbolicModel, storm::api::createTask(states, false)); + } + + result->filter(filter->asQualitativeCheckResult()); return result; }); } template void verifyWithDdEngine(std::shared_ptr const& model, SymbolicInput const& input) { - verifyProperties(input.properties, [&model] (std::shared_ptr const& formula) { + verifyProperties(input.properties, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { + bool filterForInitialStates = states->isInitialFormula(); + auto task = storm::api::createTask(formula, filterForInitialStates); + auto symbolicModel = model->as>(); std::unique_ptr result = storm::api::verifyWithDdEngine(model->as>(), storm::api::createTask(formula, true)); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(symbolicModel->getReachableStates(), symbolicModel->getInitialStates())); + + std::unique_ptr filter; + if (filterForInitialStates) { + filter = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()); + } else { + filter = storm::api::verifyWithDdEngine(symbolicModel, storm::api::createTask(states, false)); + } + + result->filter(filter->asQualitativeCheckResult()); return result; }); } diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index 10cd7f33e..b954d4720 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -1,5 +1,6 @@ #include "storm/logic/BoundedUntilFormula.h" +#include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -10,7 +11,7 @@ namespace storm { namespace logic { - BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundType const& timeBoundType) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundType(timeBoundType), lowerBound(lowerBound), upperBound(upperBound) { + BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundReference(timeBoundReference), lowerBound(lowerBound), upperBound(upperBound) { STORM_LOG_THROW(lowerBound || upperBound, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound."); } @@ -26,17 +27,11 @@ namespace storm { return visitor.visit(*this, data); } - TimeBoundType const& BoundedUntilFormula::getTimeBoundType() const { - return timeBoundType; + TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference() const { + return timeBoundReference; } - bool BoundedUntilFormula::isStepBounded() const { - return timeBoundType == TimeBoundType::Steps; - } - - bool BoundedUntilFormula::isTimeBounded() const { - return timeBoundType == TimeBoundType::Time; - } + bool BoundedUntilFormula::isLowerBoundStrict() const { return lowerBound.get().isStrict(); @@ -86,6 +81,22 @@ namespace storm { return bound; } + template <> + storm::RationalNumber BoundedUntilFormula::getLowerBound() const { + checkNoVariablesInBound(this->getLowerBound()); + storm::RationalNumber bound = this->getLowerBound().evaluateAsRational(); + STORM_LOG_THROW(bound >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return bound; + } + + template <> + storm::RationalNumber BoundedUntilFormula::getUpperBound() const { + checkNoVariablesInBound(this->getUpperBound()); + storm::RationalNumber bound = this->getLowerBound().evaluateAsRational(); + STORM_LOG_THROW(bound >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return bound; + } + template <> uint64_t BoundedUntilFormula::getLowerBound() const { checkNoVariablesInBound(this->getLowerBound()); diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h index 5dc2a3889..754d94cdf 100644 --- a/src/storm/logic/BoundedUntilFormula.h +++ b/src/storm/logic/BoundedUntilFormula.h @@ -12,7 +12,7 @@ namespace storm { namespace logic { class BoundedUntilFormula : public BinaryPathFormula { public: - BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundType const& timeBoundType = TimeBoundType::Time); + BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference); virtual bool isBoundedUntilFormula() const override; @@ -20,9 +20,8 @@ namespace storm { virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; - TimeBoundType const& getTimeBoundType() const; - bool isStepBounded() const; - bool isTimeBounded() const; + TimeBoundReference const& getTimeBoundReference() const; + bool isLowerBoundStrict() const; bool hasLowerBound() const; @@ -49,7 +48,7 @@ namespace storm { private: static void checkNoVariablesInBound(storm::expressions::Expression const& bound); - TimeBoundType timeBoundType; + TimeBoundReference timeBoundReference; boost::optional lowerBound; boost::optional upperBound; }; diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index 9038a2307..3f871908e 100644 --- a/src/storm/logic/Formula.cpp +++ b/src/storm/logic/Formula.cpp @@ -175,6 +175,10 @@ namespace storm { return std::shared_ptr(new BooleanLiteralFormula(true)); } + bool Formula::isInitialFormula() const { + return this->isAtomicLabelFormula() && this->asAtomicLabelFormula().getLabel() == "init"; + } + PathFormula& Formula::asPathFormula() { return dynamic_cast(*this); } diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index 2ad5e9477..a76dd0ef7 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -93,10 +93,12 @@ namespace storm { bool isInFragment(FragmentSpecification const& fragment) const; FormulaInformation info() const; - + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data = boost::any()) const = 0; static std::shared_ptr getTrueFormula(); + + bool isInitialFormula() const; PathFormula& asPathFormula(); PathFormula const& asPathFormula() const; diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index c47b8ea5d..ee0967d22 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -58,10 +58,14 @@ namespace storm { result = result && !f.getLeftSubformula().isPathFormula(); result = result && !f.getRightSubformula().isPathFormula(); } - if (f.isStepBounded()) { + auto tbr = f.getTimeBoundReference(); + if (tbr.isStepBound()) { result = result && inherited.getSpecification().areStepBoundedUntilFormulasAllowed(); - } else { + } else if(tbr.isTimeBound()) { result = result && inherited.getSpecification().areTimeBoundedUntilFormulasAllowed(); + } else { + assert(tbr.isRewardBound()); + result = result && inherited.getSpecification().areRewardBoundedUntilFormulasAllowed(); } result = result && boost::any_cast(f.getLeftSubformula().accept(*this, data)); result = result && boost::any_cast(f.getRightSubformula().accept(*this, data)); diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 0d4771552..19c4116aa 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -141,6 +141,7 @@ namespace storm { onlyEventuallyFormuluasInConditionalFormulas = true; stepBoundedUntilFormulas = false; timeBoundedUntilFormulas = false; + rewardBoundedUntilFormulas = false; varianceAsMeasureType = false; qualitativeOperatorResults = true; @@ -423,7 +424,16 @@ namespace storm { this->timeBoundedUntilFormulas = newValue; return *this; } - + + bool FragmentSpecification::areRewardBoundedUntilFormulasAllowed() const { + return this->rewardBoundedUntilFormulas; + } + + FragmentSpecification& FragmentSpecification::setRewardBoundedUntilFormulasAllowed(bool newValue) { + this->rewardBoundedUntilFormulas = newValue; + return *this; + } + FragmentSpecification& FragmentSpecification::setOperatorsAllowed(bool newValue) { this->setProbabilityOperatorsAllowed(newValue); this->setRewardOperatorsAllowed(newValue); diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 587d49bf3..619394189 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -102,6 +102,9 @@ namespace storm { bool areTimeBoundedUntilFormulasAllowed() const; FragmentSpecification& setTimeBoundedUntilFormulasAllowed(bool newValue); + + bool areRewardBoundedUntilFormulasAllowed() const; + FragmentSpecification& setRewardBoundedUntilFormulasAllowed(bool newValue); bool isVarianceMeasureTypeAllowed() const; FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue); @@ -162,6 +165,7 @@ namespace storm { bool onlyEventuallyFormuluasInConditionalFormulas; bool stepBoundedUntilFormulas; bool timeBoundedUntilFormulas; + bool rewardBoundedUntilFormulas; bool varianceAsMeasureType; bool quantitativeOperatorResults; bool qualitativeOperatorResults; diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h index aef71b040..7200cc89d 100644 --- a/src/storm/logic/TimeBoundType.h +++ b/src/storm/logic/TimeBoundType.h @@ -2,11 +2,47 @@ namespace storm { namespace logic { - + enum class TimeBoundType { Steps, - Time + Time, + Reward }; + + class TimeBoundReference { + TimeBoundType type; + std::string rewardName; + + public: + explicit TimeBoundReference(TimeBoundType t) : type(t) { + // For rewards, use the other constructor. + assert(t != TimeBoundType::Reward); + } + + explicit TimeBoundReference(std::string const& rewardName) : type(TimeBoundType::Reward), rewardName(rewardName) { + assert(rewardName != ""); // Empty reward name is reserved. + } + + + bool isStepBound() const { + return type == TimeBoundType::Steps; + } + + bool isTimeBound() const { + return type == TimeBoundType::Time; + } + + bool isRewardBound() const { + return type == TimeBoundType::Reward; + } + + std::string const& getRewardName() const { + assert(isRewardBound()); + return rewardName; + } + }; + + } } diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index 96ede4769..8c0945adb 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -47,7 +47,7 @@ namespace storm { upperBound = TimeBound(f.isUpperBoundStrict(), f.getUpperBound().substitute(substitution)); } - return std::static_pointer_cast(std::make_shared(left, right, lowerBound, upperBound, f.getTimeBoundType())); + return std::static_pointer_cast(std::make_shared(left, right, lowerBound, upperBound, f.getTimeBoundReference())); } boost::any VariableSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 16574947f..ba7a727c4 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -83,7 +83,7 @@ namespace storm { SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); + STORM_LOG_THROW(!pathFormula.getTimeBoundReference().isStepBound(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); double lowerBound = 0; double upperBound = 0; if (pathFormula.hasLowerBound()) { diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 5de82a7d1..facfd3da2 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -60,7 +60,7 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();; ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); + STORM_LOG_THROW(!pathFormula.getTimeBoundReference().isStepBound(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); double lowerBound = 0; double upperBound = 0; if (pathFormula.hasLowerBound()) { diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 7f555e6d2..2f90c23d5 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -34,7 +34,7 @@ namespace storm { template bool SparseMarkovAutomatonCslModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setReachabilityRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true))) { + if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true))) { return true; } else { // Check whether we consider a multi-objective formula @@ -54,7 +54,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on MAs are not supported."); + STORM_LOG_THROW(!pathFormula.getTimeBoundReference().isStepBound(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on MAs are not supported."); double lowerBound = 0; double upperBound = 0; if (pathFormula.hasLowerBound()) { @@ -106,7 +106,15 @@ namespace storm { std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } - + + template + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask 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."); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); + } + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 971c7b383..94db9727d 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -25,6 +25,7 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr checkMultiObjectiveFormula(CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 50e26ddae..bc83d20f9 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -32,7 +32,7 @@ namespace storm { namespace helper { template ::SupportsExponential, int>::type> - void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Start by computing four sparse matrices: // * a matrix aMarkovian with all (discretized) transitions from Markovian non-goal states to all Markovian non-goal states. @@ -46,7 +46,7 @@ namespace storm { // The matrices with transitions from Markovian states need to be digitized. // Digitize aMarkovian. Based on whether the transition is a self-loop or not, we apply the two digitization rules. - uint_fast64_t rowIndex = 0; + uint64_t rowIndex = 0; for (auto state : markovianNonGoalStates) { for (auto& element : aMarkovian.getRow(rowIndex)) { ValueType eTerm = std::exp(-exitRates[state] * delta); @@ -96,7 +96,7 @@ namespace storm { // and 1_G being the characteristic vector for all goal states. // * perform one timed-step using v_MS := A_MSwG * v_MS + A_MStoPS * v_PS + (A * 1_G)|MS std::vector markovianNonGoalValuesSwap(markovianNonGoalValues); - for (uint_fast64_t currentStep = 0; currentStep < numberOfSteps; ++currentStep) { + for (uint64_t currentStep = 0; currentStep < numberOfSteps; ++currentStep) { // Start by (re-)computing bProbabilistic = bProbabilisticFixed + aProbabilisticToMarkovian * vMarkovian. aProbabilisticToMarkovian.multiplyWithVector(markovianNonGoalValues, bProbabilistic); storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); @@ -119,14 +119,14 @@ namespace storm { } template ::SupportsExponential, int>::type> - void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded reachability probabilities is unsupported for this value type."); } template ::SupportsExponential, int>::type> std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + uint64_t numberOfStates = transitionMatrix.getRowGroupCount(); // 'Unpack' the bounds to make them more easily accessible. double lowerBound = boundsPair.first; @@ -140,7 +140,7 @@ namespace storm { ValueType delta = (2 * storm::settings::getModule().getPrecision()) / (upperBound * maxExitRate * maxExitRate); // (2) Compute the number of steps we need to make for the interval. - uint_fast64_t numberOfSteps = static_cast(std::ceil((upperBound - lowerBound) / delta)); + uint64_t numberOfSteps = static_cast(std::ceil((upperBound - lowerBound) / delta)); STORM_LOG_INFO("Performing " << numberOfSteps << " iterations (delta=" << delta << ") for interval [" << lowerBound << ", " << upperBound << "]." << std::endl); // (3) Compute the non-goal states and initialize two vectors @@ -165,7 +165,7 @@ namespace storm { storm::utility::vector::setVectorValues(vAllMarkovian, ~psiStates % markovianStates, vMarkovian); // Compute the number of steps to reach the target interval. - numberOfSteps = static_cast(std::ceil(lowerBound / delta)); + numberOfSteps = static_cast(std::ceil(lowerBound / delta)); STORM_LOG_INFO("Performing " << numberOfSteps << " iterations (delta=" << delta << ") for interval [0, " << lowerBound << "]." << std::endl); // Compute the bounded reachability for interval [0, b-a]. @@ -213,9 +213,10 @@ namespace storm { } template - std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); - + std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique) { + + uint64_t numberOfStates = transitionMatrix.getRowGroupCount(); + // If there are no goal states, we avoid the computation and directly return zero. if (psiStates.empty()) { return std::vector(numberOfStates, storm::utility::zero()); @@ -226,40 +227,55 @@ namespace storm { return std::vector(numberOfStates, storm::utility::one()); } + // Otherwise, reduce the long run average probabilities to long run average rewards. + // Every Markovian goal state gets reward one. + std::vector stateRewards(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + storm::utility::vector::setVectorValues(stateRewards, markovianStates & psiStates, storm::utility::one()); + storm::models::sparse::StandardRewardModel rewardModel(std::move(stateRewards)); + + return computeLongRunAverageRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, rewardModel, minMaxLinearEquationSolverFactory, useLpBasedTechnique); + + } + + template + std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique) { + + uint64_t numberOfStates = transitionMatrix.getRowGroupCount(); + // Start by decomposing the Markov automaton into its MECs. storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions); // Get some data members for convenience. - std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); // Now start with compute the long-run average for all end components in isolation. std::vector lraValuesForEndComponents; // While doing so, we already gather some information for the following steps. - std::vector stateToMecIndexMap(numberOfStates); + std::vector stateToMecIndexMap(numberOfStates); storm::storage::BitVector statesInMecs(numberOfStates); - for (uint_fast64_t currentMecIndex = 0; currentMecIndex < mecDecomposition.size(); ++currentMecIndex) { + for (uint64_t currentMecIndex = 0; currentMecIndex < mecDecomposition.size(); ++currentMecIndex) { storm::storage::MaximalEndComponent const& mec = mecDecomposition[currentMecIndex]; // Gather information for later use. for (auto const& stateChoicesPair : mec) { - uint_fast64_t state = stateChoicesPair.first; + uint64_t state = stateChoicesPair.first; statesInMecs.set(state); stateToMecIndexMap[state] = currentMecIndex; } // Compute the LRA value for the current MEC. - lraValuesForEndComponents.push_back(computeLraForMaximalEndComponent(dir, transitionMatrix, exitRateVector, markovianStates, psiStates, mec)); + lraValuesForEndComponents.push_back(computeLraForMaximalEndComponent(dir, transitionMatrix, exitRateVector, markovianStates, rewardModel, mec, minMaxLinearEquationSolverFactory, useLpBasedTechnique)); } // For fast transition rewriting, we build some auxiliary data structures. storm::storage::BitVector statesNotContainedInAnyMec = ~statesInMecs; - uint_fast64_t firstAuxiliaryStateIndex = statesNotContainedInAnyMec.getNumberOfSetBits(); - uint_fast64_t lastStateNotInMecs = 0; - uint_fast64_t numberOfStatesNotInMecs = 0; - std::vector statesNotInMecsBeforeIndex; + uint64_t firstAuxiliaryStateIndex = statesNotContainedInAnyMec.getNumberOfSetBits(); + uint64_t lastStateNotInMecs = 0; + uint64_t numberOfStatesNotInMecs = 0; + std::vector statesNotInMecsBeforeIndex; statesNotInMecsBeforeIndex.reserve(numberOfStates); for (auto state : statesNotContainedInAnyMec) { while (lastStateNotInMecs <= state) { @@ -274,11 +290,11 @@ namespace storm { typename storm::storage::SparseMatrixBuilder sspMatrixBuilder(0, 0, 0, false, true, numberOfStatesNotInMecs + mecDecomposition.size()); // If the source state is not contained in any MEC, we copy its choices (and perform the necessary modifications). - uint_fast64_t currentChoice = 0; + uint64_t currentChoice = 0; for (auto state : statesNotContainedInAnyMec) { sspMatrixBuilder.newRowGroup(currentChoice); - for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice, ++currentChoice) { + for (uint64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice, ++currentChoice) { std::vector auxiliaryStateToProbabilityMap(mecDecomposition.size()); b.push_back(storm::utility::zero()); @@ -294,7 +310,7 @@ namespace storm { } // Now insert all (cumulative) probability values that target an MEC. - for (uint_fast64_t mecIndex = 0; mecIndex < auxiliaryStateToProbabilityMap.size(); ++mecIndex) { + for (uint64_t mecIndex = 0; mecIndex < auxiliaryStateToProbabilityMap.size(); ++mecIndex) { if (auxiliaryStateToProbabilityMap[mecIndex] != 0) { sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + mecIndex, auxiliaryStateToProbabilityMap[mecIndex]); } @@ -303,15 +319,15 @@ namespace storm { } // Now we are ready to construct the choices for the auxiliary states. - for (uint_fast64_t mecIndex = 0; mecIndex < mecDecomposition.size(); ++mecIndex) { + for (uint64_t mecIndex = 0; mecIndex < mecDecomposition.size(); ++mecIndex) { storm::storage::MaximalEndComponent const& mec = mecDecomposition[mecIndex]; sspMatrixBuilder.newRowGroup(currentChoice); for (auto const& stateChoicesPair : mec) { - uint_fast64_t state = stateChoicesPair.first; - boost::container::flat_set const& choicesInMec = stateChoicesPair.second; + uint64_t state = stateChoicesPair.first; + boost::container::flat_set const& choicesInMec = stateChoicesPair.second; - for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + for (uint64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { std::vector auxiliaryStateToProbabilityMap(mecDecomposition.size()); // If the choice is not contained in the MEC itself, we have to add a similar distribution to the auxiliary state. @@ -330,7 +346,7 @@ namespace storm { } // Now insert all (cumulative) probability values that target an MEC. - for (uint_fast64_t targetMecIndex = 0; targetMecIndex < auxiliaryStateToProbabilityMap.size(); ++targetMecIndex) { + for (uint64_t targetMecIndex = 0; targetMecIndex < auxiliaryStateToProbabilityMap.size(); ++targetMecIndex) { if (auxiliaryStateToProbabilityMap[targetMecIndex] != 0) { sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + targetMecIndex, auxiliaryStateToProbabilityMap[targetMecIndex]); } @@ -380,14 +396,37 @@ namespace storm { return SparseMdpPrctlHelper::computeReachabilityRewards(dir, transitionMatrix, backwardTransitions, rewardModel, psiStates, false, false, minMaxLinearEquationSolverFactory).values; } - template - ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec) { + template + ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique) { + + // If the mec only consists of a single state, we compute the LRA value directly + if (++mec.begin() == mec.end()) { + uint64_t state = mec.begin()->first; + STORM_LOG_THROW(markovianStates.get(state), storm::exceptions::InvalidOperationException, "Markov Automaton has Zeno behavior. Computation of Long Run Average values not supported."); + ValueType result = rewardModel.hasStateRewards() ? rewardModel.getStateReward(state) : storm::utility::zero(); + if (rewardModel.hasStateActionRewards() || rewardModel.hasTransitionRewards()) { + STORM_LOG_ASSERT(mec.begin()->second.size() == 1, "Markovian state has nondeterministic behavior."); + uint64_t choice = *mec.begin()->second.begin(); + result += exitRateVector[state] * rewardModel.getTotalStateActionReward(state, choice, transitionMatrix, storm::utility::zero()); + } + return result; + } + + if (useLpBasedTechnique) { + return computeLraForMaximalEndComponentLP(dir, transitionMatrix, exitRateVector, markovianStates, rewardModel, mec); + } else { + return computeLraForMaximalEndComponentVI(dir, transitionMatrix, exitRateVector, markovianStates, rewardModel, mec, minMaxLinearEquationSolverFactory); + } + } + + template + ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec) { std::unique_ptr lpSolverFactory(new storm::utility::solver::LpSolverFactory()); std::unique_ptr solver = lpSolverFactory->create("LRA for MEC"); solver->setOptimizationDirection(invert(dir)); // First, we need to create the variables for the problem. - std::map stateToVariableMap; + std::map stateToVariableMap; for (auto const& stateChoicesPair : mec) { std::string variableName = "x" + std::to_string(stateChoicesPair.first); stateToVariableMap[stateChoicesPair.first] = solver->addUnboundedContinuousVariable(variableName); @@ -396,12 +435,15 @@ namespace storm { solver->update(); // Now we encode the problem as constraints. - std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); for (auto const& stateChoicesPair : mec) { - uint_fast64_t state = stateChoicesPair.first; + uint64_t state = stateChoicesPair.first; // Now, based on the type of the state, create a suitable constraint. if (markovianStates.get(state)) { + STORM_LOG_ASSERT(stateChoicesPair.second.size() == 1, "Markovian state " << state << " is not deterministic: It has " << stateChoicesPair.second.size() << " choices."); + uint64_t choice = *stateChoicesPair.second.begin(); + storm::expressions::Expression constraint = stateToVariableMap.at(state); for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) { @@ -409,7 +451,8 @@ namespace storm { } constraint = constraint + solver->getManager().rational(storm::utility::one() / exitRateVector[state]) * k; - storm::expressions::Expression rightHandSide = goalStates.get(state) ? solver->getManager().rational(storm::utility::one() / exitRateVector[state]) : solver->getManager().rational(storm::utility::zero()); + + storm::expressions::Expression rightHandSide = solver->getManager().rational(rewardModel.getTotalStateActionReward(state, choice, transitionMatrix, (ValueType) (storm::utility::one() / exitRateVector[state]))); if (dir == OptimizationDirection::Minimize) { constraint = constraint <= rightHandSide; } else { @@ -425,8 +468,8 @@ namespace storm { for (auto element : transitionMatrix.getRow(choice)) { constraint = constraint - stateToVariableMap.at(element.getColumn()) * solver->getManager().rational(element.getValue()); } - - storm::expressions::Expression rightHandSide = solver->getManager().rational(storm::utility::zero()); + + storm::expressions::Expression rightHandSide = solver->getManager().rational(rewardModel.getTotalStateActionReward(state, choice, transitionMatrix, storm::utility::zero())); if (dir == OptimizationDirection::Minimize) { constraint = constraint <= rightHandSide; } else { @@ -440,8 +483,125 @@ namespace storm { solver->optimize(); return storm::utility::convertNumber(solver->getContinuousValue(k)); } - + template + ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentVI(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + + // Initialize data about the mec + + storm::storage::BitVector mecStates(transitionMatrix.getRowGroupCount(), false); + storm::storage::BitVector mecChoices(transitionMatrix.getRowCount(), false); + for (auto const& stateChoicesPair : mec) { + mecStates.set(stateChoicesPair.first); + for (auto const& choice : stateChoicesPair.second) { + mecChoices.set(choice); + } + } + storm::storage::BitVector markovianMecStates = mecStates & markovianStates; + storm::storage::BitVector probabilisticMecStates = mecStates & ~markovianStates; + storm::storage::BitVector probabilisticMecChoices = transitionMatrix.getRowFilter(probabilisticMecStates) & mecChoices; + STORM_LOG_THROW(!markovianMecStates.empty(), storm::exceptions::InvalidOperationException, "Markov Automaton has Zeno behavior. Computation of Long Run Average values not supported."); + + // Get the uniformization rate + + ValueType uniformizationRate = storm::utility::vector::max_if(exitRateVector, markovianMecStates); + // To ensure that the model is aperiodic, we need to make sure that every Markovian state gets a self loop. + // Hence, we increase the uniformization rate a little. + uniformizationRate += storm::utility::one(); // Todo: try other values such as *=1.01 + + // Get the transitions of the submodel, that is + // * a matrix aMarkovian with all (uniformized) transitions from Markovian mec states to all Markovian mec states. + // * a matrix aMarkovianToProbabilistic with all (uniformized) transitions from Markovian mec states to all probabilistic mec states. + // * a matrix aProbabilistic with all transitions from probabilistic mec states to other probabilistic mec states. + // * a matrix aProbabilisticToMarkovian with all transitions from probabilistic mec states to all Markovian mec states. + typename storm::storage::SparseMatrix aMarkovian = transitionMatrix.getSubmatrix(true, markovianMecStates, markovianMecStates, true); + typename storm::storage::SparseMatrix aMarkovianToProbabilistic = transitionMatrix.getSubmatrix(true, markovianMecStates, probabilisticMecStates); + typename storm::storage::SparseMatrix aProbabilistic = transitionMatrix.getSubmatrix(false, probabilisticMecChoices, probabilisticMecStates); + typename storm::storage::SparseMatrix aProbabilisticToMarkovian = transitionMatrix.getSubmatrix(false, probabilisticMecChoices, markovianMecStates); + // The matrices with transitions from Markovian states need to be uniformized. + uint64_t subState = 0; + for (auto state : markovianMecStates) { + ValueType uniformizationFactor = exitRateVector[state] / uniformizationRate; + for (auto& entry : aMarkovianToProbabilistic.getRow(subState)) { + entry.setValue(entry.getValue() * uniformizationFactor); + } + for (auto& entry : aMarkovian.getRow(subState)) { + if (entry.getColumn() == subState) { + entry.setValue(storm::utility::one() - uniformizationFactor * (storm::utility::one() - entry.getValue())); + } else { + entry.setValue(entry.getValue() * uniformizationFactor); + } + } + ++subState; + } + + // Compute the rewards obtained in a single uniformization step + + std::vector markovianChoiceRewards; + markovianChoiceRewards.reserve(aMarkovian.getRowCount()); + for (auto const& state : markovianMecStates) { + ValueType stateRewardScalingFactor = storm::utility::one() / uniformizationRate; + ValueType actionRewardScalingFactor = exitRateVector[state] / uniformizationRate; + assert(transitionMatrix.getRowGroupSize(state) == 1); + uint64_t choice = transitionMatrix.getRowGroupIndices()[state]; + markovianChoiceRewards.push_back(rewardModel.getTotalStateActionReward(state, choice, transitionMatrix, stateRewardScalingFactor, actionRewardScalingFactor)); + } + + std::vector probabilisticChoiceRewards; + probabilisticChoiceRewards.reserve(aProbabilistic.getRowCount()); + for (auto const& state : probabilisticMecStates) { + uint64_t groupStart = transitionMatrix.getRowGroupIndices()[state]; + uint64_t groupEnd = transitionMatrix.getRowGroupIndices()[state + 1]; + for (uint64_t choice = probabilisticMecChoices.getNextSetIndex(groupStart); choice < groupEnd; choice = probabilisticMecChoices.getNextSetIndex(choice + 1)) { + probabilisticChoiceRewards.push_back(rewardModel.getTotalStateActionReward(state, choice, transitionMatrix, storm::utility::zero())); + } + } + + // start the iterations + + ValueType precision = storm::utility::convertNumber(storm::settings::getModule().getPrecision()) / uniformizationRate; + std::vector v(aMarkovian.getRowCount(), storm::utility::zero()); + std::vector w = v; + std::vector x(aProbabilistic.getRowGroupCount(), storm::utility::zero()); + std::vector b = probabilisticChoiceRewards; + auto solver = minMaxLinearEquationSolverFactory.create(std::move(aProbabilistic)); + solver->setCachingEnabled(true); + + while (true) { + + // Compute the expected total rewards for the probabilistic states + solver->solveEquations(dir, x, b); + + // now compute the values for the markovian states. We also keep track of the maximal and minimal difference between two values (for convergence checking) + auto vIt = v.begin(); + uint64_t row = 0; + ValueType newValue = markovianChoiceRewards[row] + aMarkovianToProbabilistic.multiplyRowWithVector(row, x) + aMarkovian.multiplyRowWithVector(row, w); + ValueType maxDiff = newValue - *vIt; + ValueType minDiff = maxDiff; + *vIt = newValue; + for (++vIt, ++row; row < aMarkovian.getRowCount(); ++vIt, ++row) { + newValue = markovianChoiceRewards[row] + aMarkovianToProbabilistic.multiplyRowWithVector(row, x) + aMarkovian.multiplyRowWithVector(row, w); + ValueType diff = newValue - *vIt; + maxDiff = std::max(maxDiff, diff); + minDiff = std::min(minDiff, diff); + *vIt = newValue; + } + + // Check for convergence + if (maxDiff - minDiff < precision) { + break; + } + + // update the rhs of the MinMax equation system + ValueType referenceValue = v.front(); + storm::utility::vector::applyPointwise(v, w, [&referenceValue] (ValueType const& v_i) -> ValueType { return v_i - referenceValue; }); + aProbabilisticToMarkovian.multiplyWithVector(w, b); + storm::utility::vector::addVectors(b, probabilisticChoiceRewards, b); + + } + return v.front() * uniformizationRate; + + } template std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); @@ -449,27 +609,39 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); + template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, double delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, double delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); + template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); + template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec); + + template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentVI(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMarkovAutomatonCslHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); + + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); + template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, storm::RationalNumber delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, storm::RationalNumber delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template storm::RationalNumber SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); + template storm::RationalNumber SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); + + template storm::RationalNumber SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec); + + template storm::RationalNumber SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentVI(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); } } diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 20d6c9598..f41c8e287 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -29,32 +29,44 @@ namespace storm { template - static std::vector computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique = false); + + template + static std::vector computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique = false); template static std::vector computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); private: template ::SupportsExponential, int>::type = 0> - static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template ::SupportsExponential, int>::type = 0> - static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template ::SupportsExponential, int>::type = 0> + static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); /*! * Computes the long-run average value for the given maximal end component of a Markov automaton. * + * Implementations are based on Linear Programming (LP) and Value Iteration (VI). + * * @param dir Sets whether the long-run average is to be minimized or maximized. * @param transitionMatrix The transition matrix of the underlying Markov automaton. * @param markovianStates A bit vector storing all markovian states. * @param exitRateVector A vector with exit rates for all states. Exit rates of probabilistic states are * assumed to be zero. - * @param goalStates A bit vector indicating which states are to be considered as goal states. + * @param rewardModel The considered reward model + * @param actionRewards The action rewards (earned instantaneously). * @param mec The maximal end component to consider for computing the long-run average. + * @param minMaxLinearEquationSolverFactory The factory for creating MinMaxLinearEquationSolvers (if needed by the performed method * @return The long-run average of being in a goal state for the given MEC. */ - template - static ValueType computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); + template + static ValueType computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique = false); + template + static ValueType computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec); + template + static ValueType computeLraForMaximalEndComponentVI(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + }; } diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index b2da20897..485bc41bf 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -266,7 +266,7 @@ namespace storm { template void SparseMultiObjectivePreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data) { - STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); + STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.getTimeBoundReference().isStepBound(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); if (formula.hasLowerBound()) { STORM_LOG_THROW(!formula.getLowerBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The lower time bound for the formula " << formula << " still contains variables"); diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp index bdcf68c8f..9155057d3 100644 --- a/src/storm/modelchecker/results/CheckResult.cpp +++ b/src/storm/modelchecker/results/CheckResult.cpp @@ -113,6 +113,15 @@ namespace storm { return dynamic_cast(*this); } + template + QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult() { + return static_cast &>(*this); + } + + template + QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const { + return static_cast const&>(*this); + } template SymbolicQualitativeCheckResult& CheckResult::asSymbolicQualitativeCheckResult() { @@ -155,6 +164,9 @@ namespace storm { } // Explicitly instantiate the template functions. + template QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult(); + template QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const; + template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; template ExplicitParetoCurveCheckResult& CheckResult::asExplicitParetoCurveCheckResult(); @@ -184,9 +196,15 @@ namespace storm { #ifdef STORM_HAVE_CARL + template QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult(); + template QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const; + template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; + template QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult(); + template QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const; + template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; diff --git a/src/storm/modelchecker/results/CheckResult.h b/src/storm/modelchecker/results/CheckResult.h index 2cff249c9..43954a220 100644 --- a/src/storm/modelchecker/results/CheckResult.h +++ b/src/storm/modelchecker/results/CheckResult.h @@ -66,14 +66,10 @@ namespace storm { QualitativeCheckResult const& asQualitativeCheckResult() const; template - QuantitativeCheckResult& asQuantitativeCheckResult() { - return static_cast &>(*this); - } + QuantitativeCheckResult& asQuantitativeCheckResult(); + template - QuantitativeCheckResult const& asQuantitativeCheckResult() const { - return static_cast const&>(*this); - } - + QuantitativeCheckResult const& asQuantitativeCheckResult() const; ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const; diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index bffd8a7e9..721608047 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -139,6 +139,30 @@ namespace storm { return StandardRewardModel(std::move(newStateRewardVector), std::move(newStateActionRewardVector), std::move(newTransitionRewardMatrix)); } + template + template + ValueType StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, MatrixValueType const& stateRewardWeight, MatrixValueType const& actionRewardWeight) const { + ValueType result = this->hasStateRewards() ? (this->hasStateActionRewards() ? (ValueType) (this->getStateReward(stateIndex) * stateRewardWeight + this->getStateActionReward(choiceIndex) * actionRewardWeight) + : (ValueType) (this->getStateReward(stateIndex) * stateRewardWeight)) + : (this->hasStateActionRewards() ? (ValueType) (this->getStateActionReward(choiceIndex) * actionRewardWeight) + : storm::utility::zero()); + if (this->hasTransitionRewards()) { + auto rewMatrixEntryIt = this->getTransitionRewardMatrix().begin(choiceIndex); + for (auto const& transitionEntry : transitionMatrix.getRow(choiceIndex)) { + assert(rewMatrixEntryIt != this->getTransitionRewardMatrix().end(choiceIndex)); + if (transitionEntry.getColumn() < rewMatrixEntryIt->getColumn()) { + continue; + } else { + // We assume that the transition reward matrix is a submatrix of the given transition matrix. Hence, the following must hold + assert(transitionEntry.getColumn() == rewMatrixEntryIt->getColumn()); + result += actionRewardWeight * rewMatrixEntryIt->getValue() * storm::utility::convertNumber(transitionEntry.getValue()); + ++rewMatrixEntryIt; + } + } + } + return result; + } + template template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards) { @@ -362,6 +386,8 @@ namespace storm { template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + template double StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, double const& stateRewardWeight, double const& actionRewardWeight) const; + template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); @@ -385,6 +411,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + template storm::RationalNumber StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, storm::RationalNumber const& stateRewardWeight, storm::RationalNumber const& actionRewardWeight) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalNumber const & newValue); @@ -398,6 +425,7 @@ namespace storm { template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; + template storm::RationalFunction StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, storm::RationalFunction const& stateRewardWeight, storm::RationalFunction const& actionRewardWeight) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalFunction const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalFunction const & newValue); diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index 2a3033ea7..c58f38312 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -4,6 +4,7 @@ #include #include "storm/storage/SparseMatrix.h" +#include "storm/utility/constants.h" #include "storm/utility/OsDetection.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -161,6 +162,19 @@ namespace storm { * @return The transition reward matrix if there is one. */ boost::optional> const& getOptionalTransitionRewardMatrix() const; + + /*! + * Retrieves the total reward for the given state action pair (including (scaled) state rewards, action rewards and transition rewards + * + * @param stateIndex The index of the considered state + * @param choiceIndex The index of the considered choice + * @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix. + * @param stateRewardWeight The weight that is used to scale the state reward + * @param actionRewardWeight The weight that is used to scale the action based rewards (includes action and transition rewards). + * @return + */ + template + ValueType getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, MatrixValueType const& stateRewardWeight = storm::utility::one(), MatrixValueType const& actionRewardWeight = storm::utility::one()) const; /*! * Creates a new reward model by restricting the actions of the action-based rewards. diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index bee6b5117..32148b3c3 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -77,7 +77,10 @@ namespace storm { conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)]; conditionalFormula.name("conditional formula"); - timeBound = (qi::lit("[") > expressionParser > qi::lit(",") > expressionParser > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_1, qi::_2)] | ((qi::lit("<=")[qi::_a = true, qi::_b = false] | qi::lit("<")[qi::_a = true, qi::_b = true] | qi::lit(">=")[qi::_a = false, qi::_b = false] | qi::lit(">")[qi::_a = false, qi::_b = true]) >> expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_1, qi::_a, qi::_b)]; + timeBound = ((-rewardModelName >> qi::lit("[")) > expressionParser > qi::lit(",") > expressionParser > qi::lit("]")) + [qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_3, qi::_1)] + | (-rewardModelName >> (qi::lit("<=")[qi::_a = true, qi::_b = false] | qi::lit("<")[qi::_a = true, qi::_b = true] | qi::lit(">=")[qi::_a = false, qi::_b = false] | qi::lit(">")[qi::_a = false, qi::_b = true]) >> expressionParser) + [qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_2, qi::_a, qi::_b, qi::_1)]; timeBound.name("time bound"); pathFormula = conditionalFormula(qi::_r1); @@ -128,7 +131,7 @@ namespace storm { #pragma clang diagnostic push #pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses" - filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > -(qi::lit(",") > qi::lit("\"init\"") > qi::lit(")")))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterType, phoenix::ref(*this), qi::_1, qi::_2)]; + filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)]; filterProperty.name("filter property"); #pragma clang diagnostic pop @@ -212,17 +215,20 @@ namespace storm { return static_cast(manager); } - std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const { + std::tuple, boost::optional, boost::optional> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, boost::optional const& rewardName) const { + // As soon as it somehow does not break everything anymore, I will change return types here. + storm::logic::TimeBound lower(false, lowerBound); storm::logic::TimeBound upper(false, upperBound); - return std::make_pair(lower, upper); + return std::make_tuple(lower, upper, rewardName); } - std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const { + std::tuple, boost::optional, boost::optional> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, boost::optional const& rewardName) const { + // As soon as it somehow does not break everything anymore, I will change return types here. if (upperBound) { - return std::make_pair(boost::none, storm::logic::TimeBound(strict, bound)); + return std::make_tuple(boost::none, storm::logic::TimeBound(strict, bound), rewardName); } else { - return std::make_pair(storm::logic::TimeBound(strict, bound), boost::none); + return std::make_tuple(storm::logic::TimeBound(strict, bound), boost::none, rewardName); } } @@ -255,9 +261,13 @@ namespace storm { return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } - std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { if (timeBound) { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundType::Time)); + if (std::get<2>(timeBound.get())) { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, std::get<0>(timeBound.get()), std::get<1>(timeBound.get()), storm::logic::TimeBoundReference(std::get<2>(timeBound.get()).get()))); + } else { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, std::get<0>(timeBound.get()), std::get<1>(timeBound.get()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); + } } else { return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); } @@ -271,9 +281,14 @@ namespace storm { return std::shared_ptr(new storm::logic::NextFormula(subformula)); } - std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula) { + std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula) { if (timeBound) { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundType::Time)); + if (std::get<2>(timeBound.get())) { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, std::get<0>(timeBound.get()), std::get<1>(timeBound.get()), storm::logic::TimeBoundReference(std::get<2>(timeBound.get()).get()))); + } else { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, std::get<0>(timeBound.get()), std::get<1>(timeBound.get()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); + } + } else { return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); } @@ -332,8 +347,8 @@ namespace storm { return std::shared_ptr(new storm::logic::MultiObjectiveFormula(subformulas)); } - storm::jani::Property FormulaParserGrammar::createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula) { - storm::jani::FilterExpression filterExpression(formula, filterType); + storm::jani::Property FormulaParserGrammar::createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states) { + storm::jani::FilterExpression filterExpression(formula, filterType, states); ++propertyCount; if (propertyName) { @@ -343,7 +358,7 @@ namespace storm { } } - storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterType(boost::optional const& propertyName, std::shared_ptr const& formula) { + storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula) { ++propertyCount; if (propertyName) { return storm::jani::Property(propertyName.get(), formula); diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index 79b272246..d8039bade 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -181,7 +181,7 @@ namespace storm { qi::rule(storm::logic::FormulaContext), Skipper> globallyFormula; qi::rule(storm::logic::FormulaContext), Skipper> untilFormula; - qi::rule, boost::optional>(), qi::locals, Skipper> timeBound; + qi::rule, boost::optional, boost::optional>(), qi::locals, Skipper> timeBound; qi::rule(), Skipper> rewardPathFormula; qi::rule(), qi::locals, Skipper> cumulativeRewardFormula; @@ -197,11 +197,11 @@ namespace storm { bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, bool integer); void addProperty(std::vector& properties, boost::optional const& name, std::shared_ptr const& formula); - - std::pair, boost::optional> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const; - std::pair, boost::optional> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const; - - // Methods that actually create the expression objects. + + std::tuple, boost::optional, boost::optional> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, boost::optional const& rewardName) const; + std::tuple, boost::optional, boost::optional> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, boost::optional const& rewardName) const; + + // Methods that actually create the expression objects. std::shared_ptr createInstantaneousRewardFormula(storm::expressions::Expression const& timeBound) const; std::shared_ptr createCumulativeRewardFormula(storm::expressions::Expression const& timeBound, bool strict) const; std::shared_ptr createTotalRewardFormula() const; @@ -209,10 +209,10 @@ namespace storm { std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; - std::shared_ptr createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; + std::shared_ptr createEventuallyFormula(boost::optional, boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; - std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula); + std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula); std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const; storm::logic::OperatorInformation createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; std::shared_ptr createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; @@ -223,8 +223,8 @@ namespace storm { std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); std::shared_ptr createMultiObjectiveFormula(std::vector> const& subformulas); - storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula); - storm::jani::Property createPropertyWithDefaultFilterType(boost::optional const& propertyName, std::shared_ptr const& formula); + storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states); + storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula); // An error handler function. phoenix::function handler; diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index ecb3ed0ff..28ac7ae7c 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -297,7 +297,7 @@ namespace storm { } } } else if (propertyStructure.count("reward-instants") > 0) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant/Cumul. Reward for reward constraints not supported currently."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant Reward for reward constraints not supported currently."); } //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given."); @@ -353,7 +353,7 @@ namespace storm { upperBound--; } STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "Step-bounds cannot be negative"); - return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::Steps); + return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)); } else if (propertyStructure.count("time-bounds") > 0) { storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds")); STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound."); @@ -364,10 +364,26 @@ namespace storm { double upperBound = pi.upperBound.evaluateAsDouble(); STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative"); STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative"); - return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::Time); + return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)); } else if (propertyStructure.count("reward-bounds") > 0 ) { + storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("reward-bounds")); + STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound."); + STORM_LOG_THROW(propertyStructure.at("reward-bounds").count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); + storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("reward-bounds").at("exp"), "Reward expression in " + context, globalVars, constants); + STORM_LOG_THROW(!rewExpr.isVariable(), storm::exceptions::NotSupportedException, "Storm currently does not support complex reward expressions."); + std::string rewardName = rewExpr.getVariables().begin()->getName(); + STORM_LOG_WARN("Reward-type (steps, time) is deduced from model type."); + double lowerBound = 0.0; + if(pi.hasLowerBound()) { + lowerBound = pi.lowerBound.evaluateAsDouble(); + } + double upperBound = pi.upperBound.evaluateAsDouble(); + STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative"); + STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative"); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by storm"); + return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(rewardName)); + } if (args[0]->isTrueFormula()) { return std::make_shared(args[1], formulaContext); diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index c13bb492d..c140e7520 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp @@ -19,7 +19,7 @@ namespace storm { const std::string MinMaxEquationSolverSettings::absoluteOptionName = "absolute"; MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(moduleName) { - std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration"}; + std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "acyclic"}; this->addOption(storm::settings::OptionBuilder(moduleName, solvingMethodOptionName, false, "Sets which min/max linear equation solving technique is preferred.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a min/max linear equation solving technique.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(minMaxSolvingTechniques)).setDefaultValueString("vi").build()).build()); @@ -36,6 +36,8 @@ namespace storm { return storm::solver::MinMaxMethod::ValueIteration; } else if (minMaxEquationSolvingTechnique == "policy-iteration" || minMaxEquationSolvingTechnique == "pi") { return storm::solver::MinMaxMethod::PolicyIteration; + } else if (minMaxEquationSolvingTechnique == "acyclic") { + return storm::solver::MinMaxMethod::Acyclic; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown min/max equation solving technique '" << minMaxEquationSolvingTechnique << "'."); } diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 5f1e0c176..4bdb08f3e 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -170,7 +170,7 @@ namespace storm { std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { std::unique_ptr> result; auto method = storm::settings::getModule().getMinMaxEquationSolvingMethod(); - if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration) { + if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) { result = std::make_unique>(std::forward(matrix), std::make_unique>()); } else if (method == MinMaxMethod::Topological) { result = std::make_unique>(std::forward(matrix)); @@ -187,7 +187,7 @@ namespace storm { std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { std::unique_ptr> result; auto method = storm::settings::getModule().getMinMaxEquationSolvingMethod(); - STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration, storm::exceptions::InvalidSettingsException, "For this data type only value iteration and policy iteration are available."); + STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic, storm::exceptions::InvalidSettingsException, "For this data type only value iteration, policy iteration, and acyclic value iteration are available."); return std::make_unique>(std::forward(matrix), std::make_unique>()); } #endif diff --git a/src/storm/solver/SolverSelectionOptions.cpp b/src/storm/solver/SolverSelectionOptions.cpp index fe42f299a..2a39108ea 100644 --- a/src/storm/solver/SolverSelectionOptions.cpp +++ b/src/storm/solver/SolverSelectionOptions.cpp @@ -10,7 +10,8 @@ namespace storm { return "value"; case MinMaxMethod::Topological: return "topological"; - + case MinMaxMethod::Acyclic: + return "acyclic"; } return "invalid"; } diff --git a/src/storm/solver/SolverSelectionOptions.h b/src/storm/solver/SolverSelectionOptions.h index 32af0a4eb..94584c7c3 100644 --- a/src/storm/solver/SolverSelectionOptions.h +++ b/src/storm/solver/SolverSelectionOptions.h @@ -6,7 +6,7 @@ namespace storm { namespace solver { - ExtendEnumsWithSelectionField(MinMaxMethod, PolicyIteration, ValueIteration, Topological) + ExtendEnumsWithSelectionField(MinMaxMethod, PolicyIteration, ValueIteration, Topological, Acyclic) ExtendEnumsWithSelectionField(GameMethod, PolicyIteration, ValueIteration) ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk, Z3) diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 0a93a70f4..627dcd131 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -29,6 +29,7 @@ namespace storm { switch (method) { case MinMaxMethod::ValueIteration: this->solutionMethod = SolutionMethod::ValueIteration; break; case MinMaxMethod::PolicyIteration: this->solutionMethod = SolutionMethod::PolicyIteration; break; + case MinMaxMethod::Acyclic: this->solutionMethod = SolutionMethod::Acyclic; break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } @@ -91,6 +92,8 @@ namespace storm { return solveEquationsValueIteration(dir, x, b); case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration: return solveEquationsPolicyIteration(dir, x, b); + case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::Acyclic: + return solveEquationsAcyclic(dir, x, b); default: STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "This solver does not implement the selected solution method"); } @@ -293,6 +296,113 @@ namespace storm { return status == Status::Converged || status == Status::TerminatedEarly; } + template + bool StandardMinMaxLinearEquationSolver::solveEquationsAcyclic(OptimizationDirection dir, std::vector& x, std::vector const& b) const { + uint64_t numGroups = this->A.getRowGroupCount(); + + // Allocate memory for the scheduler (if required) + if (this->isTrackSchedulerSet()) { + if (this->schedulerChoices) { + this->schedulerChoices->resize(numGroups); + } else { + this->schedulerChoices = std::vector(numGroups); + } + } + + // We now compute a topological sort of the row groups. + // If caching is enabled, it might be possible to obtain this sort from the cache. + if (this->isCachingEnabled()) { + if (rowGroupOrdering) { + for (auto const& group : *rowGroupOrdering) { + computeOptimalValueForRowGroup(group, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[group] : nullptr); + } + return true; + } else { + rowGroupOrdering = std::make_unique>(); + rowGroupOrdering->reserve(numGroups); + } + } + + auto transposedMatrix = this->A.transpose(true); + + // We store the groups that have already been processed, i.e., the groups for which x[group] was already set to the correct value. + storm::storage::BitVector processedGroups(numGroups, false); + // Furthermore, we keep track of all candidate groups for which we still need to check whether this group can be processed now. + // A group can be processed if all successors have already been processed. + // Notice that the BitVector candidates is considered in a reversed way, i.e., group i is a candidate iff candidates.get(numGroups - i - 1) is true. + // This is due to the observation that groups with higher indices usually need to be processed earlier. + storm::storage::BitVector candidates(numGroups, true); + uint64_t candidate = numGroups - 1; + for (uint64_t numCandidates = candidates.size(); numCandidates > 0; --numCandidates) { + candidates.set(numGroups - candidate - 1, false); + + // Check if the candidate row group has an unprocessed successor + bool hasUnprocessedSuccessor = false; + for (auto const& entry : this->A.getRowGroup(candidate)) { + if (!processedGroups.get(entry.getColumn())) { + hasUnprocessedSuccessor = true; + break; + } + } + + uint64_t nextCandidate = numGroups - candidates.getNextSetIndex(numGroups - candidate - 1 + 1) - 1; + + if (!hasUnprocessedSuccessor) { + // This candidate can be processed. + processedGroups.set(candidate); + computeOptimalValueForRowGroup(candidate, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[candidate] : nullptr); + if (this->isCachingEnabled()) { + rowGroupOrdering->push_back(candidate); + } + + // Add new candidates + for (auto const& predecessorEntry : transposedMatrix.getRow(candidate)) { + uint64_t predecessor = predecessorEntry.getColumn(); + if (!candidates.get(numGroups - predecessor - 1)) { + candidates.set(numGroups - predecessor - 1, true); + nextCandidate = std::max(nextCandidate, predecessor); + ++numCandidates; + } + } + } + candidate = nextCandidate; + } + + assert(candidates.empty()); + STORM_LOG_THROW(processedGroups.full(), storm::exceptions::InvalidOperationException, "The MinMax equation system is not acyclic."); + return true; + } + + template + void StandardMinMaxLinearEquationSolver::computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector& x, std::vector const& b, uint_fast64_t* choice) const { + uint64_t row = this->A.getRowGroupIndices()[group]; + uint64_t groupEnd = this->A.getRowGroupIndices()[group + 1]; + assert(row != groupEnd); + + auto bIt = b.begin() + row; + ValueType& xi = x[group]; + xi = this->A.multiplyRowWithVector(row, x) + *bIt; + uint64_t optimalRow = row; + + for (++row, ++bIt; row < groupEnd; ++row, ++bIt) { + ValueType choiceVal = this->A.multiplyRowWithVector(row, x) + *bIt; + if (minimize(dir)) { + if (choiceVal < xi) { + xi = choiceVal; + optimalRow = row; + } + } else { + if (choiceVal > xi) { + xi = choiceVal; + optimalRow = row; + } + } + } + if (choice != nullptr) { + *choice = optimalRow - this->A.getRowGroupIndices()[group]; + } + } + template void StandardMinMaxLinearEquationSolver::repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const { if(!linEqSolverA) { @@ -356,6 +466,7 @@ namespace storm { linEqSolverA.reset(); auxiliaryRowVector.reset(); auxiliaryRowGroupVector.reset(); + rowGroupOrdering.reset(); MinMaxLinearEquationSolver::clearCache(); } diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.h b/src/storm/solver/StandardMinMaxLinearEquationSolver.h index f7e1e40c6..050ce0bde 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.h +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.h @@ -12,7 +12,7 @@ namespace storm { StandardMinMaxLinearEquationSolverSettings(); enum class SolutionMethod { - ValueIteration, PolicyIteration + ValueIteration, PolicyIteration, Acyclic }; void setSolutionMethod(SolutionMethod const& solutionMethod); @@ -51,9 +51,12 @@ namespace storm { private: bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; bool solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; + bool solveEquationsAcyclic(OptimizationDirection dir, std::vector& x, std::vector const& b) const; bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const; + void computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector& x, std::vector const& b, uint_fast64_t* choice = nullptr) const; + enum class Status { Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress }; @@ -62,7 +65,8 @@ namespace storm { mutable std::unique_ptr> linEqSolverA; mutable std::unique_ptr> auxiliaryRowVector; // A.rowCount() entries mutable std::unique_ptr> auxiliaryRowGroupVector; // A.rowGroupCount() entries - + mutable std::unique_ptr> rowGroupOrdering; // A.rowGroupCount() entries + Status updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations) const; void reportStatus(Status status, uint64_t iterations) const; diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 99a716415..1a005d2d0 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -104,17 +104,25 @@ namespace storm { } template - SparseMatrixBuilder::SparseMatrixBuilder(SparseMatrix&& matrix) : initialRowCountSet(false), initialRowCount(0), initialColumnCountSet(false), initialColumnCount(0), initialEntryCountSet(false), initialEntryCount(0), forceInitialDimensions(false), hasCustomRowGrouping(!matrix.trivialRowGrouping), initialRowGroupCountSet(false), initialRowGroupCount(0), rowGroupIndices(), columnsAndValues(std::move(matrix.columnsAndValues)), rowIndications(std::move(matrix.rowIndications)), currentEntryCount(matrix.entryCount), lastRow(matrix.rowCount - 1), lastColumn(columnsAndValues.back().getColumn()), highestColumn(matrix.getColumnCount() - 1), currentRowGroup() { + SparseMatrixBuilder::SparseMatrixBuilder(SparseMatrix&& matrix) : initialRowCountSet(false), initialRowCount(0), initialColumnCountSet(false), initialColumnCount(0), initialEntryCountSet(false), initialEntryCount(0), forceInitialDimensions(false), hasCustomRowGrouping(!matrix.trivialRowGrouping), initialRowGroupCountSet(false), initialRowGroupCount(0), rowGroupIndices(), columnsAndValues(std::move(matrix.columnsAndValues)), rowIndications(std::move(matrix.rowIndications)), currentEntryCount(matrix.entryCount), currentRowGroup() { + + lastRow = matrix.rowCount == 0 ? 0 : matrix.rowCount - 1; + lastColumn = columnsAndValues.empty() ? 0 : columnsAndValues.back().getColumn(); + highestColumn = matrix.getColumnCount() == 0 ? 0 : matrix.getColumnCount() - 1; // If the matrix has a custom row grouping, we move it and remove the last element to make it 'open' again. if (hasCustomRowGrouping) { rowGroupIndices = std::move(matrix.rowGroupIndices); - rowGroupIndices.get().pop_back(); - currentRowGroup = rowGroupIndices.get().size() - 1; + if (!rowGroupIndices->empty()) { + rowGroupIndices.get().pop_back(); + } + currentRowGroup = rowGroupIndices->empty() ? 0 : rowGroupIndices.get().size() - 1; } // Likewise, we need to 'open' the row indications again. - rowIndications.pop_back(); + if (!rowIndications.empty()) { + rowIndications.pop_back(); + } } template @@ -191,7 +199,10 @@ namespace storm { template SparseMatrix SparseMatrixBuilder::build(index_type overriddenRowCount, index_type overriddenColumnCount, index_type overriddenRowGroupCount) { - uint_fast64_t rowCount = lastRow + 1; + + bool hasEntries = currentEntryCount != 0; + + uint_fast64_t rowCount = hasEntries ? lastRow + 1 : 0; if (initialRowCountSet && forceInitialDimensions) { STORM_LOG_THROW(rowCount <= initialRowCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowCount << " rows, but got " << rowCount << "."); rowCount = std::max(rowCount, initialRowCount); @@ -203,12 +214,17 @@ namespace storm { rowIndications.push_back(currentEntryCount); } + // If there are no rows, we need to erase the start index of the current (non-existing) row. + if (rowCount == 0) { + rowIndications.pop_back(); + } + // We put a sentinel element at the last position of the row indices array. This eases iteration work, // as now the indices of row i are always between rowIndications[i] and rowIndications[i + 1], also for // the first and last row. rowIndications.push_back(currentEntryCount); - - uint_fast64_t columnCount = highestColumn + 1; + assert(rowCount == rowIndications.size() - 1); + uint_fast64_t columnCount = hasEntries ? highestColumn + 1 : 0; if (initialColumnCountSet && forceInitialDimensions) { STORM_LOG_THROW(columnCount <= initialColumnCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialColumnCount << " columns, but got " << columnCount << "."); columnCount = std::max(columnCount, initialColumnCount); @@ -300,7 +316,7 @@ namespace storm { } highestColumn = maxColumn; - lastColumn = columnsAndValues[columnsAndValues.size() - 1].getColumn(); + lastColumn = columnsAndValues.empty() ? 0 : columnsAndValues[columnsAndValues.size() - 1].getColumn(); } template diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp index 9a82be279..f7aa3236d 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp @@ -1,6 +1,6 @@ #include "storm/storage/expressions/ToRationalNumberVisitor.h" -#include "storm/utility/macros.h" + #include "storm/utility/constants.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/NotSupportedException.h" @@ -75,7 +75,7 @@ namespace storm { break; case BinaryNumericalFunctionExpression::OperatorType::Power: STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalNumber), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer."); - uint_fast64_t exponentAsInteger = storm::utility::convertNumber(secondOperandAsRationalNumber); + uint_fast64_t exponentAsInteger = storm::utility::convertNumber(secondOperandAsRationalNumber); result = storm::utility::pow(firstOperandAsRationalNumber, exponentAsInteger); return result; break; @@ -128,22 +128,12 @@ namespace storm { template boost::any ToRationalNumberVisitor::visit(IntegerLiteralExpression const& expression, boost::any const&) { - (void)expression; -#ifdef STORM_HAVE_CARL - return RationalNumberType(carl::rationalize(static_cast(expression.getValue()))); -#else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build."); -#endif + return RationalNumberType(carl::rationalize(static_cast(expression.getValue()))); } template boost::any ToRationalNumberVisitor::visit(RationalLiteralExpression const& expression, boost::any const&) { - (void)expression; -#ifdef STORM_HAVE_CARL return expression.getValue(); -#else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build."); -#endif } template @@ -151,8 +141,8 @@ namespace storm { valueMapping[variable] = value; } -#ifdef STORM_HAVE_CARL + template class ToRationalNumberVisitor; -#endif + } } diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 65cab6fb1..5fde8267a 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -194,11 +194,14 @@ namespace storm { upperExclusive = f.isUpperBoundStrict(); } modernjson::json propertyInterval = constructPropertyInterval(lower, lowerExclusive, upper, upperExclusive); - - if(f.isStepBounded()) { + + auto tbr = f.getTimeBoundReference(); + if(tbr.isStepBound()) { opDecl["step-bounds"] = propertyInterval; - } else { + } else if(tbr.isRewardBound()) { opDecl["time-bounds"] = propertyInterval; + } else { + opDecl["reward-bounds"] = propertyInterval; } return opDecl; } diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp index e46d2ee50..73c6d0dec 100644 --- a/src/storm/storage/jani/Property.cpp +++ b/src/storm/storage/jani/Property.cpp @@ -5,19 +5,17 @@ namespace storm { std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) { - return os << "Obtain " << toString(fe.getFilterType()) << " of the 'initial'-states with values described by '" << *fe.getFormula() << "'"; + return os << "Obtain " << toString(fe.getFilterType()) << " of the '" << fe.getStatesFormula() << "'-states with values described by '" << *fe.getFormula() << "'"; } Property::Property(std::string const& name, std::shared_ptr const& formula, std::string const& comment) - : name(name), comment(comment), filterExpression(FilterExpression(formula)) - { - + : name(name), comment(comment), filterExpression(FilterExpression(formula)) { + // Intentionally left empty. } Property::Property(std::string const& name, FilterExpression const& fe, std::string const& comment) - : name(name), comment(comment), filterExpression(fe) - { - + : name(name), comment(comment), filterExpression(fe) { + // Intentionally left empty. } std::string const& Property::getName() const { @@ -48,6 +46,5 @@ namespace storm { return os << "(" << p.getName() << ") : " << p.getFilter(); } - } } diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h index 52db07fef..74aceab5c 100644 --- a/src/storm/storage/jani/Property.h +++ b/src/storm/storage/jani/Property.h @@ -2,6 +2,10 @@ #include "storm/modelchecker/results/FilterType.h" #include "storm/logic/Formulas.h" +#include "storm/logic/FragmentSpecification.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" namespace storm { namespace jani { @@ -30,28 +34,35 @@ namespace storm { public: FilterExpression() = default; - explicit FilterExpression(std::shared_ptr formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : formula(formula), ft(ft) {} + explicit FilterExpression(std::shared_ptr formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES, std::shared_ptr const& statesFormula = std::make_shared("init")) : formula(formula), ft(ft), statesFormula(statesFormula) { + STORM_LOG_THROW(statesFormula->isInFragment(storm::logic::propositional()), storm::exceptions::InvalidArgumentException, "Can only filter by propositional formula."); + } std::shared_ptr const& getFormula() const { return formula; } + std::shared_ptr const& getStatesFormula() const { + return statesFormula; + } + storm::modelchecker::FilterType getFilterType() const { return ft; } FilterExpression substitute(std::map const& substitution) const { - return FilterExpression(formula->substitute(substitution), ft); + return FilterExpression(formula->substitute(substitution), ft, statesFormula->substitute(substitution)); } FilterExpression substituteLabels(std::map const& labelSubstitution) const { - return FilterExpression(formula->substitute(labelSubstitution), ft); + return FilterExpression(formula->substitute(labelSubstitution), ft, statesFormula->substitute(labelSubstitution)); } private: // For now, we assume that the states are always the initial states. std::shared_ptr formula; storm::modelchecker::FilterType ft; + std::shared_ptr statesFormula; }; diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 35d79c13f..67ac0a6b8 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -256,7 +256,7 @@ namespace storm { template<> uint_fast64_t convertNumber(ClnRationalNumber const& number) { - return carl::toInt(number); + return carl::toInt(number); } template<> @@ -386,7 +386,7 @@ namespace storm { template<> uint_fast64_t convertNumber(GmpRationalNumber const& number){ - return carl::toInt(number); + return carl::toInt(number); } template<> @@ -549,8 +549,8 @@ namespace storm { #endif template<> - uint_fast64_t convertNumber(RationalFunction const& func) { - return carl::toInt(convertNumber(func)); + carl::uint convertNumber(RationalFunction const& func) { + return carl::toInt(convertNumber(func)); } template<> diff --git a/src/test/storm/parser/FormulaParserTest.cpp b/src/test/storm/parser/FormulaParserTest.cpp index 012555e8b..6269a082c 100644 --- a/src/test/storm/parser/FormulaParserTest.cpp +++ b/src/test/storm/parser/FormulaParserTest.cpp @@ -71,6 +71,35 @@ TEST(FormulaParserTest, ProbabilityOperatorTest) { EXPECT_FALSE(formula->asProbabilityOperatorFormula().hasOptimalityType()); } +TEST(FormulaParserTest, UntilOperatorTest) { + // API does not allow direct test of until, so we have to pack it in a probability operator. + storm::parser::FormulaParser formulaParser; + + std::string input = "P<0.9 [\"a\" U \"b\"]"; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& nested1 = formula->asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(nested1.isUntilFormula()); + EXPECT_FALSE(nested1.isBoundedUntilFormula()); + + input = "P<0.9 [\"a\" U<=3 \"b\"]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& nested2 = formula->asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(nested2.isBoundedUntilFormula()); + EXPECT_TRUE(nested2.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); + EXPECT_EQ(3, nested2.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); + + input = "P<0.9 [\"a\" U{\"rewardname\"}<=3 \"b\"]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& nested3 = formula->asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(nested3.isBoundedUntilFormula()); + EXPECT_TRUE(nested3.asBoundedUntilFormula().getTimeBoundReference().isRewardBound()); // This will fail, as we have not finished the parser. + //EXPECT_EQ("rewardname", nested3.asBoundedUntilFormula().getTimeBoundReference().getRewardName()); + EXPECT_EQ(3, nested3.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); + // TODO: Extend as soon as it does not crash anymore. +} + + TEST(FormulaParserTest, RewardOperatorTest) { storm::parser::FormulaParser formulaParser;