Darknety
|
68539592f2
|
Modelchecker-Prctl removed from original split
|
5 years ago |
|
Darknety
|
6e1238b10b
|
Modelchecker-Prctl tests split
|
5 years ago |
Tim Quatmann
|
9fabb01478
|
GlpkLpSolver: No exception if an integer solution exceeds the integer tolerance. (Just print an error).
|
5 years ago |
|
Tim Quatmann
|
654f705d2e
|
DetSchedsLpChecker: Glpk does not allow point intervals as bounds for variables.
|
5 years ago |
Matthias Volk
|
aa620f73f6
|
Travis: use newer Linux versions
|
5 years ago |
|
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 |
|
Jan Karuc
|
b8b6dab6db
|
Modelchecker test split
|
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
|
175a1d8686
|
Updated changelog.
|
5 years ago |
|
Tim Quatmann
|
f01577eacd
|
Merge branch 'deterministicScheds'
|
5 years ago |
|
Tim Quatmann
|
b7cd16df68
|
Updated Changelog
|
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 |
|
Tim Quatmann
|
20fe90a527
|
Merge branch 'master' into deterministicScheds
|
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
|
83832c990a
|
Merge branch 'master' into deterministicScheds
|
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
|
afda2eb2a0
|
.gitignore: added files in l3pp/.git
|
5 years ago |
|
Tim Quatmann
|
d67f1b4898
|
cmake: Fixed compilation of shipped glpk under mac os
|
5 years ago |
|
Tim Quatmann
|
6008f489e2
|
bumped version of shipped glpk
|
5 years ago |
|
Tim Quatmann
|
cad5ed26d9
|
Merge branch 'master' into deterministicScheds
|
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 |
|
Tim Quatmann
|
632d7ee2fc
|
Merge branch 'prism-parser-improvements'
|
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
|
48e98119d5
|
Merge branch 'master' into prism-parser-improvements
|
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
|
d4199b544d
|
Merge branch 'master' into prism-parser-improvements
|
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
|
bf735f0b00
|
Fixed doxygen issue with old cmake version (issue #55)
|
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
|
2c46b38130
|
Updated CHANGELOG
|
5 years ago |
