| Summary: | "Clock rate(54) must be 0 or 1" error while doing SMC | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Petr Bulychev <pbulychev> |
| Component: | Engine | Assignee: | Alexandre David <adavid> |
| Status: | NEW --- | ||
| Severity: | minor | CC: | marius, pbulychev |
| Priority: | P2 | ||
| Version: | unspecified | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| Architecture: | |||
| Attachments: |
query
model screenshot |
||
Created attachment 237 [details]
query
Created attachment 238 [details]
model
Created attachment 239 [details]
screenshot
It looks like that some code that is not price-type aware is looking at the successors from the initial state and then it raises this problem. This issue is similar to the simulator. The work around is to declare an extra committed initial state which has an edge to the original initial state (so the priced-expression is not reachable directly from the initial state and the issue is not raised). |
I have a simple model (see attachment) and when I'm doing SMC I'm getting an error "Clock rate(54) must be 0 or 1" (see screenshot). The same error is shown when I just open a model in UPPAAL. When I got this error the first time (for large model) it has not been shown each time I'm doing SMC. But when I localized it it's shown each time I open the model in UPPAAL, do SMC or open the simulator tab. Here is the console output: ServerException: [Process._id0:Process.energy] Clock rate(54) must be 0 or 1. at com.uppaal.engine.Parser.parseProlog(Parser.java:38) at com.uppaal.engine.Parser.parseInitial(Parser.java:225) at com.uppaal.engine.DotProtocol.getInitial(DotProtocol.java:50) at com.uppaal.engine.EngineStub.getInitial(EngineStub.java:456) at com.uppaal.engine.Engine.getSystem(Engine.java:189) at com.uppaal.gui.SystemInspector.a(Unknown Source) at com.uppaal.gui.verifier.Verification.a(Unknown Source) at on.fH.run(Unknown Source) at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1110) at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:603) at java.lang.Thread.run(Thread.java:636)