Properties Verification of PTA

[Dong Yuanfa]

Hi, could you help me?

Can PRISM perform PTCTL requirement specification verification? If so, how can the PTCTL specification z.P>o.95[(×≤3)U(z=8)] be represented by codes in PRISM, and how represent "z"?

[Dave Parker]

Hi Dong,

We don't support full PTCTL, but for this specific example it is
feasible because you just have a single formula clock z. You can achieve
this by adding another clock to your model, which is never used/reset. I
believe you will need to use the digital clocks engine since your
property includes references to the clocks in the target.

https://prismmodelchecker.org/manual/ConfiguringPRISM/ComputationEngines#pta

By the way, this forum is mainly for developer questions. It is better
to use the general one for this kind of question:

http://groups.google.com/group/prismmodelchecker

Best wishes,

Dave

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchecke...@googlegroups.com
> <mailto:prismmodelchecke...@googlegroups.com>.
> To view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker-dev/968b88b2-f1da-4892-979d-173e7ee5994bn%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker-dev/968b88b2-f1da-4892-979d-173e7ee5994bn%40googlegroups.com?utm_medium=email&utm_source=footer>.