Tim Quatmann
|
a0e68a9d22
|
MultiObjectiveSchedRestModelCheckerTest: The test should not be executed if the installed z3 version is too old for optimization.
|
5 years ago |
|
TimQu
|
1807775c6c
|
Removed test of SparseModelNondeterministicTransitionBasedMemoryProduct which is no longer in use.
|
5 years ago |
|
TimQu
|
bba5c65afb
|
The MultiObjectiveSchedRestModelCheckerTest now also works without Gurobi.
|
5 years ago |
|
TimQu
|
d8338676ff
|
Delete unused files.
|
5 years ago |
|
Tim Quatmann
|
3881ae73f2
|
glpk: Fixed pop()ing for the case where no constraints have to be deleted.
|
5 years ago |
|
Tim Quatmann
|
c977a1f5fa
|
Fix for detecting infeasible models in glpk.
|
5 years ago |
|
Tim Quatmann
|
293fec426e
|
Flagged several options as advanced.
|
5 years ago |
|
Tim Quatmann
|
7c535cca84
|
Fixed upcasting of Exceptions in PrismParser.
|
5 years ago |
|
Tim Quatmann
|
d1f4e111b1
|
DetSchedsLpChecker: Do not assume Gurobi as LPSolver.
|
5 years ago |
|
Tim Quatmann
|
f8754c0f50
|
LPSolvers: Allowing premature termination by specifying a mip gap. Fixes for incremental solving with Z3Lpsolver.
|
5 years ago |
Matthias Volk
|
32c5a6f9da
|
Added return statement
|
5 years ago |
|
Tim Quatmann
|
0bbbb2f6fb
|
glpk: fixes for incremental solving
|
5 years ago |
|
Matthias Volk
|
4ee31063a4
|
Removed double whitespaces in outputs
|
5 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
|
5 years ago |
|
Tim Quatmann
|
6041e60aca
|
more work on incremental support for glpk
|
5 years ago |
|
Tim Quatmann
|
1323c099dd
|
Test for incremental LP solving.
|
5 years ago |
|
Tim Quatmann
|
078eb86c48
|
GLPK: added support for incremental solving
|
5 years ago |
|
Tim Quatmann
|
fb22c3fe68
|
Tests: Illegal synchronized writes are now detected already during parsing.
The corresponding test case has thus been moved.
|
5 years ago |
|
Tim Quatmann
|
6dd6c502e7
|
Prism: Error upon synchronized write to global variable.
|
5 years ago |
|
Tim Quatmann
|
3db50f570d
|
PrismProgram: Correctly set line numbers for renamed modules.
|
5 years ago |
|
Matthias Volk
|
4f36e7e431
|
Check if counterexample exists for k-shortest path
|
5 years ago |
|
TimQu
|
5f3065ec5a
|
PrismParser: Check for expression type. Support for formulas in arbitrary order.
|
5 years ago |
|
TimQu
|
013695a6ce
|
Fixed compile issue: boost::split seems to need an lvalue for the input string.
|
5 years ago |
|
TimQu
|
734cb2d456
|
PrismParser: Allow Formula assignments in random order.
|
5 years ago |
|
Matthias Volk
|
ddff929cbd
|
Scheduler extraction is only supported for quantitative checks
|
5 years ago |
|
Tim Quatmann
|
12ef18a239
|
PrismParser: Various improvements of error output. Support for using formulas before they were declared.
|
5 years ago |
|
Matthias Volk
|
b0abbb5088
|
Support for k-shortest path counterexamples
|
5 years ago |
|
Matthias Volk
|
bb71c078fa
|
Export to dot format allows for maximal line width in state labels and valuations
|
5 years ago |
|
Matthias Volk
|
9a5a6d72c6
|
Moved some cex code into counterexample module
|
5 years ago |
|
Matthias Volk
|
6a77ce210a
|
Moved setting nofixdl to build settings
|
5 years ago |
|
Matthias Volk
|
b8991ca4bf
|
Fixed compile issue due to merge
|
5 years ago |
|
Matthias Volk
|
e4e069a98c
|
Slight refactoring of transformations
|
5 years ago |
|
Matthias Volk
|
fab86e8823
|
DFT wellformedness check can be performed stricter as precondition for analysis
|
5 years ago |
|
Matthias Volk
|
1767c40f2d
|
Refactored FDEPConflictFinder
|
5 years ago |
|
Matthias Volk
|
fb81571da5
|
Silenced some more compiler warnings
|
5 years ago |
|
Matthias Volk
|
38c7762254
|
Added missing include to fix compilation issue on Linux
|
5 years ago |
|
TimQu
|
9438d56ab3
|
added cli option for transforming continuous time models to discrete time.
|
5 years ago |
|
TimQu
|
b07acd0e3f
|
deterministicScheds: changed setting to --purescheds and added memory pattern 'counter'
|
5 years ago |
|
TimQu
|
48bddc29b7
|
NondeterministicMemoryProduct: Disabled support for Markov automata since Nondeterminism was added to Markovian states.
|
5 years ago |
|
TimQu
|
22a19d68ba
|
Fixed an issue with multi-objective model checking preprocessor not correctly preserving reachability rewards
|
5 years ago |
|
Matthias Volk
|
4c1958c245
|
Fixed some compiler warnings
|
5 years ago |
|
TimQu
|
bb439d076b
|
DetScheds: Fixed wrong computation of the number of schedulers.
|
5 years ago |
Jip Spel
|
ed3fa3f82b
|
Fix TODOs
|
5 years ago |
dehnert
|
0842cb1bd7
|
DdJaniModelBuilder: adding source locations to guards to correctly track action fragments writing global variables
|
5 years ago |
|
Jip Spel
|
a39f297b8c
|
Fix OrderTest and add assert in Order
|
5 years ago |
|
Jip Spel
|
f98250968c
|
Fix checking monotonicity on samples
|
5 years ago |
|
Tim Quatmann
|
555fd90536
|
Silenced a few warnings.
|
5 years ago |
|
Tim Quatmann
|
d61d1bd3fe
|
Fixed type uintX -> uintX_t
|
5 years ago |
|
Tim Quatmann
|
cb00c21db2
|
Fixed type uintX -> uintX_t
|
5 years ago |
|
Tim Quatmann
|
8d99ae4f4c
|
Added some more trace output for sound value iteration.
|
5 years ago |
