Help needed regarding creation of variable of supported variable type in ParametricSparseMatrix

[oyendrila-dobe]

Hi, I have generated a parametric model from a prism file and am working on it. I need to change the value of transitions associated with the actions of a state of the model. I found the function set_value() useful for this purpose but need some help in converting say, 5, to a compatible data type for the function. I'm guessing create_integer() or create_integer_variable() might be what I'm looking for, but I'm not sure how to invoke it. Any help in this matter would be really appreciated.

[sjunges]

If I understand you right, you are trying to do something along the following lines (in pseudo code..)

model = from_prism() model.transition_matrix.at(row,column).set_value("x+y").

Is that correct? In particular, do you want to set it to a constant value or to some polynomial? Once I understand what you want to do, I will try to construct an example that does so.

[oyendrila-dobe]

Yes. Just to be sure, each transition here is comprised of column value and probability value. I'm trying to set the probability value, like you said, to either an integer (0 or 1) or to a parameterized expression ( say, p^ - 2). Basically trying to force a change in the transition probability of one state to another.

[sjunges]

Hi,

please have look at: 04-parametric-models.py

I hope that helps. Let me know if you have questions.

Please be aware that

• storm was never designed to alter models, so you have to be careful with inserting zeros etc.
• stormpy has limited support for these operations
• the internal data structures are awkward. They are encapsulated by pycarl, and that project is not getting much attention... You might want to add some functionality there that eases the operations.

It might also be possible to translate to rational functions in the right format from storm.expressions to pycarl rational functions in the right format (with the benefit of better usability). However, these methods would need to be added. I am happy to give you pointers.

[sjunges]

I just realised that we already had another example : 02-building-models.py

[oyendrila-dobe]

I think these should be enough for my current requirements. Thanks for the quick help.

[oyendrila-dobe]

Hi, Is there any way to add a new transition? Like set.value() is allowing me to change the probability of the transition, is there any way to change the column value for the transition? Or is there any way to add a new transition in the parametric sparse matrix, after I have parsed the model? Actually I'm working on until formula for hyperproperties and need to alter transition probabilities as a part of the algorithm.

[volkm]

Hi, unfortunately the functionality to modify a model in stormpy is currently limited. The main reasons for the limitation are the data structures in Storm itself. We are using a sparse matrix representation for models, which is not really intended for later modification. Therefore, for the moment you can not add or remove transitions after you created the matrix. You can however change the probability of transitions.

I see two possibilities for you to achieve the required model modifications:

1. You can either change the input file according to each modification and reload the model after each change. Stormpy also supports an explicit text format as input which makes changes easy.

2. Or you can start with a complete model where all transitions you will need in the future are already incorporated with a non-zero probability. By setting transitions probabilities to zero you can then mimic the removal of transitions.

[oyendrila-dobe]

I'll try to incorporate the second idea. Thank you so much.

[oyendrila-dobe]

Does stormpy optimize the probability values when building a model from a prism program? For a given prism program, I am getting anomalies in the values in the transition matrix. Please find my prism file and the corresponding transition matrix produced. Any insight would be much appreciated. model.txt

[sjunges]

Can you make your question more precise? What is the matrix you expect, what is the matrix that you get? Also, the matrix is rather large. It would help if you make the matrix smaller or highlight what I should look at.

In particular, if I look at row 10, then everything seems fine?

[oyendrila-dobe]

I'm sorry for throwing such a huge output at you. So if you look at row 20, it should have 1+z at col 20, however it adds 1 at col 22. Again at row 14, there should have been a value at col 20, 22 and 14, instead now there's just one value at col 13.

[tquatmann]

There is no guarantee that row i contains the transitions for the state 's=i'. When building a model from a Prism file, the internal order of the states is arbitrary. You could export a mapping from state indices to variable assignment. However, in your case it seems that you explicitly enumerate the transition probabilities for each state. It might make more sense to read the model from the explicit .drn format.

I converted your example to drn using the command line interface of storm: ./storm-pars --prism model-1.txt --buildfull --io:exportexplicit model1.drn

Please tell us if we should elaborate on this.

[tquatmann]

I'm sorry, I was not very clear. When loading a PRISM file, the resulting state order is arbitrary. When loading a DRN file, the resulting state order is as in the DRN file. So if you want to preserve a specific order, you should load your model from a DRN file. The DRN file I sent you has the same order as in the matrix you initially sent us (that's why it produces the same output).

Regarding the variable assignment (we call that state valuations) I would recommend to have a look at this file: https://github.com/moves-rwth/stormpy/blob/master/examples/building_models/03-building-models.py

On 10. Dec 2019, at 18:39, Oyendrila Dobe notifications@github.com wrote:

Thanks for the suggestion but it produces the same output. The model building stage renames the states to optimize in some sort. The probability remains the same. Like for my given model, state 20 in my model file is mapped to state 13 in the generated model. I'm not sure how to handle this. Could you elaborate on the export a mapping from state indices to variable assignment part

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/moves-rwth/stormpy/issues/9?email_source=notifications&email_token=AEHCDKTERQCFAZZQCI3BLVLQX7H4XA5CNFSM4JTRRT6KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEGQDK7A#issuecomment-564147580, or unsubscribe https://github.com/notifications/unsubscribe-auth/AEHCDKQWSIATME2GPY36LPTQX7H4XANCNFSM4JTRRT6A.

[oyendrila-dobe]

Yes yes I figured that out a little while back. Thank you so much @tquatmann for elaborating on it. Much appreciated.

[oyendrila-dobe]

Is there any way to evaluate expr1 <= expr2 and store it as an expression? expr1 and expr2 are factorized rational functions made up of parameters of a DTMC.

[sjunges]

The questions you are posing are not related in any way to the first question. I would kindly ask you to keep the questions related to the topic and topic title. Feel free to open a seperate issue though. That helps other people in finding the problem and answer, and helps us in referring to these answers.

Furthermore, given the rather detailed questions you are asking, you might want to consider sending a mail with your questions aggregated. Github Issues are not meant to be a forum thread.