Cant Specify The Property On The Model , and Says Some Error Message .( BB84 Protocol)

[nepl...@gmail.com]

Hi , Group , 
I am Stuck in Modelling The BB84 algorithm and cant parse and build model , and cant either Specify the PCTL properties on it , So AnyBody Can Please help , 
I had Uploaded some File of the model and The Error Message in and as Screenshot .
Hoping for Quick Help ,

Regards 

Kushal Dhakal 

[Joachim Klein]

Hi,

> I am Stuck in Modelling The BB84 algorithm and cant parse and build
> model , and cant either Specify the PCTL properties on it , So AnyBody
> Can Please help ,
> I had Uploaded some File of the model and The Error Message in and as
> Screenshot .

Regarding the parsing / model building error:

You have to ensure that there is no potential overflow in the variables.
In the marked line, if nc=N, then the nc'=nc+1 will overflow. Depending
on what you want the model to do, you could either strengthen the guard:

(eve_state = 2) & (eve_bas = ch_bas) & (nc < N) -> ...

or ensure that the assignment does not overflow, but stays saturated at N:

... (nc' = min(N, nc+1))


Regarding the property editor: In that text field, you place the
property you would like to check, see
http://www.prismmodelchecker.org/manual/PropertySpecification/Introduction

So, for your model, guessing from the comments, you might be interested in

P[ F bob_state=6 ]
or
P[ F bob_state=7 ]


Cheers,
Joachim Klein