mCRL2xi can be crashed with an incorrect specification

[gjveltink]

When trying to rewrite 'makeList(-1)' using the following specification within mCRL2xi the application crashes.

---

map
	makeList: Int -> List(Int);

var
	n: Int;

eqn
	% makeList(n) = if(n <= 0, [], makeList(n - 1) <| n);
	makeList(n) = if(n == 0, [], makeList(n - 1) <| n); % rewrite of 'makeList(-1)' crashes mCRL2xi 

---

Problem.mcrl2.txt

[mlaveaux]

When the rewrite system is infinite makeList(-1) ->* makeList(-2) ..., then all kinds of tools can crash due to running out of stack memory (or at some point main memory). In general this is not a recoverable operation although some tools such as the mcrl2ide divert the rewriting to another thread which might be able to avoid this situation.

[gjveltink]

Yes, I understand that mCRL2xi can crash with this specification, but I seem to remember, that it did not do so in the past. However, maybe I'm confusing this with the behaviour of mcrl2ide.

[gjveltink]

sorry, closed this inadvertently.

[mlaveaux]

For mcrl2ide we have only recently added the ability to rewrite data expressions, but from my testing it is at least somewhat robust against this case. Both cancelling the rewriting and letting it continue until it runs out of memory does not crash the mcrl2ide on my machine. I don't think mcrl2xi ever had the ability to not crash with (or abort) infinite rewrites.

[mlaveaux]

One discussion we had during the mCRL2 meeting is if it would be useful to remove mcrl2xi in favor of just having the mcrl2ide instead of adapting mcrl2xi for the next release. Would this be something that could work for you, or are there features in mcrl2ide that are missing for this to be a good alternative.

[gjveltink]

I have to admit, that up to now I was not aware of the fact that mcrl2ide now can rewrite data terms. I will try this out in class next week! The only thing that might be missing is the setting of (some of) the different options, that can be set in mcrl2xi.

[gjveltink]

OK, I have given it a try in mcrl2ide and have observed that, like in mcrl2xi before, I get a syntax error when the "init" clause is missing. :-(