This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 512 - "Clock rate(54) must be 0 or 1" error while doing SMC
Summary: "Clock rate(54) must be 0 or 1" error while doing SMC
Status: NEW
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: PC Linux
: P2 minor
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2011-04-11 11:04 CEST by Petr Bulychev
Modified: 2011-04-11 11:34 CEST (History)
2 users (show)

See Also:
Architecture:

Attachments
query (144 bytes, application/octet-stream)
2011-04-11 11:05 CEST, Petr Bulychev 		Details
model (700 bytes, text/xml)
2011-04-11 11:05 CEST, Petr Bulychev 		Details
screenshot (49.72 KB, image/png)
2011-04-11 11:06 CEST, Petr Bulychev 		Details
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Description Petr Bulychev 2011-04-11 11:04:34 CEST 
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)
Comment 1 Petr Bulychev 2011-04-11 11:05:14 CEST 
Created attachment 237 [details]
query
Comment 2 Petr Bulychev 2011-04-11 11:05:31 CEST 
Created attachment 238 [details]
model
Comment 3 Petr Bulychev 2011-04-11 11:06:43 CEST 
Created attachment 239 [details]
screenshot
Comment 4 Marius Mikučionis 2011-04-11 11:34:37 CEST 
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).