dehnert
1be735ec1b
fixed tests in response to 'fixing' flattenModules
Former-commit-id: 07f28fb20a
8 years ago
dehnert
b3e77730a9
added uniqueness mechanism in flattenModules to compensate for missing uniqueness in allsat of solvers
Former-commit-id: b4ebd17f68
8 years ago
dehnert
b14f866e01
added more flatten tests
Former-commit-id: 7e35a90c88
8 years ago
dehnert
3e9f9552b1
fixed tests: using shared_ptr instead of unique_ptr for SMT solver factory in abstraction
Former-commit-id: 6159a20565
8 years ago
dehnert
18b0f07581
tweaked Bdd toExpression a bit to be more versatile
Former-commit-id: 858948f1b7
8 years ago
dehnert
52577e2740
added game abstraction tests for sylvan and made them work (in particular implemented toExpression for sylvan BDDs)
Former-commit-id: 8fdc34cb55
8 years ago
dehnert
53f83c9214
moved menu-game abstraction to separate folder and made everything compile again
Former-commit-id: a833ca1152
8 years ago
Mavo
5b8cf447c7
Small changes in tests to compile without Carl
Former-commit-id: 6ec191ce0a
8 years ago
TimQu
f681206393
building markov automata from prism code
Former-commit-id: 791c49c7cf
9 years ago
PBerger
0f84cdcadb
Fixed performance tests.
WARNING: I had to remove the SolverSelection in the call due to the new API - the performance tests might now all use the same Solver.
Former-commit-id: 7d5ed3191d
9 years ago
dehnert
83c4b1647c
solvers now can allocated auxiliary memory
Former-commit-id: 76dc1a1679
9 years ago
dehnert
95b95d9c64
fixed some minor issues and renamed equation solver methods slightly to make the names a bit more compact
Former-commit-id: de103e19ad
9 years ago
dehnert
9ab33528b4
started to fill value iteration implementation in new general min-max solver
Former-commit-id: e54cb8a0f9
9 years ago
dehnert
b4e0cabef6
started working on general min-max solver that uses an underlying linear equation solver. provided necessary factories. adapted code and removed old min-max solvers
Former-commit-id: c1895472c7
9 years ago
dehnert
8153306ced
fixed wrong call to Eigen's iterative solvers
Former-commit-id: 0e2e836729
9 years ago
dehnert
2a7dc0fad0
renamed MarkovChainSettings
Former-commit-id: 39024731f8
9 years ago
dehnert
07c787b49d
added unsupported solvers of eigen
Former-commit-id: e11b335c2d
9 years ago
dehnert
69da4ff147
fixed some more problems with Eigen solver
Former-commit-id: c6ed18c4ab
9 years ago
dehnert
00d331ebb4
moved linear equation solver factories to the respective solver files (and away from utility). restructured settings in factories and the way they are forwarded to the linear equation solvers. fixed all resulting errors
Former-commit-id: 27e1ae2466
9 years ago
PBerger
b99a063cce
Replaced calls to std::abs with calls to std::fabs and included cmath.
Former-commit-id: 40fb587e2f
9 years ago
dehnert
3ba5902821
removed debug output and fixed small bug in adaptation of Eigen
Former-commit-id: 5e1a70d933
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
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
023325b53d
added tests for Eigen solver
Former-commit-id: ede9efcee2
9 years ago
dehnert
bb700457de
some minor fixes
Former-commit-id: f114c397f6
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
4cc780cbc0
tests compiling and running again
Former-commit-id: f84c73d0ae
9 years ago
dehnert
d35c99e844
renamed central model builder function
Former-commit-id: 92cfaeae19
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
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
82023d280d
JANI model builder for MDPs is working now, but too slow
Former-commit-id: 8b36f65251
9 years ago
dehnert
3919f90712
started debugging JANI MDP building
Former-commit-id: b122d605be
9 years ago
dehnert
a4ef3cf778
added CTMC tests for JANI model builder
Former-commit-id: 783646bbed
9 years ago
dehnert
7750480714
JANI model builder for DTMCs working
Former-commit-id: 25f12f3e05
9 years ago
dehnert
310db8a234
started to include reachability in JANI model generation
Former-commit-id: d54f35b999
9 years ago
dehnert
6313e4c31b
fixed a bug in symbolic model generator
Former-commit-id: de49f7b812
9 years ago
dehnert
adf8232896
more work and fixes for symbolic JANI builder
Former-commit-id: 5ca11938c1
9 years ago
dehnert
c4327e91a9
more work on symbolic JANI model builder
Former-commit-id: 4fe002c4f8
9 years ago
dehnert
9c75e9dbd7
more work on JANI model generation
Former-commit-id: c5a5df87ee
9 years ago
dehnert
ecc1a80358
added conversion from PRISM to JANI. Added simplistic tests for that.
Former-commit-id: 5b31fa589c
9 years ago
sjunges
3b5c27acba
more test-files included, two small fixes in parser
Former-commit-id: 0e9000c988
9 years ago
sjunges
b64dc408ac
test case for die.jani parsing
Former-commit-id: b58a9102a6
9 years ago
dehnert
d38e7d5eb9
started working on jani data structures
Former-commit-id: 30deb6d38d
9 years ago
dehnert
7d03f0e4d0
improved error checking for custom parallel composition. added small tests.
Former-commit-id: 8f6b6913d6
9 years ago
dehnert
bf65ef726c
system composition in PRISM appears to be working
Former-commit-id: e7f0dd84e8
9 years ago