Download APNN Description of the model.
Examples models for APNN-Toolbox
This Net is divided into two sections(Left-section (refered as l) and Right-section (refered as r)).Reader is on right side and Writer is on left side.
The algorithm uses three types of messages: 'requested' and 'returned' sent from the reader to the writer and
'granted' sent from the writer to the reader. After finishing the production of a new value along the quiescent
action a, the writer takes either a step via action b or one via action d, to reach its critical state, 'writing'.
A token on 'available' represents the previously written value which not has been read by the reader.
Action b or d may yield an updated value. A token on returned represents control over the shared variable 'returned'
from the reader to the writer, after the reader has read the previous value. Actions a and d then yield a new value.
Along the quiescent action h, the reader, after finishing the use of the previously read value, sends a request for
an updated value to the writer. Upon granting a new value along action e, the reader starts 'reading'. However,
it may happen that the reader remains stuck in its local state 'pending' forever:The writer either remains 'producing'
forever, or the writer produces infinitely many new values and neglects fairness for the action e.
The assumption of fairness would help in the later case.
Download APNN Description of the model.