When trying to port the midas project to Rodin 2.1.1, I encountered an out of memory error. (The max heap was about 1.8g -- the maximum with a 32bit jvm.) The model is admittedly big, but maybe it reveals an important bottleneck.
The project archive can be obtained from:
http://deploy-eprints.ecs.soton.ac.uk/84/1/MidasBundle.rar
The memory error occurred at 74% during building with the stack trace:
!ENTRY org.rodinp.core 4 4 2011-05-10 15:43:57.407
!MESSAGE while running tool org.eventb.core.autoPOM on /Midas/MidasMchR3.bpo
!STACK 0
java.lang.OutOfMemoryError: GC overhead limit exceeded
at java.util.Arrays.copyOf(Arrays.java:2734)
at java.util.Vector.ensureCapacityHelper(Vector.java:226)
at java.util.Vector.addElement(Vector.java:573)
at com.sun.org.apache.xml.internal.dtm.ref.sax2dtm.SAX2DTM2.startElement(SAX2DTM2.java:2168)
at com.sun.org.apache.xalan.internal.xsltc.dom.SAXImpl.startElement(SAXImpl.java:917)
at com.sun.org.apache.xerces.internal.parsers.AbstractSAXParser.startElement(AbstractSAXParser.java:501)
at com.sun.org.apache.xerces.internal.parsers.AbstractXMLDocumentParser.emptyElement(AbstractXMLDocumentParser.java:179)
at com.sun.org.apache.xerces.internal.impl.XMLNSDocumentScannerImpl.scanStartElement(XMLNSDocumentScannerImpl.java:377)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentFragmentScannerImpl$FragmentContentDriver.next(XMLDocumentFragmentScannerImpl.java:2755)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentScannerImpl.next(XMLDocumentScannerImpl.java:648)
at com.sun.org.apache.xerces.internal.impl.XMLNSDocumentScannerImpl.next(XMLNSDocumentScannerImpl.java:140)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentFragmentScannerImpl.scanDocument(XMLDocumentFragmentScannerImpl.java:511)
at com.sun.org.apache.xerces.internal.parsers.XML11Configuration.parse(XML11Configuration.java:808)
at com.sun.org.apache.xerces.internal.parsers.XML11Configuration.parse(XML11Configuration.java:737)
at com.sun.org.apache.xerces.internal.parsers.XMLParser.parse(XMLParser.java:119)
at com.sun.org.apache.xerces.internal.parsers.AbstractSAXParser.parse(AbstractSAXParser.java:1205)
at com.sun.org.apache.xalan.internal.xsltc.dom.XSLTCDTMManager.getDTM(XSLTCDTMManager.java:440)
at com.sun.org.apache.xalan.internal.xsltc.dom.XSLTCDTMManager.getDTM(XSLTCDTMManager.java:234)
at com.sun.org.apache.xalan.internal.xsltc.trax.TransformerImpl.getDOM(TransformerImpl.java:524)
at com.sun.org.apache.xalan.internal.xsltc.trax.TransformerImpl.transform(TransformerImpl.java:709)
at com.sun.org.apache.xalan.internal.xsltc.trax.TransformerImpl.transform(TransformerImpl.java:313)
at org.rodinp.internal.core.version.Converter.computeConversion(Unknown Source)
at org.rodinp.internal.core.version.Converter.convert(Unknown Source)
at org.rodinp.internal.core.version.ConversionEntry.upgrade(Unknown Source)
at org.rodinp.internal.core.Buffer.attemptUpgrade(Unknown Source)
at org.rodinp.internal.core.Buffer.load(Unknown Source)
at org.rodinp.internal.core.RodinFileElementInfo.parseFile(Unknown Source)
at org.rodinp.internal.core.RodinFile.buildStructure(Unknown Source)
at org.rodinp.internal.core.Openable.generateInfos(Unknown Source)
at org.rodinp.internal.core.Openable.openWhenClosed(Unknown Source)
at org.rodinp.internal.core.Openable.getElementInfo(Unknown Source)
at org.rodinp.internal.core.Openable.getElementInfo(Unknown Source)
I'm surprised of this error because I could build (with auto prover) this project with -Xmx1512m, and the heap never exceeded 1462 Mo (well, the GC was running very often while loading the largest proof files, but eventually the build succeeded without memory errors). Tested with Rodin 2.1.1 / Ubuntu 11.04.
In particular, the largest files are
54520 MidasRegMchB2C.bpr
52744 MidasMchR3.bpr
and the file conversion succeeded for both of them.
Which configuration are you running ?
By the way, there are many corrupted files in this project: the log shows hundreds of duplicate events.
Thanks for trying. I am running Ubuntu 10.04, 32 bit. Rodin 2.1.1. The heap was about 1.8g. The heap space also remained below 1500. I will try again. Maybe the bug cannot be reproduced.
I tried again with a fresh workspace. This time, I could build the project. If the problem comes up again, I let you know.