Is Time Cumulative?

[Valdivino Santiago]

Hello all,

I have the following .props file (a piece of it):

const double T;

// Label: 1 - 0

label "a_1" = (o = 1) & (g = 0);

label "b_1" = (o = 1) & (g = 1);

...

// Label: 12 - 11

label "a_12" = (o = 12) & (g = 11);

label "b_12" = (o = 12) & (g = 12);

...

And I have these properties:

filter(avg, P=? [ "a_1" U<=T "b_1"], o = 1)

filter(avg, P=? [ "a_12" U<=T "b_12"], o = 12)

We see that I want to get the avg probabilities of all states that satisfy o = 1 (o = 12). These are my states from where I want to make my analysis. I set T = 500. The point is that avg probabilities are much more higher in the first case (o = 1) than in the second case (o = 12). 

The question is this: is T cumulative? I mean, when evaluating the properties, and in this way I defined the properties, PRISM considers T as cumulative (since the (single) initial state of the model)? I wish that T is computed from the states that satisfy  o = 1 (o = 12).

Any hints?

Thank you.

Valdivino, 

[Gethin Norman]

Valdivino,

what prism is returning is the probabilities of reaching the goal within T time units when starting from the states specified in the filter and not from the initial state. So you are getting the probabilities you want.

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 http://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

[Valdivino Santiago]

Thanks Gethin.

Best

Valdivino.