Why "com.uppaal.engine.EngineCrashException: Server received SIGABRT signal"?

[Lqs66]

When I load my large model into UPPAAL's verifier engine, I get the following error:

com.uppaal.engine.EngineCrashException: Server received SIGABRT signal
	at com.uppaal.engine.protocol.serializer.GenericResponseDeserializer.deserialize(GenericResponseDeserializer.java:34)
	at com.uppaal.engine.protocol.serializer.GenericResponseDeserializer.deserialize(GenericResponseDeserializer.java:19)
	at com.google.gson.internal.bind.TreeTypeAdapter.read(TreeTypeAdapter.java:69)
	at com.google.gson.Gson.fromJson(Gson.java:1058)
	at com.uppaal.engine.protocol.JsonMessageParser.parse(JsonMessageParser.java:70)
	at com.uppaal.engine.protocol.JsonProtocol.getGenericResponse(JsonProtocol.java:447)
	at com.uppaal.engine.protocol.JsonProtocol.getUploadResponse(JsonProtocol.java:177)
	at com.uppaal.engine.protocol.JsonProtocol.upload(JsonProtocol.java:195)
	at com.uppaal.engine.EngineStub.upload(EngineStub.java:448)
	at com.uppaal.engine.Engine$5.run(Engine.java:364)
	at com.uppaal.engine.Engine$5.run(Engine.java:360)
	at com.uppaal.engine.Engine.lambda$submit$8(Engine.java:654)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
	at java.base/java.lang.Thread.run(Thread.java:840)
Caused by: com.uppaal.engine.EngineInvocationException: Concurrent execution encountered an exception
	at com.uppaal.engine.Engine.submit(Engine.java:647)
	at com.uppaal.engine.Engine.submitLicenseLess(Engine.java:637)
	at com.uppaal.engine.Engine.getSystem(Engine.java:360)
	at aq.a(Unknown Source)
	at aq.h(Unknown Source)
	at iv.d(Unknown Source)
	at aM.stateChanged(Unknown Source)
	at java.desktop/javax.swing.JTabbedPane.fireStateChanged(JTabbedPane.java:444)
	at java.desktop/javax.swing.JTabbedPane$ModelListener.stateChanged(JTabbedPane.java:295)
	at java.desktop/javax.swing.DefaultSingleSelectionModel.fireStateChanged(DefaultSingleSelectionModel.java:148)
	at java.desktop/javax.swing.DefaultSingleSelectionModel.setSelectedIndex(DefaultSingleSelectionModel.java:79)
	at java.desktop/javax.swing.JTabbedPane.setSelectedIndexImpl(JTabbedPane.java:648)
	at java.desktop/javax.swing.JTabbedPane.setSelectedIndex(JTabbedPane.java:623)
	at java.desktop/javax.swing.plaf.basic.BasicTabbedPaneUI$Handler.mousePressed(BasicTabbedPaneUI.java:4101)
	at com.formdev.flatlaf.ui.FlatTabbedPaneUI$Handler.mousePressed(FlatTabbedPaneUI.java:2191)
	at java.desktop/java.awt.AWTEventMulticaster.mousePressed(AWTEventMulticaster.java:287)
	at java.desktop/java.awt.Component.processMouseEvent(Component.java:6623)
	at java.desktop/javax.swing.JComponent.processMouseEvent(JComponent.java:3389)
	at java.desktop/java.awt.Component.processEvent(Component.java:6391)
	at java.desktop/java.awt.Container.processEvent(Container.java:2266)
	at java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5001)
	at java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2324)
	at java.desktop/java.awt.Component.dispatchEvent(Component.java:4833)
	at java.desktop/java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4948)
	at java.desktop/java.awt.LightweightDispatcher.processMouseEvent(Container.java:4572)
	at java.desktop/java.awt.LightweightDispatcher.dispatchEvent(Container.java:4516)
	at java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2310)
	at java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2780)
	at java.desktop/java.awt.Component.dispatchEvent(Component.java:4833)
	at java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:775)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:720)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:714)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:399)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:86)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:97)
	at java.desktop/java.awt.EventQueue$5.run(EventQueue.java:747)
	at java.desktop/java.awt.EventQueue$5.run(EventQueue.java:745)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:399)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:86)
	at java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:744)
	at java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
	at java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)

I would like to know how to fix this problem?

Here is my model: model.zip

UPPAAL version is 5.0.0

[mikucionisaau]

I can open the model and there's nothing special, except that it tries to load a dynamic library, which is not attached...

Could it be that the issue is within the library?

I strongly suggest to have an independent (unit) test which uses the library: in such setting you can control all the build options, including sanitizers (-fsanitize=address), so you can easily check for memory issues.

[Lqs66]

This seems to be an issue with the Java GUI, when I use . /verifyta ~/Desktop/uppllvm/python/rtl.xml, my .so executes correctly.

But I have other problems:
/home/lqs66/Desktop/uppllvm/python/rtl.xml:/nta/template[1]/transition[5]/label[1]:1: [error] Guard must be side-effect free.

This seems to be caused by me setting the external function to guard.

[mikucionisaau]

I just noticed that the model has a process with name, which includes -1 -- that is not a valid name and UPPAAL-5.0 issues errors on it (apart from missing library).

[Lqs66]

I just noticed that the model has a process with name, which includes -1 -- that is not a valid name and UPPAAL-5.0 issues errors on it (apart from missing library).

Thanks for the correction, I fixed the problem.