Uppaal 5.1.0-beta3 Wrong Number of process locations

56 Views Asked by At

I decided to reproduce the following model from the uppaal SMC tutorial

tutorial print.

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

0

There are 0 best solutions below