Thomas Neele

I agree with @Valo13's observations, but not completely with @jgroote's. The simplification made in `lpsconfcheck` that causes it to under-approximate in this case, is the avoidance of expressions with quantifier...

> Wouldn't it be better to change the output slightly? That is perhaps a good idea. However, I also want to add that it might be more fruitful to spend...

I do not find the provided example very convincing. The precedence of the forall operator is lower than the implication operator (ie, the implication binds stronger. The fact that the...

I have another example that shows poor performance of the lineariser when using the `block` operator. In the attached file, a slight modification of the standard dining philosophers problem, I...

I rebased the branch on master. There were some minor merge conflicts, especially with commit 3ff435a8fcaf4c64180399850485793054f8f205. I resolved those by running the `generate_data_types.py` script repeatedly.

I would suggest to reopen this ticket and label it as 'long term'. I agree with Wieger that using .lts as output format requires a lot of memory. I don't...

An alternative I want to leave here for future reference: If we have ``` map g: Int -> (Int -> Int); ``` We can update the value of `g(1)(2)` with...

When exactly do the issues with the sum construction arise? Is that during linearisation (mcrl22lps) or during state-space generation (lps2lts)? In the latter case, you might be able to circumvent...

Next to confluence detection, we can also consider to add termination detection. This prevents unexpected stack overflows in the rewriter.

To make the issue more clear, consider the following. Load the specification above into a file `a.mcrl2` and execute: ``` mcrl22lps a.mcrl2 a.lps mcrl2i a.lps ``` In the prompt of...