Mavo
5f99e86c38
Next step toward success
Former-commit-id: 4ca8e78e36
10 years ago
dehnert
dfa8d6a8e5
started working on games again
Former-commit-id: a27d6a6838
10 years ago
Mavo
c08bd2bd87
Typo
Former-commit-id: aa3b888353
10 years ago
Mavo
ed526f2e0a
Initialized settings in build model
Former-commit-id: 09d219a8c6
10 years ago
Mavo
37596d575a
Settings always initialized now
Former-commit-id: 10764fa8b9
10 years ago
sjunges
46466ea4b6
an unhappy intermediate commit, not worth celebrating
Former-commit-id: 577674fd0d
10 years ago
TimQu
3ce8643d96
Added benchmarks
Former-commit-id: 6979a9aece
10 years ago
TimQu
8297c51d73
Fixed a bug that was not yet fixed for some reason...
Approximation is now also used if a non-linear function is detected. This is a quick 'solution' to allow functions of the form p times q.
Former-commit-id: 2a30959c21
10 years ago
sjunges
09a1fecdf3
small changes to python interface
Former-commit-id: e5ebc43e3d
10 years ago
sjunges
e4725aa4a1
Instead of returning the program, return the prepared formulas
Former-commit-id: a06fbaad2b
10 years ago
sjunges
2d44d4f822
getUndefinedConstantsAsString added to storm::prism::program
Former-commit-id: 8dbfbf2566
10 years ago
sjunges
9f61f75231
error when build fails during setup, as well as some extensions to the python interface
Former-commit-id: 804cf37d8c
10 years ago
TimQu
f86c4f65f7
examples and small fix regarding changes of elimination model checker
Former-commit-id: 2cc4247372
10 years ago
sjunges
e45ce6f293
replaced stdpair by struct for model,program pairs
Former-commit-id: 11177caa6f
10 years ago
sjunges
a365ce7a0b
further work on python api
Former-commit-id: 1294a73a6c
10 years ago
sjunges
c431cbe375
merge
Former-commit-id: d031d65685
10 years ago
sjunges
83561a319f
merge
Former-commit-id: e5f945771c
10 years ago
Mavo
3b9a48136c
Sort transitions before building them
Former-commit-id: eba930f0b6
10 years ago
Mavo
c8d2cf1724
Better distinction between parametric and non-parametric DFTs
Former-commit-id: 57ac698a38
10 years ago
Mavo
20a5d8e96f
Side conditions for rational functions cannot be checked directly
Former-commit-id: c5e6d79c9d
10 years ago
Mavo
f38eeff1ef
First try on parsing of rational functions
Former-commit-id: 63a6ae0d14
10 years ago
Mavo
8271045b27
ToString is const
Former-commit-id: d512894cf4
10 years ago
dehnert
3e23a9ad40
some typos
Former-commit-id: 8b28f77ab4
10 years ago
Mavo
4c09f9ce29
Minor improvements
Former-commit-id: 63dfd49048
10 years ago
dehnert
94b817c531
removed debug output
Former-commit-id: f9f58b55f4
10 years ago
sjunges
4e16571f8a
removed missing function.
Former-commit-id: e980d16031
10 years ago
dehnert
b1c103811b
conditional probabilities in MDPs should now also work in the min-case
Former-commit-id: 9b3c22470b
10 years ago
dehnert
3e38e73efe
conditional probabilities in MDPs (Baier method) available in sparse MDP model checker
Former-commit-id: 76136c5e72
10 years ago
dehnert
756b2c5e30
added globally operator to functionality of hybrid/symbolic MDP model checkers
Former-commit-id: 2672333544
10 years ago
dehnert
135dfb27b1
added globally operator to funcationlity of sparse MDP model checker
Former-commit-id: c74160579b
10 years ago
dehnert
d42f52d983
all DTMC model checkers now support checking globally formulas
Former-commit-id: b330937007
10 years ago
TimQu
6006d95193
Fixed compile errors: Added missing include and fixed call of std::max
Former-commit-id: 614689e26f
10 years ago
dehnert
84205a0bf6
refined computation of conditional probs a bit. Sebastian, if you're reading this: shouldn't you be working? :)
Former-commit-id: 83f6dbb8d2
10 years ago
dehnert
33757633c8
first version of conditional probabilities for (non-parametric) DTMCs a la Baier
Former-commit-id: b57dfab024
10 years ago
dehnert
0ffbda5aff
initial draft of long-run rewards for parametric models
Former-commit-id: 991512a57d
10 years ago
dehnert
645f130a62
introduced long-run average reward formula
Former-commit-id: 00fac9ad4b
10 years ago
dehnert
2a5780d5be
first version of long-run-average for parametric DTMCs
Former-commit-id: 85253c4f05
10 years ago
dehnert
cd8fd76520
some refactoring in an attempt to make the state-elimination procedure flexible and readable at the same time
Former-commit-id: 9cbdd21672
10 years ago
dehnert
0f6e6e4da1
added feature to compute step-bounded until probabilities in parametric models
Former-commit-id: 172e87cb55
10 years ago
dehnert
98d173ca3c
changed elimination-based model checker to be able to compute values for all states (for reachability probs and reachability rewards)
Former-commit-id: 016a25734a
10 years ago
dehnert
8ed4a5f849
some refactoring in elimination-based model checker
Former-commit-id: 1fb6741479
10 years ago
TimQu
1225b056f2
a little refactoring
Former-commit-id: 9af14c006c
10 years ago
sjunges
bfd6e62c69
updated python api + setup.py
Former-commit-id: c2a2e9eb1e
10 years ago
sjunges
1e1400d68d
merge
Former-commit-id: eb9efc4bb2
10 years ago
sjunges
096778a5d0
assorted fixes (builder for no-fix-deadline, semicolon, xercesbuild)
Former-commit-id: 7ae9bcd61e
10 years ago
TimQu
8ab7cae974
early termination
Former-commit-id: a1752a6fb7
10 years ago
dehnert
d5601bd328
bugfix
Former-commit-id: 19d2ba3260
10 years ago
dehnert
fc41c3a6dd
some more work on other elimination orders
Former-commit-id: a8ff636ad0
10 years ago
TimQu
c0b5190022
Extended interface of linEqSolvers a little,
eq solver is now called repeatedly with increased precision, until the result is good enough..
Former-commit-id: b076950dc8
10 years ago
dehnert
dd5af80d5a
work towards easier deployment of other ordering heuristics
Former-commit-id: f48dff3630
10 years ago