Error: Invalid upper bound <0.0 in time-bounded until formula.

[Fatma Gara]

Hello every body

When building my model, i have encountered this problem= Error: Invalid upper bound <0.0 in time-bounded until formula.

and when i check the manual i found that ." If type 7→ ctmc, and if the ‘Auto-time’ checkbox is not selected, the value described in the ‘Time’ field will be provided as a parameter to the simulator engine function. If the value is not a valid positive real number (> 0.0), an error will be given."

Can somebody help me?

Best regards

[Gethin Norman]

Fatima,

as the error states in one of the properties you are checking is a time bounded until formula where the bound is less than 0 which which is not feasible since time starts at 0.

thanks

Gethin

> --
> You received this message because you are subscribed to the Google Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchec...@googlegroups.com.
> To post to this group, send email to prismmod...@googlegroups.com.
> Visit this group at https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.