Problem with result regeneration of Rubinstein Protocol

[UR]

Hi 

I am trying to regenerate the results for the case "Rubinstein protocol" but I am facing couple of confusions:

 http://www.prismmodelchecker.org/casestudies/negotiation.php

by verifying the property P = ? [ true U s=2 & b=3 & (bid=PVAL | cbid=PVAL)], and varying the value of PVAL in interval [10000,11000]

with offset: 10^4, and using Lin(10)-Lin(10), which perhaps means Buyer Conceder increment to be 10, and Seller Conceder decrement to be 10

(Please correct me if I am wrong). The result I am getting are very strange. According to the information mentioned in case study page and main article, the result should be as in "figure1.png" for Acceptance Probability. Whereas the result I am getting are in different (please see the rest of the attachments). I have changed the values of time limit mostly which are mentioned in the figures. 

My questions are where am I wrong?

Is the main figure (figure1) generated in prism?, if yes how to regenerate it? 

What is Acceptance Cumulative Probability? are the figures related to it are generated using simulation mode or verification?

I would really appreciate a detailed answer.

Thanks,

UR

[Gethin Norman]

This is an external case study from the paper:

Paolo Ballarini, Michael Fisher and Michael Wooldridge.
Automated Game Analysis via Probabilistic Model Checking: A Case Study.
In Proc. 3rd Workshop on Model Checking and Artificial Intelligence (MoChArt'05), volume 149 of ENTCS, pages 125-137,
Elsevier. February 2006.

So unfortunately I do not know very much about the case study, and therefore cannot give detailed answers.

I would expect that Paolo did the modelling and analysis so you could try contacting him (see https://sites.google.com/site/pballarini/), however this is a long time ago.

For information the figure was generated by Matlab and not prism. However, this does not mean the results were generated by prism. Matlab has much better graph drawing capabilities (particularly back in 2006 when this case study was performed) and we have often used Matlab for drawing graphs from results generated by prism.

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.
> <figure1.png><boulware500-960><boulware400-480-2><boulware400-480><default values>