| Summary: | Clocks on urgent edge: Simulator does not notify on error | ||
|---|---|---|---|
| Product: | UPPAAL Stratego | Reporter: | Martin Kristjansen <mk> |
| Component: | GUI | Assignee: | Marius Mikučionis <marius> |
| Status: | ASSIGNED --- | ||
| Severity: | normal | ||
| Priority: | P5 | ||
| Version: | unspecified | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| Architecture: | |||
| Attachments: |
Model with clock guard on urgent edge
mixed guard crashes simulator |
||
Created attachment 347 [details]
mixed guard crashes simulator
the issue is not specific to urgent/broadcast. the problem is in engine simulator code where it tries to determine if system has any urgent transitions enabled and crashes upon clock guard as it does not have the symbolic state context (only the discrete). transfered to github: https://github.com/UPPAALModelChecker/UPPAAL-Meta/issues/14 |
Created attachment 346 [details] Model with clock guard on urgent edge I am running the uppaal64-4.1.20-stratego-8-beta3. I have a model, where there is a clock guard on a edge with an urgent transition. I know this is not allowed, and verifyta gives a correct message on the form: ` [warning] Clock guards are not allowed on urgent edges.` In the simulator, however, a JSON exception is given when (I think) the bad transition is evaluated in the simulator. The exception is `Expected "START_OBJECT", got "EOF"`. From the command line the stack trace is: Expected "START_OBJECT", got "EOF" at com.uppaal.engine.protocol.JsonMessageParser.expectNullableJsonToken(JsonMessageParser.java:274) at com.uppaal.engine.protocol.JsonMessageParser.visitObject(JsonMessageParser.java:136) at com.uppaal.engine.protocol.JsonProtocol.getGenericResponse(JsonProtocol.java:432) at com.uppaal.engine.protocol.JsonProtocol.getTransitions(JsonProtocol.java:105) at com.uppaal.engine.EngineStub.getTransitions(EngineStub.java:687) at com.uppaal.engine.Engine.getTransitions(Engine.java:290) at on.gU.run(Unknown Source) I have attached a model (of Multi-Core Rate-Monotic scheduling), which can be used to reproduce the error. Go into the simulator, press random, and when the last task instance is to go from its initial location, the exception is thrown.