TimQu
|
8bb25234a3
|
fixed prism model code (formula used before definition)
Former-commit-id: d610960b0e
|
10 years ago |
|
TimQu
|
4a4a9ad954
|
fixed/improved the qualitative checks
Former-commit-id: 5e889a0d95
|
10 years ago |
Mavo
|
dcf5468b29
|
Fixed linker error with static function
Former-commit-id: 95e220763d
|
10 years ago |
|
Mavo
|
17ba53dafa
|
Division by Interval not supported
Former-commit-id: 86b2f555c9
|
10 years ago |
TimQu
|
18623f304b
|
some benchmarks
Former-commit-id: 3f3e9306fe
|
10 years ago |
dehnert
|
2096c54b84
|
more explicit instantiations for rational function and some more tests for eigen solver
Former-commit-id: b97e838b22
|
10 years ago |
|
dehnert
|
4e14ecb869
|
made elimination-based linear solver work in an alpha version. changed minor things in Eigen's SparseLU implementation to make it work with rational numbers and rational functions
Former-commit-id: e5622bd981
|
10 years ago |
|
TimQu
|
cf648b5bf1
|
output of runtimes and other statistics
Former-commit-id: 3eaf89f5d5
|
10 years ago |
|
TimQu
|
19fa7767a0
|
scheduler retrival for value iteration of native minMaxLinEqSolver
Former-commit-id: 641991da86
|
10 years ago |
|
TimQu
|
b58c9d67b9
|
step bounded objectives
Former-commit-id: 067f4b8dae
|
10 years ago |
|
TimQu
|
18c1fc3b3f
|
removed debug output
Former-commit-id: 575700421c
|
10 years ago |
|
TimQu
|
2fed3b647c
|
scheduler benchmark now considers expected reachability reward (total reward was infinite).
Bugfix.
Former-commit-id: f53d19194c
|
10 years ago |
|
TimQu
|
5604733854
|
improvements for preprocessing regarding finite/infinite rewards
Former-commit-id: a57e979bdd
|
10 years ago |
|
dehnert
|
35bb3a3c26
|
renamed elimination settings
Former-commit-id: 5155d0a465
|
10 years ago |
|
dehnert
|
8ce9e56af8
|
some refactoring of state-elimination-related things
Former-commit-id: c51fd9c47c
|
10 years ago |
|
dehnert
|
ec640c12b7
|
minor fixes to Eigen adapter
Former-commit-id: 9095bbc9d4
|
10 years ago |
|
dehnert
|
a17cffbbe3
|
added missing switch case for new eigen solver
Former-commit-id: fbbb6e5828
|
10 years ago |
|
dehnert
|
023325b53d
|
added tests for Eigen solver
Former-commit-id: ede9efcee2
|
10 years ago |
|
dehnert
|
002bd58b2d
|
added shipped version of Eigen to CMakeList
Former-commit-id: b262c2023e
|
10 years ago |
|
dehnert
|
48e1d20c92
|
added eigen to resources
Former-commit-id: a07c2d6368
|
10 years ago |
|
dehnert
|
bb700457de
|
some minor fixes
Former-commit-id: f114c397f6
|
10 years ago |
|
dehnert
|
512a1ec558
|
added special label 'deadlock' to models and builders
Former-commit-id: 4edc57216e
|
10 years ago |
|
dehnert
|
74ee726e35
|
fixed some typos
Former-commit-id: de3cd92c62
|
10 years ago |
|
dehnert
|
94fd4cd9a8
|
fixed bug related to instantaneous reward properties in formula parser
Former-commit-id: 8d799f8678
|
10 years ago |
|
dehnert
|
2accd81aaa
|
fixed bug in reward generation for PRISM models
Former-commit-id: 72399da7ed
|
10 years ago |
|
dehnert
|
f3701f66fb
|
bugfix for symbolic reachability reward computation
Former-commit-id: c197203539
|
10 years ago |
ThomasH
|
7fef54ab10
|
modify the ma builder such that it resprects priorities
Former-commit-id: 2aa01e8e5d
|
10 years ago |
|
ThomasH
|
3f4b82cf39
|
add priorities to the transition model
Former-commit-id: 18205915db
|
10 years ago |
|
dehnert
|
fd3b8adc00
|
fixed bug in formula parser
Former-commit-id: 19c1492e09
|
10 years ago |
|
ThomasH
|
3f23d7b322
|
add advanced state labeling (wrt a given formula)
Former-commit-id: 84e0ede9a0
|
10 years ago |
|
dehnert
|
6810c0d50f
|
fixed bug in computation of instantaneous rewards on DTMCs
Former-commit-id: f15c616d40
|
10 years ago |
|
dehnert
|
c88e540a1a
|
fixed bug in graph preprocessing algorithms that support a maximal number of steps
Former-commit-id: aed124e5f8
|
10 years ago |
|
dehnert
|
2c23b1ed99
|
fixed bug in sparse DTMC model checker
Former-commit-id: 41d21093c0
|
10 years ago |
|
dehnert
|
cae04c0e20
|
fixed bug in symbolic quantitative check result
Former-commit-id: 00a6c46d38
|
10 years ago |
|
dehnert
|
71bfb45220
|
added check for multiple writes to the same global variable in explicit JANI next-state generator
Former-commit-id: 5fc1bb01a9
|
10 years ago |
|
TimQu
|
ad1e530756
|
added subsystemBuilder for preprocessing infinite rewards
Former-commit-id: 1dbec569cc
|
10 years ago |
|
dehnert
|
7861df4f20
|
JANI next-state generator appears to be working (without rewards)
Former-commit-id: 3ca5c3ccf2
|
10 years ago |
|
TimQu
|
669e9c6352
|
fix regarding creation of downward closure in 3D
Former-commit-id: f35406a83a
|
10 years ago |
|
dehnert
|
08112d98aa
|
more work on JANI next state generator and the corresponding tests
Former-commit-id: e170c9989c
|
10 years ago |
|
TimQu
|
4b406c5e74
|
bugfix
Former-commit-id: 5134b17c0b
|
10 years ago |
|
TimQu
|
7d2db7b591
|
fixed zeroconf model files
Former-commit-id: efe00efde6
|
10 years ago |
|
TimQu
|
f442d9a434
|
disabled the "conservative" choice selection for value iteration because it produced wrong results (and we don't need this anymore)
Former-commit-id: 9a8cced48f
|
10 years ago |
|
dehnert
|
05fecb03b3
|
started on introducing multiple initial locations in JANI models
Former-commit-id: cf009b3e14
|
10 years ago |
|
dehnert
|
b62f8819b9
|
JANI next-state generator can now generate transitions from silent edges
Former-commit-id: 57e37b5850
|
10 years ago |
|
TimQu
|
e6c89a6f45
|
more on total rewards
Former-commit-id: f25801534a
|
10 years ago |
|
TimQu
|
3b9740c95d
|
fixed model files for team benchmark
Former-commit-id: e253457611
|
10 years ago |
|
TimQu
|
de35d40905
|
total reward formulas
Former-commit-id: 878065b902
|
10 years ago |
|
dehnert
|
000a8c2d77
|
more work on JANI next-state generator
Former-commit-id: d94ab2b81e
|
10 years ago |
|
TimQu
|
0e1293cabb
|
creation of check results for numerical and achievability queries
Former-commit-id: 3c628996d4
|
10 years ago |
|
TimQu
|
f461c990b5
|
introduced post processor plus a little renaiming of things
Former-commit-id: f73f8eb2ff
|
10 years ago |
