Bug 512

Summary: "Clock rate(54) must be 0 or 1" error while doing SMC
Product: UPPAAL Reporter: Petr Bulychev <pbulychev>
Component: EngineAssignee: Alexandre David <adavid>
Status: NEW ---    
Severity: minor CC: marius, pbulychev
Priority: P2    
Version: unspecified   
Hardware: PC   
OS: Linux   
Architecture:
Attachments: query
model
screenshot

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).