Using allow or block can have a large effect on the linearization speed

[jgroote]

The enclosed example shows that alphabet axioms are not applied under certain circumstances. It would be useful if they would be applied in more general cases.

Reported by Rutger van Beusekom. Verum. my.mcrl.txt

[jgroote]

P.s. the enclosed file indicates which situations are problematic. Folding the equations in init, i.e. by writing

init hide({foo}, block({foo}, W))

can have very different behaviour than using non folded equations, each applying a single operator, as observed by Tim Willemse.

[tneele]

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 use the block operator to block the actions { get, put, up, down }. This leads to: calculating the communication operator modulo the block operator on 59048 action summands However, if I replace that block operator with an allow operator that allows the other actions, i.e., allow( { lock,free }, ... ), then the lineariser is fast.

dining5.mcrl2.txt

[wiegerw]

The original issue has now been resolved. The dining philosophers case looks like an entirely different issue to me. I will rename the issue to reflect that.

[jgroote]

The example of Thomas Neele has 19090 resulting summands and as such it is a very different specification than one obtains when using the allow. When the allow is used allowing all summands that block allows, we see that the alphabet axioms are not applied as effectively as with the allow. With the allow 4652 intermediate action summands are generated with the block operator there are 59048. The difference in time in applying the communication operator is in the same order of magnitude. This means that the essential difference is in the effectiveness of applying the alphabet axioms and it is not an issue of the lineariser.

It is unclear however whether the alphabet axiomas for the block operator are suitable to resolve the problem, nor is it clear whether we want to invest much time into this.

In particular one can consier resolving this issue by linearising many parallel linear processes simultaneously, instead of spending time on improving the alphabet reduction.

dining5.mcrl2.txt