stormpy

stormpy copied to clipboard

Formula has a property .threshold which invokes calling a function that should only be called when a bound is present. Debuggers may want to display this property (which they do,...

sjunges

Package stormpy as a wheel

6

Hi, it is easy to compile stormpy as a python wheel: ``` python3 -m build --wheel => Successfully built stormpy-1.8.0-cp312-cp312-macosx_14_0_arm64.whl pip install ./dist/stormpy-1.8.0-cp312-cp312-macosx_14_0_arm64.whl ``` Why not package it as a...

linusheck

Add interpreter lock release to POMDP check function

4

The POMDP check function binding is lacking the release of the global interpreter lock that allows other processes to take control of a stopped belief exploration model checker. Thanks to...

AlexBork

Circular import error

7

I'm trying to use the ```parse_prism_program``` method. The python script can recognize all the other modules except the core module. I have installed stormpy in a directory, and moved the...

oyendrila-dobe

Based on https://github.com/moves-rwth/stormpy/pull/154

sjunges

The argument `force_fully_observable` for `check_model_sparse` simply performs a cast from POMDP to MDP. It would be better to explicitly handle this transformation with existing stormpy methods instead of implicitly doing...

volkm

We bind quite some vectors and sets, which are currently copied explicitly every time, see https://pybind11.readthedocs.io/en/stable/advanced/cast/stl.html. It may be good to think about this. Another problem is that for sets,...

sjunges

can't check DTMC model

6

I created a DTMC model by `stormpy.parse_prism_program` And I want to check the property I defined, but some error occured. The python code I wrote follows: ```python path = "/home/yangjunfeng/Verify/abstract/cartpole/prism_model/cartpole_level5_train3_8.pm"...

Serendipity953

Automatic formatting via black + CI support

2

- Use [black](https://black.readthedocs.io/) for automatic Python code formatting. After installing the black package, code can be formatted using `black .` - CI support for checking and applying code formatting, similar...

volkm

need to be merged after https://github.com/moves-rwth/storm/pull/582

volkm