Tim Quatmann
|
f8754c0f50
|
LPSolvers: Allowing premature termination by specifying a mip gap. Fixes for incremental solving with Z3Lpsolver.
|
6 years ago |
|
Tim Quatmann
|
20fe90a527
|
Merge branch 'master' into deterministicScheds
|
6 years ago |
Matthias Volk
|
32c5a6f9da
|
Added return statement
|
6 years ago |
|
Tim Quatmann
|
0bbbb2f6fb
|
glpk: fixes for incremental solving
|
6 years ago |
|
Matthias Volk
|
4ee31063a4
|
Removed double whitespaces in outputs
|
6 years ago |
|
Tim Quatmann
|
78d99328b6
|
PrismParser: Making module renaming a LocatedInformation so we can properly store the line number of it. Also silenced a warning related to virtual destructors
|
6 years ago |
|
Tim Quatmann
|
6041e60aca
|
more work on incremental support for glpk
|
6 years ago |
|
Tim Quatmann
|
1323c099dd
|
Test for incremental LP solving.
|
6 years ago |
|
Tim Quatmann
|
078eb86c48
|
GLPK: added support for incremental solving
|
6 years ago |
|
Tim Quatmann
|
83832c990a
|
Merge branch 'master' into deterministicScheds
|
6 years ago |
|
Tim Quatmann
|
fb22c3fe68
|
Tests: Illegal synchronized writes are now detected already during parsing.
The corresponding test case has thus been moved.
|
6 years ago |
|
Tim Quatmann
|
afda2eb2a0
|
.gitignore: added files in l3pp/.git
|
6 years ago |
|
Tim Quatmann
|
d67f1b4898
|
cmake: Fixed compilation of shipped glpk under mac os
|
6 years ago |
|
Tim Quatmann
|
6008f489e2
|
bumped version of shipped glpk
|
6 years ago |
|
Tim Quatmann
|
cad5ed26d9
|
Merge branch 'master' into deterministicScheds
|
6 years ago |
|
Tim Quatmann
|
6dd6c502e7
|
Prism: Error upon synchronized write to global variable.
|
6 years ago |
|
Tim Quatmann
|
3db50f570d
|
PrismProgram: Correctly set line numbers for renamed modules.
|
6 years ago |
|
Tim Quatmann
|
632d7ee2fc
|
Merge branch 'prism-parser-improvements'
|
6 years ago |
|
Matthias Volk
|
4f36e7e431
|
Check if counterexample exists for k-shortest path
|
6 years ago |
|
TimQu
|
5f3065ec5a
|
PrismParser: Check for expression type. Support for formulas in arbitrary order.
|
6 years ago |
|
TimQu
|
48e98119d5
|
Merge branch 'master' into prism-parser-improvements
|
6 years ago |
|
TimQu
|
013695a6ce
|
Fixed compile issue: boost::split seems to need an lvalue for the input string.
|
6 years ago |
|
TimQu
|
734cb2d456
|
PrismParser: Allow Formula assignments in random order.
|
6 years ago |
|
Matthias Volk
|
ddff929cbd
|
Scheduler extraction is only supported for quantitative checks
|
6 years ago |
|
Tim Quatmann
|
d4199b544d
|
Merge branch 'master' into prism-parser-improvements
|
6 years ago |
|
Tim Quatmann
|
12ef18a239
|
PrismParser: Various improvements of error output. Support for using formulas before they were declared.
|
6 years ago |
|
Matthias Volk
|
bf735f0b00
|
Fixed doxygen issue with old cmake version (issue #55)
|
6 years ago |
|
Matthias Volk
|
b0abbb5088
|
Support for k-shortest path counterexamples
|
6 years ago |
|
Matthias Volk
|
bb71c078fa
|
Export to dot format allows for maximal line width in state labels and valuations
|
6 years ago |
Alexander Bork
|
11f89de9e8
|
Added preprocessing to reduce the POMDP state space before analysis
|
6 years ago |
|
Matthias Volk
|
9a5a6d72c6
|
Moved some cex code into counterexample module
|
6 years ago |
|
Matthias Volk
|
6a77ce210a
|
Moved setting nofixdl to build settings
|
6 years ago |
|
Matthias Volk
|
2c46b38130
|
Updated CHANGELOG
|
6 years ago |
|
Matthias Volk
|
b8991ca4bf
|
Fixed compile issue due to merge
|
6 years ago |
|
Matthias Volk
|
e4e069a98c
|
Slight refactoring of transformations
|
6 years ago |
|
Matthias Volk
|
fab86e8823
|
DFT wellformedness check can be performed stricter as precondition for analysis
|
6 years ago |
|
Matthias Volk
|
1767c40f2d
|
Refactored FDEPConflictFinder
|
6 years ago |
|
Matthias Volk
|
fb81571da5
|
Silenced some more compiler warnings
|
6 years ago |
|
Matthias Volk
|
38c7762254
|
Added missing include to fix compilation issue on Linux
|
6 years ago |
|
TimQu
|
cbecc6d192
|
Merge branch 'master' into deterministicScheds
|
6 years ago |
|
TimQu
|
9438d56ab3
|
added cli option for transforming continuous time models to discrete time.
|
6 years ago |
|
TimQu
|
b07acd0e3f
|
deterministicScheds: changed setting to --purescheds and added memory pattern 'counter'
|
6 years ago |
|
TimQu
|
48bddc29b7
|
NondeterministicMemoryProduct: Disabled support for Markov automata since Nondeterminism was added to Markovian states.
|
6 years ago |
|
TimQu
|
22a19d68ba
|
Fixed an issue with multi-objective model checking preprocessor not correctly preserving reachability rewards
|
6 years ago |
|
Matthias Volk
|
4c1958c245
|
Fixed some compiler warnings
|
6 years ago |
Jip Spel
|
179c46570b
|
Added missing file
|
6 years ago |
|
Alexander Bork
|
4b8664c521
|
Added reward under-approximation
|
6 years ago |
|
Jip Spel
|
e89b743f65
|
Update changelog
|
6 years ago |
|
Jip Spel
|
5c1d597292
|
Add line for changelog
|
6 years ago |
|
Jip Spel
|
a3d7c4c3f2
|
Merge branch 'master' into storm-pars-analysis-monotonicity
|
6 years ago |
