How to use PRISM in programm.

Skip to first unread message


Jul 25, 2023, 2:53:18 AM7/25/23
to PRISM model checker
Hello Prof.Parker.
      I'm now doing  some experiment about probablistic model chcking on AI agent trained in Pyhthon.  So I want to modulate PRISM in the program to complete the probabilistic model checking of the DTMC model built in Python.
       I have coonected Python to PRISM using py4j. Currently I can only try to call the functions(e.g. computeUntilProbs(dtmcSimple,Remain,target))in the explicit package in the PRISM source code via wrapper, but this seems to take a lot of time(100,000 states may take several hours) to complete the verification, which the explicit engine through the GUI interface only take 0.x s.
      So I wonder if I find the right way to use the  explicit package in the PRISM source code. Or is there any tips to use PRISM with source code.

Dave Parker

Aug 1, 2023, 11:41:54 AM8/1/23

For now, the preferred way to control PRISM programmatically is to do so
via Java. There are instructions and examples here:

People have used py4j to to do this from Python in the past, but it is a
bit tricky.

We are currently working on a proper Python wrapper/API for PRISM.
Hopefully a first version will be available relatively soon, for you to
experiment with.

Best wishes,

Reply all
Reply to author
0 new messages