I decided to reproduce the following model from the uppaal SMC tutorial
When I check its syntax using UPPAAL (5.1.0-beta3) I run into the error "Wrong number of process locations" I already isolated the process errors and I noticed that if I remove the clientSpawner from the system, it works.
Error stack trace:
java.lang.NullPointerException: Cannot invoke "com.uppaal.engine.protocol.viewmodel.GenericResponse.getResponse()" because "res" is null
at com.uppaal.engine.protocol.JsonProtocol.getGenericResponse(JsonProtocol.java:449)
at com.uppaal.engine.protocol.JsonProtocol.getConcreteSuccessor(JsonProtocol.java:486)
at com.uppaal.engine.EngineStub.getConcreteSuccessor(EngineStub.java:355)
at com.uppaal.engine.Engine$3.run(Engine.java:304)
at com.uppaal.engine.Engine$3.run(Engine.java:299)
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:833)
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.submit(Engine.java:631)
at com.uppaal.engine.Engine.getConcreteSuccessor(Engine.java:299)
at com.uppaal.engine.Engine.getConcreteSuccessor(Engine.java:320)
at hK.b(Unknown Source)
at hK.a(Unknown Source)
at java.desktop/javax.swing.DefaultListSelectionModel.fireValueChanged(DefaultListSelectionModel.java:224)
at java.desktop/javax.swing.DefaultListSelectionModel.fireValueChanged(DefaultListSelectionModel.java:204)
at java.desktop/javax.swing.DefaultListSelectionModel.fireValueChanged(DefaultListSelectionModel.java:251)
at java.desktop/javax.swing.DefaultListSelectionModel.changeSelection(DefaultListSelectionModel.java:448)
at java.desktop/javax.swing.DefaultListSelectionModel.changeSelection(DefaultListSelectionModel.java:458)
at java.desktop/javax.swing.DefaultListSelectionModel.setSelectionInterval(DefaultListSelectionModel.java:502)
at java.desktop/javax.swing.JList.setSelectedIndex(JList.java:2232)
at hs.b(Unknown Source)
at hv.intervalAdded(Unknown Source)
at java.desktop/javax.swing.AbstractListModel.fireIntervalAdded(AbstractListModel.java:157)
at hJ.a(Unknown Source)
at hI.a(Unknown Source)
at java.desktop/java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:318)
at java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:771)
at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:722)
at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:716)
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:741)
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)
These are my global declarations
// Place global declarations here.
const int CLIENTS = 5;
typedef int[0,CLIENTS-1] clientid_t;
broadcast chan ack[clientid_t], req[clientid_t], term[clientid_t];
clientid_t c;
dynamic Client(int id);
This is the ClientSpawner model
This is the Client Model
This is the Server Model
The only variables missing from global declarations are x and next and they are defined in the local declaration according to its usage
This is the system declaration
// Place template instantiations here.
server = Server();
clientSpawner = ClientSpawner();
// List one or more processes to be composed into a system.
system server, clientSpawner;
Does anyone know how to solve this?
I tried it in uppaal 5.0.0 as well. Same problem
I tried removing clientSpawner from the model and the syntax is correct