sjunges
9 years ago
68 changed files with 1834 additions and 413 deletions
-
8.travis.yml
-
23CHANGELOG.md
-
2CMakeLists.txt
-
37doc/checklist_new_release.md
-
118doc/scripts/test_build_configurations.py
-
5doc/scripts/test_build_configurations.txt
-
4resources/3rdparty/CMakeLists.txt
-
2resources/3rdparty/carl/CMakeLists.txt
-
260resources/examples/testfiles/dtmc/crowds_cost_bounded.pm
-
13src/storm-cli-utilities/model-handling.h
-
3src/storm-pars-cli/storm-pars.cpp
-
8src/storm-pars/api/region.h
-
19src/storm-pars/modelchecker/region/RegionModelChecker.cpp
-
17src/storm-pars/modelchecker/region/RegionModelChecker.h
-
98src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
-
17src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
-
7src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
-
4src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
-
6src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp
-
2src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h
-
6src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp
-
2src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h
-
36src/storm-pars/transformer/ParameterLifter.cpp
-
26src/storm-pars/transformer/ParameterLifter.h
-
2src/storm/CMakeLists.txt
-
2src/storm/adapters/Smt2ExpressionAdapter.h
-
4src/storm/api/counterexamples.cpp
-
2src/storm/api/counterexamples.h
-
4src/storm/builder/ExplicitModelBuilder.cpp
-
435src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
-
57src/storm/logic/ComparisonType.h
-
138src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
-
7src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h
-
48src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
-
215src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
-
11src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
-
8src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
-
95src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp
-
14src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h
-
18src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp
-
10src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.h
-
9src/storm/models/ModelBase.h
-
7src/storm/models/sparse/Model.cpp
-
9src/storm/models/sparse/Model.h
-
5src/storm/models/sparse/NondeterministicModel.cpp
-
13src/storm/models/sparse/NondeterministicModel.h
-
5src/storm/models/symbolic/Model.cpp
-
2src/storm/models/symbolic/Model.h
-
2src/storm/models/symbolic/NondeterministicModel.h
-
5src/storm/solver/AbstractEquationSolver.cpp
-
5src/storm/solver/AbstractEquationSolver.h
-
2src/storm/solver/SmtlibSmtSolver.cpp
-
52src/storm/storage/SparseMatrix.cpp
-
12src/storm/storage/SparseMatrix.h
-
74src/storm/storage/prism/Program.cpp
-
6src/storm/storage/prism/Program.h
-
2src/storm/storage/sparse/PrismChoiceOrigins.cpp
-
2src/storm/storage/sparse/PrismChoiceOrigins.h
-
2src/storm/storage/sparse/StateStorage.cpp
-
54src/storm/transformer/GoalStateMerger.cpp
-
6src/storm/transformer/GoalStateMerger.h
-
24src/storm/utility/counterexamples.h
-
5src/storm/utility/numerical.cpp
-
30src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp
-
99src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp
-
8travis/build-helper.sh
-
12travis/generate_travis.py
-
2version.cmake
@ -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) |
|||
@ -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 |
|||
|
|||
|
|||
|
|||
|
|||
@ -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 |
|||
@ -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 |
|||
|
|||
|
|||
@ -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<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalNumber>>(); |
|||
uint_fast64_t const initState = *dtmc->getInitialStates().begin();; |
|||
std::unique_ptr<storm::modelchecker::CheckResult> result; |
|||
|
|||
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[0], true)); |
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("0")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]); |
|||
|
|||
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[1], true)); |
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("1/8")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]); |
|||
|
|||
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[2], true)); |
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("21/128")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[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<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalNumber>>(); |
|||
uint_fast64_t const initState = *dtmc->getInitialStates().begin();; |
|||
std::unique_ptr<storm::modelchecker::CheckResult> result; |
|||
|
|||
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[0], true)); |
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("24/25")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]); |
|||
|
|||
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[1], true)); |
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("624/625")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]); |
|||
|
|||
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[2], true)); |
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("1/625")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]); |
|||
|
|||
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[3], true)); |
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("24/625")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[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<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalNumber>>(); |
|||
uint_fast64_t const initState = *dtmc->getInitialStates().begin();; |
|||
std::unique_ptr<storm::modelchecker::CheckResult> result; |
|||
|
|||
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[0], true)); |
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("78686542099694893/1268858272000000000")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]); |
|||
|
|||
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[1], true)); |
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("13433618626105041/1268858272000000000")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]); |
|||
|
|||
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[2], true)); |
|||
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); |
|||
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("620529/1364000")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]); |
|||
} |
|||
@ -1,4 +1,4 @@ |
|||
set(STORM_VERSION_MAJOR 1) |
|||
set(STORM_VERSION_MINOR 1) |
|||
set(STORM_VERSION_MINOR 2) |
|||
set(STORM_VERSION_PATCH 0) |
|||
|
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue