search

moves-rwth / prophesy

Parameter Synthesis in Markov Models
https://moves-rwth.github.io/prophesy/
GNU General Public License v3.0
6 stars 3 forks source link

Model repair feature encounters compilation error #4

Closed oyendrila-dobe closed 4 years ago

oyendrila-dobe commented 4 years ago

I tried running the model_repair.py as the example given in the script, python modelrepair.py --prism-file ../benchmarkfiles/brp/brp_16-2.pm --pctl-string "P<=0.95 [F \\"target\\"]" --cost-function "(+ (* (- pK 0.6) (- pK 0.6)) (* (- pL 0.7) (- pL 0.7)))". However, it encounters a error AttributeError: 'NoneType' object has no attribute 'check_tools' The full trace is as follows:

  File "modelrepair.py", line 176, in <module>
    model_repair()
  File "/Users/oreo/.pyenv/versions/3.7.5rc1/lib/python3.7/site-packages/Click-7.0-py3.7.egg/click/core.py", line 764, in __call__
    return self.main(*args, **kwargs)
  File "/Users/oreo/.pyenv/versions/3.7.5rc1/lib/python3.7/site-packages/Click-7.0-py3.7.egg/click/core.py", line 717, in main
    rv = self.invoke(ctx)
  File "/Users/oreo/.pyenv/versions/3.7.5rc1/lib/python3.7/site-packages/Click-7.0-py3.7.egg/click/core.py", line 956, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "/Users/oreo/.pyenv/versions/3.7.5rc1/lib/python3.7/site-packages/Click-7.0-py3.7.egg/click/core.py", line 555, in invoke
    return callback(*args, **kwargs)
  File "modelrepair.py", line 143, in model_repair
    mc = _get_selected_pmc(modelchecker)
  File "modelrepair.py", line 53, in _get_selected_pmc
    configuration.check_tools()
AttributeError: 'NoneType' object has no attribute 'check_tools'

My guess is in file config.py, configuration=None is never reset, (I'm guessing load_configuration was supposed to be invoked on it to initialize it). Not sure if I'm missing something.

sjunges commented 4 years ago

Hi,

the short answer is that this script should not have been in the master branch to start with. I will try to fix the error, but meanwhile: do you really have a cost function or what are you trying to achieve? I will likely move this script into the main parameter synthesis script as-we-go, so it would be good if I preserve the behaviour you are interested in.

Please notice that I recently started to extend the documentation.

Best, Sebastian

oyendrila-dobe commented 4 years ago

I basically need to find a way to get the created model for the input DTMC. I tried to find where in the parameter_synthesis file I could get that, but I could not trace back calls to the modelchecker.py, where I think I could get the built model from. The model_repair file seemed to have an easy call to model creation part of the code. Hence, I was trying that. Any help in this regard would be really appreciated.

sjunges commented 4 years ago

So you input a model describing a DTMC and you want to get an object that represents this DTMC for further processing? Then I don't see a reason to use prophesy. Stormpy should be all you really need. Maybe this document helps? https://moves-rwth.github.io/stormpy/getting_started.html#a-quick-tour-through-stormpy

The more information you give in that regard, the better I can help you.

oyendrila-dobe commented 4 years ago

I need the built model for a pDTMC, hence I was thinking of reusing the code of prophesy. But the tutorial you pointed out does make things more clear. Thank you.