dehnert
25db3f9d0f
Fixed error that prevents compilation if Z3 is not present.
Former-commit-id: d8de79f2ae
10 years ago
dehnert
0f4b19ffc9
Merge branch 'master' into SmtSolvers
Former-commit-id: 7a70be824a
10 years ago
dehnert
85a4376e39
Now StoRM can be properly compiled without support for MathSAT if needed.
Former-commit-id: 28da4f5ed8
10 years ago
dehnert
7b8c382303
Added tests for Mathsat expression adapter.
Former-commit-id: 4f8ef4c3c3
10 years ago
dehnert
f54b5671ea
Done refactoring MathSAT expression adapter.
Former-commit-id: 6edb98b86c
10 years ago
dehnert
a061cdbed8
Started refactoring MathSAT adapter.
Former-commit-id: 93b1fdedb3
10 years ago
dehnert
84bfd58884
Minor refactoring of Z3 expression adapter.
Former-commit-id: b31ae87a98
10 years ago
dehnert
c859029094
Added some checks for illegal return values.
Former-commit-id: 88d5942780
10 years ago
dehnert
5e9e7b875b
Proper output of MathSAT version on command line.
Former-commit-id: 2bccdc8d1a
10 years ago
dehnert
b5d55335a6
All tests passing again.
Former-commit-id: ffa8bef2d2
10 years ago
dehnert
ba14ba3613
Further work on MathSAT solver.
Former-commit-id: dd67b23505
10 years ago
dehnert
81571878f7
Further refactoring of MathSAT solver.
Former-commit-id: 317a9f9545
10 years ago
dehnert
c474920fa4
Started refactoring SMT solvers. Now displaying MathSAT version in CLI.
Former-commit-id: 1736a0bb6b
10 years ago
dehnert
7ff3dcecfb
Added test for interpolation to MathSat tests.
Former-commit-id: ac94857726
10 years ago
dehnert
6eb415f87f
Tests for MathSAT now run through on Mac OS.
Former-commit-id: 9f6cf0af6a
10 years ago
dehnert
d8be64f0d7
Started on making MathSatSmtSolver work properly.
Former-commit-id: c370658b26
10 years ago
dehnert
554287e082
Fixed minor issue that caused problems with the measure-driven initial partition and rewards.
Former-commit-id: 7379da548d829c2415bf6f28d24e11475589badc
10 years ago
dehnert
6db0522c69
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: e3833019fecbcf1e5c0196b999766811c5070db4
10 years ago
dehnert
7d0ae06f9f
Fixed creation of empty blocks under certain circumstances in bisimulation.
Former-commit-id: f1240e234b0cc3cf9fc9cb87f3ee6ba95772fb55
10 years ago
dehnert
3231ea6c06
Moved to new macros.
Former-commit-id: d97c947c2247e2716f2c98b33b9492ab2a8e7879
10 years ago
dehnert
2912ec23fe
Merge branch 'master' into SmtSolvers
Former-commit-id: f1b42f43c32286e1ad59770189c27653d0b7464b
10 years ago
dehnert
91084a5da4
APs true/false can now be queried for a state.
Former-commit-id: 3c16df45091fb606c97b2abdd987497101f78b5a
10 years ago
dehnert
0bc685969d
Moved from call to list::size to counting member in bisimulation partition to avoid gcc's O(n) list::size.
Former-commit-id: aaae9886b7979077c199eda87b90cddd40cffe26
10 years ago
dehnert
894c3bb497
Added missing header.
Former-commit-id: 30d5444d231846824f79b24067157f6af1cbf0b4
10 years ago
dehnert
39fb2650cd
Included missing header.
Former-commit-id: dd278656bf991d11e9f45005453732890f690737
10 years ago
dehnert
7014d289e8
Fixed some issues related to bisimulation in the presence of state rewards.
Former-commit-id: 7f26a7bcf911b291d14f3fe5bd1a0a9c77ed671a
10 years ago
svkurowski
287281d053
Enable checking MDP models from the CLI
(cherry picked from commit 30b9811512ffa7aebf88ec17f72b37905c8cdbc1 [formerly fa0555dd74cd639840b2572dd5f382bcd3f5c3f1])
Former-commit-id: 271bda31cb8fcc50011d6aad7c02ad80ccb814ad
10 years ago
dehnert
980b7790a7
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: c0ccc12e57c23e6300650ecc0f350157a935ee28
10 years ago
dehnert
609a948495
Put noexcept in Macro and use deprecated throw() for MSVC to make it happy.
Former-commit-id: 3d83fefcdac0e67be549c81bb05188729dbff178
10 years ago
dehnert
fd617efc91
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: 4e2f42814adc2c0d2f20824e8a911a260745349f
10 years ago
dehnert
79798e2cb1
Fixed the reward-issue even harder.
Former-commit-id: 2ca1c229e1732824aca34f32cad8248cfeade28a
10 years ago
dehnert
b07963bd46
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: 78421578db65cb689c7aed3f788049365ac80b1d
10 years ago
dehnert
a7bce9e520
Removed debug output and fixed the reward issue a bit more.
Former-commit-id: ecbbeff14ef2b7fadf76ae74afdb8d11b44c80cd
10 years ago
dehnert
0d2440d4a9
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: 0f0e18abadb9d9abc631d9abbf68a06ecbf33cd7
10 years ago
dehnert
7cd0dfe8b0
Fixed an issue regarding the reward model generation.
Former-commit-id: 237acf99f9d4671d0deaf8f940d6dbb3ee731eea
10 years ago
dehnert
7644a74fcd
Removed some superfluous lines in test.
Former-commit-id: 2c2bd0ba67a7ef8f7568dbe56d2d0d00df08f4e3
10 years ago
dehnert
1b4d2a92db
Started working on making bisimulation work for models with (state-based) rewards.
Former-commit-id: b1029210f677bc1c99e0f90327f5b7f92c3a2a87
10 years ago
dehnert
370a0ae476
Fixed some issues in bisimulation and added some tests.
Former-commit-id: 98801de9db21fc4aeb4eaa50ec328533449a5e19
10 years ago
dehnert
f8a06b69f5
Fixed a clang-warning related to a throws declaration.
Former-commit-id: 933ad7925a2a42482192bd1b95468db1b8f10685
10 years ago
dehnert
2f20abf47f
The user can now select on the command line which reward model of a symbolic model is to be used (as a second [optional] argument to --symbolic).
Former-commit-id: 02f998e5dd
10 years ago
svkurowski
a0b54fbca4
Add src/utility/storm-version.cpp to ignored files
This file is generated by CMake.
A more robust solution would be to configure this file out-of-source
much like build/include/storm-config.h.
Former-commit-id: 05eacc7a5b
10 years ago
PBerger
9fc68a554c
Cherry-picked a fix for GCC from branch.
Former-commit-id: 98f7c52b34
10 years ago
David_Korzeniewski
25d87bae06
Builds fine, still no tests yet
Former-commit-id: 3d9d85679a
10 years ago
David_Korzeniewski
2e92d66bf3
Cmake scripts for linking mathsat and gmp or mpir which is required by mathsat
Former-commit-id: b13b68115a
10 years ago
PBerger
1cf8674fa5
Added noexcept Destructors to the exceptions to fix the picky Clang3.5 compiler errors.
Former-commit-id: f620e5ed7d
10 years ago
dehnert
aa4836e085
Minor bugfix in bisimulation options.
Former-commit-id: 7a579aef50
10 years ago
dehnert
ed6f3dae9f
Renamed the newly added method.
Former-commit-id: 72ea9afb61
10 years ago
dehnert
2437601a85
Added function to compute distances of states to some other set of states.
Former-commit-id: 2bf19c1b2d
10 years ago
dehnert
f3048d31c2
Small bugfix for bisimulation decomposition.
Former-commit-id: eae1447df4
10 years ago
dehnert
72c178dd08
Merge branch 'weakBisimulation'
Former-commit-id: a602e8e58f
10 years ago