Extract MDP model to PRISM

[team-daniel]

Hello, I have an MDP model using Alergia. I would like to export this to PRISM for the use of model checking, does anyone know how I would go about this as there is nothing in the documentation?

Many thanks in advance!

[zwergziege]

You should be able to use mdp_2_prism_format(mdp: Mdp, name: str, output_path=None) from aalpy.utils to export, or you could use model_check_properties(model: Mdp, properties: str) directly.

[team-daniel]

Thank you for your quick reply, I have implemented the mdp_2_prism_format function and the model works in the PRISM GUI which is fantastic!

When I use the model_check_properties I get the error [Errno 2] No such file or directory: 'prism.sh'

I have called this line beforehand.
aalpy.paths.path_to_prism = '/home/user/Documents/Prism/bin/prism.sh'

do you know how to fix this? I appreciate all your help, you have been fantastic!

[team-daniel]

I am on Linux FYI

[zwergziege]

Unfortunately, I don't know what the issue could be. Setting aalpy.paths.path_to_prism works on my machine (running Ubuntu). Are you sure that <prism root>/bin/prism.sh is correct? For me (and in the official download) it's just <prism root>/bin/prism. I know it's a bit silly, but that's the only thing that came to mind on short notice.

[emuskardin]

As zwergziege said, maybe .sh should not be there.
We usually do it like this:

# Windows
aalpy.paths.path_to_prism = "C:/Program Files/prism-4.7/bin/prism.bat"
# Linux
aalpy.paths.path_to_prism = "/home/emuskar/Programs/prism-4.8-linux64-x86/bin/prism"

[team-daniel]

Thank you both, you have been a major help to me! You have fixed my issue, I just needed to remove the .sh from the assignment. It's always the simplest fix. Thank you again!

[emuskardin]

Hi,

mdp_2_prism_format method in https://github.com/DES-Lab/AALpy/blob/master/aalpy/utils/ModelChecking.py

Hints: Make sure that learned modes is input complete, MDPs class have a function for that.

from aalpy.utils import generate_random_mdp, mdp_2_prism_format

random_mdp = generate_random_mdp(10, 3, 3)

if not random_mdp.is_input_complete():
    random_mdp.make_input_complete(missing_transition_go_to='sink_state')

mdp_2_prism_format(random_mdp, 'random_mdp', 'save_file.prism')