sjunges
|
f5e8c5ba73
|
Merge branch 'dft-approximation' of https://sselab.de/lab9/private/git/storm into dft-approximation
Former-commit-id: feef06888a
|
8 years ago |
sjunges
|
b044b2aca4
|
..
Former-commit-id: c06171dddc
|
8 years ago |
dehnert
|
c84254f665
|
another step, debugging in progress
Former-commit-id: 41c25470a2 [formerly 10e321e3d0 ]
Former-commit-id: 38f405c114
|
8 years ago |
Mavo
|
cd1aec7750
|
Heuristic using the difference between upper and lower bound
Former-commit-id: a514e33d69
|
8 years ago |
Mavo
|
6fcc97a7b4
|
Implemented modularisation for MTTF via parallel composition of CTMCs
Former-commit-id: 552949346b
|
8 years ago |
sjunges
|
875feebdb8
|
modularisation checks for restrictors
Former-commit-id: 6c4eb363cd
|
8 years ago |
Mavo
|
1c95722711
|
Do not skip states if approx = 0.0
Former-commit-id: 37dbb9739c
|
8 years ago |
Mavo
|
9947d9b64c
|
Add up exploration time
Former-commit-id: f417ecc021
|
8 years ago |
sjunges
|
f1e69e42cd
|
Merge branch 'dft-approximation' of https://sselab.de/lab9/private/git/storm into dft-approximation
Former-commit-id: 595c5e7891
|
8 years ago |
sjunges
|
464a497093
|
smt checker v1, and better error messages
Former-commit-id: ab7391e85d
|
8 years ago |
Mavo
|
d95bb71f75
|
Tried to gain more performance
Former-commit-id: 9af2ab7ce0
|
8 years ago |
Mavo
|
64699a7bad
|
Several improvements
Former-commit-id: 047ebde33b
|
8 years ago |
Mavo
|
dae1a7eefe
|
Do not use cold BEs in first step of approximation formula
Former-commit-id: d204be9633
|
8 years ago |
Mavo
|
02c4195f31
|
Better upper bound for independent subtrees
Former-commit-id: 64f5a1ca60
|
8 years ago |
dehnert
|
c4f8c1fbcb
|
one step more
Former-commit-id: 95773b13c3 [formerly 28ca90f221 ]
Former-commit-id: 51d197d2b5
|
8 years ago |
Mavo
|
a2c484bba4
|
Support for probability approximation without modularisation
Former-commit-id: 921c8d310c
|
8 years ago |
Mavo
|
b669a3acef
|
Only sort bucket queue if more than 10% is unsorted
Former-commit-id: 7ebd1e49c8
|
8 years ago |
Mavo
|
6778a018ad
|
Use heuristic probability
Former-commit-id: 747b34cfdc
|
8 years ago |
Mavo
|
d814143c09
|
Merge branch 'dft-approximation' of https://sselab.de/lab9/private/git/storm into dft-approximation
Former-commit-id: 8e9ec487c5
|
8 years ago |
Mavo
|
c12bbe2904
|
Disable old way of computing permutations as there is a bug for >31 elements
Former-commit-id: ae7af404f3
|
8 years ago |
dehnert
|
2471036df4
|
more work on jit-thing: transitioning to proper handling of synchronizing edges
Former-commit-id: 3af1772192 [formerly 890c529dd1 ]
Former-commit-id: 818295a085
|
8 years ago |
Mavo
|
aa9cc2e0e5
|
Merge branch 'dft-approximation' of https://sselab.de/lab9/private/git/storm into dft-approximation
Former-commit-id: f2fe83ee35
|
8 years ago |
Mavo
|
876b147aa8
|
Fixed bug with iterator
Former-commit-id: f7248a57c1
|
8 years ago |
Mavo
|
d9b1285644
|
Alternative way of computing permutations (at the moment in parallel)
Former-commit-id: f5886860bc
|
8 years ago |
sjunges
|
ce9d7db67a
|
fixed knuths die in pdtmc
Former-commit-id: f52f34571d [formerly 20c9ef124a ]
Former-commit-id: f6d23f46eb
|
8 years ago |
sjunges
|
56b301fbbf
|
ignore some 3rd party libs
Former-commit-id: d0bc9fae26 [formerly 8c878dfd9d ]
Former-commit-id: 072c73b61c
|
8 years ago |
Mavo
|
386d4c7f05
|
Use heuristic NONE to explore complete state space
Former-commit-id: 25990b5dda
|
8 years ago |
Mavo
|
8e159133da
|
Compute lower/upper bounds only when needed
Former-commit-id: 8f3af1ab10
|
8 years ago |
dehnert
|
eaf422689b
|
terminal states now supported by jit-based builder
Former-commit-id: bf4eb4654d [formerly 5d2f364967 ]
Former-commit-id: 84aa362762
|
8 years ago |
dehnert
|
247c47c2be
|
Merge remote-tracking branch 'origin/jani_support' into jani_explicit_jit
Former-commit-id: 1f6700769a [formerly 2c9602d8a2 ]
Former-commit-id: cf30bffed7
|
8 years ago |
dehnert
|
e8810a3be4
|
more work: up
Former-commit-id: e7fa235111 [formerly 6323071a5b ]
Former-commit-id: 72073e0de4
|
8 years ago |
dehnert
|
02ca60282d
|
forgotten files
Former-commit-id: 3d9bce824d [formerly a347808794 ]
Former-commit-id: a11fa06972
|
8 years ago |
dehnert
|
169293bfe5
|
started on proper deadlock handling
Former-commit-id: a10c6b86ab [formerly c0b400e239 ]
Former-commit-id: 549a0e9880
|
8 years ago |
dehnert
|
71f2e83bc0
|
completed moving from monolithic generation to callback-based approach. added building labels to jit-based model builder, added support for options of other builders (selection of labels, reward models, etc)
Former-commit-id: 5729c1c8ca [formerly 890198a907 ]
Former-commit-id: df2528638d
|
8 years ago |
Mavo
|
a9f97bd210
|
Set heuristic to probability
Former-commit-id: a7d8fd7738
|
8 years ago |
Mavo
|
58f8707293
|
Tighter over-approximation
Former-commit-id: 824e74f88d
|
8 years ago |
dehnert
|
1c1120ef66
|
more work on jit-based builder
Former-commit-id: 579adb85eb [formerly 574a25aa3d ]
Former-commit-id: 2a1d2ca2c2
|
8 years ago |
dehnert
|
9de219a6b9
|
more work on jit-based model builder
Former-commit-id: 150ac22d6b [formerly 85061a73c7 ]
Former-commit-id: cd18eec45b
|
8 years ago |
Mavo
|
0d9cdd6ef8
|
Use Heuristic None
Former-commit-id: 63f78f3db0
|
8 years ago |
Mavo
|
20b00e8f1d
|
Propagate dont care to currently not failable BEs
Former-commit-id: 1fcb15f4ec
|
8 years ago |
Mavo
|
8b78ed2340
|
Renamed rateratio to probability
Former-commit-id: 6d07985b1d
|
8 years ago |
Mavo
|
945447e7e0
|
Use DFS as default
Former-commit-id: 34f9e80d1b
|
8 years ago |
Mavo
|
815bbf10ab
|
Remove map and use linear search in BucketPriorityQueue
Former-commit-id: 3fc131facb
|
8 years ago |
Mavo
|
ef7d4ac87b
|
Do not sort BEs anymore
Former-commit-id: 1789ad3644
|
8 years ago |
Mavo
|
8d38358c11
|
Use BucketPriorityQueue instead of DynamicPriorityQueue
Former-commit-id: 7a22ef5b16
|
8 years ago |
dehnert
|
17384cd9e9
|
fixed wrong include
Former-commit-id: 46271a3866 [formerly 86b53e6740 ]
Former-commit-id: 10466b1fdd
|
8 years ago |
dehnert
|
ed49f82ae3
|
Merge branch 'future' into jani_support
Former-commit-id: f8f9f065f8 [formerly 9bca0600b0 ]
Former-commit-id: 47ce69307d
|
8 years ago |
dehnert
|
cb97da887c
|
went from deque to vector-based representation of splitter queue in bisimulation
Former-commit-id: 7047192641
|
8 years ago |
Mavo
|
d1d77ff4df
|
Changed deque to vector in bisimulation to gain performance boost
Former-commit-id: 5db8e917b4
|
8 years ago |
Mavo
|
82a3964e5d
|
Only fix queue when needed
Former-commit-id: 50231c4554
|
8 years ago |