A forum for Spin users
You are not logged in.
Pages: 1
I want to flush channel c, i.e. remove all contents from c without reading it. What is the most effective (yielding smallest state space) way to do that?
Details:
I have a process that models powerOffs, which also reset channel c. Should the process (atomically) read from c until it is empty (as on page 373 of the spin book)? That way, xr c in another process is broken. Should I reinitialize channel c? Or is there some channel flush command I have not yet come across?
Offline
Thanks, that seems to be even better than the example on page 373 of the spin book.
However, now two processes are "reading" from channel c, so xr c in the original process that really reads c is causing problems:
spin: ./powerOffFailureModel.pml:15, Error: invalid use of 'else' combined with i/o and xr/xs assertions, statement separator near 'skip'
Is there no way to keep xr c for the special case that only one process is reading c and some other processes are completely flushing c?
Offline
the warning about the use of 'else' instead of len(c) == 0 or empty(c) is unrelated to the xr/xs issue of course.
isn't there a possibility to let the process that normally reads from the channel to do the flushing?
other than that, of you're sure things are otherwise consistent with xr/xs use, you can always compile with -DXUSAFE
which eliminates the checks for violations of xr/xs assumptions, but still enforces them in PO reduction....
Offline
Pages: 1