Spinroot

A forum for Spin users

You are not logged in.

#1 2018-05-09 13:51:27

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Most effective way to flush a channel

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

#2 2018-05-09 17:46:46

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Most effective way to flush a channel

d_step {
  do
  :: nempty(q) -> q?_,_    // assuming there are two fields per message
  :: else -> break
  od
  skip     // to avoid the jump out of the d_step
}

Offline

#3 2018-05-16 20:15:32

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Re: Most effective way to flush a channel

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

#4 2018-05-17 16:01:11

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Most effective way to flush a channel

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

Board footer

Powered by FluxBB