dehnert
df9ff5dfdb
removed debug output in test and delete dylib if building fails
Former-commit-id: 0f6a0a8c2c
[formerly 2a2ca2ac40
]
Former-commit-id: 8e841483d1
8 years ago
dehnert
070e115b60
tests for JIT based model builder
Former-commit-id: 3155cb2bab
[formerly 151d6606fd
]
Former-commit-id: dcdeddf54a
8 years ago
dehnert
812e1c4235
adapted test to new check policy and made jani variable and expression variable have the same name in PRISM-to-JANI conversion
Former-commit-id: 137bdc8d9b
[formerly f0aab7368d
]
Former-commit-id: f1ee093be3
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
dehnert
299b2d7a56
some start on JIT-based model builder
Former-commit-id: b0bffd4908
[formerly 95829c4970
]
Former-commit-id: 8e98da5dd4
8 years ago
sjunges
7ef857137e
tests updated to respect headers now missing in parsers
Former-commit-id: fb6703d9b5
[formerly 5f89b42a60
]
Former-commit-id: 1751efe563
8 years ago
dehnert
1b42af776c
missing test-input file
Former-commit-id: 7562813973
[formerly e18ad2f0df
]
Former-commit-id: 367bbd2756
8 years ago
dehnert
0f1c1f28ab
fixed bug related to input-enabling automata, tests now passing
Former-commit-id: 98512a79f3
[formerly 176a5b5c34
]
Former-commit-id: 33fac8df7a
8 years ago
dehnert
d3cf9a4e7f
adding Markov automaton tests to explicit JANI model builder
Former-commit-id: 634fe9c08e
[formerly 73bbe89f78
]
Former-commit-id: bb9339a947
8 years ago
dehnert
3504d09500
added quite some debug output to see where things are going wrong
Former-commit-id: 4f61d66074
[formerly e11d6fb2b0
]
Former-commit-id: d72214ef96
8 years ago
dehnert
36e07006f9
added test for legality check of synch vectors
Former-commit-id: 6bef2f5a98
[formerly df607c9c1a
]
Former-commit-id: 78cc502eb2
8 years ago
dehnert
d22d1daaa6
adapted more tests
Former-commit-id: 4d75a4fe50
[formerly ad1ad61873
]
Former-commit-id: d359f2c9c1
8 years ago
dehnert
ba35120683
fixing problems as a consequence of moving from PRISM programs to SymbolicModelDescription
Former-commit-id: 01c8004a32
[formerly 824ae03428
]
Former-commit-id: 028527340f
8 years ago
dehnert
62ca16b20a
alpha-draft of synchronization vectors in JANI
Former-commit-id: 31eec25d2e
[formerly ecd02f99e6
]
Former-commit-id: 43c14e1dac
8 years ago
dehnert
c2cab571f5
made tests work again
Former-commit-id: bd3e831b0d
[formerly cef4348674
]
Former-commit-id: 8fd0b70c1e
8 years ago
sjunges
ba81925c1d
renamed smt2smtsolver to smtlibsmtsolver and cleaned make files
Former-commit-id: 78c74dc9a5
8 years ago
sjunges
19bf801456
Fixed MDP tests
Former-commit-id: 058bcbc4c6
8 years ago
sjunges
d97b0b2897
cleaned tests
Former-commit-id: 8d376e3c75
8 years ago
sjunges
b6465020a2
towards working tests in pla
Former-commit-id: 3542f8a1d0
8 years ago
sjunges
ba1f6bf3d5
jani property stub
Former-commit-id: 37f8f63d43
[formerly 54bc32bfd0
]
Former-commit-id: e934d063fd
8 years ago
sjunges
2637d51afc
set formula
Former-commit-id: e5d9a4ca30
8 years ago
sjunges
9632ca9f6f
fixed tests
Former-commit-id: c14b7234e2
8 years ago
sjunges
0ef2b55c75
made some region settings attribute to the model checker instead of global
Former-commit-id: e53ca96760
8 years ago
sjunges
548ba8bbeb
somehow managed my way through the policy guessing, several minor extensions to solvers
Former-commit-id: c4bb6453e7
8 years ago
sjunges
4999cfa8a0
By performance tests, you served us well but we do not love you any longer
Former-commit-id: 048c3447cb
8 years ago
sjunges
d8d8f70f0c
functional tests now work with the refactored code base
Former-commit-id: 2d7d7e111a
8 years ago
Mavo
5b8cf447c7
Small changes in tests to compile without Carl
Former-commit-id: 6ec191ce0a
8 years ago
sjunges
88af02e723
towards new jani version
Former-commit-id: 0c5e6825ca
[formerly b98985e8eb
]
Former-commit-id: 9f5ef53aec
9 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