dehnert
99b9f11d49
removed eigen-3.2.6
Former-commit-id: 74fc9f0dbe
9 years ago
dehnert
852afd1718
fixed crowds models to work with exact arithmetic. fixed dynamic state priority queue implementation. added setting to use dedicated elimination-based model checker instead of regular model checker (+ elimination solver)
Former-commit-id: 1b0802ff05
9 years ago
dehnert
82d4164c39
added obeying a state ordering to elimination linear equation solver
Former-commit-id: 5a62842963
9 years ago
dehnert
a699272dc6
renamed storm::Variable to storm::RationalFunctionVariable to avoid confusion with storm::expressions::Variable. fixed some Eigen tests
Former-commit-id: 62c70330c2
9 years ago
dehnert
f3fa90cc37
more work towards exact solving
Former-commit-id: 38edbcf2ca
9 years ago
PBerger
be9648fc18
Added -fPIC to Sylvan. Since it is linked into Storm it is necessary for relocation to be possible, hence PIC.
Added includes for cmath at various points. This is a default include on Mac OS but not on any sane systems.
Changed calls to std::abs to std::fabs to resolve ambigious call errors.
Former-commit-id: 4d3da21bce
9 years ago
dehnert
d3de111b3b
more work to enable storm to use rational arithmetic
Former-commit-id: 72933b5184
9 years ago
dehnert
af35a4c3ed
Merge branch 'jani_support' into exact_solver
Former-commit-id: 63cf5c5117
9 years ago
dehnert
3bb36997a1
minor bugfix
Former-commit-id: 409e84e8f5
9 years ago
dehnert
8f12b3b8c4
added option 'exact' (in addition to parametric)
Former-commit-id: ccc026a44d
9 years ago
Mavo
dcf5468b29
Fixed linker error with static function
Former-commit-id: 95e220763d
9 years ago
Mavo
17ba53dafa
Division by Interval not supported
Former-commit-id: 86b2f555c9
9 years ago
dehnert
2096c54b84
more explicit instantiations for rational function and some more tests for eigen solver
Former-commit-id: b97e838b22
9 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
9 years ago
dehnert
35bb3a3c26
renamed elimination settings
Former-commit-id: 5155d0a465
9 years ago
dehnert
8ce9e56af8
some refactoring of state-elimination-related things
Former-commit-id: c51fd9c47c
9 years ago
dehnert
ec640c12b7
minor fixes to Eigen adapter
Former-commit-id: 9095bbc9d4
9 years ago
dehnert
a17cffbbe3
added missing switch case for new eigen solver
Former-commit-id: fbbb6e5828
9 years ago
dehnert
023325b53d
added tests for Eigen solver
Former-commit-id: ede9efcee2
9 years ago
dehnert
002bd58b2d
added shipped version of Eigen to CMakeList
Former-commit-id: b262c2023e
9 years ago
dehnert
48e1d20c92
added eigen to resources
Former-commit-id: a07c2d6368
9 years ago
dehnert
bb700457de
some minor fixes
Former-commit-id: f114c397f6
9 years ago
dehnert
512a1ec558
added special label 'deadlock' to models and builders
Former-commit-id: 4edc57216e
9 years ago
dehnert
74ee726e35
fixed some typos
Former-commit-id: de3cd92c62
9 years ago
dehnert
94fd4cd9a8
fixed bug related to instantaneous reward properties in formula parser
Former-commit-id: 8d799f8678
9 years ago
dehnert
2accd81aaa
fixed bug in reward generation for PRISM models
Former-commit-id: 72399da7ed
9 years ago
dehnert
f3701f66fb
bugfix for symbolic reachability reward computation
Former-commit-id: c197203539
9 years ago
dehnert
fd3b8adc00
fixed bug in formula parser
Former-commit-id: 19c1492e09
9 years ago
dehnert
6810c0d50f
fixed bug in computation of instantaneous rewards on DTMCs
Former-commit-id: f15c616d40
9 years ago
dehnert
c88e540a1a
fixed bug in graph preprocessing algorithms that support a maximal number of steps
Former-commit-id: aed124e5f8
9 years ago
dehnert
2c23b1ed99
fixed bug in sparse DTMC model checker
Former-commit-id: 41d21093c0
9 years ago
dehnert
cae04c0e20
fixed bug in symbolic quantitative check result
Former-commit-id: 00a6c46d38
9 years ago
dehnert
71bfb45220
added check for multiple writes to the same global variable in explicit JANI next-state generator
Former-commit-id: 5fc1bb01a9
9 years ago
dehnert
7861df4f20
JANI next-state generator appears to be working (without rewards)
Former-commit-id: 3ca5c3ccf2
9 years ago
dehnert
08112d98aa
more work on JANI next state generator and the corresponding tests
Former-commit-id: e170c9989c
9 years ago
dehnert
05fecb03b3
started on introducing multiple initial locations in JANI models
Former-commit-id: cf009b3e14
9 years ago
dehnert
b62f8819b9
JANI next-state generator can now generate transitions from silent edges
Former-commit-id: 57e37b5850
9 years ago
dehnert
000a8c2d77
more work on JANI next-state generator
Former-commit-id: d94ab2b81e
9 years ago
dehnert
1d3539ab9a
factored out some parts from the PRISM next-state generator into the superclass
Former-commit-id: bb40e2ec4b
9 years ago
TimQu
1a18ea3aec
fixed the case where a maximal end componend decomposition is requested for an empty subsystem
Former-commit-id: 96ba0262ce
9 years ago
dehnert
4cc780cbc0
tests compiling and running again
Former-commit-id: f84c73d0ae
9 years ago
dehnert
4063d88913
added option to build all labels/reward models for next-state generators
Former-commit-id: cfb9787d6c
9 years ago
dehnert
d35c99e844
renamed central model builder function
Former-commit-id: 92cfaeae19
9 years ago
dehnert
9f6bd1805f
modified the entry point code to deal with the new generator-builder-structure
Former-commit-id: f01a19e346
9 years ago
dehnert
ddf165d4d3
more work on tearing PRISM-specific functionality out of the explicit model builder
Former-commit-id: a835c9072e
9 years ago
dehnert
6655ee41d8
started to restructure explicit model builder to make it fit for JANI models
Former-commit-id: 69603dd97b
9 years ago
dehnert
efda4e2950
changed the ordering of operations a bit to get more performance
Former-commit-id: 90fc1243f1
9 years ago
dehnert
ca57e22abc
started profiling
Former-commit-id: b7e034c16b
9 years ago
dehnert
c393449ca6
[fixing] a bug a day keeps insanity away
Former-commit-id: ef9bb46429
9 years ago
dehnert
3d4552cbf8
started working on improved JANI model building that still allows for more relaxed rules than PRISM when it comes to writing global variables
Former-commit-id: 9b216dc98e
9 years ago