Bluetooth Device discovery case study in PRISM

[Yanmei.Wang13]

Dear group member,
As for the Bluetooth Device Discovery i have TWO questions about the following situations:
1. i tried to change the values of initial condition of receiver like "init
receiver=0 & y1=0 & freq1=0 & train1=0 & // initial state of the receiver
rec=1 & // nothing received yet
f1=1 & t1=1 & // initial frequency of the receiver (based on its clock)
(send=1 |((freq=2)|(freq=4)|(freq=6)|(freq=8)|(freq=10)|(freq=12)|(freq=14)|(freq=16))) // condition required on the sender
endinit"
but the log tells me something like the following saying that i did not specify the exact one initial state. I really do not know how to change the code to set exact one state and also the property cheking code to check for stats distribution.

Model checking: P=? [ F rec=mrec {"init"} ]
Model constants: mrec=1,k=1,T=0

Building model...
Model constants: mrec=1,k=1,T=0

Computing reachable states...

Reachability (BFS): 3 iterations in 0.01 seconds (average 0.001667, setup 0.00)

Time for model construction: 15.984 seconds.

Type: DTMC
States: 1082130432 (536870912 initial)
Transitions: 1627389952

Transition matrix: 1610 nodes (3 terminal), 1627389952 minterms, vars: 52r/52c

Prob0: 1 iterations in 0.00 seconds (average 0.001000, setup 0.00)

Prob1: 1 iterations in 0.00 seconds (average 0.000000, setup 0.00)

yes = 1082130432, no = 0, maybe = 0

Error: Filter should be satisfied in exactly 1 state (but ""init"" is true in 536870912 states).

2. In the case study you provide graphs about the number of states distribution with change of time, i wonder how can i deduct this graph, i tried many ways but it seems that it did not work, can you please help me?
Thank you so much for your time.
Kris,
Sincerely

[Gethin Norman]

Kris,

1. In the property you are using the filter {“init”} over multiple initial states which therefore returns an error. You need to state which values you want (i.e. P=? [ F rec=mrec {"init”}{max} ] would return the max over all initial states). Filters have since been updated and for details on the current functionality see:

http://www.prismmodelchecker.org/manual/PropertySpecification/Filters

2. The graphs were not generated by PRISM. The graphs were complex to construct:

- first you need to output the values for all initial states (there are 17,179,869,184 initial states involving the analysis of 32 separate models)
- then you need to go through the values and count the number of each value (using a script in some programming language)
- finally use the counts to construct the graphs (using some graph plotting software)

This was done a very long time ago (in 2004), but I do remember Matlab was used for graph plotting.

I would just like to repeat: this is a very complex case study and required a detailed knowledge of 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 an 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.

[yanmei...@student.xjtlu.edu.cn]

Dear Gethin,

Thank you for your help Gethin, i adopted your advice and tried to set the initial state of receiver.

Question1: I will try all the possible combinations of t1=[0..1] and f1[1..16], are these 32 combinations in total the 32 separate DTMC models of whole initial states?

Question2: When i tried to set initial sate of receiver by changing states of receiver into 1 like receiver=1(listening on frequencies) & rec=0 and check property for max Rewards, PRISM returns a value of "Inifity", i do not quite understand.

Question3: I tried to set the initial frequency of receiver with f1=[1..16] & t1=[0..1] and for each combination i get a number of sate such as "f1=1 & t1=0 has state=3411945339", for property "init" ? R=? [F rec=mrec] :0, but i do not quite understand this, what does this mean?

Question 4: In the case study you mentioned "We compute the expected time for completion of the inquiry process, i.e. the time elapsed until the bound mrec on the number of replies heard by the sender has been met. We compute this for all 17,179,869,184 possible initial states. " the expected time for completion of the inquiry process can be computed, but the property checking can only get max or min time for mrec=1 or 2.., how can i calculate this expected time for inquiry process?

You also mentioned that we compute the expected time for all "17,179,869,184 possible initial states", does this mean that i should set different combinations of receiver's initial states can run them on PRISM for "17,179,869,184 " times ? Is this possible ?

Hope that you can correct my understanding if i was wrong, looking forward to your reply and many thanks.

  

在 2016年11月3日星期四 UTC+8上午4:06:00，Gethin Norman写道：