Exact solutions for both MDPs and DTMCs using linear programming.

[nicodelpiano]

Exact Solutions using Linear Programming

This PR implements the method described in [1] to provide exact solutions for both MDPs
and DTMCs models using exact arithmetic.

New methods

The method computeReachProbsExactLinearProg was added for both DTMCModelChecker and MDPModelChecker classes to implement arbitrary precision arithmetic solutions. This implementation follows the algorithm portrayed in [1], which basically creates the linear programming problem, solves it, and prints 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.

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

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

[kleinj]

Hi,

this looks interesting! Some comments/suggestions/issues that I ran into when trying out the code:

1. Compilation: I had trouble compiling on OS X. The first issue is the use of sed -i in the Makefile. The OS X sed uses different semantics for the -i parameter:

   -i extension Edit files in-place, saving backups with the specified extension. If a
   zero-length extension is given, no backup will be saved.

   So, this is incompatible with GNU sed. However, see next point.

2. I'm not sure if it's a good idea to modify the

   public final int EXACT_LP_REQUIREMENTS_INSTALLED = 1;

   in PrismSettings.java in the first place from the Makefile. As PrismSettings.java is a file under version control, this will show up as a changed file, etc. I.e., modified/auto-generated files should not be under version control. Perhaps there is a different scheme for bringing this information to PRISM's attention? The .jar file for the glpk would perhaps be a good option?

3. Then, after I removed the sed call, I could not compile glpk on OS X, with an error of

   glpapi07.c:274:7: error: use of undeclared identifier 'mpf_t'
   mpf_t fix_prob;

   I guess that's due to some missing GMP library headers? I have libgmp installed via HomeBrew, but somehow they don't seem to be picked up. On a Debian system (with libgmp installed) it compiled.

4. As GLPK depends on GMP, it would make sense to similarily compile and package libgmp in the PRISM Makefile. Otherwise, a binary distribution of PRISM will not work if the user system does not have GMP installed.

5. There is another issue with the autogen.sh included in the glpk library. On OS X, the libtool command is not the GNU tool but something else. Usually, libtool and libtoolize are available as glibtool and glibtoolize (Stack Overflow thread).
   For me, the suggestion of running autoreconf -fvi instead of autogen.sh worked to generate the correct Makefiles (using glibtool and glibtoolize).

6. There is then the question how we want to package the sources of library dependencies. I'm not very fond of using wget to pull some source over http and then execute the Makefile. Another option would be to include the tgz in the PRISM repository and use the patch method or to just pull the whole sources into the PRISM repository, just as is done for lpsolve and cudd. @davexparker ?

7. As compiling GLPK can take a bit of time, it would probably make sense to make it configurable at make time whether that library should be built. There is currently no mechanism for that, but we should be able to come up with something. As far as I can tell, PRISM should behave gracefully if the library is not present, i.e., just acknowledge that using the exact LP methods is not available, right?

8. How is the glpk-java.jar that is included in the repository generated?

9. In the paper you linked (I only skimmed it, so might be wrong) they propose to take an existing optimal scheduler (constructed using inexact methods) as an input for the exact LP solution. This part is not included in your code, right? So, you get an exact solution but it might not be as fast as if you already knew a "near-optimal" solution?

10. If I understood correctly, the LP solver could provide you with the exact values as rational numbers (with probably quite big integers). In the param package of PRISM there is already a BigRational class that can be used to store those kinds of numbers exactly. So, I guess it would make sense to store the result in a StateValues object with BigRationals. However, the explicit model checker can not deal with BigRationals there, so you would need to convert back to a StateValues with Doubles... It might make sense to pull out the two solver functions into a separate class, as there is the potential to use them as well for solving using the current exact mode, i.e., where the model is a ParamModel with BigRationals for probabilities.

11. It would probably be nice to have an option to output the LP in text format for debugging purposes, perhaps there is already some functionality for that in the GLPK library?

I have a few other minor things that I'll add as comments inline to the commit.

[kleinj]

You should change the String here to "prism.exactlp.enabled" or similar.

[nicodelpiano]

Hi Joachim,

thanks for this great feedback!

Items 1 and 5. As I can't test this on a MAC, I didn't come up with this issues, but these could be fixed just by adding separated cases for OS X in the proper Makefiles with your suggestions.

Item 2. Yes, definitely. This would change constantly so it's not right to have that defined. I'll discuss how to change this with Vojtech and get back to this.

Items 3 and 4. Also, I had this problem of missing GMP in mind. This should be solved too, but I don't know whether we should include this as an external package or not.

Item 6. My first approach was to put the whole glpk and libglpk code in /ext. Then, the GLPK guys suggested me to use wget, so I thought it'd be better to not increase the weight of the whole project. But this could be changed as you suggest.

Item 7. I thought this possibility but haven't discussed it yet. Do you suggest a Makefile option like --exactlp which builds the external packages?

Item 8. I added this jar because, if the user decide not to compile or it doesn't have the requirements for build glpk (this continues the installation of PRISM), the code that uses the external library glpk won't be able to compile. I tested this jar in both 32 and 64 bit Debian, but I don't know if this is the best approach to solve this.

Item 11. Yes, I think this could be a nice feature as described here [1].

I'll get back to the missing answers as soon as I talk and clarify them with Vojtech or Dave. Thanks again!

[kleinj]

Hi Nico,

thanks, your last commit looks good.

Item 7. I thought this possibility but haven't discussed it yet. Do you suggest a Makefile option like --exactlp which builds the external packages?

Well, for a configure style build system you'd have a switch -with-exactlp and -without-exactlp. As PRISM just has the Makefile, I guess having an environment variable WITH_EXACTLP=0/1 would be one solution, with a default value set by the Makefile if it is not externally set. So, it should then be possible to do

make WITH_EXACTLP=1

for example.

Item 8. I added this jar because, if the user decide not to compile or it doesn't have the requirements for build glpk (this continues the installation of PRISM), the code that uses the external library glpk won't be able to compile. I tested this jar in both 32 and 64 bit Debian, but I don't know if this is the best approach to solve this.

So, basically it's just a dummy jar that provides the Java interfaces that are used by DTMCModelChecker and MDPModelChecker, but that would raise an error if actually used? That makes sense. I checked on OS X by manually setting EXACT_LP_REQUIREMENTS_INSTALLED=0 in the Makefile (for OS X) that the resulting PRISM does indeed work and just ignores the -exact-lp setting.

So, it would probably make sense if you'd detail how you have generated that dummy jar or provide a script, so it can be regenerated later on.

Cheers,
Joachim

[nicodelpiano]

Hi Joachim,

make WITH_EXACTLP=1

Nice, this option sounds good. Working on it to reorganize the code inside the Makefile.

So, basically it's just a dummy jar that provides the Java interfaces that are used by DTMCModelChecker and MDPModelChecker, but that would raise an error if actually used? That makes sense. I checked on OS X by manually setting EXACT_LP_REQUIREMENTS_INSTALLED=0 in the Makefile (for OS X) that the resulting PRISM does indeed work and just ignores the -exact-lp setting.

So, it would probably make sense if you'd detail how you have generated that dummy jar or provide a script, so it can be regenerated later on.

Well, basically that .jar can be generated from the glpk and glpk_java bindings. After compiling glpk_java, the .jar is located in ext/glpk_java/src/glpk_java/swig/. The one I uploaded now has the flag EXACTLP_REQUIREMENTS set to 0, so, if the compilation of either glpk or glpk_java fails, PRISM would compile as the linkings to the library exist. I don't know if this is the best option, though, as if someone else changes this .jar, it would be different to the tracked one in the repository. This would be OK if we can leave this dummy glpk-java.jar unmodified as an interface provider.

Let me know if something is not clear, or if you have any suggestions to deal with this.

Thanks!
Nico.

[kleinj]

Hi Nico,

ok, that makes sense. If that's not to much trouble having a Makefile target (for the maintainer) to regenerate the dummy glpk-java.jar would probably be a good idea. That way, if someone specifically triggers rebuilding the dummy jar (changed library version perhaps) they can then commit the newly generated jar to the repository. Likewise, perhaps you could rename the jar that it stored in the repository to something like dummy-glpk-java.jar? Then it's clear what the purpose it.

For the flag, it might make sense to rename to GLPK_AVAILABLE or something like that, as there might be other users of the glpk library apart from your code in the future.

BTW, if you still need a portable way to replace a string in a file (without using sed), you should be able to use:

perl -pi -e 's/foo/bar/' file

Cheers,
Joachim

[pranavashok]

Hi @kleinj, Hi @nicodelpiano,

Any updates on the status of this pull request? We'd like to use/extend this code a bit and were wondering whether there are any plans of merging it into the main repo.

Cheers,
Pranav

[kleinj]

Hi,

we are currently looking how to schedule merging the various pending feature branches. For this PR, there remain some minor technical questions about the integration of the library in the build process. But it should be safe to build upon Nico's work and have that keep working later on when the PR is merged into the main branch.

Cheers,
Joachim

[pranavashok]

Hi Joachim,

Sounds great. We'll move ahead with it then.

Cheers,
Pranav