Rubinstein protocol

[UR]

Hi 

I am trying to execute the code for "Rubinstein protocol" at:

http://www.prismmodelchecker.org/casestudies/examples/negotiation.pm

but while verifying the property:

P=? [true U s=2  & b=3 & (bid=2 | cbid=10500)]

it throws me an error, it seems the code has some issues, according to prism there is some problem with: line 72, column 9, 10th command of buyer module. 

Can anyone help fixing the issue, and identifying what are the columns? and how to tighten the guard?

Thanks,

UR

[Gethin Norman]

I have had a look at the model and the problem was that the variables td and ts could go out of range when incremented. I have updated the model file (by strengthening the relevant guards) so this can no longer happen. (If you are interested I have updated the guards on lines 72, 74, 169 and 171).

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.

[UR]

Gethin,

Thanks for the correction. It executes without any error. But now the problem is the regeneration of the results, I am trying to regenerate the results and see how Acceptance probability  will vary with the variation of PVAL, by varying the value of PVAL \in [10000-11000] as mentioned in the following property:

P = ? [ true U s=2 & b=3 & (bid=PVAL | cbid=PVAL)]

but the result which I am getting are no where near the graph. What am I doing wrong ? any thoughts? 

Another thing, please correct me if I am wrong, Lin(10) means linear strategy when the gradient (means change in the value of Bid/CBid) is unit 10.

Any thought how to regenerate the graph in "Linear strategies: Slow is better than Fast" section? Are they generated in Prism?

I will be thankful for the help.

UR