diff --git a/.travis.yml b/.travis.yml index fcc0a9a2f..4995abe2d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -291,6 +291,10 @@ jobs: - docker cp storm:/storm/. . after_failure: - find build -iname '*err*.log' -type f -print -exec cat {} \; + after_success: + - docker login -u "$DOCKER_USERNAME" -p "$DOCKER_PASSWORD"; + - docker commit storm mvolk/storm-debug:travis; + - docker push mvolk/storm-debug:travis; - stage: Test all os: linux compiler: gcc @@ -303,4 +307,8 @@ jobs: - docker cp storm:/storm/. . after_failure: - find build -iname '*err*.log' -type f -print -exec cat {} \; + after_success: + - docker login -u "$DOCKER_USERNAME" -p "$DOCKER_PASSWORD"; + - docker commit storm mvolk/storm:travis; + - docker push mvolk/storm:travis; diff --git a/CHANGELOG.md b/CHANGELOG.md index 9976e61cb..5832b1e35 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,9 +7,12 @@ The releases of major and minor versions contain an overview of changes since th Version 1.2.x ------------- -### Version 1.2.0 -- C++ api changes: Building model takes BuilderOptions instead of extended list of Booleans, does not depend on settings anymore. -- storm-cli-utilities now contains cli related stuff, instead of storm-lib +### Version 1.2.1 (to be released) +- Multi-dimensional reward bounded reachability properties for DTMCs. + +### Version 1.2.0 (2017/12) +- C++ api changes: Building model takes `BuilderOptions` instead of extended list of Booleans, does not depend on settings anymore. +- `storm-cli-utilities` now contains cli related stuff, instead of `storm-lib` - Symbolic (MT/BDD) bisimulation - Fixed issue related to variable names that can not be used in Exprtk. - DRN parser improved @@ -22,9 +25,9 @@ Version 1.2.x - Performance improvements for conditional properties on MDPs - Automatically convert MA without probabilistic states into CTMC - Fixed implemention of Fox and Glynn' algorithm -- storm-pars: support for welldefinedness constraints in mdps. -- storm-dft: split DFT settings into IO settings and fault tree settings -- storm-dft: removed obsolete explicit model builder for DFTs +- `storm-pars`: support for welldefinedness constraints in mdps. +- `storm-dft`: split DFT settings into IO settings and fault tree settings +- `storm-dft`: removed obsolete explicit model builder for DFTs - Features for developers: * Solvers can now expose requirements * unbounded reachability and reachability rewards now correctly respect solver requirements @@ -36,10 +39,9 @@ Version 1.1.x ------------- ### Version 1.1.0 (2017/8) - - Support for long-run average rewards on MDPs and Markov automata using a value-iteration based approach. - Storm can now check MDPs and Markov Automata (i.e. MinMax equation systems) via Linear Programming. -- Parametric model checking is now handled in a separated library/executable called storm-pars. +- Parametric model checking is now handled in a separated library/executable called `storm-pars`. - Wellformedness constraints on PMCs: * include constraints from rewards * are in smtlib2 @@ -50,15 +52,14 @@ Version 1.1.x - Support for parsing/building models given in the explicit input format of IMCA. - 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. -- 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 +- `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 Version 1.0.x ------------- ### Version 1.0.1 (2017/4) - - Multi-objective model checking support now fully included - Several improvements in parameter lifting - Several improvements in JANI parsing diff --git a/CMakeLists.txt b/CMakeLists.txt index c0d958476..0edec97d7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -105,6 +105,8 @@ if(STORM_COMPILE_WITH_CCACHE) else() message(STATUS "Storm - Could not find ccache.") endif() +else() + message(STATUS "Storm - Disabled use of ccache.") endif() # Directory for test resources. diff --git a/doc/checklist_new_release.md b/doc/checklist_new_release.md new file mode 100644 index 000000000..05be534aa --- /dev/null +++ b/doc/checklist_new_release.md @@ -0,0 +1,37 @@ +The following steps should be performed before releasing a new storm version. +Note that in most case a simultaneous release of [carl](https://github.com/smtrat/carl), [storm](https://github.com/moves-rwth/storm), [pycarl](https://github.com/moves-rwth/pycarl/) and [stormpy](https://github.com/moves-rwth/stormpy/) is preferred. + +1. Update `CHANGELOG.md` + To get all the commits from an author since the last tag execute: + ```console + git log last_tag..HEAD --author "author_name" + ``` + +2. Update used carl version: + * Update `GIT_TAG` in `resources/3rdparty/carl/CMakeLists.txt` + * Maybe update `CARL_MINVERSION` in `resources/3rdparty/CMakeLists.txt` + +3. Check that storm builds without errors and all tests are successful + * [Travis](https://travis-ci.org/moves-rwth/storm) should run successfully + * Invoke the script test_build_configurations.py to build and check different cmake configurations + +4. Set new storm version: + * Set new storm version in `version.cmake` + +5. Set new tag in git + ```console + git tag -a new_version + git push origin new_version + ``` + Next we push the tag to GitHub. This step requires the GitHub repo to to be configured as a remote. + ```console + git remote add github https://github.com/moves-rwth/storm.git + git push github new_version + ``` + The new tag should now be visible on [GitHub](https://github.com/moves-rwth/storm/tags) + +6. [Add new release](https://github.com/moves-rwth/storm/releases/new) in GitHub + +7. Update [Homebrew formula](https://github.com/moves-rwth/homebrew-storm) + +8. Announce new storm version on [website](http://www.stormchecker.org/news.html) diff --git a/doc/scripts/test_build_configurations.py b/doc/scripts/test_build_configurations.py new file mode 100644 index 000000000..56baccf0d --- /dev/null +++ b/doc/scripts/test_build_configurations.py @@ -0,0 +1,118 @@ +import subprocess +import os +import shutil +import time +import math +import sys + +logfileDir = "test_build_configurations_logs" +pathToConfigFile = "" +globalCmakeArguments = "" +globalMakeArguments = "" + +if len(sys.argv) == 1 or len(sys.argv) > 5: + print "Usage: " + sys.argv[0] + "/path/to/storm /path/to/configurations.txt \"optional make arguments\" \"optional cmake arguments\"" + print "Example: " + sys.argv[0] + " ~/storm test_build_configurations.txt \"-j 48 -k\" \"-DZ3_ROOT=/path/to/z3/\"" + sys.exit(0) + +pathToStorm = sys.argv[1] +pathToConfigFile = sys.argv[2] + +if len(sys.argv) > 3: + globalMakeArguments = sys.argv[3] + print globalMakeArguments +if len(sys.argv) > 4: + globalCmakeArguments = sys.argv[4] + print globalCmakeArguments + +# create directory for log files +if not os.path.exists(logfileDir): + os.makedirs(logfileDir) + +unsuccessfulConfigs = "" +globalStartTime = time.time() + +with open(pathToConfigFile) as configfile: + localStartTime = time.time() + configId=0 + for localCmakeArguments in configfile: + + cmakeArguments = globalCmakeArguments + " " + localCmakeArguments.strip('\n') + buildDir = os.path.join(pathToStorm, "build{}".format(configId)) + logfilename = os.path.join(logfileDir, "build{}".format(configId) + "_" + time.strftime("%Y-%m-%d-%H-%M-%S") + ".log") + + + print "Building configuration {} with cmake options ".format(configId) + cmakeArguments + print "\tCreating log file " + logfilename + " ..." + with open(logfilename, "w") as logfile: + success=True + logfile.write("Log for test configuration " + cmakeArguments + "\n") + + print "\tCreating build directory" + buildDir + " ..." + if os.path.exists(buildDir): + print "\t\tRemoving existing directory " + buildDir + shutil.rmtree(buildDir, ignore_errors=True) + os.makedirs(buildDir) + logfile.write("Build directory is " + buildDir + "\n") + print "\t\tdone" + + if success: + print "\tInvoking cmake ..." + cmakeCommand = "cmake .. {}".format(cmakeArguments) + logfile.write ("\n\n CALLING CMAKE \n\n" + cmakeCommand + "\n") + try: + cmakeOutput = subprocess.check_output("cd " + buildDir + "; " + cmakeCommand , shell=True,stderr=subprocess.STDOUT) + print "\t\tdone" + logfile.write(cmakeOutput) + except subprocess.CalledProcessError as e: + success=False + print "\t\tfail" + print e.output + logfile.write(e.output) + + if success: + print "\tInvoking make ..." + makeCommand = "make {}".format(globalMakeArguments) + logfile.write ("\n\n CALLING MAKE \n\n" + makeCommand + "\n") + try: + makeOutput = subprocess.check_output("cd " + buildDir + "; " + makeCommand , shell=True,stderr=subprocess.STDOUT) + print "\t\tdone" + logfile.write(makeOutput) + except subprocess.CalledProcessError as e: + success=False + print "\t\tfail" + print e.output + logfile.write(e.output) + + if success: + print "\tInvoking make check..." + makeCheckCommand = "make check" + logfile.write ("\n\n CALLING MAKE CHECK \n\n" + makeCheckCommand + "\n") + try: + makeCheckOutput = subprocess.check_output("cd " + buildDir + "; " + makeCheckCommand , shell=True,stderr=subprocess.STDOUT) + print "\t\tdone" + logfile.write(makeCheckOutput) + except subprocess.CalledProcessError as e: + success=False + print "\t\tfail" + print e.output + logfile.write(e.output) + + localEndTime = time.time() + if success: + print "\tConfiguration build and tested successfully within {} minutes.".format(int((localEndTime - localStartTime)/60)) + else: + print "\tAn error occurred for this configuration." + unsuccessfulConfigs += buildDir + " with arguments " + cmakeArguments + "\n" + + configId += 1 +globalEndTime = time.time() +print "All tests completed after {} minutes.".format(int((globalEndTime - globalStartTime)/60)) +if unsuccessfulConfigs == "": + print "All configurations were build and tested successfully." +else: + print "The following configurations failed: \n" + unsuccessfulConfigs + + + + diff --git a/doc/scripts/test_build_configurations.txt b/doc/scripts/test_build_configurations.txt new file mode 100644 index 000000000..3688e8eab --- /dev/null +++ b/doc/scripts/test_build_configurations.txt @@ -0,0 +1,5 @@ +-DSTORM_USE_CLN_EA=OFF -DSTORM_USE_CLN_RF=OFF +-DSTORM_USE_CLN_EA=OFF -DSTORM_USE_CLN_RF=ON +-DSTORM_USE_CLN_EA=ON -DSTORM_USE_CLN_RF=OFF +-DSTORM_USE_CLN_EA=ON -DSTORM_USE_CLN_RF=ON +-DCMAKE_BUILD_TYPE=DEBUG -DSTORM_DEVELOPER=ON \ No newline at end of file diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index b69832778..979c5cbe8 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -208,7 +208,7 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake) ############################################################# set(STORM_HAVE_CARL OFF) -set(CARL_MINVERSION "17.08") +set(CARL_MINVERSION "17.12") if (NOT STORM_FORCE_SHIPPED_CARL) if (NOT "${STORM_CARL_DIR_HINT}" STREQUAL "") find_package(carl QUIET PATHS ${STORM_CARL_DIR_HINT} NO_DEFAULT_PATH) @@ -226,7 +226,7 @@ if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL) else() message(SEND_ERROR "File ${carlLOCATION} does not exist, did you build carl?") endif() - if("${carl_VERSION}" VERSION_LESS "${CARL_MINVERSION}") + if("${carl_VERSION_MAJOR}.${carl_VERSION_MINOR}" VERSION_LESS "${CARL_MINVERSION}") message(SEND_ERROR "Carl outdated, require ${CARL_MINVERSION}, have ${carl_VERSION}") endif() diff --git a/resources/3rdparty/carl/CMakeLists.txt b/resources/3rdparty/carl/CMakeLists.txt index dcab4ec30..4b819682d 100644 --- a/resources/3rdparty/carl/CMakeLists.txt +++ b/resources/3rdparty/carl/CMakeLists.txt @@ -8,7 +8,7 @@ message(STORM_3RDPARTY_BINARY_DIR: ${STORM_3RDPARTY_BINARY_DIR}) ExternalProject_Add(carl-config GIT_REPOSITORY https://github.com/smtrat/carl - GIT_TAG 17.10 + GIT_TAG 17.12 PREFIX here SOURCE_DIR source_dir BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl diff --git a/resources/examples/testfiles/dtmc/crowds_cost_bounded.pm b/resources/examples/testfiles/dtmc/crowds_cost_bounded.pm new file mode 100644 index 000000000..d781dadc9 --- /dev/null +++ b/resources/examples/testfiles/dtmc/crowds_cost_bounded.pm @@ -0,0 +1,260 @@ +// CROWDS [Reiter,Rubin] +// Vitaly Shmatikov, 2002 + +// Note: +// Change everything marked CWDSIZ when changing the size of the crowd +// Change everything marked CWDMAX when increasing max size of the crowd + +dtmc + +// Probability of forwarding +const double PF = 0.8; + +// Probability that a crowd member is bad +const double badC = 0.091; +// const double badC = 0.167; + +const int CrowdSize; // CWDSIZ: actual number of good crowd members +const int MaxGood=20; // CWDMAX: maximum number of good crowd members + +// Process definitions +module crowds + + // Auxiliary variables + launch: bool init true; // Start modeling? + new: bool init false; // Initialize a new protocol instance? + start: bool init false; // Start the protocol? + run: bool init false; // Run the protocol? + lastSeen: [0..MaxGood] init MaxGood; // Last crowd member to touch msg + good: bool init false; // Crowd member is good? + bad: bool init false; // ... bad? + recordLast: bool init false; // Record last seen crowd member? + badObserve: bool init false; // Bad members observes who sent msg? + deliver: bool init false; // Deliver message to destination? + done: bool init false; // Protocol instance finished? + + [] launch -> (new'=true) & (launch'=false); + // Set up a new protocol instance + [newrun] new -> (new'=false) & (start'=true); + + // SENDER + // Start the protocol + [] start -> (lastSeen'=0) & (run'=true) & (deliver'=false) & (start'=false); + + // CROWD MEMBERS + // Good or bad crowd member? + [] !good & !bad & !deliver & run -> + 1-badC : (good'=true) & (recordLast'=true) & (run'=false) + + badC : (bad'=true) & (badObserve'=true) & (run'=false); + + // GOOD MEMBERS + // Forward with probability PF, else deliver + [] good & !deliver & run -> PF : (good'=false) + 1-PF : (deliver'=true); + // Record the last crowd member who touched the msg; + // all good members may appear with equal probability + // Note: This is backward. In the real protocol, each honest + // forwarder randomly chooses the next forwarder. + // Here, the identity of an honest forwarder is randomly + // chosen *after* it has forwarded the message. + [] recordLast & CrowdSize=2 -> + 1/2 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/2 : (lastSeen'=1) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=4 -> + 1/4 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/4 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/4 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/4 : (lastSeen'=3) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=5 -> + 1/5 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/5 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/5 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/5 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + + 1/5 : (lastSeen'=4) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=10 -> + 1/10 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=9) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=15 -> + 1/15 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=9) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=10) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=11) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=12) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=13) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=14) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=20 -> + 1/20 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=9) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=10) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=11) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=12) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=13) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=14) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=15) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=16) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=17) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=18) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=19) & (recordLast'=false) & (run'=true); + + // BAD MEMBERS + // Remember from whom the message was received and deliver + // CWDMAX: 1 rule per each good crowd member + [obs0] lastSeen=0 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs1] lastSeen=1 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs2] lastSeen=2 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs3] lastSeen=3 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs4] lastSeen=4 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs5] lastSeen=5 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs6] lastSeen=6 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs7] lastSeen=7 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs8] lastSeen=8 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs9] lastSeen=9 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs10] lastSeen=10 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs11] lastSeen=11 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs12] lastSeen=12 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs13] lastSeen=13 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs14] lastSeen=14 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs15] lastSeen=15 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs16] lastSeen=16 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs17] lastSeen=17 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs18] lastSeen=18 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs19] lastSeen=19 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + + // RECIPIENT + // Delivery to destination + [] deliver & run -> (done'=true) & (deliver'=false) & (run'=false) & (good'=false) & (bad'=false); + // Start a new instance + [] done -> (new'=true) & (done'=false) & (run'=false) & (lastSeen'=MaxGood); + +endmodule + +rewards "num_runs" + [newrun] true : 1; +endrewards + +rewards "observe0" + [obs0] true : 1; +endrewards + +rewards "observe1" + [obs1] true : 1; +endrewards + +rewards "observe2" + [obs2] true : 1; +endrewards + +rewards "observe3" + [obs3] true : 1; +endrewards + +rewards "observe4" + [obs4] true : 1; +endrewards + +rewards "observe5" + [obs5] true : 1; +endrewards + +rewards "observe6" + [obs6] true : 1; +endrewards + +rewards "observe7" + [obs7] true : 1; +endrewards + +rewards "observe8" + [obs8] true : 1; +endrewards + +rewards "observe9" + [obs9] true : 1; +endrewards + +rewards "observe10" + [obs10] true : 1; +endrewards + +rewards "observe11" + [obs11] true : 1; +endrewards + +rewards "observe12" + [obs12] true : 1; +endrewards + +rewards "observe13" + [obs13] true : 1; +endrewards + +rewards "observe14" + [obs14] true : 1; +endrewards + +rewards "observe15" + [obs15] true : 1; +endrewards + +rewards "observe16" + [obs16] true : 1; +endrewards + +rewards "observe17" + [obs17] true : 1; +endrewards + +rewards "observe18" + [obs18] true : 1; +endrewards + +rewards "observe19" + [obs19] true : 1; +endrewards + +rewards "observeI" + [obs1] true : 1; + [obs2] true : 1; + [obs3] true : 1; + [obs4] true : 1; + [obs5] true : 1; + [obs6] true : 1; + [obs7] true : 1; + [obs8] true : 1; + [obs9] true : 1; + [obs10] true : 1; + [obs11] true : 1; + [obs12] true : 1; + [obs13] true : 1; + [obs14] true : 1; + [obs15] true : 1; + [obs16] true : 1; + [obs17] true : 1; + [obs18] true : 1; + [obs19] true : 1; +endrewards + + diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 8cf964ca5..4180bdc33 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -373,8 +373,7 @@ namespace storm { STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Counterexample generation is currently only supported for sparse models."); auto sparseModel = model->as>(); - STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for MDPs."); - auto mdp = sparseModel->template as>(); + STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for discrete-time models."); auto counterexampleSettings = storm::settings::getModule(); if (counterexampleSettings.isMinimalCommandSetGenerationSet()) { @@ -387,9 +386,15 @@ namespace storm { printComputingCounterexample(property); storm::utility::Stopwatch watch(true); if (useMilp) { - counterexample = storm::api::computePrismHighLevelCounterexampleMilp(program, mdp, property.getRawFormula()); + STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample generation using MILP is currently only supported for MDPs."); + counterexample = storm::api::computePrismHighLevelCounterexampleMilp(program, sparseModel->template as>(), property.getRawFormula()); } else { - counterexample = storm::api::computePrismHighLevelCounterexampleMaxSmt(program, mdp, property.getRawFormula()); + STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample generation using MaxSAT is currently only supported for discrete-time models."); + if (sparseModel->isOfType(storm::models::ModelType::Dtmc)) { + counterexample = storm::api::computePrismHighLevelCounterexampleMaxSmt(program, sparseModel->template as>(), property.getRawFormula()); + } else { + counterexample = storm::api::computePrismHighLevelCounterexampleMaxSmt(program, sparseModel->template as>(), property.getRawFormula()); + } } watch.stop(); printCounterexample(counterexample, &watch); diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 8a8c9fa6a..8546f81d1 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -165,7 +165,8 @@ namespace storm { auto parametricSettings = storm::settings::getModule(); if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) { auto dtmc = model->template as>(); - storm::api::exportParametricResultToFile(boost::make_optional(result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]),storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); + boost::optional rationalFunction = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; + storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); } }); } diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h index 27d35d526..56aba0cf3 100644 --- a/src/storm-pars/api/region.h +++ b/src/storm-pars/api/region.h @@ -81,7 +81,7 @@ namespace storm { } template - std::shared_ptr> initializeParameterLiftingRegionModelChecker(Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::shared_ptr> initializeParameterLiftingRegionModelChecker(Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) { STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually..."); @@ -105,13 +105,13 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); } - checker->specify(env, consideredModel, task); + checker->specify(env, consideredModel, task, generateSplitEstimates, allowModelSimplification); return checker; } template - std::shared_ptr> initializeValidatingRegionModelChecker(Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::shared_ptr> initializeValidatingRegionModelChecker(Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) { STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually..."); @@ -135,7 +135,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); } - checker->specify(env, consideredModel, task); + checker->specify(env, consideredModel, task, generateSplitEstimates, allowModelSimplification); return checker; } diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp index b3669e9b8..2b2e8a350 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp @@ -11,13 +11,12 @@ #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" -#include "storm/exceptions/NotSupportedException.h" -#include "storm/exceptions/InvalidStateException.h" -#include "storm/exceptions/InvalidArgumentException.h" - #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/InvalidStateException.h" +#include "storm/exceptions/InvalidArgumentException.h" namespace storm { @@ -152,6 +151,18 @@ namespace storm { auto regionCopyForResult = region; return std::make_unique>(std::move(result), std::move(regionCopyForResult)); } + + template + bool RegionModelChecker::isRegionSplitEstimateSupported() const { + return false; + } + + template + std::map::VariableType, double> RegionModelChecker::getRegionSplitEstimate() const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Region split estimation is not supported by this region model checker."); + return std::map::VariableType, double>(); + } + #ifdef STORM_HAVE_CARL template class RegionModelChecker; diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h index fc9997c3c..11cf160e4 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.h +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.h @@ -22,12 +22,14 @@ namespace storm { public: typedef typename storm::storage::ParameterRegion::CoefficientType CoefficientType; + typedef typename storm::storage::ParameterRegion::VariableType VariableType; RegionModelChecker(); virtual ~RegionModelChecker() = default; virtual bool canHandle(std::shared_ptr parametricModel, CheckTask const& checkTask) const = 0; - virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask) = 0; + virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplifications = true) = 0; + /*! * Analyzes the given region. @@ -44,7 +46,7 @@ namespace storm { * If supported by this model checker, it is possible to sample the vertices of the regions whenever AllSat/AllViolated could not be shown. */ std::unique_ptr> analyzeRegions(Environment const& env, std::vector> const& regions, std::vector const& hypotheses, bool sampleVerticesOfRegion = false) ; - + virtual ParametricType getBoundAtInitState(Environment const& env, storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters); /*! @@ -57,6 +59,17 @@ namespace storm { */ std::unique_ptr> performRegionRefinement(Environment const& env, storm::storage::ParameterRegion const& region, boost::optional const& coverageThreshold, boost::optional depthThreshold = boost::none, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown); + /*! + * Returns true if region split estimation (a) was enabled when model and check task have been specified and (b) is supported by this region model checker. + */ + virtual bool isRegionSplitEstimateSupported() const; + + /*! + * Returns an estimate of the benefit of splitting the last checked region with respect to each parameter. This method should only be called if region split estimation is supported and enabled. + * If a parameter is assigned a high value, we should prefer splitting with respect to this parameter. + */ + virtual std::map getRegionSplitEstimate() const; + }; } //namespace modelchecker diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 7bce00c6a..b5c2ab11e 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -19,6 +19,7 @@ #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/UncheckedRequirementException.h" @@ -31,7 +32,7 @@ namespace storm { } template - SparseDtmcParameterLiftingModelChecker::SparseDtmcParameterLiftingModelChecker(std::unique_ptr>&& solverFactory) : solverFactory(std::move(solverFactory)), solvingRequiresUpperRewardBounds(false) { + SparseDtmcParameterLiftingModelChecker::SparseDtmcParameterLiftingModelChecker(std::unique_ptr>&& solverFactory) : solverFactory(std::move(solverFactory)), solvingRequiresUpperRewardBounds(false), regionSplitEstimationsEnabled(false) { // Intentionally left empty } @@ -47,18 +48,19 @@ namespace storm { } template - void SparseDtmcParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask) { + void SparseDtmcParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplification) { auto dtmc = parametricModel->template as(); - specify(env, dtmc, checkTask, false); + specify_internal(env, dtmc, checkTask, generateRegionSplitEstimates, !allowModelSimplification); } template - void SparseDtmcParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool skipModelSimplification) { - + void SparseDtmcParameterLiftingModelChecker::specify_internal(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) { STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this."); - + reset(); + regionSplitEstimationsEnabled = generateRegionSplitEstimates; + if (skipModelSimplification) { this->parametricModel = parametricModel; this->specifyFormula(env, checkTask); @@ -137,9 +139,9 @@ namespace storm { // if there are maybestates, create the parameterLifter if (!maybeStates.empty()) { // Create the vector of one-step probabilities to go to target states. - std::vector b = this->parametricModel->getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), psiStates); + std::vector b = this->parametricModel->getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), statesWithProbability01.second); - parameterLifter = std::make_unique>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates); + parameterLifter = std::make_unique>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates, regionSplitEstimationsEnabled); } // We know some bounds for the results so set them @@ -179,7 +181,7 @@ namespace storm { std::vector b = rewardModel.getTotalRewardVector(this->parametricModel->getTransitionMatrix()); - parameterLifter = std::make_unique>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates); + parameterLifter = std::make_unique>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates, regionSplitEstimationsEnabled); } // We only know a lower bound for the result @@ -297,6 +299,9 @@ namespace storm { } else { maxSchedChoices = solver->getSchedulerChoices(); } + if (isRegionSplitEstimateSupported()) { + computeRegionSplitEstimates(x, solver->getSchedulerChoices(), region, dirForParameters); + } } // Get the result for the complete model (including maybestates) @@ -309,6 +314,68 @@ namespace storm { return std::make_unique>(std::move(result)); } + template + void SparseDtmcParameterLiftingModelChecker::computeRegionSplitEstimates(std::vector const& quantitativeResult, std::vector const& schedulerChoices, storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) { + std::map::VariableType, double> deltaLower, deltaUpper; + for (auto const& p : region.getVariables()) { + deltaLower.insert(std::make_pair(p, 0.0)); + deltaUpper.insert(std::make_pair(p, 0.0)); + } + auto const& choiceValuations = parameterLifter->getRowLabels(); + auto const& matrix = parameterLifter->getMatrix(); + auto const& vector = parameterLifter->getVector(); + + std::vector stateResults; + for (uint64_t state = 0; state < schedulerChoices.size(); ++state) { + uint64_t rowOffset = matrix.getRowGroupIndices()[state]; + uint64_t optimalChoice = schedulerChoices[state]; + auto const& optimalChoiceVal = choiceValuations[rowOffset + optimalChoice]; + assert(optimalChoiceVal.getUnspecifiedParameters().empty()); + stateResults.clear(); + for (uint64_t row = rowOffset; row < matrix.getRowGroupIndices()[state + 1]; ++row) { + stateResults.push_back(matrix.multiplyRowWithVector(row, quantitativeResult) + vector[row]); + } + bool checkUpperParameters = false; + do { + auto const& consideredParameters = checkUpperParameters ? optimalChoiceVal.getUpperParameters() : optimalChoiceVal.getLowerParameters(); + for (auto const& p : consideredParameters) { + // Find the 'best' choice that assigns the parameter to the other bound + ConstantType bestValue; + bool foundBestValue = false; + for (uint64_t choice = 0; choice < stateResults.size(); ++choice) { + if (choice != optimalChoice) { + auto const& otherBoundParsOfChoice = checkUpperParameters ? choiceValuations[rowOffset + choice].getLowerParameters() : choiceValuations[rowOffset + choice].getUpperParameters(); + if (otherBoundParsOfChoice.find(p) != otherBoundParsOfChoice.end()) { + ConstantType const& choiceValue = stateResults[choice]; + if (!foundBestValue || (storm::solver::minimize(dirForParameters) ? choiceValue < bestValue : choiceValue > bestValue)) { + foundBestValue = true; + bestValue = choiceValue; + } + } + } + } + if (checkUpperParameters) { + deltaLower[p] += storm::utility::convertNumber(bestValue); + } else { + deltaUpper[p] += storm::utility::convertNumber(bestValue); + } + + } + checkUpperParameters = !checkUpperParameters; + } while (checkUpperParameters); + } + + regionSplitEstimates.clear(); + for (auto const& p : region.getVariables()) { + if (deltaLower[p] > deltaUpper[p]) { + regionSplitEstimates.insert(std::make_pair(p, deltaUpper[p])); + } else { + regionSplitEstimates.insert(std::make_pair(p, deltaLower[p])); + } + } + + } + template void SparseDtmcParameterLiftingModelChecker::reset() { maybeStates.resize(0); @@ -321,6 +388,7 @@ namespace storm { x.clear(); lowerResultBound = boost::none; upperResultBound = boost::none; + regionSplitEstimationsEnabled = false; } template @@ -355,6 +423,18 @@ namespace storm { return result; } + template + bool SparseDtmcParameterLiftingModelChecker::isRegionSplitEstimateSupported() const { + return regionSplitEstimationsEnabled && !stepBound; + } + + template + std::map::VariableType, double> SparseDtmcParameterLiftingModelChecker::getRegionSplitEstimate() const { + STORM_LOG_THROW(isRegionSplitEstimateSupported(), storm::exceptions::InvalidOperationException, "Region split estimation requested but are not enabled (or supported)."); + return regionSplitEstimates; + } + + template class SparseDtmcParameterLiftingModelChecker, double>; template class SparseDtmcParameterLiftingModelChecker, storm::RationalNumber>; diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h index 18bb302b9..03dc1747a 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h @@ -23,12 +23,16 @@ namespace storm { virtual ~SparseDtmcParameterLiftingModelChecker() = default; virtual bool canHandle(std::shared_ptr parametricModel, CheckTask const& checkTask) const override; - virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask) override; - void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool skipModelSimplification); - + + virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates = false, bool allowModelSimplification = true) override; + void specify_internal(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification); + boost::optional> getCurrentMinScheduler(); boost::optional> getCurrentMaxScheduler(); + virtual bool isRegionSplitEstimateSupported() const override; + virtual std::map::VariableType, double> getRegionSplitEstimate() const override; + protected: virtual void specifyBoundedUntilFormula(Environment const& env, CheckTask const& checkTask) override; @@ -39,7 +43,9 @@ namespace storm { virtual storm::modelchecker::SparseInstantiationModelChecker& getInstantiationChecker() override; virtual std::unique_ptr computeQuantitativeValues(Environment const& env, storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) override; - + + void computeRegionSplitEstimates(std::vector const& quantitativeResult, std::vector const& schedulerChoices, storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters); + virtual void reset() override; private: @@ -59,6 +65,9 @@ namespace storm { boost::optional> minSchedChoices, maxSchedChoices; std::vector x; boost::optional lowerResultBound, upperResultBound; + + bool regionSplitEstimationsEnabled; + std::map::VariableType, double> regionSplitEstimates; }; } } diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index 04a5c41e1..de1f47b24 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp @@ -45,13 +45,14 @@ namespace storm { } template - void SparseMdpParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask) { + void SparseMdpParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplifications) { auto mdp = parametricModel->template as(); - specify(env, mdp, checkTask, false); + specify_internal(env, mdp, checkTask, generateRegionSplitEstimates, false); } template - void SparseMdpParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool skipModelSimplification) { + void SparseMdpParameterLiftingModelChecker::specify_internal(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) { + STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this."); diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h index 09a3e44cb..d29525e2e 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h @@ -25,8 +25,8 @@ namespace storm { virtual ~SparseMdpParameterLiftingModelChecker() = default; virtual bool canHandle(std::shared_ptr parametricModel, CheckTask const& checkTask) const override; - virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask) override; - void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool skipModelSimplification); + virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates = false, bool allowModelSimplification = true) override; + void specify_internal(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification); boost::optional> getCurrentMinScheduler(); boost::optional> getCurrentMaxScheduler(); diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp index e95cf2d61..2e9bf221b 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp @@ -15,7 +15,7 @@ namespace storm { } template - void ValidatingSparseDtmcParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask) { + void ValidatingSparseDtmcParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplifications) { STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this."); auto dtmc = parametricModel->template as(); @@ -27,8 +27,8 @@ namespace storm { auto simplifiedTask = checkTask.substituteFormula(*simplifier.getSimplifiedFormula()); - impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true); - preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true); + impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, false, true); + preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, false, true); } template diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h index f441353fb..e99792eed 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h @@ -12,7 +12,7 @@ namespace storm { ValidatingSparseDtmcParameterLiftingModelChecker(); virtual ~ValidatingSparseDtmcParameterLiftingModelChecker() = default; - virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask) override; + virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates = false, bool allowModelSimplifications = true) override; protected: virtual SparseParameterLiftingModelChecker& getImpreciseChecker() override; diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp index 7cdb1c7b0..444dd334c 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp @@ -16,7 +16,7 @@ namespace storm { template - void ValidatingSparseMdpParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask) { + void ValidatingSparseMdpParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplifications) { STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this."); auto mdp = parametricModel->template as(); @@ -28,8 +28,8 @@ namespace storm { auto simplifiedTask = checkTask.substituteFormula(*simplifier.getSimplifiedFormula()); - impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true); - preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true); + impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, false, true); + preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, false, true); } template diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h index fdb304747..9147e574e 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h @@ -12,7 +12,7 @@ namespace storm { ValidatingSparseMdpParameterLiftingModelChecker(); virtual ~ValidatingSparseMdpParameterLiftingModelChecker() = default; - virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask) override; + virtual void specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates = false, bool allowModelSimplifications = true) override; protected: virtual SparseParameterLiftingModelChecker& getImpreciseChecker() override; diff --git a/src/storm-pars/transformer/ParameterLifter.cpp b/src/storm-pars/transformer/ParameterLifter.cpp index 551529c4c..9eba6e8f2 100644 --- a/src/storm-pars/transformer/ParameterLifter.cpp +++ b/src/storm-pars/transformer/ParameterLifter.cpp @@ -12,8 +12,9 @@ namespace storm { namespace transformer { template - ParameterLifter::ParameterLifter(storm::storage::SparseMatrix const& pMatrix, std::vector const& pVector, storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns) { + ParameterLifter::ParameterLifter(storm::storage::SparseMatrix const& pMatrix, std::vector const& pVector, storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns, bool generateRowLabels) { + // get a mapping from old column indices to new ones std::vector oldToNewColumnIndexMapping(selectedColumns.size(), selectedColumns.size()); uint_fast64_t newIndex = 0; @@ -45,10 +46,16 @@ namespace storm { ++pMatrixEntryCount; } } + ParametricType const& pVectorEntry = pVector[rowIndex]; std::set vectorEntryVariables; if (!storm::utility::isConstant(pVectorEntry)) { storm::utility::parametric::gatherOccurringVariables(pVectorEntry, vectorEntryVariables); + if (generateRowLabels) { + // If row labels are to be generated, we do not allow unspecified valuations. + // Therefore, we also 'lift' parameters that only occurr on a vector. + occurringVariables.insert(vectorEntryVariables.begin(), vectorEntryVariables.end()); + } nonConstVectorEntries.set(pVectorEntryCount, true); } ++pVectorEntryCount; @@ -57,6 +64,10 @@ namespace storm { auto rowValuations = getVerticesOfAbstractRegion(occurringVariables); for (auto const& val : rowValuations) { + if (generateRowLabels) { + rowLabels.push_back(val); + } + // Insert matrix entries for each valuation. For non-constant entries, a dummy value is inserted and the function and the valuation are collected. // The placeholder for the collected function/valuation are stored in the matrixAssignment. The matrixAssignment is completed after the matrix is finished for (auto const& entry: pMatrix.getRow(rowIndex)) { @@ -78,7 +89,8 @@ namespace storm { vector.push_back(storm::utility::one()); AbstractValuation vectorVal(val); for(auto const& vectorVar : vectorEntryVariables) { - if(occurringVariables.find(vectorVar) == occurringVariables.end()) { + if (occurringVariables.find(vectorVar) == occurringVariables.end()) { + assert(!generateRowLabels); vectorVal.addParameterUnspecified(vectorVar); } } @@ -148,6 +160,11 @@ namespace storm { std::vector const& ParameterLifter::getVector() const { return vector; } + + template + std::vector::AbstractValuation> const& ParameterLifter::getRowLabels() const { + return rowLabels; + } template std::vector::AbstractValuation> ParameterLifter::getVerticesOfAbstractRegion(std::set const& variables) const { @@ -223,6 +240,21 @@ namespace storm { return result; } + template + std::set::VariableType> const& ParameterLifter::AbstractValuation::getLowerParameters() const { + return lowerPars; + } + + template + std::set::VariableType> const& ParameterLifter::AbstractValuation::getUpperParameters() const { + return upperPars; + } + + template + std::set::VariableType> const& ParameterLifter::AbstractValuation::getUnspecifiedParameters() const { + return unspecifiedPars; + } + template std::vector> ParameterLifter::AbstractValuation::getConcreteValuations(storm::storage::ParameterRegion const& region) const { auto result = region.getVerticesOfRegion(unspecifiedPars); diff --git a/src/storm-pars/transformer/ParameterLifter.h b/src/storm-pars/transformer/ParameterLifter.h index ab16e5a88..c7837fa5c 100644 --- a/src/storm-pars/transformer/ParameterLifter.h +++ b/src/storm-pars/transformer/ParameterLifter.h @@ -39,7 +39,7 @@ namespace storm { * @param selectedRows a Bitvector that specifies which rows of the matrix and the vector are considered. * @param selectedColumns a Bitvector that specifies which columns of the matrix are considered. */ - ParameterLifter(storm::storage::SparseMatrix const& pMatrix, std::vector const& pVector, storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns); + ParameterLifter(storm::storage::SparseMatrix const& pMatrix, std::vector const& pVector, storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns, bool generateRowLabels = false); void specifyRegion(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters); @@ -49,13 +49,6 @@ namespace storm { // Returns the resulting vector. Should only be called AFTER specifying a region std::vector const& getVector() const; - - private: - /* - * We minimize the number of function evaluations by only calling evaluate() once for each unique pair of function and valuation. - * The result of each evaluation is then written to all positions in the matrix (and the vector) where the corresponding (function,valuation) occurred. - */ - /* * During initialization, the actual regions are not known. Hence, we consider abstract valuations, * where it is only known whether a parameter will be set to either the lower/upper bound of the region or whether this is unspecified @@ -72,6 +65,9 @@ namespace storm { std::size_t getHashValue() const; AbstractValuation getSubValuation(std::set const& pars) const; + std::set const& getLowerParameters() const; + std::set const& getUpperParameters() const; + std::set const& getUnspecifiedParameters() const; /*! * Returns the concrete valuation(s) (w.r.t. the provided region) represented by this abstract valuation. @@ -83,6 +79,17 @@ namespace storm { std::set lowerPars, upperPars, unspecifiedPars; }; + // Returns for each row the abstract valuation for this row + // Note: the returned vector might be empty if row label generaion was disabled initially + std::vector const& getRowLabels() const; + + + private: + /* + * We minimize the number of function evaluations by only calling evaluate() once for each unique pair of function and valuation. + * The result of each evaluation is then written to all positions in the matrix (and the vector) where the corresponding (function,valuation) occurred. + */ + /*! * Collects all occurring pairs of functions and (abstract) valuations. * We also store a placeholder for the result of each pair. The result is computed and written into the placeholder whenever a region and optimization direction is specified. @@ -121,7 +128,8 @@ namespace storm { // Returns the 2^(variables.size()) vertices of the region std::vector getVerticesOfAbstractRegion(std::set const& variables) const; - + std::vector rowLabels; + storm::storage::SparseMatrix matrix; //The resulting matrix; std::vector::iterator, ConstantType&>> matrixAssignment; // Connection of matrix entries with placeholders diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index 0ed4b0d1c..0cf8d3183 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -74,3 +74,5 @@ add_dependencies(binaries storm-main) # installation install(TARGETS storm RUNTIME DESTINATION bin LIBRARY DESTINATION lib) install(TARGETS storm-main RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(DIRECTORY ${CMAKE_BINARY_DIR}/include/ DESTINATION include/storm + FILES_MATCHING PATTERN "*.h") diff --git a/src/storm/adapters/Smt2ExpressionAdapter.h b/src/storm/adapters/Smt2ExpressionAdapter.h index f1b96b71e..5abaf290d 100644 --- a/src/storm/adapters/Smt2ExpressionAdapter.h +++ b/src/storm/adapters/Smt2ExpressionAdapter.h @@ -133,7 +133,7 @@ namespace storm { STORM_LOG_DEBUG("Declaring the variable " + variableString); declaredVariables.back().insert(variableString); std::string varDeclaration = "( declare-fun " + variableString + " () "; - switch (variableToCheck.getType()){ + switch (variableToCheck.type()){ case carl::VariableType::VT_BOOL: varDeclaration += "Bool"; break; diff --git a/src/storm/api/counterexamples.cpp b/src/storm/api/counterexamples.cpp index 98c2f07bf..483dc57d4 100644 --- a/src/storm/api/counterexamples.cpp +++ b/src/storm/api/counterexamples.cpp @@ -10,9 +10,9 @@ namespace storm { return storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(env, program, *mdp, formula); } - std::shared_ptr computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr> mdp, std::shared_ptr const& formula) { + std::shared_ptr computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { Environment env; - return storm::counterexamples::SMTMinimalLabelSetGenerator::computeCounterexample(env, program, *mdp, formula); + return storm::counterexamples::SMTMinimalLabelSetGenerator::computeCounterexample(env, program, *model, formula); } } diff --git a/src/storm/api/counterexamples.h b/src/storm/api/counterexamples.h index d8f3d1ddd..6481c4efd 100644 --- a/src/storm/api/counterexamples.h +++ b/src/storm/api/counterexamples.h @@ -8,7 +8,7 @@ namespace storm { std::shared_ptr computePrismHighLevelCounterexampleMilp(storm::prism::Program const& program, std::shared_ptr> mdp, std::shared_ptr const& formula); - std::shared_ptr computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr> mdp, std::shared_ptr const& formula); + std::shared_ptr computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula); } } diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index cec17679b..86322ba80 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -311,8 +311,8 @@ namespace storm { buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates); // Initialize the model components with the obtained information. - storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel(), std::move(markovianStates)); - + storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel(), std::move(markovianStates)); + // Now finalize all reward models. for (auto& rewardModelBuilder : rewardModelBuilders) { modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount())); diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index 008a81e0f..74203f65d 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1,5 +1,4 @@ -#ifndef STORM_COUNTEREXAMPLES_SMTMINIMALLABELSETGENERATOR_MDP_H_ -#define STORM_COUNTEREXAMPLES_SMTMINIMALLABELSETGENERATOR_MDP_H_ +#pragma once #include #include @@ -11,12 +10,16 @@ #include "storm/storage/prism/Program.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/sparse/PrismChoiceOrigins.h" -#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" + #include "storm/utility/counterexamples.h" #include "storm/utility/cli.h" @@ -41,6 +44,9 @@ namespace storm { // The set of relevant labels. boost::container::flat_set relevantLabels; + // The set of labels that matter in terms of minimality. + boost::container::flat_set minimalityLabels; + // A set of labels that is definitely known to be taken in the final solution. boost::container::flat_set knownLabels; @@ -55,6 +61,9 @@ namespace storm { // The variables associated with the relevant labels. std::vector labelVariables; + // The variables associated with the labels that matter in terms of minimality. + std::vector minimalityLabelVariables; + // A mapping from relevant labels to their indices in the variable vector. std::map labelToIndexMap; @@ -90,30 +99,30 @@ namespace storm { * Computes the set of relevant labels in the model. Relevant labels are choice labels such that there exists * a scheduler that satisfies phi until psi with a nonzero probability. * - * @param mdp The MDP to search for relevant labels. + * @param model The model to search for relevant labels. * @param phiStates A bit vector representing all states that satisfy phi. * @param psiStates A bit vector representing all states that satisfy psi. + * @param dontCareLabels A set of labels that are "don't care" labels wrt. minimality. * @return A structure containing the relevant labels as well as states. */ - static RelevancyInformation determineRelevantStatesAndLabels(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static RelevancyInformation determineRelevantStatesAndLabels(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& dontCareLabels) { // Create result. RelevancyInformation relevancyInformation; // Compute all relevant states, i.e. states for which there exists a scheduler that has a non-zero // probabilitiy of satisfying phi until psi. - storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); relevancyInformation.relevantStates = storm::utility::graph::performProbGreater0E(backwardTransitions, phiStates, psiStates); relevancyInformation.relevantStates &= ~psiStates; STORM_LOG_DEBUG("Found " << relevancyInformation.relevantStates.getNumberOfSetBits() << " relevant states."); - STORM_LOG_DEBUG(relevancyInformation.relevantStates); // Retrieve some references for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices(); + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); // Now traverse all choices of all relevant states and check whether there is a successor target state. - // If so, the associated labels become relevant. Also, if a choice of relevant state has at least one + // If so, the associated labels become relevant. Also, if a choice of a relevant state has at least one // relevant successor, the choice becomes relevant. for (auto state : relevancyInformation.relevantStates) { relevancyInformation.relevantChoicesForRelevantStates.emplace(state, std::list()); @@ -127,6 +136,7 @@ namespace storm { for (auto const& label : labelSets[row]) { relevancyInformation.relevantLabels.insert(label); } + if (!currentChoiceRelevant) { currentChoiceRelevant = true; relevancyInformation.relevantChoicesForRelevantStates[state].push_back(row); @@ -137,15 +147,15 @@ namespace storm { } // Compute the set of labels that are known to be taken in any case. - relevancyInformation.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(mdp, labelSets, psiStates, relevancyInformation.relevantLabels); + relevancyInformation.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(model, labelSets, psiStates, relevancyInformation.relevantLabels); if (!relevancyInformation.knownLabels.empty()) { boost::container::flat_set remainingLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(remainingLabels, remainingLabels.end())); relevancyInformation.relevantLabels = remainingLabels; } - std::cout << "Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels." << std::endl; - + std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), dontCareLabels.begin(), dontCareLabels.end(), std::inserter(relevancyInformation.minimalityLabels, relevancyInformation.minimalityLabels.begin())); + STORM_LOG_DEBUG("Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels."); return relevancyInformation; } @@ -157,7 +167,7 @@ namespace storm { * @param relevantCommands A set of relevant labels for which to create the expressions. * @return A mapping from relevant labels to their corresponding expressions. */ - static VariableInformation createVariables(std::shared_ptr const& manager, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, RelevancyInformation const& relevancyInformation, bool createReachabilityVariables) { + static VariableInformation createVariables(std::shared_ptr const& manager, storm::models::sparse::Model const& model, storm::storage::BitVector const& psiStates, RelevancyInformation const& relevancyInformation, bool createReachabilityVariables) { VariableInformation variableInformation; variableInformation.manager = manager; @@ -175,6 +185,11 @@ namespace storm { variableInformation.labelVariables.push_back(manager->declareBooleanVariable(variableName.str())); + // Record if the label is among the ones that matter for minimality. + if (relevancyInformation.minimalityLabels.find(label) != relevancyInformation.minimalityLabels.end()) { + variableInformation.minimalityLabelVariables.push_back(variableInformation.labelVariables.back()); + } + // Clear contents of the stream to construct new expression name. variableName.clear(); variableName.str(""); @@ -194,7 +209,7 @@ namespace storm { if (createReachabilityVariables) { variableInformation.hasReachabilityVariables = true; - storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); for (auto state : relevancyInformation.relevantStates) { variableInformation.relevantStatesToOrderVariableIndexMap[state] = variableInformation.stateOrderVariables.size(); @@ -250,13 +265,10 @@ namespace storm { /*! * Asserts the constraints that are initially needed for the Fu-Malik procedure. * - * @param program The program for which to build the constraints. - * @param mdp The MDP that results from the given program. - * @param context The Z3 context in which to build the expressions. * @param solver The solver in which to assert the constraints. * @param variableInformation A structure with information about the variables for the labels. */ - static void assertFuMalikInitialConstraints(storm::prism::Program const& program, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, z3::context& context, z3::solver& solver, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation) { + static void assertFuMalikInitialConstraints(z3::solver& solver, VariableInformation const& variableInformation) { // Assert that at least one of the labels must be taken. z3::expr formula = variableInformation.labelVariables.at(0); for (uint_fast64_t index = 1; index < variableInformation.labelVariables.size(); ++index) { @@ -269,12 +281,12 @@ namespace storm { * Asserts cuts that are derived from the explicit representation of the model and rule out a lot of * suboptimal solutions. * - * @param mdp The labeled MDP for which to compute the cuts. + * @param model The labeled model for which to compute the cuts. * @param context The Z3 context in which to build the expressions. * @param solver The solver to use for the satisfiability evaluation. */ - static void assertExplicitCuts(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { - // Walk through the MDP and + static void assertExplicitCuts(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + // Walk through the model and // * identify labels enabled in initial states // * identify labels that can directly precede a given action // * identify labels that directly reach a target state @@ -288,10 +300,10 @@ namespace storm { std::map, std::set>> followingLabels; std::map>> synchronizingLabels; - // Get some data from the MDP for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); - storm::storage::BitVector const& initialStates = mdp.getInitialStates(); - storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + // Get some data from the model for convenient access. + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + storm::storage::BitVector const& initialStates = model.getInitialStates(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); for (auto currentState : relevancyInformation.relevantStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) { @@ -549,16 +561,16 @@ namespace storm { * @param program The symbolic representation of the model in terms of a program. * @param solver The solver to use for the satisfiability evaluation. */ - static void assertSymbolicCuts(storm::prism::Program& program, storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + static void assertSymbolicCuts(storm::prism::Program& program, storm::models::sparse::Model const& model, std::vector> const& labelSets, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { // A container storing the label sets that may precede a given label set. std::map, std::set>> precedingLabelSets; // A container that maps labels to their reachable synchronization sets. std::map>> synchronizingLabels; - // Get some data from the MDP for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); - storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + // Get some data from the model for convenient access. + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Compute the set of labels that may precede a given action. for (auto currentState : relevancyInformation.relevantStates) { @@ -596,28 +608,6 @@ namespace storm { // cuts. std::unique_ptr localSolver(new storm::solver::Z3SmtSolver(program.getManager())); storm::expressions::ExpressionManager const& localManager = program.getManager(); -// -// // Create a context and register all variables of the program with their correct type. -// z3::context localContext; -// z3::solver localSolver(localContext); -// std::map solverVariables; -// for (auto const& booleanVariable : program.getGlobalBooleanVariables()) { -// solverVariables.emplace(booleanVariable.getName(), localContext.bool_const(booleanVariable.getName().c_str())); -// } -// for (auto const& integerVariable : program.getGlobalIntegerVariables()) { -// solverVariables.emplace(integerVariable.getName(), localContext.int_const(integerVariable.getName().c_str())); -// } -// -// for (auto const& module : program.getModules()) { -// for (auto const& booleanVariable : module.getBooleanVariables()) { -// solverVariables.emplace(booleanVariable.getName(), localContext.bool_const(booleanVariable.getName().c_str())); -// } -// for (auto const& integerVariable : module.getIntegerVariables()) { -// solverVariables.emplace(integerVariable.getName(), localContext.int_const(integerVariable.getName().c_str())); -// } -// } -// -// storm::adapters::Z3ExpressionAdapter expressionAdapter(localContext, false, solverVariables); // Then add the constraints for bounds of the integer variables.. for (auto const& integerVariable : program.getGlobalIntegerVariables()) { @@ -890,22 +880,22 @@ namespace storm { /*! * Asserts constraints necessary to encode the reachability of at least one target state from the initial states. */ - static void assertReachabilityCuts(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + static void assertReachabilityCuts(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { if (!variableInformation.hasReachabilityVariables) { throw storm::exceptions::InvalidStateException() << "Impossible to assert reachability cuts without the necessary variables."; } - // Get some data from the MDP for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); - storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + // Get some data from the model for convenient access. + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // First, we add the formulas that encode // (1) if an incoming transition is chosen, an outgoing one is chosen as well (for non-initial states) // (2) an outgoing transition out of the initial states is taken. storm::expressions::Expression initialStateExpression = variableInformation.manager->boolean(false); for (auto relevantState : relevancyInformation.relevantStates) { - if (!mdp.getInitialStates().get(relevantState)) { + if (!model.getInitialStates().get(relevantState)) { // Assert the constraints (1). boost::container::flat_set relevantPredecessors; for (auto const& predecessorEntry : backwardTransitions.getRow(relevantState)) { @@ -1319,7 +1309,7 @@ namespace storm { std::stringstream variableName; std::vector result; - std::vector adderVariables = createCounterCircuit(variableInformation, variableInformation.labelVariables); + std::vector adderVariables = createCounterCircuit(variableInformation, variableInformation.minimalityLabelVariables); for (uint_fast64_t i = 0; i < adderVariables.size(); ++i) { variableName.str(""); variableName.clear(); @@ -1359,32 +1349,32 @@ namespace storm { } /*! - * Analyzes the given sub-MDP that has a maximal reachability of zero (i.e. no psi states are reachable) and tries to construct assertions that aim to make at least one psi state reachable. + * Analyzes the given sub-model that has a maximal reachability of zero (i.e. no psi states are reachable) and tries to construct assertions that aim to make at least one psi state reachable. * * @param solver The solver to use for the satisfiability evaluation. - * @param subMdp The sub-MDP resulting from restricting the original MDP to the given command set. - * @param originalMdp The original MDP. + * @param subModel The sub-model resulting from restricting the original model to the given command set. + * @param originalModel The original model. * @param phiStates A bit vector characterizing all phi states in the model. * @param psiState A bit vector characterizing all psi states in the model. * @param commandSet The currently chosen set of commands. * @param variableInformation A structure with information about the variables of the solver. */ - static void analyzeZeroProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Mdp const& subMdp, std::vector> const& subLabelSets, storm::models::sparse::Mdp const& originalMdp, std::vector> const& originalLabelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { - storm::storage::BitVector reachableStates(subMdp.getNumberOfStates()); + static void analyzeZeroProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Model const& subModel, std::vector> const& subLabelSets, storm::models::sparse::Model const& originalModel, std::vector> const& originalLabelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + storm::storage::BitVector reachableStates(subModel.getNumberOfStates()); STORM_LOG_DEBUG("Analyzing solution with zero probability."); // Initialize the stack for the DFS. bool targetStateIsReachable = false; std::vector stack; - stack.reserve(subMdp.getNumberOfStates()); - for (auto initialState : subMdp.getInitialStates()) { + stack.reserve(subModel.getNumberOfStates()); + for (auto initialState : subModel.getInitialStates()) { stack.push_back(initialState); reachableStates.set(initialState, true); } - storm::storage::SparseMatrix const& transitionMatrix = subMdp.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices(); + storm::storage::SparseMatrix const& transitionMatrix = subModel.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); // Now determine which states and labels are actually reachable. boost::container::flat_set reachableLabels; @@ -1423,12 +1413,12 @@ namespace storm { } storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; - storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getBackwardTransitions(), phiStates, psiStates); + storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subModel.getBackwardTransitions(), phiStates, psiStates); boost::container::flat_set locallyRelevantLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); + std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); STORM_LOG_DEBUG("Found " << reachableLabels.size() << " reachable labels and " << reachableStates.getNumberOfSetBits() << " reachable states."); // Search for states on the border of the reachable state space, i.e. states that are still reachable @@ -1440,7 +1430,7 @@ namespace storm { bool isBorderChoice = false; // Determine whether the state has the option to leave the reachable state space and go to the unreachable relevant states. - for (auto const& successorEntry : originalMdp.getTransitionMatrix().getRow(currentChoice)) { + for (auto const& successorEntry : originalModel.getTransitionMatrix().getRow(currentChoice)) { if (unreachableRelevantStates.get(successorEntry.getColumn())) { isBorderChoice = true; } @@ -1482,33 +1472,33 @@ namespace storm { } /*! - * Analyzes the given sub-MDP that has a non-zero maximal reachability and tries to construct assertions that aim to guide the solver to solutions + * Analyzes the given sub-model that has a non-zero maximal reachability and tries to construct assertions that aim to guide the solver to solutions * with an improved probability value. * * @param solver The solver to use for the satisfiability evaluation. - * @param subMdp The sub-MDP resulting from restricting the original MDP to the given command set. - * @param originalMdp The original MDP. + * @param subModel The sub-model resulting from restricting the original model to the given command set. + * @param originalModel The original model. * @param phiStates A bit vector characterizing all phi states in the model. * @param psiState A bit vector characterizing all psi states in the model. * @param commandSet The currently chosen set of commands. * @param variableInformation A structure with information about the variables of the solver. */ - static void analyzeInsufficientProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Mdp const& subMdp, std::vector> const& subLabelSets, storm::models::sparse::Mdp const& originalMdp, std::vector> const& originalLabelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + static void analyzeInsufficientProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Model const& subModel, std::vector> const& subLabelSets, storm::models::sparse::Model const& originalModel, std::vector> const& originalLabelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { STORM_LOG_DEBUG("Analyzing solution with insufficient probability."); - storm::storage::BitVector reachableStates(subMdp.getNumberOfStates()); + storm::storage::BitVector reachableStates(subModel.getNumberOfStates()); // Initialize the stack for the DFS. std::vector stack; - stack.reserve(subMdp.getNumberOfStates()); - for (auto initialState : subMdp.getInitialStates()) { + stack.reserve(subModel.getNumberOfStates()); + for (auto initialState : subModel.getInitialStates()) { stack.push_back(initialState); reachableStates.set(initialState, true); } - storm::storage::SparseMatrix const& transitionMatrix = subMdp.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices(); + storm::storage::SparseMatrix const& transitionMatrix = subModel.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); // Now determine which states and labels are actually reachable. boost::container::flat_set reachableLabels; @@ -1541,12 +1531,12 @@ namespace storm { STORM_LOG_DEBUG("Successfully determined reachable state space."); storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; - storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getBackwardTransitions(), phiStates, psiStates); + storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subModel.getBackwardTransitions(), phiStates, psiStates); boost::container::flat_set locallyRelevantLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); + std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); // Search for states for which we could enable another option and possibly improve the reachability probability. std::set> cutLabels; @@ -1589,40 +1579,43 @@ namespace storm { /*! - * Returns the submdp obtained from removing all choices that do not originate from the specified filterLabelSet. - * Also returns the Labelsets of the submdp + * Returns the sub-model obtained from removing all choices that do not originate from the specified filterLabelSet. + * Also returns the Labelsets of the sub-model. */ - static std::pair, std::vector>> restrictMdpToLabelSet(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, boost::container::flat_set const& filterLabelSet) { - - STORM_LOG_THROW(mdp.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); + static std::pair>, std::vector>> restrictModelToLabelSet(storm::models::sparse::Model const& model, boost::container::flat_set const& filterLabelSet) { + bool customRowGrouping = model.isOfType(storm::models::ModelType::Mdp); + std::vector> resultLabelSet; - storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, mdp.getTransitionMatrix().getColumnCount(), 0, true, true, mdp.getTransitionMatrix().getRowGroupCount()); + storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, model.getTransitionMatrix().getColumnCount(), 0, true, customRowGrouping, model.getTransitionMatrix().getRowGroupCount()); // Check for each choice of each state, whether the choice commands are fully contained in the given command set. uint_fast64_t currentRow = 0; - for(uint_fast64_t state = 0; state < mdp.getNumberOfStates(); ++state) { + for(uint_fast64_t state = 0; state < model.getNumberOfStates(); ++state) { bool stateHasValidChoice = false; - for (uint_fast64_t choice = mdp.getTransitionMatrix().getRowGroupIndices()[state]; choice < mdp.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { - bool choiceValid = std::includes(filterLabelSet.begin(), filterLabelSet.end(), labelSets[choice].begin(), labelSets[choice].end()); + for (uint_fast64_t choice = model.getTransitionMatrix().getRowGroupIndices()[state]; choice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { + auto const& choiceLabelSet = model.getChoiceOrigins()->asPrismChoiceOrigins().getCommandSet(choice); + bool choiceValid = std::includes(filterLabelSet.begin(), filterLabelSet.end(), choiceLabelSet.begin(), choiceLabelSet.end()); // If the choice is valid, copy over all its elements. if (choiceValid) { - if (!stateHasValidChoice) { + if (!stateHasValidChoice && customRowGrouping) { transitionMatrixBuilder.newRowGroup(currentRow); } stateHasValidChoice = true; - for (auto const& entry : mdp.getTransitionMatrix().getRow(choice)) { + for (auto const& entry : model.getTransitionMatrix().getRow(choice)) { transitionMatrixBuilder.addNextValue(currentRow, entry.getColumn(), entry.getValue()); } - resultLabelSet.push_back(labelSets[choice]); + resultLabelSet.push_back(choiceLabelSet); ++currentRow; } } // If no choice of the current state may be taken, we insert a self-loop to the state instead. if (!stateHasValidChoice) { - transitionMatrixBuilder.newRowGroup(currentRow); + if (customRowGrouping) { + transitionMatrixBuilder.newRowGroup(currentRow); + } transitionMatrixBuilder.addNextValue(currentRow, state, storm::utility::one()); // Insert an empty label set for this choice resultLabelSet.emplace_back(); @@ -1630,28 +1623,48 @@ namespace storm { } } - storm::models::sparse::Mdp resultMdp(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(mdp.getStateLabeling())); + std::shared_ptr> resultModel; + if (model.isOfType(storm::models::ModelType::Dtmc)) { + resultModel = std::make_shared>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling())); + } else { + resultModel = std::make_shared>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling())); + } - return std::make_pair(std::move(resultMdp), std::move(resultLabelSet)); + return std::make_pair(resultModel, std::move(resultLabelSet)); } - public: - + static T computeMaximalReachabilityProbability(Environment const& env, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + T result = storm::utility::zero(); + + std::vector allStatesResult; + + STORM_LOG_DEBUG("Invoking model checker."); + if (model.isOfType(storm::models::ModelType::Dtmc)) { + allStatesResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false, storm::solver::GeneralLinearEquationSolverFactory()); + } else { + storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; + allStatesResult = std::move(modelCheckerHelper.computeUntilProbabilities(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false, false, storm::solver::GeneralMinMaxLinearEquationSolverFactory()).values); + } + for (auto state : model.getInitialStates()) { + result = std::max(result, allStatesResult[state]); + } + return result; + } + public: /*! - * Computes the minimal command set that is needed in the given MDP to exceed the given probability threshold for satisfying phi until psi. + * Computes the minimal command set that is needed in the given model to exceed the given probability threshold for satisfying phi until psi. * - * @param program The program that was used to build the MDP. - * @param mdp The MDP in which to find the minimal command set. + * @param program The program that was used to build the model. + * @param model The sparse model in which to find the minimal command set. * @param phiStates A bit vector characterizing all phi states in the model. * @param psiStates A bit vector characterizing all psi states in the model. - * @param probabilityThreshold The probability value that must be achieved or exceeded. - * @param strictBound A flag indicating whether the probability must be achieved (in which case the flag must be set) or strictly exceeded - * (if the flag is set to false). + * @param probabilityThreshold The threshold that is to be achieved or exceeded. + * @param strictBound Indicates whether the threshold needs to be achieved (true) or exceeded (false). * @param checkThresholdFeasible If set, it is verified that the model can actually achieve/exceed the given probability value. If this check * is made and fails, an exception is thrown. */ - static boost::container::flat_set getMinimalCommandSet(Environment const& env,storm::prism::Program program, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { + static boost::container::flat_set getMinimalCommandSet(Environment const& env, storm::prism::Program program, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { #ifdef STORM_HAVE_Z3 // Set up all clocks used for time measurement. auto totalClock = std::chrono::high_resolution_clock::now(); @@ -1672,37 +1685,33 @@ namespace storm { // (0) Obtain the label sets for each choice. // The label set of a choice corresponds to the set of prism commands that induce the choice. - STORM_LOG_THROW(mdp.hasChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to minimal command set is impossible for model without choice origns."); - STORM_LOG_THROW(mdp.getChoiceOrigins()->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without prism choice origins."); - storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); + STORM_LOG_THROW(model.hasChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to minimal command set is impossible for model without choice origins."); + STORM_LOG_THROW(model.getChoiceOrigins()->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without prism choice origins."); + storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = model.getChoiceOrigins()->asPrismChoiceOrigins(); std::vector> labelSets; - labelSets.reserve(mdp.getNumberOfChoices()); - for (uint_fast64_t choice = 0; choice < mdp.getNumberOfChoices(); ++choice) { + labelSets.reserve(model.getNumberOfChoices()); + for (uint_fast64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) { labelSets.push_back(choiceOrigins.getCommandSet(choice)); } // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; if (checkThresholdFeasible) { - storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; - STORM_LOG_DEBUG("Invoking model checker."); - std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(env, false, mdp.getTransitionMatrix(), mdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::solver::GeneralMinMaxLinearEquationSolverFactory()).values); - for (auto state : mdp.getInitialStates()) { - maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); - } + maximalReachabilityProbability = computeMaximalReachabilityProbability(env, model, phiStates, psiStates); + STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= probabilityThreshold) || (!strictBound && maximalReachabilityProbability > probabilityThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."); std::cout << std::endl << "Maximal reachability in model is " << maximalReachabilityProbability << "." << std::endl << std::endl; } // (2) Identify all states and commands that are relevant, because only these need to be considered later. - RelevancyInformation relevancyInformation = determineRelevantStatesAndLabels(mdp, labelSets, phiStates, psiStates); + RelevancyInformation relevancyInformation = determineRelevantStatesAndLabels(model, labelSets, phiStates, psiStates, dontCareLabels); // (3) Create a solver. - std::shared_ptr manager(new storm::expressions::ExpressionManager()); - std::unique_ptr solver(new storm::solver::Z3SmtSolver(*manager)); + std::shared_ptr manager = std::make_shared(); + std::unique_ptr solver = std::make_unique(*manager); // (4) Create the variables for the relevant commands. - VariableInformation variableInformation = createVariables(manager, mdp, psiStates, relevancyInformation, includeReachabilityEncoding); + VariableInformation variableInformation = createVariables(manager, model, psiStates, relevancyInformation, includeReachabilityEncoding); STORM_LOG_DEBUG("Created variables."); // (5) Now assert an adder whose result variables can later be used to constrain the nummber of label @@ -1713,12 +1722,12 @@ namespace storm { // (6) Add constraints that cut off a lot of suboptimal solutions. STORM_LOG_DEBUG("Asserting cuts."); - assertExplicitCuts(mdp, labelSets, psiStates, variableInformation, relevancyInformation, *solver); + assertExplicitCuts(model, labelSets, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted explicit cuts."); - assertSymbolicCuts(program, mdp, labelSets, variableInformation, relevancyInformation, *solver); + assertSymbolicCuts(program, model, labelSets, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted symbolic cuts."); if (includeReachabilityEncoding) { - assertReachabilityCuts(mdp, labelSets, psiStates, variableInformation, relevancyInformation, *solver); + assertReachabilityCuts(model, labelSets, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted reachability cuts."); } @@ -1729,9 +1738,18 @@ namespace storm { // satisfying phi until psi exceeds the given threshold, the set of labels is minimal and can be returned. // Otherwise, the current solution has to be ruled out and the next smallest solution is retrieved from // the solver. + + boost::container::flat_set commandSet(relevancyInformation.knownLabels); + + // If there are no relevant labels, return directly. + if (relevancyInformation.relevantLabels.empty()) { + return commandSet; + } else if (relevancyInformation.minimalityLabels.empty()) { + commandSet.insert(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end()); + return commandSet; + } // Set up some variables for the iterations. - boost::container::flat_set commandSet(relevancyInformation.relevantLabels); bool done = false; uint_fast64_t iterations = 0; uint_fast64_t currentBound = 0; @@ -1744,24 +1762,16 @@ namespace storm { totalSolverTime += std::chrono::high_resolution_clock::now() - solverClock; STORM_LOG_DEBUG("Computed minimal command set of size " << (commandSet.size() + relevancyInformation.knownLabels.size()) << "."); - // Restrict the given MDP to the current set of labels and compute the reachability probability. + // Restrict the given model to the current set of labels and compute the reachability probability. modelCheckingClock = std::chrono::high_resolution_clock::now(); commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end()); - auto subMdpChoiceOrigins = restrictMdpToLabelSet(mdp, labelSets, commandSet); - storm::models::sparse::Mdp const& subMdp = subMdpChoiceOrigins.first; - std::vector> const& subLabelSets = subMdpChoiceOrigins.second; + auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet); + std::shared_ptr> const& subModel = subChoiceOrigins.first; + std::vector> const& subLabelSets = subChoiceOrigins.second; - storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; - STORM_LOG_DEBUG("Invoking model checker."); - std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(env, false, subMdp.getTransitionMatrix(), subMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::solver::GeneralMinMaxLinearEquationSolverFactory()).values); - STORM_LOG_DEBUG("Computed model checking results."); + // Now determine the maximal reachability probability in the sub-model. + maximalReachabilityProbability = computeMaximalReachabilityProbability(env, *subModel, phiStates, psiStates); totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock; - - // Now determine the maximal reachability probability by checking all initial states. - maximalReachabilityProbability = 0; - for (auto state : mdp.getInitialStates()) { - maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); - } // Depending on whether the threshold was successfully achieved or not, we proceed by either analyzing the bad solution or stopping the iteration process. analysisClock = std::chrono::high_resolution_clock::now(); @@ -1770,11 +1780,11 @@ namespace storm { ++zeroProbabilityCount; // If there was no target state reachable, analyze the solution and guide the solver into the right direction. - analyzeZeroProbabilitySolution(*solver, subMdp, subLabelSets, mdp, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + analyzeZeroProbabilitySolution(*solver, *subModel, subLabelSets, model, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); } else { // If the reachability probability was greater than zero (i.e. there is a reachable target state), but the probability was insufficient to exceed // the given threshold, we analyze the solution and try to guide the solver into the right direction. - analyzeInsufficientProbabilitySolution(*solver, subMdp, subLabelSets, mdp, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + analyzeInsufficientProbabilitySolution(*solver, *subModel, subLabelSets, model, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); } } else { done = true; @@ -1811,51 +1821,157 @@ namespace storm { #endif } - static std::shared_ptr computeCounterexample(Environment const& env,storm::prism::Program program, storm::models::sparse::Mdp const& mdp, std::shared_ptr const& formula) { -#ifdef STORM_HAVE_Z3 - std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; + static void extendCommandSetLowerBound(storm::models::sparse::Model const& model, boost::container::flat_set& commandSet, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + auto startTime = std::chrono::high_resolution_clock::now(); + + // Create sub-model that only contains the choices allowed by the given command set. + std::shared_ptr> subModel = restrictModelToLabelSet(model, commandSet).first; + // Then determine all prob0E(psi) states that are reachable in the sub-model. + storm::storage::BitVector reachableProb0EStates = storm::utility::graph::getReachableStates(subModel->getTransitionMatrix(), subModel->getInitialStates(), phiStates, psiStates); + + // Create a queue of reachable prob0E(psi) states so we can check which commands need to be added + // to give them a strategy that avoids psi states. + std::queue prob0EWorklist; + for (auto const& e : reachableProb0EStates) { + prob0EWorklist.push(e); + } + + // As long as there are reachable prob0E(psi) states, we add commands so they can stay within + // prob0E(states). + while (!prob0EWorklist.empty()) { + uint_fast64_t state = prob0EWorklist.front(); + prob0EWorklist.pop(); + + // Now iterate over the original choices of the prob0E(psi) state and add at least one. + bool hasLabeledChoice = false; + uint64_t smallestCommandSetSize = 0; + uint64_t smallestCommandChoice = model.getTransitionMatrix().getRowGroupIndices()[state]; + + // Determine the choice with the least amount of commands (bad heuristic). + for (uint64_t choice = smallestCommandChoice; choice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { + bool onlyProb0ESuccessors = true; + for (auto const& successorEntry : model.getTransitionMatrix().getRow(choice)) { + if (!psiStates.get(successorEntry.getColumn())) { + onlyProb0ESuccessors = false; + break; + } + } + + if (onlyProb0ESuccessors) { + auto const& labelSet = model.getChoiceOrigins()->asPrismChoiceOrigins().getCommandSet(choice); + hasLabeledChoice |= !labelSet.empty(); + + if (smallestCommandChoice == 0 || labelSet.size() < smallestCommandSetSize) { + smallestCommandSetSize = labelSet.size(); + smallestCommandChoice = choice; + } + } + } + + if (hasLabeledChoice) { + // Take all labels of the selected choice. + auto const& labelSet = model.getChoiceOrigins()->asPrismChoiceOrigins().getCommandSet(smallestCommandChoice); + commandSet.insert(labelSet.begin(), labelSet.end()); + + // Check for which successor states choices need to be added + for (auto const& successorEntry : model.getTransitionMatrix().getRow(smallestCommandChoice)) { + if (!storm::utility::isZero(successorEntry.getValue())) { + if (!reachableProb0EStates.get(successorEntry.getColumn())) { + reachableProb0EStates.set(successorEntry.getColumn()); + prob0EWorklist.push(successorEntry.getColumn()); + } + } + } + } + } + + auto endTime = std::chrono::high_resolution_clock::now(); + std::cout << std::endl << "Extended command for lower bounded property to size " << commandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; + } + + static boost::container::flat_set computeCounterexampleCommandSet(Environment const& env, storm::prism::Program program, storm::models::sparse::Model const& model, std::shared_ptr const& formula) { + STORM_LOG_THROW(model.isOfType(storm::models::ModelType::Dtmc) || model.isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "MaxSAT-based counterexample generation is supported only for discrete-time models."); + std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; + STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element."); storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula(); STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas."); - storm::logic::ComparisonType comparisonType = probabilityOperator.getComparisonType(); - STORM_LOG_THROW(comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual, storm::exceptions::InvalidPropertyException, "Counterexample generation only supports formulas with an upper probability bound."); STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation."); - + + storm::logic::ComparisonType comparisonType = probabilityOperator.getComparisonType(); bool strictBound = comparisonType == storm::logic::ComparisonType::Less; - double threshold = probabilityOperator.getThresholdAs(); - + double threshold = probabilityOperator.getThresholdAs(); + storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(mdp); - + storm::modelchecker::SparsePropositionalModelChecker> modelchecker(model); + if (probabilityOperator.getSubformula().isUntilFormula()) { + STORM_LOG_THROW(!storm::logic::isLowerBound(comparisonType), storm::exceptions::NotSupportedException, "Lower bounds in counterexamples are only supported for eventually formulas."); storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula(); - + std::unique_ptr leftResult = modelchecker.check(env, untilFormula.getLeftSubformula()); std::unique_ptr rightResult = modelchecker.check(env, untilFormula.getRightSubformula()); - + storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult(); storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult(); - + phiStates = leftQualitativeResult.getTruthValuesVector(); psiStates = rightQualitativeResult.getTruthValuesVector(); } else if (probabilityOperator.getSubformula().isEventuallyFormula()) { storm::logic::EventuallyFormula const& eventuallyFormula = probabilityOperator.getSubformula().asEventuallyFormula(); - + std::unique_ptr subResult = modelchecker.check(env, eventuallyFormula.getSubformula()); - + storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult(); - - phiStates = storm::storage::BitVector(mdp.getNumberOfStates(), true); + + phiStates = storm::storage::BitVector(model.getNumberOfStates(), true); psiStates = subQualitativeResult.getTruthValuesVector(); } - + + bool lowerBoundedFormula = false; + if (storm::logic::isLowerBound(comparisonType)) { + // If the formula specifies a lower bound, we need to modify the phi and psi states. + // More concretely, we convert P(min)>lambda(F psi) to P(max)<(1-lambda)(G !psi) = P(max)<(1-lambda)(!psi U prob0E(psi)) + // where prob0E(psi) is the set of states for which there exists a strategy \sigma_0 that avoids + // reaching psi states completely. + + // This means that from all states in prob0E(psi) we need to include labels such that \sigma_0 + // is actually included in the resulting model. This prevents us from guaranteeing the minimality of + // the returned counterexample, so we warn about that. + STORM_LOG_WARN("Generating counterexample for lower-bounded property. The resulting command set need not be minimal."); + + // Modify bound appropriately. + comparisonType = storm::logic::invertPreserveStrictness(comparisonType); + threshold = storm::utility::one() - threshold; + + // Modify the phi and psi states appropriately. + storm::storage::BitVector statesWithProbability0E = storm::utility::graph::performProb0E(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates); + phiStates = ~psiStates; + psiStates = std::move(statesWithProbability0E); + + // Remember our transformation so we can add commands to guarantee that the prob0E(a) states actually + // have a strategy that voids a states. + lowerBoundedFormula = true; + } + // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto commandSet = getMinimalCommandSet(env, program, mdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isEncodeReachabilitySet()); + auto commandSet = getMinimalCommandSet(env, program, model, phiStates, psiStates, threshold, strictBound, boost::container::flat_set(), true, storm::settings::getModule().isEncodeReachabilitySet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal command set of size " << commandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; + + // Extend the command set properly. + if (lowerBoundedFormula) { + extendCommandSetLowerBound(model, commandSet, phiStates, psiStates); + } + return commandSet; + } + + static std::shared_ptr computeCounterexample(Environment const& env, storm::prism::Program program, storm::models::sparse::Model const& model, std::shared_ptr const& formula) { +#ifdef STORM_HAVE_Z3 + auto commandSet = computeCounterexampleCommandSet(env, program, model, formula); return std::make_shared(program.restrictCommands(commandSet)); @@ -1870,4 +1986,3 @@ namespace storm { } // namespace counterexamples } // namespace storm -#endif /* STORM_COUNTEREXAMPLES_SMTMINIMALLABELSETGENERATOR_MDP_H_ */ diff --git a/src/storm/logic/ComparisonType.h b/src/storm/logic/ComparisonType.h index bf932fc2b..19475960f 100644 --- a/src/storm/logic/ComparisonType.h +++ b/src/storm/logic/ComparisonType.h @@ -4,32 +4,45 @@ #include namespace storm { - namespace logic { - enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual }; - - inline bool isStrict(ComparisonType t) { - return (t == ComparisonType::Less || t == ComparisonType::Greater); - } - - inline bool isLowerBound(ComparisonType t) { - return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual); + namespace logic { + enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual }; + + inline bool isStrict(ComparisonType t) { + return (t == ComparisonType::Less || t == ComparisonType::Greater); + } + + inline bool isLowerBound(ComparisonType t) { + return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual); + } + + inline ComparisonType invert(ComparisonType t) { + switch(t) { + case ComparisonType::Less: + return ComparisonType::GreaterEqual; + case ComparisonType::LessEqual: + return ComparisonType::Greater; + case ComparisonType::Greater: + return ComparisonType::LessEqual; + case ComparisonType::GreaterEqual: + return ComparisonType::Less; } + } - inline ComparisonType invert(ComparisonType t) { - switch(t) { - case ComparisonType::Less: - return ComparisonType::GreaterEqual; - case ComparisonType::LessEqual: - return ComparisonType::Greater; - case ComparisonType::Greater: - return ComparisonType::LessEqual; - case ComparisonType::GreaterEqual: - return ComparisonType::Less; - } + inline ComparisonType invertPreserveStrictness(ComparisonType t) { + switch(t) { + case ComparisonType::Less: + return ComparisonType::Greater; + case ComparisonType::LessEqual: + return ComparisonType::GreaterEqual; + case ComparisonType::Greater: + return ComparisonType::Less; + case ComparisonType::GreaterEqual: + return ComparisonType::LessEqual; } + } - std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType); - } + std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType); + } } #endif /* STORM_LOGIC_COMPARISONTYPE_H_ */ diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 8ce496426..bd93a44ef 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -8,6 +8,8 @@ #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" +#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h" +#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h" #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/utility/graph.h" #include "storm/utility/macros.h" @@ -42,12 +44,13 @@ namespace storm { // Build a subsystem of the preprocessor result model that discards states that yield infinite reward for all schedulers. // We can also merge the states that will have reward zero anyway. storm::storage::BitVector maybeStates = preprocessorResult.rewardLessInfinityEStates.get() & ~preprocessorResult.reward0AStates; + storm::storage::BitVector finiteRewardChoices = preprocessorResult.preprocessedModel->getTransitionMatrix().getRowFilter(preprocessorResult.rewardLessInfinityEStates.get(), preprocessorResult.rewardLessInfinityEStates.get()); std::set relevantRewardModels; for (auto const& obj : this->objectives) { obj.formula->gatherReferencedRewardModels(relevantRewardModels); } storm::transformer::GoalStateMerger merger(*preprocessorResult.preprocessedModel); - auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, preprocessorResult.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end())); + auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, preprocessorResult.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end()), finiteRewardChoices); // Initialize data specific for the considered model type initializeModelTypeSpecificData(*mergerResult.model); @@ -175,20 +178,17 @@ namespace storm { std::unique_ptr> solver = solverFactory.create(env, ecQuotient->matrix); solver->setTrackScheduler(true); solver->setHasUniqueSolution(true); + solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); auto req = solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize, true); - boost::optional lowerBound = this->computeWeightedResultBound(true, weightVector, objectivesWithNoUpperTimeBound); - if (lowerBound) { - solver->setLowerBound(lowerBound.get()); + setBoundsToSolver(*solver, req.requiresLowerBounds(), req.requiresUpperBounds(), weightVector, objectivesWithNoUpperTimeBound, ecQuotient->matrix, ecQuotient->rowsWithSumLessOne, ecQuotient->auxChoiceValues); + if (solver->hasLowerBound()) { req.clearLowerBounds(); } - boost::optional upperBound = this->computeWeightedResultBound(false, weightVector, objectivesWithNoUpperTimeBound); - if (upperBound) { - solver->setUpperBound(upperBound.get()); + if (solver->hasUpperBound()) { req.clearUpperBounds(); } STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked."); solver->setRequirementsChecked(true); - solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); // Use the (0...0) vector as initial guess for the solution. std::fill(ecQuotient->auxStateValues.begin(), ecQuotient->auxStateValues.end(), storm::utility::zero()); @@ -208,11 +208,11 @@ namespace storm { if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) { storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], -storm::utility::one()); } - for (uint_fast64_t objIndex2 = 0; objIndex2 < this->objectives.size(); ++objIndex2) { - if (objIndex != objIndex2) { - objectiveResults[objIndex2] = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - } - } + for (uint_fast64_t objIndex2 = 0; objIndex2 < this->objectives.size(); ++objIndex2) { + if (objIndex != objIndex2) { + objectiveResults[objIndex2] = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + } + } } else { storm::storage::SparseMatrix deterministicMatrix = transitionMatrix.selectRowsFromRowGroups(this->optimalChoices, true); storm::storage::SparseMatrix deterministicBackwardTransitions = deterministicMatrix.transpose(); @@ -262,17 +262,19 @@ namespace storm { std::vector b = storm::utility::vector::filterVector(deterministicStateRewards, maybeStates); // Now solve the resulting equation system. - std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(submatrix)); + std::unique_ptr> solver = linearEquationSolverFactory.create(env, submatrix); auto req = solver->getRequirements(env); solver->clearBounds(); - if (obj.lowerResultBound) { + storm::storage::BitVector submatrixRowsWithSumLessOne = deterministicMatrix.getRowFilter(maybeStates, maybeStates) % maybeStates; + submatrixRowsWithSumLessOne.complement(); + this->setBoundsToSolver(*solver, req.requiresLowerBounds(), req.requiresUpperBounds(), objIndex, submatrix, submatrixRowsWithSumLessOne, b); + if (solver->hasLowerBound()) { req.clearLowerBounds(); - solver->setLowerBound(*obj.lowerResultBound); } - if (obj.upperResultBound) { - solver->setUpperBound(*obj.upperResultBound); + if (solver->hasUpperBound()) { req.clearUpperBounds(); } + STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the LinearEquationSolver was not met."); solver->solveEquations(env, x, b); @@ -311,11 +313,26 @@ namespace storm { // Remove neutral end components, i.e., ECs in which no reward is earned. auto ecElimResult = storm::transformer::EndComponentEliminator::transform(transitionMatrix, subsystemStates, ecChoicesHint & newReward0Choices, reward0EStates); + storm::storage::BitVector rowsWithSumLessOne(ecElimResult.matrix.getRowCount(), false); + for (uint64_t row = 0; row < rowsWithSumLessOne.size(); ++row) { + if (ecElimResult.matrix.getRow(row).getNumberOfEntries() == 0) { + rowsWithSumLessOne.set(row, true); + } else { + for (auto const& entry : transitionMatrix.getRow(ecElimResult.newToOldRowMapping[row])) { + if (!subsystemStates.get(entry.getColumn())) { + rowsWithSumLessOne.set(row, true); + break; + } + } + } + } + ecQuotient = EcQuotient(); ecQuotient->matrix = std::move(ecElimResult.matrix); ecQuotient->ecqToOriginalChoiceMapping = std::move(ecElimResult.newToOldRowMapping); ecQuotient->originalToEcqStateMapping = std::move(ecElimResult.oldToNewStateMapping); ecQuotient->origReward0Choices = std::move(newReward0Choices); + ecQuotient->rowsWithSumLessOne = std::move(rowsWithSumLessOne); ecQuotient->auxStateValues.reserve(transitionMatrix.getRowGroupCount()); ecQuotient->auxStateValues.resize(ecQuotient->matrix.getRowGroupCount()); ecQuotient->auxChoiceValues.reserve(transitionMatrix.getRowCount()); @@ -323,6 +340,91 @@ namespace storm { } } + template + void StandardPcaaWeightVectorChecker::setBoundsToSolver(storm::solver::AbstractEquationSolver& solver, bool requiresLower, bool requiresUpper, uint64_t objIndex, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector const& rewards) const { + + // Check whether bounds are already available + if (this->objectives[objIndex].lowerResultBound) { + solver.setLowerBound(this->objectives[objIndex].lowerResultBound.get()); + } + if (this->objectives[objIndex].upperResultBound) { + solver.setUpperBound(this->objectives[objIndex].upperResultBound.get()); + } + + if ((requiresLower && !solver.hasLowerBound()) || (requiresUpper && !solver.hasUpperBound())) { + computeAndSetBoundsToSolver(solver, requiresLower, requiresUpper, transitions, rowsWithSumLessOne, rewards); + } + } + + template + void StandardPcaaWeightVectorChecker::setBoundsToSolver(storm::solver::AbstractEquationSolver& solver, bool requiresLower, bool requiresUpper, std::vector const& weightVector, storm::storage::BitVector const& objectiveFilter, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector const& rewards) const { + + // Check whether bounds are already available + boost::optional lowerBound = this->computeWeightedResultBound(true, weightVector, objectiveFilter); + if (lowerBound) { + solver.setLowerBound(lowerBound.get()); + } + boost::optional upperBound = this->computeWeightedResultBound(false, weightVector, objectiveFilter); + if (upperBound) { + solver.setUpperBound(upperBound.get()); + } + + if ((requiresLower && !solver.hasLowerBound()) || (requiresUpper && !solver.hasUpperBound())) { + computeAndSetBoundsToSolver(solver, requiresLower, requiresUpper, transitions, rowsWithSumLessOne, rewards); + } + } + + template + void StandardPcaaWeightVectorChecker::computeAndSetBoundsToSolver(storm::solver::AbstractEquationSolver& solver, bool requiresLower, bool requiresUpper, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector const& rewards) const { + + // Compute the one step target probs + std::vector oneStepTargetProbs(transitions.getRowCount(), storm::utility::zero()); + for (auto const& row : rowsWithSumLessOne) { + oneStepTargetProbs[row] = storm::utility::one() - transitions.getRowSum(row); + } + + if (requiresLower && !solver.hasLowerBound()) { + // Compute lower bounds + std::vector negativeRewards; + negativeRewards.reserve(transitions.getRowCount()); + uint64_t row = 0; + for (auto const& rew : rewards) { + if (rew < storm::utility::zero()) { + negativeRewards.resize(row, storm::utility::zero()); + negativeRewards.push_back(-rew); + } + ++row; + } + if (!negativeRewards.empty()) { + negativeRewards.resize(row, storm::utility::zero()); + std::vector lowerBounds = storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer(transitions, negativeRewards, oneStepTargetProbs).computeUpperBounds(); + storm::utility::vector::scaleVectorInPlace(lowerBounds, -storm::utility::one()); + solver.setLowerBounds(std::move(lowerBounds)); + } else { + solver.setLowerBound(storm::utility::zero()); + } + } + + // Compute upper bounds + if (requiresUpper && !solver.hasUpperBound()) { + std::vector positiveRewards; + positiveRewards.reserve(transitions.getRowCount()); + uint64_t row = 0; + for (auto const& rew : rewards) { + if (rew > storm::utility::zero()) { + positiveRewards.resize(row, storm::utility::zero()); + positiveRewards.push_back(rew); + } + ++row; + } + if (!positiveRewards.empty()) { + positiveRewards.resize(row, storm::utility::zero()); + solver.setUpperBound(storm::modelchecker::helper::BaierUpperRewardBoundsComputer(transitions, positiveRewards, oneStepTargetProbs).computeUpperBound()); + } else { + solver.setUpperBound(storm::utility::zero()); + } + } + } template void StandardPcaaWeightVectorChecker::transformReducedSolutionToOriginalModel(storm::storage::SparseMatrix const& reducedMatrix, diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h index 86cd79c7f..2f0a27f33 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h @@ -1,5 +1,6 @@ #pragma once +#include "storm/solver/AbstractEquationSolver.h" #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/Scheduler.h" @@ -93,6 +94,11 @@ namespace storm { void updateEcQuotient(std::vector const& weightedRewardVector); + + void setBoundsToSolver(storm::solver::AbstractEquationSolver& solver, bool requiresLower, bool requiresUpper, uint64_t objIndex, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector const& rewards) const; + void setBoundsToSolver(storm::solver::AbstractEquationSolver& solver, bool requiresLower, bool requiresUpper, std::vector const& weightVector, storm::storage::BitVector const& objectiveFilter, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector const& rewards) const; + void computeAndSetBoundsToSolver(storm::solver::AbstractEquationSolver& solver, bool requiresLower, bool requiresUpper, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector const& rewards) const; + /*! * Transforms the results of a min-max-solver that considers a reduced model (without end components) to a result for the original (unreduced) model */ @@ -141,6 +147,7 @@ namespace storm { std::vector ecqToOriginalChoiceMapping; std::vector originalToEcqStateMapping; storm::storage::BitVector origReward0Choices; + storm::storage::BitVector rowsWithSumLessOne; std::vector auxStateValues; std::vector auxChoiceValues; diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 922adc4de..36e6eb9a2 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -36,21 +36,32 @@ namespace storm { template bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true)); + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true)); } template std::unique_ptr SparseDtmcPrctlModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); - STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); - STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); - std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); - std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *linearEquationSolverFactory, checkTask.getHint()); - std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); - return result; + if (pathFormula.isMultiDimensional() || pathFormula.getTimeBoundReference().isRewardBound()) { + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking non-trivial bounded until probabilities can only be computed for the initial states of the model."); + storm::logic::OperatorInformation opInfo; + if (checkTask.isBoundSet()) { + opInfo.bound = checkTask.getBound(); + } + auto formula = std::make_shared(checkTask.getFormula().asSharedPointer(), opInfo); + auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeRewardBoundedValues(env, this->getModel(), formula, *linearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } else { + STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); + std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeStepBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *linearEquationSolverFactory, checkTask.getHint()); + std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + return result; + } } template @@ -85,9 +96,20 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); - STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + if (rewardPathFormula.isMultiDimensional() || rewardPathFormula.getTimeBoundReference().isRewardBound()) { + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking non-trivial bounded until probabilities can only be computed for the initial states of the model."); + storm::logic::OperatorInformation opInfo; + if (checkTask.isBoundSet()) { + opInfo.bound = checkTask.getBound(); + } + auto formula = std::make_shared(checkTask.getFormula().asSharedPointer(), checkTask.getRewardModel(), opInfo); + auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeRewardBoundedValues(env, this->getModel(), formula, *linearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } else { + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 0d0ec5928..fd52e4437 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -15,6 +15,18 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" #include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h" +#include "storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h" + +#include "storm/environment/solver/SolverEnvironment.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/IOSettings.h" + +#include "storm/utility/Stopwatch.h" +#include "storm/utility/ProgressMeasurement.h" +#include "storm/utility/export.h" #include "storm/utility/macros.h" #include "storm/utility/ConstantsComparator.h" @@ -29,12 +41,12 @@ namespace storm { namespace modelchecker { namespace helper { template - std::vector SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { + std::vector SparseDtmcPrctlHelper::computeStepBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis. storm::storage::BitVector maybeStates; - + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); } else { @@ -68,8 +80,168 @@ namespace storm { return result; } + template + std::vector analyzeTrivialDtmcEpochModel(typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel) { + + std::vector epochResult; + epochResult.reserve(epochModel.epochInStates.getNumberOfSetBits()); + auto stepSolutionIt = epochModel.stepSolutions.begin(); + auto stepChoiceIt = epochModel.stepChoices.begin(); + for (auto const& state : epochModel.epochInStates) { + while (*stepChoiceIt < state) { + ++stepChoiceIt; + ++stepSolutionIt; + } + if (epochModel.objectiveRewardFilter.front().get(state)) { + if (*stepChoiceIt == state) { + epochResult.push_back(epochModel.objectiveRewards.front()[state] + *stepSolutionIt); + } else { + epochResult.push_back(epochModel.objectiveRewards.front()[state]); + } + } else { + if (*stepChoiceIt == state) { + epochResult.push_back(*stepSolutionIt); + } else { + epochResult.push_back(storm::utility::zero()); + } + } + } + return epochResult; + } + + template + std::vector analyzeNonTrivialDtmcEpochModel(Environment const& env, typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel, std::vector& x, std::vector& b, std::unique_ptr>& linEqSolver, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional const& lowerBound, boost::optional const& upperBound) { + + // Update some data for the case that the Matrix has changed + if (epochModel.epochMatrixChanged) { + x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); + linEqSolver = linearEquationSolverFactory.create(env, epochModel.epochMatrix, storm::solver::LinearEquationSolverTask::SolveEquations); + linEqSolver->setCachingEnabled(true); + auto req = linEqSolver->getRequirements(env, storm::solver::LinearEquationSolverTask::SolveEquations); + if (lowerBound) { + linEqSolver->setLowerBound(lowerBound.get()); + req.clearLowerBounds(); + } + if (upperBound) { + linEqSolver->setUpperBound(upperBound.get()); + req.clearUpperBounds(); + } + STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked."); + } + + // Prepare the right hand side of the equation system + b.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero()); + std::vector const& objectiveValues = epochModel.objectiveRewards.front(); + for (auto const& choice : epochModel.objectiveRewardFilter.front()) { + b[choice] = objectiveValues[choice]; + } + auto stepSolutionIt = epochModel.stepSolutions.begin(); + for (auto const& choice : epochModel.stepChoices) { + b[choice] += *stepSolutionIt; + ++stepSolutionIt; + } + assert(stepSolutionIt == epochModel.stepSolutions.end()); + + // Solve the minMax equation system + linEqSolver->solveEquations(env, x, b); + + return storm::utility::vector::filterVector(x, epochModel.epochInStates); + } + + template<> + std::map SparseDtmcPrctlHelper::computeRewardBoundedValues(Environment const& env, storm::models::sparse::Dtmc const& model, std::shared_ptr rewardBoundedFormula, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The specified property is not supported by this value type."); + return std::map(); + } + template + std::map SparseDtmcPrctlHelper::computeRewardBoundedValues(Environment const& env, storm::models::sparse::Dtmc const& model, std::shared_ptr rewardBoundedFormula, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + storm::utility::Stopwatch swAll(true), swBuild, swCheck; + + storm::modelchecker::helper::rewardbounded::MultiDimensionalRewardUnfolding rewardUnfolding(model, rewardBoundedFormula); + + // Get lower and upper bounds for the solution. + auto lowerBound = rewardUnfolding.getLowerObjectiveBound(); + auto upperBound = rewardUnfolding.getUpperObjectiveBound(); + + // Initialize epoch models + auto initEpoch = rewardUnfolding.getStartEpoch(); + auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch); + + // initialize data that will be needed for each epoch + std::vector x, b; + std::unique_ptr> linEqSolver; + Environment preciseEnv = env; + ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision(initEpoch, storm::utility::convertNumber(storm::settings::getModule().getPrecision())); + preciseEnv.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber(precision)); + + // In case of cdf export we store the necessary data. + std::vector> cdfData; + + // Set the correct equation problem format + rewardUnfolding.setEquationSystemFormatForEpochModel(linearEquationSolverFactory.getEquationProblemFormat(preciseEnv)); + bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(preciseEnv) == solver::LinearEquationSolverProblemFormat::EquationSystem; + + storm::utility::ProgressMeasurement progress("epochs"); + progress.setMaxCount(epochOrder.size()); + progress.startNewMeasurement(0); + uint64_t numCheckedEpochs = 0; + for (auto const& epoch : epochOrder) { + swBuild.start(); + auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); + swBuild.stop(); swCheck.start(); + // If the epoch matrix is empty we do not need to solve a linear equation system + if ((convertToEquationSystem && epochModel.epochMatrix.isIdentityMatrix()) || (!convertToEquationSystem && epochModel.epochMatrix.getEntryCount() == 0)) { + rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialDtmcEpochModel(epochModel)); + } else { + rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialDtmcEpochModel(preciseEnv, epochModel, x, b, linEqSolver, linearEquationSolverFactory, lowerBound, upperBound)); + } + swCheck.stop(); + if (storm::settings::getModule().isExportCdfSet() && !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) { + std::vector cdfEntry; + for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) { + uint64_t offset = rewardUnfolding.getDimension(i).isUpperBounded ? 0 : 1; + cdfEntry.push_back(storm::utility::convertNumber(rewardUnfolding.getEpochManager().getDimensionOfEpoch(epoch, i) + offset) * rewardUnfolding.getDimension(i).scalingFactor); + } + cdfEntry.push_back(rewardUnfolding.getInitialStateResult(epoch)); + cdfData.push_back(std::move(cdfEntry)); + } + ++numCheckedEpochs; + progress.updateProgress(numCheckedEpochs); + } + + std::map result; + for (auto const& initState : model.getInitialStates()) { + result[initState] = rewardUnfolding.getInitialStateResult(initEpoch, initState); + } + + swAll.stop(); + + if (storm::settings::getModule().isExportCdfSet()) { + std::vector headers; + for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) { + headers.push_back(rewardUnfolding.getDimension(i).formula->toString()); + } + headers.push_back("Result"); + storm::utility::exportDataToCSVFile(storm::settings::getModule().getExportCdfDirectory() + "cdf.csv", cdfData, headers); + } + + if (storm::settings::getModule().isShowStatisticsSet()) { + STORM_PRINT_AND_LOG("---------------------------------" << std::endl); + STORM_PRINT_AND_LOG("Statistics:" << std::endl); + STORM_PRINT_AND_LOG("---------------------------------" << std::endl); + STORM_PRINT_AND_LOG(" #checked epochs: " << epochOrder.size() << "." << std::endl); + STORM_PRINT_AND_LOG(" overall Time: " << swAll << "." << std::endl); + STORM_PRINT_AND_LOG("Epoch Model building Time: " << swBuild << "." << std::endl); + STORM_PRINT_AND_LOG("Epoch Model checking Time: " << swCheck << "." << std::endl); + STORM_PRINT_AND_LOG("---------------------------------" << std::endl); + } + + return result; + } + + template std::vector SparseDtmcPrctlHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); @@ -427,7 +599,7 @@ namespace storm { } // Build the new transition matrix and the new targets. - result.transitionMatrix = builder.build(); + result.transitionMatrix = builder.build(addDeadlockState ? (deadlockState + 1) : deadlockState); storm::storage::BitVector newTargetStates = targetStates % result.beforeStates; newTargetStates.resize(result.transitionMatrix.get().getRowCount()); for (auto state : targetStates % statesWithProbabilityGreater0) { @@ -440,19 +612,36 @@ namespace storm { std::vector newStateRewards(result.beforeStates.getNumberOfSetBits()); storm::utility::vector::selectVectorValues(newStateRewards, result.beforeStates, stateRewards.get()); - newStateRewards.reserve(newStateRewards.size() + statesWithProbabilityGreater0.getNumberOfSetBits() + 1); + newStateRewards.reserve(result.transitionMatrix.get().getRowCount()); for (auto state : statesWithProbabilityGreater0) { newStateRewards.push_back(stateRewards.get()[state]); } // Add a zero reward to the deadlock state. - newStateRewards.push_back(storm::utility::zero()); + if (addDeadlockState) { + newStateRewards.push_back(storm::utility::zero()); + } result.stateRewards = std::move(newStateRewards); } - } return result; } + + template + storm::storage::BitVector SparseDtmcPrctlHelper::BaierTransformedModel::getNewRelevantStates() const { + storm::storage::BitVector newRelevantStates(transitionMatrix.get().getRowCount()); + for (uint64_t i = 0; i < this->beforeStates.getNumberOfSetBits(); ++i) { + newRelevantStates.set(i); + } + return newRelevantStates; + } + + template + storm::storage::BitVector SparseDtmcPrctlHelper::BaierTransformedModel::getNewRelevantStates(storm::storage::BitVector const& oldRelevantStates) const { + storm::storage::BitVector result = oldRelevantStates % this->beforeStates; + result.resize(transitionMatrix.get().getRowCount()); + return result; + } template std::vector SparseDtmcPrctlHelper::computeConditionalProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { @@ -472,6 +661,13 @@ namespace storm { // Now compute reachability probabilities in the transformed model. storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); + storm::storage::BitVector newRelevantValues; + if (goal.hasRelevantValues()) { + newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues()); + } else { + newRelevantValues = transformedModel.getNewRelevantStates(); + } + goal.setRelevantValues(std::move(newRelevantValues)); std::vector conditionalProbabilities = computeUntilProbabilities(env, std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory); storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities); @@ -498,6 +694,13 @@ namespace storm { // Now compute reachability probabilities in the transformed model. storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); + storm::storage::BitVector newRelevantValues; + if (goal.hasRelevantValues()) { + newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues()); + } else { + newRelevantValues = transformedModel.getNewRelevantStates(); + } + goal.setRelevantValues(std::move(newRelevantValues)); std::vector conditionalRewards = computeReachabilityRewards(env, std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), transformedModel.stateRewards.get(), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory); storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalRewards); } diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 6564c4f5d..ead15de74 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -5,6 +5,7 @@ #include +#include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/hints/ModelCheckerHint.h" @@ -26,7 +27,10 @@ namespace storm { template > class SparseDtmcPrctlHelper { public: - static std::vector computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); + + static std::vector computeStepBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); + + static std::map computeRewardBoundedValues(Environment const& env, storm::models::sparse::Dtmc const& model, std::shared_ptr rewardBoundedFormula, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::vector computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); @@ -59,7 +63,10 @@ namespace storm { BaierTransformedModel() : noTargetStates(false) { // Intentionally left empty. } - + + storm::storage::BitVector getNewRelevantStates(storm::storage::BitVector const& oldRelevantStates) const; + storm::storage::BitVector getNewRelevantStates() const; + storm::storage::BitVector beforeStates; boost::optional> transitionMatrix; boost::optional targetStates; diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 8c7b0dc7e..10311c2a2 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -87,7 +87,7 @@ namespace storm { } template - std::vector analyzeTrivialEpochModel(OptimizationDirection dir, typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel) { + std::vector analyzeTrivialMdpEpochModel(OptimizationDirection dir, typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel) { // Assert that the epoch model is indeed trivial assert(epochModel.epochMatrix.getEntryCount() == 0); @@ -137,7 +137,7 @@ namespace storm { } template - std::vector analyzeNonTrivialEpochModel(Environment const& env, OptimizationDirection dir, typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel, std::vector& x, std::vector& b, std::unique_ptr>& minMaxSolver, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional const& lowerBound, boost::optional const& upperBound) { + std::vector analyzeNonTrivialMdpEpochModel(Environment const& env, OptimizationDirection dir, typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel, std::vector& x, std::vector& b, std::unique_ptr>& minMaxSolver, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional const& lowerBound, boost::optional const& upperBound) { // Update some data for the case that the Matrix has changed if (epochModel.epochMatrixChanged) { @@ -215,9 +215,9 @@ namespace storm { swBuild.stop(); swCheck.start(); // If the epoch matrix is empty we do not need to solve a linear equation system if (epochModel.epochMatrix.getEntryCount() == 0) { - rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialEpochModel(dir, epochModel)); + rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialMdpEpochModel(dir, epochModel)); } else { - rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialEpochModel(preciseEnv, dir, epochModel, x, b, minMaxSolver, minMaxLinearEquationSolverFactory, lowerBound, upperBound)); + rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialMdpEpochModel(preciseEnv, dir, epochModel, x, b, minMaxSolver, minMaxLinearEquationSolverFactory, lowerBound, upperBound)); } swCheck.stop(); if (storm::settings::getModule().isExportCdfSet() && !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) { diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp index ec599fd37..efc3c81f7 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -10,6 +10,8 @@ #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Dtmc.h" #include "storm/transformer/EndComponentEliminator.h" @@ -24,14 +26,13 @@ namespace storm { namespace rewardbounded { template - MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::vector> const& objectives) : model(model), objectives(objectives) { + MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Model const& model, std::vector> const& objectives) : model(model), objectives(objectives) { initialize(); } template - MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::shared_ptr objectiveFormula) : model(model) { + MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Model const& model, std::shared_ptr objectiveFormula) : model(model) { - STORM_LOG_THROW(objectiveFormula->hasOptimalityType(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); if (objectiveFormula->isProbabilityOperatorFormula()) { if (objectiveFormula->getSubformula().isMultiObjectiveFormula()) { for (auto const& subFormula : objectiveFormula->getSubformula().asMultiObjectiveFormula().getSubformulas()) { @@ -91,7 +92,7 @@ namespace storm { // lower bounded until formulas with non-trivial left hand side are excluded as this would require some additional effort (in particular the ProductModel::transformMemoryState method). STORM_LOG_THROW(dimension.isUpperBounded || subformula.getLeftSubformula(dim).isTrueFormula(), storm::exceptions::NotSupportedException, "Lower bounded until formulas are only supported by this method if the left subformula is 'true'. Got " << subformula << " instead."); if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) { - dimensionWiseEpochSteps.push_back(std::vector(model.getNumberOfChoices(), 1)); + dimensionWiseEpochSteps.push_back(std::vector(model.getTransitionMatrix().getRowCount(), 1)); dimension.scalingFactor = storm::utility::one(); } else { STORM_LOG_ASSERT(subformula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound."); @@ -114,7 +115,7 @@ namespace storm { dimension.objectiveIndex = objIndex; dimension.isUpperBounded = true; if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) { - dimensionWiseEpochSteps.push_back(std::vector(model.getNumberOfChoices(), 1)); + dimensionWiseEpochSteps.push_back(std::vector(model.getTransitionMatrix().getRowCount(), 1)); dimension.scalingFactor = storm::utility::one(); } else { STORM_LOG_ASSERT(subformula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound."); @@ -166,8 +167,8 @@ namespace storm { epochManager = EpochManager(dimensions.size()); // Convert the epoch steps to a choice-wise representation - epochSteps.reserve(model.getNumberOfChoices()); - for (uint64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) { + epochSteps.reserve(model.getTransitionMatrix().getRowCount()); + for (uint64_t choice = 0; choice < model.getTransitionMatrix().getRowCount(); ++choice) { Epoch step; uint64_t dim = 0; for (auto const& dimensionSteps : dimensionWiseEpochSteps) { @@ -396,7 +397,7 @@ namespace storm { // std::cout << "Setting epoch class for epoch " << epochManager.toString(epoch) << std::endl; auto productObjectiveRewards = productModel->computeObjectiveRewards(epochClass, objectives); - storm::storage::BitVector stepChoices(productModel->getProduct().getNumberOfChoices(), false); + storm::storage::BitVector stepChoices(productModel->getProduct().getTransitionMatrix().getRowCount(), false); uint64_t choice = 0; for (auto const& step : productModel->getSteps()) { if (!epochManager.isZeroEpoch(step) && epochManager.getSuccessorEpoch(epoch, step) != epoch) { @@ -421,7 +422,7 @@ namespace storm { } } - storm::storage::BitVector zeroObjRewardChoices(productModel->getProduct().getNumberOfChoices(), true); + storm::storage::BitVector zeroObjRewardChoices(productModel->getProduct().getTransitionMatrix().getRowCount(), true); for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { if (violatedLowerBoundedDimensions.isDisjointFrom(objectiveDimensions[objIndex])) { zeroObjRewardChoices &= storm::utility::vector::filterZero(productObjectiveRewards[objIndex]); @@ -433,15 +434,68 @@ namespace storm { storm::storage::BitVector productInStates = productModel->getInStates(epochClass); // The epoch model only needs to consider the states that are reachable from a relevant state storm::storage::BitVector consideredStates = storm::utility::graph::getReachableStates(epochModel.epochMatrix, productInStates, allProductStates, ~allProductStates); - // std::cout << "numInStates = " << productInStates.getNumberOfSetBits() << std::endl; - // std::cout << "numConsideredStates = " << consideredStates.getNumberOfSetBits() << std::endl; // We assume that there is no end component in which objective reward is earned STORM_LOG_ASSERT(!storm::utility::graph::checkIfECWithChoiceExists(epochModel.epochMatrix, epochModel.epochMatrix.transpose(true), allProductStates, ~zeroObjRewardChoices & ~stepChoices), "There is a scheduler that yields infinite reward for one objective. This case should be excluded"); - auto ecElimResult = storm::transformer::EndComponentEliminator::transform(epochModel.epochMatrix, consideredStates, zeroObjRewardChoices & ~stepChoices, consideredStates); - epochModel.epochMatrix = std::move(ecElimResult.matrix); - epochModelToProductChoiceMap = std::move(ecElimResult.newToOldRowMapping); + // Create the epoch model matrix + std::vector productToEpochModelStateMapping; + if (model.isOfType(storm::models::ModelType::Dtmc)) { + assert(zeroObjRewardChoices.size() == productModel->getProduct().getNumberOfStates()); + assert(stepChoices.size() == productModel->getProduct().getNumberOfStates()); + STORM_LOG_ASSERT(equationSolverProblemFormatForEpochModel.is_initialized(), "Linear equation problem format was not set."); + bool convertToEquationSystem = equationSolverProblemFormatForEpochModel.get() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + // For DTMCs we consider the subsystem induced by the considered states. + // The transitions for states with zero reward are filtered out to guarantee a unique solution of the eq-system. + auto backwardTransitions = epochModel.epochMatrix.transpose(true); + storm::storage::BitVector nonZeroRewardStates = storm::utility::graph::performProbGreater0(backwardTransitions, consideredStates, consideredStates & (~zeroObjRewardChoices | stepChoices)); + // If there is at least one considered state with reward zero, we have to add a 'zero-reward-state' to the epoch model. + bool requiresZeroRewardState = nonZeroRewardStates != consideredStates; + uint64_t numEpochModelStates = nonZeroRewardStates.getNumberOfSetBits(); + uint64_t zeroRewardInState = numEpochModelStates; + if (requiresZeroRewardState) { + ++numEpochModelStates; + } + storm::storage::SparseMatrixBuilder builder; + if (!nonZeroRewardStates.empty()) { + builder = storm::storage::SparseMatrixBuilder(epochModel.epochMatrix.getSubmatrix(true, nonZeroRewardStates, nonZeroRewardStates, convertToEquationSystem)); + } + if (requiresZeroRewardState) { + if (convertToEquationSystem) { + // add a diagonal entry + builder.addNextValue(zeroRewardInState, zeroRewardInState, storm::utility::zero()); + } + epochModel.epochMatrix = builder.build(numEpochModelStates, numEpochModelStates); + } else { + assert (!nonZeroRewardStates.empty()); + epochModel.epochMatrix = builder.build(); + } + if (convertToEquationSystem) { + epochModel.epochMatrix.convertToEquationSystem(); + } + + epochModelToProductChoiceMap.clear(); + epochModelToProductChoiceMap.reserve(numEpochModelStates); + productToEpochModelStateMapping.assign(nonZeroRewardStates.size(), zeroRewardInState); + for (auto const& productState : nonZeroRewardStates) { + productToEpochModelStateMapping[productState] = epochModelToProductChoiceMap.size(); + epochModelToProductChoiceMap.push_back(productState); + } + if (requiresZeroRewardState) { + uint64_t zeroRewardProductState = (consideredStates & ~nonZeroRewardStates).getNextSetIndex(0); + assert(zeroRewardProductState < consideredStates.size()); + epochModelToProductChoiceMap.push_back(zeroRewardProductState); + } + } else if (model.isOfType(storm::models::ModelType::Mdp)) { + // Eliminate zero-reward end components + auto ecElimResult = storm::transformer::EndComponentEliminator::transform(epochModel.epochMatrix, consideredStates, zeroObjRewardChoices & ~stepChoices, consideredStates); + epochModel.epochMatrix = std::move(ecElimResult.matrix); + epochModelToProductChoiceMap = std::move(ecElimResult.newToOldRowMapping); + productToEpochModelStateMapping = std::move(ecElimResult.oldToNewStateMapping); + } else { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unsupported model type."); + } + epochModel.stepChoices = storm::storage::BitVector(epochModel.epochMatrix.getRowCount(), false); for (uint64_t choice = 0; choice < epochModel.epochMatrix.getRowCount(); ++choice) { if (stepChoices.get(epochModelToProductChoiceMap[choice])) { @@ -466,14 +520,14 @@ namespace storm { epochModel.epochInStates = storm::storage::BitVector(epochModel.epochMatrix.getRowGroupCount(), false); for (auto const& productState : productInStates) { - STORM_LOG_ASSERT(ecElimResult.oldToNewStateMapping[productState] < epochModel.epochMatrix.getRowGroupCount(), "Selected product state does not exist in the epoch model."); - epochModel.epochInStates.set(ecElimResult.oldToNewStateMapping[productState], true); + STORM_LOG_ASSERT(productToEpochModelStateMapping[productState] < epochModel.epochMatrix.getRowGroupCount(), "Selected product state does not exist in the epoch model."); + epochModel.epochInStates.set(productToEpochModelStateMapping[productState], true); } std::vector toEpochModelInStatesMap(productModel->getProduct().getNumberOfStates(), std::numeric_limits::max()); std::vector epochModelStateToInStateMap = epochModel.epochInStates.getNumberOfSetBitsBeforeIndices(); for (auto const& productState : productInStates) { - toEpochModelInStatesMap[productState] = epochModelStateToInStateMap[ecElimResult.oldToNewStateMapping[productState]]; + toEpochModelInStatesMap[productState] = epochModelStateToInStateMap[productToEpochModelStateMapping[productState]]; } productStateToEpochModelInStateMap = std::make_shared const>(std::move(toEpochModelInStatesMap)); @@ -487,6 +541,13 @@ namespace storm { } + template + void MultiDimensionalRewardUnfolding::setEquationSystemFormatForEpochModel(storm::solver::LinearEquationSolverProblemFormat eqSysFormat) { + STORM_LOG_ASSERT(model.isOfType(storm::models::ModelType::Dtmc), "Trying to set the equation problem format although the model is not deterministic."); + equationSolverProblemFormatForEpochModel = eqSysFormat; + } + + template template::type> typename MultiDimensionalRewardUnfolding::SolutionType MultiDimensionalRewardUnfolding::getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const { diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h index 11a15a82a..e1b96c64c 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -8,7 +8,8 @@ #include "storm/modelchecker/prctl/helper/rewardbounded/EpochManager.h" #include "storm/modelchecker/prctl/helper/rewardbounded/ProductModel.h" #include "storm/modelchecker/prctl/helper/rewardbounded/Dimension.h" -#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Model.h" +#include "storm/solver/LinearEquationSolverProblemFormat.h" #include "storm/utility/vector.h" #include "storm/storage/memorystructure/MemoryStructure.h" #include "storm/utility/Stopwatch.h" @@ -43,8 +44,8 @@ namespace storm { * @param objectives The (preprocessed) objectives * */ - MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::vector> const& objectives); - MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::shared_ptr objectiveFormula); + MultiDimensionalRewardUnfolding(storm::models::sparse::Model const& model, std::vector> const& objectives); + MultiDimensionalRewardUnfolding(storm::models::sparse::Model const& model, std::shared_ptr objectiveFormula); ~MultiDimensionalRewardUnfolding() = default; @@ -53,6 +54,8 @@ namespace storm { EpochModel& setCurrentEpoch(Epoch const& epoch); + void setEquationSystemFormatForEpochModel(storm::solver::LinearEquationSolverProblemFormat eqSysFormat); + /*! * Returns the precision required for the analyzis of each epoch model in order to achieve the given overall precision */ @@ -106,7 +109,7 @@ namespace storm { EpochSolution const& getEpochSolution(std::map const& solutions, Epoch const& epoch); SolutionType const& getStateSolution(EpochSolution const& epochSolution, uint64_t const& productState); - storm::models::sparse::Mdp const& model; + storm::models::sparse::Model const& model; std::vector> objectives; std::unique_ptr> productModel; @@ -118,6 +121,9 @@ namespace storm { EpochModel epochModel; boost::optional currentEpoch; + // In case of DTMCs we have different options for the equation problem format the epoch model will have. + boost::optional equationSolverProblemFormatForEpochModel; + EpochManager epochManager; std::vector> dimensions; diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp index fa327d34e..af41c8a4f 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp @@ -9,6 +9,8 @@ #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Dtmc.h" #include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/NotSupportedException.h" @@ -19,7 +21,7 @@ namespace storm { namespace rewardbounded { template - ProductModel::ProductModel(storm::models::sparse::Mdp const& model, std::vector> const& objectives, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector const& originalModelSteps) : dimensions(dimensions), objectiveDimensions(objectiveDimensions), epochManager(epochManager), memoryStateManager(dimensions.size()) { + ProductModel::ProductModel(storm::models::sparse::Model const& model, std::vector> const& objectives, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector const& originalModelSteps) : dimensions(dimensions), objectiveDimensions(objectiveDimensions), epochManager(epochManager), memoryStateManager(dimensions.size()) { for (uint64_t dim = 0; dim < dimensions.size(); ++dim) { if (!dimensions[dim].memoryLabel) { @@ -34,7 +36,7 @@ namespace storm { storm::storage::SparseModelMemoryProduct productBuilder(memory.product(model)); setReachableProductStates(productBuilder, originalModelSteps, memoryStateMap); - product = productBuilder.build()->template as>(); + product = productBuilder.build(); uint64_t numModelStates = productBuilder.getOriginalModel().getNumberOfStates(); MemoryState upperMemStateBound = memoryStateManager.getUpperMemoryStateBound(); @@ -57,7 +59,7 @@ namespace storm { } // Map choice indices of the product to the state where it origins - choiceToStateMap.reserve(getProduct().getNumberOfChoices()); + choiceToStateMap.reserve(getProduct().getTransitionMatrix().getRowCount()); for (uint64_t productState = 0; productState < numProductStates; ++productState) { uint64_t groupSize = getProduct().getTransitionMatrix().getRowGroupSize(productState); for (uint64_t i = 0; i < groupSize; ++i) { @@ -66,7 +68,7 @@ namespace storm { } // Compute the epoch steps for the product - steps.resize(getProduct().getNumberOfChoices(), 0); + steps.resize(getProduct().getTransitionMatrix().getRowCount(), 0); for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) { uint64_t numChoices = productBuilder.getOriginalModel().getTransitionMatrix().getRowGroupSize(modelState); uint64_t firstChoice = productBuilder.getOriginalModel().getTransitionMatrix().getRowGroupIndices()[modelState]; @@ -92,9 +94,9 @@ namespace storm { template - storm::storage::MemoryStructure ProductModel::computeMemoryStructure(storm::models::sparse::Mdp const& model, std::vector> const& objectives) const { + storm::storage::MemoryStructure ProductModel::computeMemoryStructure(storm::models::sparse::Model const& model, std::vector> const& objectives) const { - storm::modelchecker::SparsePropositionalModelChecker> mc(model); + storm::modelchecker::SparsePropositionalModelChecker> mc(model); // Create a memory structure that remembers whether (sub)objectives are satisfied storm::storage::MemoryStructure memory = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(model); @@ -285,7 +287,7 @@ namespace storm { } template - storm::models::sparse::Mdp const& ProductModel::getProduct() const { + storm::models::sparse::Model const& ProductModel::getProduct() const { return *product; } @@ -341,7 +343,7 @@ namespace storm { for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { auto const& formula = *objectives[objIndex].formula; if (formula.isProbabilityOperatorFormula()) { - storm::modelchecker::SparsePropositionalModelChecker> mc(getProduct()); + storm::modelchecker::SparsePropositionalModelChecker> mc(getProduct()); std::vector dimensionIndexMap; for (auto const& globalDimensionIndex : objectiveDimensions[objIndex]) { dimensionIndexMap.push_back(globalDimensionIndex); diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.h b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.h index 4aaf90796..3f5b2a9a7 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.h +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.h @@ -7,7 +7,7 @@ #include "storm/modelchecker/prctl/helper/rewardbounded/EpochManager.h" #include "storm/modelchecker/prctl/helper/rewardbounded/MemoryStateManager.h" #include "storm/modelchecker/prctl/helper/rewardbounded/Dimension.h" -#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Model.h" #include "storm/utility/vector.h" #include "storm/storage/memorystructure/MemoryStructure.h" #include "storm/storage/memorystructure/SparseModelMemoryProduct.h" @@ -26,9 +26,9 @@ namespace storm { typedef typename MemoryStateManager::MemoryState MemoryState; - ProductModel(storm::models::sparse::Mdp const& model, std::vector> const& objectives, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector const& originalModelSteps); + ProductModel(storm::models::sparse::Model const& model, std::vector> const& objectives, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector const& originalModelSteps); - storm::models::sparse::Mdp const& getProduct() const; + storm::models::sparse::Model const& getProduct() const; std::vector const& getSteps() const; bool productStateExists(uint64_t const& modelState, uint64_t const& memoryState) const; @@ -50,7 +50,7 @@ namespace storm { private: - storm::storage::MemoryStructure computeMemoryStructure(storm::models::sparse::Mdp const& model, std::vector> const& objectives) const; + storm::storage::MemoryStructure computeMemoryStructure(storm::models::sparse::Model const& model, std::vector> const& objectives) const; std::vector computeMemoryStateMap(storm::storage::MemoryStructure const& memory) const; @@ -66,7 +66,7 @@ namespace storm { EpochManager const& epochManager; MemoryStateManager memoryStateManager; - std::shared_ptr> product; + std::shared_ptr> product; std::vector steps; std::map reachableStates; std::map inStates; diff --git a/src/storm/models/ModelBase.h b/src/storm/models/ModelBase.h index 9eace3911..e816adac6 100644 --- a/src/storm/models/ModelBase.h +++ b/src/storm/models/ModelBase.h @@ -71,7 +71,14 @@ namespace storm { * @return The number of (non-zero) transitions of the model. */ virtual uint_fast64_t getNumberOfTransitions() const = 0; - + + /*! + * Returns the number of choices ine the model. + * + * @return The number of choices in of the model. + */ + virtual uint_fast64_t getNumberOfChoices() const = 0; + /*! * Prints information about the model to the specified stream. * diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index 0fb7fc4fc..0cb7ec8cc 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -98,7 +98,12 @@ namespace storm { uint_fast64_t Model::getNumberOfTransitions() const { return this->getTransitionMatrix().getNonzeroEntryCount(); } - + + template + uint_fast64_t Model::getNumberOfChoices() const { + return this->getTransitionMatrix().getRowCount(); + } + template storm::storage::BitVector const& Model::getInitialStates() const { return this->getStates("init"); diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index b796a30f9..aa61eb3bd 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -76,7 +76,14 @@ namespace storm { * @return The number of (non-zero) transitions of the model. */ virtual uint_fast64_t getNumberOfTransitions() const override; - + + /*! + * Returns the number of choices ine the model. + * + * @return The number of choices in of the model. + */ + virtual uint_fast64_t getNumberOfChoices() const override; + /*! * Retrieves the initial states of the model. * diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index cd67e384f..263f67c16 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -26,11 +26,6 @@ namespace storm { // Intentionally left empty } - template - uint_fast64_t NondeterministicModel::getNumberOfChoices() const { - return this->getTransitionMatrix().getRowCount(); - } - template std::vector const& NondeterministicModel::getNondeterministicChoiceIndices() const { return this->getTransitionMatrix().getRowGroupIndices(); diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h index dd1335718..ac8603e7f 100644 --- a/src/storm/models/sparse/NondeterministicModel.h +++ b/src/storm/models/sparse/NondeterministicModel.h @@ -19,10 +19,8 @@ namespace storm { * The base class of sparse nondeterministic models. */ template> - class NondeterministicModel: public Model { + class NondeterministicModel : public Model { public: - - /*! * Constructs a model from the given data. * @@ -31,13 +29,6 @@ namespace storm { */ NondeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents const& components); NondeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents&& components); - - /*! - * Retrieves the number of (nondeterministic) choices in the model. - * - * @return The number of (nondeterministic) choices in the model. - */ - uint_fast64_t getNumberOfChoices() const; /*! * Retrieves the vector indicating which matrix rows represent non-deterministic choices of a certain state. @@ -46,6 +37,8 @@ namespace storm { */ std::vector const& getNondeterministicChoiceIndices() const; + using Model::getNumberOfChoices; + /*! * @param state State for which we want to know how many choices it has * diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index f468cc377..5364a4d4f 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -64,6 +64,11 @@ namespace storm { uint_fast64_t Model::getNumberOfTransitions() const { return transitionMatrix.getNonZeroCount(); } + + template + uint_fast64_t Model::getNumberOfChoices() const { + return reachableStates.getNonZeroCount(); + } template storm::dd::DdManager& Model::getManager() const { diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index fd0839a2b..2f39d3970 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -119,6 +119,8 @@ namespace storm { virtual uint_fast64_t getNumberOfTransitions() const override; + virtual uint_fast64_t getNumberOfChoices() const override; + /*! * Retrieves the manager responsible for the DDs that represent this model. * diff --git a/src/storm/models/symbolic/NondeterministicModel.h b/src/storm/models/symbolic/NondeterministicModel.h index c75874644..7fb42cf7b 100644 --- a/src/storm/models/symbolic/NondeterministicModel.h +++ b/src/storm/models/symbolic/NondeterministicModel.h @@ -90,7 +90,7 @@ namespace storm { * * @return The number of nondeterministic choices in the model. */ - uint_fast64_t getNumberOfChoices() const; + virtual uint_fast64_t getNumberOfChoices() const override; /*! * Retrieves the meta variables used to encode the nondeterminism in the model. diff --git a/src/storm/solver/AbstractEquationSolver.cpp b/src/storm/solver/AbstractEquationSolver.cpp index 4d0a34abc..d17a9041d 100644 --- a/src/storm/solver/AbstractEquationSolver.cpp +++ b/src/storm/solver/AbstractEquationSolver.cpp @@ -139,6 +139,11 @@ namespace storm { lowerBounds = values; } + template + void AbstractEquationSolver::setLowerBounds(std::vector&& values) { + lowerBounds = std::move(values); + } + template void AbstractEquationSolver::setUpperBounds(std::vector const& values) { upperBounds = values; diff --git a/src/storm/solver/AbstractEquationSolver.h b/src/storm/solver/AbstractEquationSolver.h index 64eab4d1d..d5000f8c7 100644 --- a/src/storm/solver/AbstractEquationSolver.h +++ b/src/storm/solver/AbstractEquationSolver.h @@ -117,6 +117,11 @@ namespace storm { */ void setLowerBounds(std::vector const& values); + /*! + * Sets lower bounds for the solution that can potentially be used by the solver. + */ + void setLowerBounds(std::vector&& values); + /*! * Sets upper bounds for the solution that can potentially be used by the solver. */ diff --git a/src/storm/solver/SmtlibSmtSolver.cpp b/src/storm/solver/SmtlibSmtSolver.cpp index 69394ec8a..aad46d81e 100644 --- a/src/storm/solver/SmtlibSmtSolver.cpp +++ b/src/storm/solver/SmtlibSmtSolver.cpp @@ -103,7 +103,7 @@ namespace storm { } void SmtlibSmtSolver::add(const storm::RationalFunctionVariable& variable, bool value){ - STORM_LOG_THROW((variable.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a constraint that consists of a non-boolean variable."); + STORM_LOG_THROW((variable.type()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a constraint that consists of a non-boolean variable."); std::set variableSet; variableSet.insert(variable); std::vector const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variableSet); diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 9d92d5e35..36dd5724e 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -87,7 +87,7 @@ namespace storm { } template - SparseMatrixBuilder::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool forceDimensions, bool hasCustomRowGrouping, index_type rowGroups) : initialRowCountSet(rows != 0), initialRowCount(rows), initialColumnCountSet(columns != 0), initialColumnCount(columns), initialEntryCountSet(entries != 0), initialEntryCount(entries), forceInitialDimensions(forceDimensions), hasCustomRowGrouping(hasCustomRowGrouping), initialRowGroupCountSet(rowGroups != 0), initialRowGroupCount(rowGroups), rowGroupIndices(), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), highestColumn(0), currentRowGroup(0) { + SparseMatrixBuilder::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool forceDimensions, bool hasCustomRowGrouping, index_type rowGroups) : initialRowCountSet(rows != 0), initialRowCount(rows), initialColumnCountSet(columns != 0), initialColumnCount(columns), initialEntryCountSet(entries != 0), initialEntryCount(entries), forceInitialDimensions(forceDimensions), hasCustomRowGrouping(hasCustomRowGrouping), initialRowGroupCountSet(rowGroups != 0), initialRowGroupCount(rowGroups), rowGroupIndices(), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), highestColumn(0), currentRowGroupCount(0) { // Prepare the internal storage. if (initialRowCountSet) { rowIndications.reserve(initialRowCount + 1); @@ -105,7 +105,7 @@ 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), 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), currentRowGroupCount() { lastRow = matrix.rowCount == 0 ? 0 : matrix.rowCount - 1; lastColumn = columnsAndValues.empty() ? 0 : columnsAndValues.back().getColumn(); @@ -117,7 +117,7 @@ namespace storm { if (!rowGroupIndices->empty()) { rowGroupIndices.get().pop_back(); } - currentRowGroup = rowGroupIndices->empty() ? 0 : rowGroupIndices.get().size() - 1; + currentRowGroupCount = rowGroupIndices->empty() ? 0 : rowGroupIndices.get().size() - 1; } // Likewise, we need to 'open' the row indications again. @@ -191,7 +191,7 @@ namespace storm { STORM_LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping."); STORM_LOG_THROW(startingRow >= lastRow, storm::exceptions::InvalidStateException, "Illegal row group with negative size."); rowGroupIndices.get().push_back(startingRow); - ++currentRowGroup; + ++currentRowGroupCount; // Close all rows from the most recent one to the starting row. for (index_type i = lastRow + 1; i < startingRow; ++i) { @@ -252,14 +252,14 @@ namespace storm { // Check whether row groups are missing some entries. if (hasCustomRowGrouping) { - uint_fast64_t rowGroupCount = currentRowGroup; + uint_fast64_t rowGroupCount = currentRowGroupCount; if (initialRowGroupCountSet && forceInitialDimensions) { STORM_LOG_THROW(rowGroupCount <= initialRowGroupCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowGroupCount << " row groups, but got " << rowGroupCount << "."); rowGroupCount = std::max(rowGroupCount, initialRowGroupCount); } rowGroupCount = std::max(rowGroupCount, overriddenRowGroupCount); - for (index_type i = currentRowGroup; i <= rowGroupCount; ++i) { + for (index_type i = currentRowGroupCount; i <= rowGroupCount; ++i) { rowGroupIndices.get().push_back(rowCount); } } @@ -271,7 +271,16 @@ namespace storm { typename SparseMatrixBuilder::index_type SparseMatrixBuilder::getLastRow() const { return lastRow; } - + + template + typename SparseMatrixBuilder::index_type SparseMatrixBuilder::getCurrentRowGroupCount() const { + if (this->hasCustomRowGrouping) { + return currentRowGroupCount; + } else { + return getLastRow() + 1; + } + } + template typename SparseMatrixBuilder::index_type SparseMatrixBuilder::getLastColumn() const { return lastColumn; @@ -2015,6 +2024,35 @@ namespace storm { return true; } + template + bool SparseMatrix::isIdentityMatrix() const { + if (this->getRowCount() != this->getColumnCount()) { + return false; + } + if (this->getNonzeroEntryCount() != this->getRowCount()) { + return false; + } + for (uint64_t row = 0; row < this->getRowCount(); ++row) { + bool rowHasEntry = false; + for (auto const& entry : this->getRow(row)) { + if (entry.getColumn() == row) { + if (!storm::utility::isOne(entry.getValue())) { + return false; + } + rowHasEntry = true; + } else { + if (!storm::utility::isZero(entry.getValue())) { + return false; + } + } + } + if (!rowHasEntry) { + return false; + } + } + return true; + } + template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix) { // Print column numbers in header. diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 92cb31b00..e07389e5a 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -219,6 +219,13 @@ namespace storm { */ index_type getLastRow() const; + /*! + * Retrieves the current row group count. + * + * @return The current row group count. + */ + index_type getCurrentRowGroupCount() const; + /*! * Retrieves the most recently used row. * @@ -296,7 +303,7 @@ namespace storm { // Stores the currently active row group. This is used for correctly constructing the row grouping of the // matrix. - index_type currentRowGroup; + index_type currentRowGroupCount; }; /*! @@ -929,6 +936,9 @@ namespace storm { template bool isSubmatrixOf(SparseMatrix const& matrix) const; + // Returns true if the matrix is the identity matrix + bool isIdentityMatrix() const; + template friend std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 0f3b622a4..92e4a18dc 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -1556,7 +1556,79 @@ namespace storm { storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0); return Program(manager, this->getModelType(), this->getConstants(), std::vector(), std::vector(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true); } - + + std::vector Program::usedConstants() const { + std::unordered_set vars; + for(auto const& m : this->modules) { + for(auto const& c : m.getCommands()) { + auto const& found_gex = c.getGuardExpression().getVariables(); + vars.insert(found_gex.begin(), found_gex.end()); + for (auto const& u : c.getUpdates()) { + auto const& found_lex = u.getLikelihoodExpression().getVariables(); + vars.insert(found_lex.begin(), found_lex.end()); + for (auto const& a : u.getAssignments()) { + auto const& found_ass = a.getExpression().getVariables(); + vars.insert(found_ass.begin(), found_ass.end()); + } + } + } + for (auto const& v : m.getBooleanVariables()) { + if (v.hasInitialValue()) { + auto const& found_def = v.getInitialValueExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + for (auto const& v : m.getIntegerVariables()) { + if (v.hasInitialValue()) { + auto const& found_def = v.getInitialValueExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + } + + for (auto const& f : this->formulas) { + auto const& found_def = f.getExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + + for (auto const& v : this->constants) { + if (v.isDefined()) { + auto const& found_def = v.getExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + + for (auto const& v : this->globalBooleanVariables) { + if (v.hasInitialValue()) { + auto const& found_def = v.getExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + + for (auto const& v : this->globalIntegerVariables) { + if (v.hasInitialValue()) { + auto const& found_def = v.getExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + + + std::unordered_set varIndices; + for (auto const& v : vars) { + varIndices.insert(v.getIndex()); + } + + std::vector usedConstants; + for(auto const& c : this->constants) { + if (varIndices.count(c.getExpressionVariable().getIndex())) { + usedConstants.push_back(c); + } + } + + return usedConstants; + + } + std::unordered_map Program::buildCommandIndexToActionNameMap() const { std::unordered_map res; for(auto const& m : this->modules) { diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index f1352c515..944a92d48 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -156,6 +156,12 @@ namespace storm { * @return The number of constants defined in the program. */ std::size_t getNumberOfConstants() const; + + /*! + * Retrieves the constants that are actually used in the program. + * @return + */ + std::vector usedConstants() const; /*! * Retrieves whether a global Boolean variable with the given name exists diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.cpp b/src/storm/storage/sparse/PrismChoiceOrigins.cpp index 5e19dc654..366b9524b 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.cpp +++ b/src/storm/storage/sparse/PrismChoiceOrigins.cpp @@ -111,4 +111,4 @@ namespace storm { } } } -} \ No newline at end of file +} diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.h b/src/storm/storage/sparse/PrismChoiceOrigins.h index ad5e50444..2a004d633 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.h +++ b/src/storm/storage/sparse/PrismChoiceOrigins.h @@ -67,4 +67,4 @@ namespace storm { }; } } -} \ No newline at end of file +} diff --git a/src/storm/storage/sparse/StateStorage.cpp b/src/storm/storage/sparse/StateStorage.cpp index a007ab2ea..a3ea05f4f 100644 --- a/src/storm/storage/sparse/StateStorage.cpp +++ b/src/storm/storage/sparse/StateStorage.cpp @@ -5,7 +5,7 @@ namespace storm { namespace sparse { template - StateStorage::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), deadlockStateIndices(), bitsPerState(bitsPerState) { + StateStorage::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 100000), initialStateIndices(), deadlockStateIndices(), bitsPerState(bitsPerState) { // Intentionally left empty. } diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index 49497237e..7707bd3f1 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -24,10 +24,10 @@ namespace storm { } template - typename GoalStateMerger::ReturnType GoalStateMerger::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector const& selectedRewardModels) const { + typename GoalStateMerger::ReturnType GoalStateMerger::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector const& selectedRewardModels, boost::optional const& choiceFilter) const { STORM_LOG_THROW(maybeStates.isDisjointFrom(targetStates) && targetStates.isDisjointFrom(sinkStates) && sinkStates.isDisjointFrom(maybeStates), storm::exceptions::InvalidArgumentException, "maybestates, targetstates, and sinkstates are assumed to be disjoint when creating the submodel. However, this is not the case."); - auto result = initialize(maybeStates, targetStates, sinkStates); + auto result = initialize(maybeStates, targetStates, sinkStates, choiceFilter); auto transitionMatrix = buildTransitionMatrix(maybeStates, result.first, result.second); auto labeling = buildStateLabeling(maybeStates, targetStates, sinkStates, result.first); @@ -39,7 +39,7 @@ namespace storm { } template - std::pair::ReturnType, uint_fast64_t> GoalStateMerger::initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const { + std::pair::ReturnType, uint_fast64_t> GoalStateMerger::initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional const& choiceFilter) const { storm::storage::SparseMatrix const& origMatrix = originalModel.getTransitionMatrix(); @@ -58,33 +58,35 @@ namespace storm { for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) { uint_fast64_t transitionsToMaybeStates = 0; bool keepThisRow(true), hasTransitionToTarget(false), hasTransitionToSink(false); - for (auto const& entry : origMatrix.getRow(row)) { - if (maybeStates.get(entry.getColumn())) { - ++transitionsToMaybeStates; - } else if (targetStates.get(entry.getColumn())) { - hasTransitionToTarget = true; - } else if (sinkStates.get(entry.getColumn())) { - hasTransitionToSink = true; - } else { - keepThisRow = false; - break; - } - } - if (keepThisRow) { - stateIsDeadlock = false; - result.keptChoices.set(row, true); - transitionCount += transitionsToMaybeStates; - if (hasTransitionToTarget) { - ++transitionCount; - targetStateRequired = true; + if (!choiceFilter || choiceFilter.get().get(row)) { + for (auto const& entry : origMatrix.getRow(row)) { + if (maybeStates.get(entry.getColumn())) { + ++transitionsToMaybeStates; + } else if (targetStates.get(entry.getColumn())) { + hasTransitionToTarget = true; + } else if (sinkStates.get(entry.getColumn())) { + hasTransitionToSink = true; + } else { + keepThisRow = false; + break; + } } - if (hasTransitionToSink) { - ++transitionCount; - sinkStateRequired = true; + if (keepThisRow) { + stateIsDeadlock = false; + result.keptChoices.set(row, true); + transitionCount += transitionsToMaybeStates; + if (hasTransitionToTarget) { + ++transitionCount; + targetStateRequired = true; + } + if (hasTransitionToSink) { + ++transitionCount; + sinkStateRequired = true; + } } } - STORM_LOG_THROW(!stateIsDeadlock, storm::exceptions::InvalidArgumentException, "Merging goal states leads to deadlocks!"); } + STORM_LOG_THROW(!stateIsDeadlock, storm::exceptions::InvalidArgumentException, "Merging goal states leads to deadlocks!"); ++stateCount; } diff --git a/src/storm/transformer/GoalStateMerger.h b/src/storm/transformer/GoalStateMerger.h index bc9dadcda..f79a127a6 100644 --- a/src/storm/transformer/GoalStateMerger.h +++ b/src/storm/transformer/GoalStateMerger.h @@ -35,6 +35,8 @@ namespace storm { * * one target state to which all transitions to a state selected by targetStates are redirected and * * one sink state to which all transitions to a state selected by sinkStates are redirected. * + * If a choiceFilter is given, choices on maybestates that are not selected by the filter will be removed. + * * Notes: * * the target (or sink) state is not created, if it is not reachable * * the target (or sink) state will get a label iff it is reachable and at least one of the given targetStates (sinkStates) have that label. @@ -43,7 +45,7 @@ namespace storm { * * It is assumed that maybeStates, targetStates, and sinkStates are pairwise disjoint. Otherwise an exception is thrown. * * The order of the maybeStates will not be affected (i.e. s_1 < s_2 in the input model implies s'_1 < s'_2 in the output model). */ - ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector const& selectedRewardModels = std::vector()) const; + ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector const& selectedRewardModels = std::vector(), boost::optional const& choiceFilter = boost::none) const; private: SparseModelType const& originalModel; @@ -53,7 +55,7 @@ namespace storm { * * @return The initialized result and the number of transitions of the result model */ - std::pair initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const; + std::pair initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional const& choiceFilter = boost::none) const; /*! * Builds the transition matrix of the resulting model diff --git a/src/storm/utility/counterexamples.h b/src/storm/utility/counterexamples.h index ec20c20cb..1ff429a5d 100644 --- a/src/storm/utility/counterexamples.h +++ b/src/storm/utility/counterexamples.h @@ -18,20 +18,20 @@ namespace storm { * @return The set of labels that is visited on all paths from any state to a target state. */ template - std::vector> getGuaranteedLabelSets(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { - STORM_LOG_THROW(mdp.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); + std::vector> getGuaranteedLabelSets(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { + STORM_LOG_THROW(model.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); - // Get some data from the MDP for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices(); - storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + // Get some data from the model for convenient access. + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Now we compute the set of labels that is present on all paths from the initial to the target states. - std::vector> analysisInformation(mdp.getNumberOfStates(), relevantLabels); + std::vector> analysisInformation(model.getNumberOfStates(), relevantLabels); std::queue worklist; - storm::storage::BitVector statesInWorkList(mdp.getNumberOfStates()); - storm::storage::BitVector markedStates(mdp.getNumberOfStates()); + storm::storage::BitVector statesInWorkList(model.getNumberOfStates()); + storm::storage::BitVector markedStates(model.getNumberOfStates()); // Initially, put all predecessors of target states in the worklist and empty the analysis information them. for (auto state : psiStates) { @@ -108,12 +108,12 @@ namespace storm { * @return The set of labels that is executed on all paths from an initial state to a target state. */ template - boost::container::flat_set getGuaranteedLabelSet(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { - std::vector> guaranteedLabels = getGuaranteedLabelSets(mdp, labelSets, psiStates, relevantLabels); + boost::container::flat_set getGuaranteedLabelSet(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { + std::vector> guaranteedLabels = getGuaranteedLabelSets(model, labelSets, psiStates, relevantLabels); boost::container::flat_set knownLabels(relevantLabels); boost::container::flat_set tempIntersection; - for (auto initialState : mdp.getInitialStates()) { + for (auto initialState : model.getInitialStates()) { std::set_intersection(knownLabels.begin(), knownLabels.end(), guaranteedLabels[initialState].begin(), guaranteedLabels[initialState].end(), std::inserter(tempIntersection, tempIntersection.end())); std::swap(knownLabels, tempIntersection); } diff --git a/src/storm/utility/numerical.cpp b/src/storm/utility/numerical.cpp index cec474ff7..38b793fa5 100644 --- a/src/storm/utility/numerical.cpp +++ b/src/storm/utility/numerical.cpp @@ -229,6 +229,7 @@ namespace storm { } else { t = j; result.right = j + result.left; + result.weights.resize(result.right - result.left + 1); // It's time to compute W. break; @@ -257,8 +258,8 @@ namespace storm { } result.totalWeight += result.weights[j]; - STORM_LOG_TRACE("Fox-Glynn: ltp = " << result.left << ", rtp = " << result.right << ", w = " << result.totalWeight << "."); - + STORM_LOG_TRACE("Fox-Glynn(lambda=" << lambda << ", eps=" << epsilon << "): ltp = " << result.left << ", rtp = " << result.right << ", w = " << result.totalWeight << "."); + return result; } diff --git a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp index 44e35f5c7..b00b44c0d 100644 --- a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -79,6 +79,36 @@ namespace { EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true)); } + + TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Prob_no_simplification) { + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P<=0.84 [F s=5 ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true), false, false); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true)); + + } TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew) { typedef typename TestFixture::ValueType ValueType; diff --git a/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp new file mode 100644 index 000000000..36ca41ff0 --- /dev/null +++ b/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp @@ -0,0 +1,99 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/SettingsManager.h" +#include "storm/utility/constants.h" +#include "storm/api/storm.h" +#include "storm/environment/Environment.h" + +TEST(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_die) { + storm::Environment env; + std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"; + std::string formulasAsString = "P=? [ F{\"coin_flips\"}<=2 \"two\" ] "; + formulasAsString += "; P=? [ F{\"coin_flips\"}<=3 \"two\" ] "; + formulasAsString += "; P=? [ F{\"coin_flips\"}<=8 \"two\" ] "; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> dtmc = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *dtmc->getInitialStates().begin();; + std::unique_ptr result; + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("0")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("1/8")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[2], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("21/128")), result->asExplicitQuantitativeCheckResult()[initState]); +} + +TEST(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_leader) { + storm::Environment env; + std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"; + std::string formulasAsString = "P=? [ F{\"num_rounds\"}<=1 \"elected\" ] "; + formulasAsString += "; P=? [ F{\"num_rounds\"}<=2 \"elected\" ] "; + formulasAsString += "; P=? [ F{\"num_rounds\"}>2 \"elected\" ] "; + formulasAsString += "; P=? [ F{\"num_rounds\"}>=2,{\"num_rounds\"}<3 \"elected\" ] "; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> dtmc = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *dtmc->getInitialStates().begin();; + std::unique_ptr result; + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("24/25")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("624/625")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[2], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("1/625")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[3], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("24/625")), result->asExplicitQuantitativeCheckResult()[initState]); +} + +TEST(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_crowds) { + storm::Environment env; + std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/crowds_cost_bounded.pm"; + std::string formulasAsString = "P=? [F{\"num_runs\"}<=3,{\"observe0\"}>1 true]"; + formulasAsString += "; P=? [F{\"num_runs\"}<=3,{\"observe1\"}>1 true]"; + formulasAsString += "; R{\"observe0\"}=? [C{\"num_runs\"}<=3]"; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, "CrowdSize=4"); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> dtmc = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *dtmc->getInitialStates().begin();; + std::unique_ptr result; + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("78686542099694893/1268858272000000000")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("13433618626105041/1268858272000000000")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[2], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("620529/1364000")), result->asExplicitQuantitativeCheckResult()[initState]); +} diff --git a/travis/build-helper.sh b/travis/build-helper.sh index 04c2dc52e..7d722dc99 100755 --- a/travis/build-helper.sh +++ b/travis/build-helper.sh @@ -50,13 +50,7 @@ run() { # Test all travis_fold start test_all cd build - # Hack to avoid memout problem with jit and sylvan - # 1. Run other tests without builder tests - ctest test --output-on-failure -E run-test-builder - # 2. Run builder tests without sylvan tests - ./bin/test-builder --gtest_filter=-"DdJaniModelBuilderTest_Sylvan.*" - # 3. Just run sylvan tests - ./bin/test-builder --gtest_filter="DdJaniModelBuilderTest_Sylvan.*" + ctest test --output-on-failure travis_fold end test_all ;; diff --git a/travis/generate_travis.py b/travis/generate_travis.py index f3ae09641..b104661f1 100644 --- a/travis/generate_travis.py +++ b/travis/generate_travis.py @@ -119,6 +119,18 @@ if __name__ == "__main__": buildConfig += " - docker cp storm:/storm/. .\n" buildConfig += " after_failure:\n" buildConfig += " - find build -iname '*err*.log' -type f -print -exec cat {} \;\n" + # Upload to dockerhub + if stage[1] == "TestAll": + buildConfig += " after_success:\n" + buildConfig += ' - docker login -u "$DOCKER_USERNAME" -p "$DOCKER_PASSWORD";\n' + if "Debug" in build: + buildConfig += " - docker commit storm mvolk/storm-debug:travis;\n" + buildConfig += " - docker push mvolk/storm-debug:travis;\n" + elif "Release" in build: + buildConfig += " - docker commit storm mvolk/storm:travis;\n" + buildConfig += " - docker push mvolk/storm:travis;\n" + else: + assert False s += buildConfig print(s) diff --git a/version.cmake b/version.cmake index 21ee2f621..d76de7858 100644 --- a/version.cmake +++ b/version.cmake @@ -1,4 +1,4 @@ set(STORM_VERSION_MAJOR 1) -set(STORM_VERSION_MINOR 1) +set(STORM_VERSION_MINOR 2) set(STORM_VERSION_PATCH 0)