Exact Solutions using Linear Programming
This is a brief description for the final submission of the GSoC 2016 program. This project implements the method described in  for providing exact solutions for both MDPs and DTMCs models using exact arithmetic on PRISM probabilistic model checker.
Full list of contributions
Last pull requests for the whole project (will be merged soon)
- Project (
- Tests (
Link to full diff (recall that it is a
rebase of all the commits made)
Link to new tests added to
Commits on the
prism-svn repository (by branch):
Commits on my first repository (by branch)
Commits on the
glpk repository (by branch)
Commits on the
libglpk-java repository (by branch)
Description of the whole project
computeReachProbsExactLinearProg was added for both
MDPModelChecker classes for implementing arbitrary precision arithmetic solutions. Its implementation follows the algorithm portrayed in , which basically creates the linear programming problem, solves it, and print out the solutions onto PRISM's log.
Extended GLPK interface
We needed to extend the GNU GLPK  library, which computes exact values using the GMP  arbitrary precision library, with an exact solutions interface to retrieve values directly from Java. The changes can be seen in the following two patches located in
ext/glpk_java/libglpk_java_exact.patch. Those patches are applied after a successful download of the two external libraries, and then they are built with the modifications.
This interface provides two types of exact solutions:
- In the form of
p/q: exact rational arithmetic, that is,
pis the exact numerator and
qthe exact denominator. Both numbers define the exact value. E.g.,
2/3is a way to state the infinite decimal expansion
0.6666.... This is easy to add in PRISM, just call to this function to obtain the arrays of numerators and denominators for each state like this:
GLPK.uint8Array_toString(GLPK.uint8ArrayArray_getitem(GLPK.glp_get_nums(lp), numState)) GLPK.uint8Array_toString(GLPK.uint8ArrayArray_getitem(GLPK.glp_get_dens(lp), numState))
These two methods provides the numerators and denominators for the exact solution of
In the form of fixed-precision. This is more user friendly (and is the one implemented currently in
computeReachProbsExactLinearProg), as the user can specify the desired precision (in bits) both from the console or the GUI, and the result is calculated using this setting.
Another approach that I implemented but then I removed, is to let the user the number of decimal digits desired. It is easy to extend the GLPK interface to provide this feature.
The installation of the PRISM library has been changed to check whether the tools required for the external libraries exist, then download the libraries from their repositories, and after that, patch them with the new interfaces and proceed with the making. This approach provides a portable solution while not increasing the weight of the project significantly.
Configuration and usage
From the GUI, the user who wants to compute exact solutions, should set from the options tab the following properties:
If the model is an MDP, the
MDP Solution Method chosen should be
Exact linear programming. The same setting goes for DTMCs but the option is
Linear equations method.
There is also a
Floating point precision option, which states the accuracy of the mantisa in bits. Recall that this is a minimum value as it is rounded up to a whole limb.
From the console, just add the flags
-precision. This is an example (extracted from the new regression tests I added in
prism ./two_dice_knuth.pm ./two_dice_knuth.pm.props -s -m -h -ex -exact-lp -precision 128 -test
which will return something like this: (this is only a small part of the results of the statement above)
128-bit results (non-zero only) for each state of the DTMC: : 0.08333333333333333333333333333333333333333 : 0.1666666666666666666666666666666666666667 : 0.3333333333333333333333333333333333333333 : 0.5 : 0.1666666666666666666666666666666666666667 : 0.25 : 0.08333333333333333333333333333333333333333 : 0.5 : 0.125 : 0.04166666666666666666666666666666666666667 : 0.25 : 0.08333333333333333333333333333333333333333 : 0.5 : 1
As PRISM uses regression testing, two new directories for exact arithmetic tests in the test-suite were added. They can be found in
Future work or extensions to this project
Currently it is needed an exact solution object that would be able to store exact values as real numbers (not just strings), using Java arbitrary-precision libraries such as Java BigNum, or something alike.
Also, this enhancement is not supported in Windows yet: it is only missing the building of the
.dlls of the external libraries and placing those files inside the project.