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
Depends on:
Reported: 2011-04-11 11:04 CEST by Petr Bulychev
Modified: 2011-04-11 11:34 CEST (History)
2 users (show)

See Also:

query (144 bytes, application/octet-stream)
2011-04-11 11:05 CEST, Petr Bulychev
model (700 bytes, text/xml)
2011-04-11 11:05 CEST, Petr Bulychev
screenshot (49.72 KB, image/png)
2011-04-11 11:06 CEST, Petr Bulychev

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: [] Clock rate(54) must be 0 or 1.
        at com.uppaal.engine.Parser.parseProlog(
        at com.uppaal.engine.Parser.parseInitial(
        at com.uppaal.engine.DotProtocol.getInitial(
        at com.uppaal.engine.EngineStub.getInitial(
        at com.uppaal.engine.Engine.getSystem(
        at com.uppaal.gui.SystemInspector.a(Unknown Source)
        at com.uppaal.gui.verifier.Verification.a(Unknown Source)
        at Source)
        at java.util.concurrent.ThreadPoolExecutor.runWorker(
        at java.util.concurrent.ThreadPoolExecutor$
Comment 1 Petr Bulychev 2011-04-11 11:05:14 CEST
Created attachment 237 [details]
Comment 2 Petr Bulychev 2011-04-11 11:05:31 CEST
Created attachment 238 [details]
Comment 3 Petr Bulychev 2011-04-11 11:06:43 CEST
Created attachment 239 [details]
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).