This project is read-only.


issues with Maximum JVM heap size pref


There's a TLC preference called "Maximum JVM heap size..."

Seems it's the actual heap size, rather than the maximum. The description in overview-page.html also seems to suggest this.

Its default setting is 25%, which on my 8GB machine (when running the 32bit version) causes this error in the TLC console:

Error occurred during initialization of VM
Could not reserve enough space for 2058240KB object heap

I was further confused because this error only shows in the TLC console, and the "Model Checking Results" window doesn't indicate an error. This was my first attempt at running a model as i followed along in the hyperbook.

Reducing the setting to 10% and recreating my model I was able to continue.
Closed Oct 7, 2016 at 5:05 PM by mku


mku wrote May 5, 2015 at 5:22 PM


is there a reason why you use a 32bit Toolbox when your machine has 8GB of memory? Generally, you want to dedicate as much memory possible to the TLC process which is obviously only possible with a 64bit TLC.


dougma wrote May 6, 2015 at 12:52 PM

I just happened to download the 32bit Toolbox because I already had the 32bit JRE installed. I appreciate that the 64bit version is a better choice.