Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Segfault in get_integer_values_states #210

Open
nmanginas opened this issue Feb 21, 2025 · 2 comments · May be fixed by #212
Open

Segfault in get_integer_values_states #210

nmanginas opened this issue Feb 21, 2025 · 2 comments · May be fixed by #212

Comments

@nmanginas
Copy link

Hi thanks for the library. I am trying to use the get_integer_values_states that was recently added to the library.
I am using the master of Storm and of stormpy, since these functions were added after 1.9.0. I don't know if this is an issue of Storm or of the bindings. The types passed differ with the docs as prism_program.variables give a set of stormpy.storage.storage.Variable while get_integer_values_states seems to expect storm::expressions::Variable . I don't know if this might be a problem.

import stormpy

prism_program = stormpy.parse_prism_program(str(specification_path))  # type: ignore
options = stormpy.BuilderOptions()  # type: ignore
options.set_build_state_valuations()
options.set_build_choice_labels()

model = stormpy.build_sparse_model_with_options(prism_program, options)  # type: ignore

[
    model.state_valuations.get_integer_values_states(variable)
    for variable in prism_program.variables
]

You can repro with the simplest MDP:

mdp 

module test

a: bool;
b: bool;

[flip_a] (a=true) -> (a'=false);
[flip_a] (a=false) -> (a'=true);
[flip_b] (b=true) -> (b'=false);
[flip_b] (b=false) -> (b'=true);

endmodule

This gives: Segmentation fault (core dumped) after building the model. Any help is appreciated.

@nmanginas
Copy link
Author

Apologies for my mistake I should be calling get_boolean_values_states.
I presumed get_integer_values_states would cast the correct type.

I am leaving this open in case you think it would be good to add a check, but
feel free to close this.

Apologies for the disturbance.

@volkm
Copy link
Contributor

volkm commented Feb 21, 2025

Thanks for the report. While the call should indeed only use the right variable type, giving a segfault is definitely not good. I added assertions in Storm, but I believe we should also add dedicated checks in stormpy.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants