search

xhajnal / DiPS

Multiple properties Probabilistic systems Model checker
BSD 3-Clause "New" or "Revised" License
4 stars 1 forks source link

test PRISM input models #87

Open xhajnal opened 3 years ago

xhajnal commented 3 years ago

Only a few models were tested, and parser may fail with even correct models since PRISM does not have a grammar of model structure

huypn12 commented 3 years ago

@xhajnal You can use stormpy for this purpose. For example 

import stormpy
try:
    prism_program = stormpy.parse_prism_program(prism_model_file)
except Exception as ex:
    print(f"Error parsing prism program {ex}")

change too broad Exception to the proper one

xhajnal commented 3 years ago

@huypn12 Thanks. Do you mean for testing or for the feature? Because to use it as a feature I need some additional dependencies over Storm, which I have failed to install on the VM for Artefact Evaluation.

TBD trace report of the Stormpy build error (currently unavailable)

huypn12 commented 3 years ago

i meant for testing if PRISM input models is syntactically valid.

Because to use it as a feature I need some additional dependencies over Storm, which I have failed to install on the VM for Artefact Evaluation.

If you need to use Stormpy, you need Storm in the first place. Once Storm is installed and registered in the system library path, you can use Pipenv and add the following line stormpy = {editable = true, git = "https://github.com/moves-rwth/stormpy.git@1.6.3"} Installing Storm is afaik just follow the document, the trick is to use a manually installed boost 1.64. Otherwise, storm wont compile