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

Temporary Storm result file not being created #3

Closed oyendrila-dobe closed 4 years ago

oyendrila-dobe commented 4 years ago

I'm trying to run get a solution function, however, in spite of getting the message that the model checker ran fine, the temporary file that stores the result of the model checker isn't getting created, hence the program crashes. Let me know if I am doing something wrong.

Screen Shot 2019-11-01 at 1 58 34 PM

This might be stupid but the file isn't actually getting created

Screen Shot 2019-11-01 at 1 59 19 PM
volkm commented 4 years ago

The computation of a rational function is only supported for DTMCs. For MDPs there is a different rational function for each scheduler and we cannot compute a unique rational function. However, the output was very misleading because the model checker did not finish successfully. I added some better error output in 965a875d0c00b7facb63363beeb5cb9f3d18382d to make clear where exactly the problem is.