/* Comes from BlueTooth Driver in Qadeer and Wu PLDI2004 paper.
   We made the record global.

   Use "concurinterproc prog.spl -thread T1 -guided true -analysis fbf":
   The combination of forward/backward/forward analysis isolates the
   problematic case.
*/

var
pendingIO:int,
stoppingFlag, stoppingEvent, stopped : bool
;

initial pendingIO==1 and not stoppingFlag and not stoppingEvent and not stopped;

proc BCSP_PnpAdd() returns ()
var status : bool;
begin
  status = BCSP_IoIncrement();
  if not status then
    if stopped then fail; endif;
  endif;
  BCSP_IoDecrement();
end

proc BCSP_PnpStop() returns ()
begin
  stoppingFlag = true;
  BCSP_IoDecrement();
  assume(stoppingEvent);
  stopped = true;
end

proc BCSP_IoIncrement() returns (status:bool)
begin
  if stoppingFlag then
    status = true;
  else
    pendingIO = pendingIO + 1;
    status = false;
  endif;
end

proc BCSP_IoDecrement() returns () 
var newpendingIO : int;
begin
  /* We simulate the atomic section differently */
  newpendingIO = pendingIO - 1;
  pendingIO = newpendingIO;
  if newpendingIO==0 then
    stoppingEvent = true;
  endif;
end

thread T0:
begin
  BCSP_PnpStop();
end

thread T1:
begin
  BCSP_PnpAdd();
end