This is a simple protocol that uses probabilistic broadcast to send information in a network. This model defines nodes that will forward a received message to their neighbour with probability psend and ignore the message with probability 1-psend. The model is initialized with the node 0 receiving the message.
These models were taken from the Prism case studies here.
Network configuration with 9 nodes
Download Probabilistic_Broadcast.plasma
The properties we checked was with what propability does a node receive a message. The variable active_i_ eventually becomes equal to 0 when the node_i_ receives the message.
Important!
F<=#1000 active0=0
F<=#1000 active1=0
F<=#1000 active2=0
F<=#1000 active3=0
F<=#1000 active4=0
F<=#1000 active5=0
F<=#1000 active6=0
F<=#1000 active7=0
F<=#1000 active8=0
Each one of the properties describe the event that a node will receive a message before 1000 simulations steps.
We added an optimization directive to one of the properties:
Important!
Optimize(psend = [0;1;0.2])This allowed us to check each of these properties for different values of psend, the probability of transmitting a message. We used the montecarlo algorithm with a parameter of 1000 simulations.
