Tim Quatmann

Newer versions of Intel TBB are incompatible

2

There have been a couple of API changes in intel thread building blocks which apparently makes it incompatible with Storm right now. For example, our `findTBB.cmake` appears to not work...

The [IntegerLiteralExpressions](https://github.com/moves-rwth/storm/blob/51f86db9ebc6c7cf99bb3ad40b5775f58f4d205c/src/storm/storage/expressions/IntegerLiteralExpression.h#L49) store their value in a 64 Bit integer. This could not be sufficient in some cases, in particular when using the [ExpressionParser](https://github.com/moves-rwth/storm/blob/51f86db9ebc6c7cf99bb3ad40b5775f58f4d205c/src/storm-parsers/parser/ExpressionParser.cpp#L84) to parse rational functions (e.g. in...

Storm should not write the (shipped) carl project to the cmake registry

2

If we have to build a shipped version of carl and one of the following happens: * something goes wrong in cmake after the configuration step of carl * something...

jit always links with carl

1

Jit currently seems to link with all the glory of Carl, which is not necessary if ValueType is double. Fixing this should reduce build times for jit.

Signal Handling and subprocesses

3

Check whether the SignalHandler properly kills all subprocesses (Sylvan, Gurobi, ...)

The matrices differ in the order of the rows within the rowGroups. While this is not a critical bug, such inconsistencies can lead to, e.g., unexpectedly different verification times. This...

Checking nondeterministic models under an arbitrary scheduler allows us to use the (faster) algorithms for DTMCs/CTMCs. This might be useful, e.g., when the nondeterminism is known to be spurious. In...

Fix Formula Parser

2

## Fixed parsing expression formulas (fixes #195) The issue was that if we see an opening bracket `(` we expected that there is a *formula* inside the brackets. This is...

storm-pars: revised region refinement

5

This PR refactors the code for the region model checking in storm-pars: - Separate region model checking code (i.e. analyze a given region) from code concerning region refinement (partitioning of...

The jani specification allows rates to occur at edges in DTMCs which are then interpreted as weights. Previously, this case was not handled properly. This implements the weighting for explicit...