Skip to content

Instantly share code, notes, and snippets.

@nicodelpiano

nicodelpiano/GSoC-FinalSubmission.md

Last active August 20, 2016 21:29
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save nicodelpiano/ffa503f8f1e4919c227b99a17df769f5 to your computer and use it in GitHub Desktop.
Save nicodelpiano/ffa503f8f1e4919c227b99a17df769f5 to your computer and use it in GitHub Desktop.
Download ZIP
This is Nicolas Del Piano's GSoC final submission
Raw
GSoC-FinalSubmission.md

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 [1] 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)

Link to full diff (recall that it is a rebase of all the commits made)

https://github.com/nicodelpiano/prism-svn/commit/7c56796ea2c3436614b268f1a18eef8d24e1974f

Link to new tests added to prism-tests

https://github.com/nicodelpiano/prism-tests/commits/exact_tests?author=nicodelpiano

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

New methods

The method computeReachProbsExactLinearProg was added for both DTMCModelChecker and MDPModelChecker classes for implementing arbitrary precision arithmetic solutions. Its implementation follows the algorithm portrayed in [1], 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 [2] library, which computes exact values using the GMP [3] 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/glpk_exact_solutions.patch and 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:

  1. In the form of p/q: exact rational arithmetic, that is, p is the exact numerator and q the exact denominator. Both numbers define the exact value. E.g., 2/3 is 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 numState.

  1. 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.

  2. 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.

Installation

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 -exact_lp and -precision. This is an example (extracted from the new regression tests I added in functionality/verify/dtmcs/exact-arithmetic/):

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]: 0.08333333333333333333333333333333333333333
[2]: 0.1666666666666666666666666666666666666667
[6]: 0.3333333333333333333333333333333333333333
[10]: 0.5
[11]: 0.1666666666666666666666666666666666666667
[16]: 0.25
[17]: 0.08333333333333333333333333333333333333333
[22]: 0.5
[23]: 0.125
[24]: 0.04166666666666666666666666666666666666667
[29]: 0.25
[30]: 0.08333333333333333333333333333333333333333
[33]: 0.5
[42]: 1

Testing

As PRISM uses regression testing, two new directories for exact arithmetic tests in the test-suite were added. They can be found in /functionality/verify/mdps/exact-arithmetic/ and /functionality/verify/dtmcs/exact-arithmetic/.

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment