search

moves-rwth / stormvogel

Storm for almost everyone
2 stars 0 forks source link

Transitions are not sorted by id when mapping to stormpy #98

Closed lukovdm closed 2 months ago

lukovdm commented 2 months ago

Related to #97

When mapping transitions to stormpy the transitions are added to the matrix in order of insertion into the dict, not in order of the keys of the dict: https://github.com/moves-rwth/stormvogel/blob/6eaaa7d1e6624aeb9e79683ba487f57f1b3e58ff/stormvogel/mapping.py#L31 This results in incorrect transitions in the matrix of the stormpy model when adding transitions out of order of the state ids.

lukovdm commented 2 months ago

I am guessing that the stormvogel state ids no logger match up with the stormpy ones if you fix this. In which case it would be helpfull to also provide a mapping between stormvogel state ids and stormpy state ids.

PimLeerkes commented 2 months ago

That problem luckily doesn't seem to occur because: If we add transitions corresponding to states in wrong order while building the model, and sort this while mapping to stormpy, it matches the existing order of the states again.

Is this what you meant?

lukovdm commented 2 months ago

Yes you are right. I think my comment was meant for #94, there you could get this problem