Matthias Volk
|
6a1ab53e35
|
Use carl version 18.06 if building from within Storm
|
6 years ago |
TimQu
|
5a16b2befa
|
minor fixes to let the total reward tests compile and pass
|
7 years ago |
|
TimQu
|
1f4c0325be
|
test cases for ctmcs and markov automata
|
7 years ago |
dehnert
|
cdfa328464
|
first attempt at adapting to Z3 interface change
|
7 years ago |
|
Matthias Volk
|
9e398ffaab
|
Minor improvements for some CMake output
|
7 years ago |
|
Matthias Volk
|
c5e356bc40
|
Proper installation of Storm
|
7 years ago |
|
dehnert
|
ca651ec61c
|
fixes github issue #24 related to MEC decomposition
|
7 years ago |
|
dehnert
|
e019bf19d1
|
fixing Z3 hint handling
|
7 years ago |
|
dehnert
|
869271259e
|
updated git version retrieval cmake plugin
|
7 years ago |
|
Matthias Volk
|
ef1cbae83c
|
Tests for DRN parser
|
7 years ago |
|
Matthias Volk
|
263e6ed5f8
|
Removed generated files from git
|
7 years ago |
|
Matthias Volk
|
df1571d737
|
Added more DFT tests
|
7 years ago |
|
Matthias Volk
|
2c9f6294a4
|
Started on DFT regression tests
|
7 years ago |
|
dehnert
|
022adf988d
|
fixed typo
|
7 years ago |
|
dehnert
|
a5bc5d30e5
|
added new gurobi version to find script
|
7 years ago |
|
dehnert
|
01dc240eea
|
fixed checking carl version
|
7 years ago |
|
dehnert
|
4591dba631
|
made maxsat-based counterexample generation be applicable to DTMCs and MDPs
|
7 years ago |
|
dehnert
|
676120229b
|
intermediate stage
|
7 years ago |
|
TimQu
|
ea6c957030
|
tests for multi-dimensional cost bounded DTMCs
|
7 years ago |
|
Matthias Volk
|
dbcc49f48f
|
Use new carl release 17.12
|
7 years ago |
|
Matthias Volk
|
945e360bcf
|
Increased minimal carl version to 17.10
|
7 years ago |
|
dehnert
|
f6eadc14ca
|
adding proper carl_DIR when using shipped carl
|
7 years ago |
|
dehnert
|
a8caaf83c2
|
made passing carl to sylvan more robust
|
7 years ago |
|
dehnert
|
1460e8f969
|
proper forwarding of Boost include directories to sylvan CMakeLists.txt
|
7 years ago |
|
TimQu
|
64a0d7ec3a
|
added missing file
|
7 years ago |
|
dehnert
|
7d65bd5e2e
|
fixing carl version check
|
7 years ago |
|
Matthias Volk
|
58c8531d34
|
Use Carl 17.10
|
7 years ago |
|
dehnert
|
3185719fe5
|
fix for linking issue under linux, adding missing l3pp dependency l3pp_ext
|
7 years ago |
|
dehnert
|
02c23865da
|
reworked memory leak solution in sylvan according to Tom van Dijks hints
|
7 years ago |
|
dehnert
|
72d58b6155
|
fix for sylvan workers not releasing mmap'ed memory
|
7 years ago |
|
dehnert
|
1f16008b75
|
added proper exception handling to sylvan-based sharpening
|
7 years ago |
|
dehnert
|
45a4b63a2e
|
fixed some issue in sylvan sharpen and forward minmax bounds to linear equation solver
|
7 years ago |
|
dehnert
|
f2e581b3df
|
rational search for symbolic linear equation solvers
|
7 years ago |
|
dehnert
|
b09cb95254
|
fixed wrong call in sylvan double to rational number conversion
|
7 years ago |
|
dehnert
|
da02237769
|
work towards symbolic rational search
|
7 years ago |
|
dehnert
|
6e8465e9f1
|
started on symbolic rational search
|
7 years ago |
|
Matthias Volk
|
4626aa0e69
|
Updated search for mathsat in cmake and fixed linker problem
|
7 years ago |
|
dehnert
|
e719a37c6c
|
fixes related to relative termination criterion
|
7 years ago |
|
TimQu
|
ade8078759
|
added test for lower bounded properties
|
7 years ago |
|
dehnert
|
bac50a32ab
|
warkaround for gcc 7.2.0: make modernjson compile again
|
7 years ago |
|
dehnert
|
c5134c364f
|
Extraction and update of TBB-parallelized stuff
|
7 years ago |
|
dehnert
|
c77b9ce404
|
gauss-seidel style multiplication for gmm++
|
7 years ago |
|
dehnert
|
43643b9699
|
bump gmm++ version to 5.2 (from 5.0)
|
7 years ago |
|
dehnert
|
f7c803827b
|
remove debug output
|
7 years ago |
|
dehnert
|
4adee85fa5
|
added checking requirements of MinMax solvers to model checker helpers
|
7 years ago |
|
TimQu
|
591a53582a
|
fixed test
|
7 years ago |
|
TimQu
|
e1aba323bf
|
more tests for reward unfolding
|
7 years ago |
|
TimQu
|
172b17d7ae
|
simple testcase for the reward unfolding
|
7 years ago |
|
dehnert
|
e2e1407f3e
|
not calling sylvan_var on leaf nodes of sylvan anymore
|
7 years ago |
|
dehnert
|
6bebb3c9d5
|
fix bug in rational number/function handling with sylvan
|
7 years ago |
