How to avoid "Probably Zeno behaviour" error, when simulating untimed model for too long?

[AsgerHB]

I have a model that does not make use of clocks, which I want to run for a very long time.
When I exceed 100 000 discrete jumps, it errors out with the following message:

Probably Zeno behavior (infinitely many discrete transitions in finite amount of time):
Executed more than 100000 discrete transition while delaying only 0 time units.
State: ( Process._id0 ) acc=71#t(0)=0#time=0

The error message is correct in the sense that I perform a lot of discrete jumps without advancing any clocks, but in this instance I want to do so.

To quickly reproduce the issue, I have created this toy example:
coinflipper.zip

This query is fine:

/* OK */ E[#<=10000;1] (max: acc)

But this query causes an error:

/* Bad */ E[#<=100000;1] (max: acc)

Is there some sort of trick to avoid this error?

[thorulf4]

I don't know of any way to disable zeno checking. However if you do a delay beyond some non zero constant (default is 0.01) then you won't get zeno behaviour errors. I would recommend adding a clock x and forcing a delay of 1 during each toss of the coin.

With this modification I successfully ran with 100.000.000 steps

If these modifications are not applicable to your use case please let us know we might be able to figure something out.

[thorulf4]

You may also use rate of exponential instead of a clock x like so:

[mikucionisaau]

Perhaps we could add an option to specify the number of edge-transitions for Zeno detection?

Right now the bound hardcoded, but we could use a floating point number to encode it, and then the user may specify inf for infinity and effectively disable the Zeno detector.