Matthias Volk
Matthias Volk
The counterexample generation using `SMTCounterExampleGenerator` only works if the input is given as a symbolic model description, for example in the Prism language. As you build the model yourself, this...
To better debug the issue, can you send me the complete Python file via email to [email protected] ?
The variable `rate_transitions` can be accessed in the `ModelComponents`. After building a model from the components, the variable becomes irrelevant. In a CTMC for example, the transition matrix always stores...
I have not looked at all details in the PR yet, I will review it in the next days.
Now it formats .py and .ipynb files ;) .rst files are not formatted but they should also not contain any Python code anymore, because the documentation is in the notebooks.
@sjunges can I merge it?
Merging after positive feedback by Sebastian.
Can you provide us the output of the log files `/some_path/Desktop/packages/storm/storm/build/resources/3rdparty/cudd-3.0.0/src/cudd3-stamp/cudd3-configure-*.log`?
Sounds like a good plan to me.
The output is indeed truncated according to the given precision, see the [code here](https://github.com/volkm/storm/blob/master/src/storm/utility/initialize.cpp#L41). The default precision should be at least 10 digits. In your case, the rewards are large...