/* Promela specification for problem rw21 */

mtype = { synch };

bit call__writeWork = 0;
bit callstartwrite = 0;
bit callstopwrite = 0;
bit callwriteWork = 0;


chan writer__1_read__write__control_start__write = [0] of { byte };
chan writer__1_read__write__control_stop__write = [0] of { byte };
chan reader__1_read__write__control_start__read = [0] of { byte };
chan reader__2_read__write__control_start__read = [0] of { byte };
chan reader__1_read__write__control_stop__read = [0] of { byte };
chan reader__2_read__write__control_stop__read = [0] of { byte };

proctype writer__1()
{
state_1:
  if
  :: atomic { writer__1_read__write__control_start__write!synch } -> goto state_2
  fi;
state_2:
  if
  :: atomic { skip;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 1 } -> goto state_3
  fi;
state_3:
  if
  :: atomic { skip;
              call__writeWork = 1;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_4
  fi;
state_4:
  if
  :: atomic { skip;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_5
  fi;
state_5:
  if
  :: atomic { writer__1_read__write__control_stop__write!synch } -> goto state_1
  fi
}

proctype reader__2()
{
state_1:
  if
  :: atomic { reader__2_read__write__control_start__read!synch } -> goto state_2
  fi;
state_2:
  if
  :: atomic { reader__2_read__write__control_stop__read!synch } -> goto state_1
  fi
}

proctype reader__1()
{
state_1:
  if
  :: atomic { reader__1_read__write__control_start__read!synch } -> goto state_2
  fi;
state_2:
  if
  :: atomic { reader__1_read__write__control_stop__read!synch } -> goto state_1
  fi
}

proctype read__write__control()
{
state_1:
  if
  :: atomic { writer__1_read__write__control_start__write?synch;
              call__writeWork = 0;
              callstartwrite = 1;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_2
  fi;
state_2:
  if
  :: atomic { writer__1_read__write__control_stop__write?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 1;
              callwriteWork = 0 } -> goto state_3
  fi;
state_3:
  if
  :: atomic { writer__1_read__write__control_stop__write?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 1;
              callwriteWork = 0 } -> goto state_3
  :: atomic { writer__1_read__write__control_start__write?synch;
              call__writeWork = 0;
              callstartwrite = 1;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_10
  :: atomic { reader__2_read__write__control_stop__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_8
  :: atomic { reader__1_read__write__control_stop__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_8
  :: atomic { reader__2_read__write__control_start__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_4
  :: atomic { reader__1_read__write__control_start__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_4
  fi;
state_4:
  if
  :: atomic { writer__1_read__write__control_stop__write?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 1;
              callwriteWork = 0 } -> goto state_4
  :: atomic { reader__2_read__write__control_stop__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_3
  :: atomic { reader__1_read__write__control_stop__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_3
  :: atomic { reader__2_read__write__control_start__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_5
  :: atomic { reader__1_read__write__control_start__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_5
  fi;
state_5:
  if
  :: atomic { writer__1_read__write__control_stop__write?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 1;
              callwriteWork = 0 } -> goto state_5
  :: atomic { reader__2_read__write__control_stop__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_4
  :: atomic { reader__1_read__write__control_stop__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_4
  :: atomic { reader__2_read__write__control_start__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_6
  :: atomic { reader__1_read__write__control_start__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_6
  fi;
state_6:
  if
  :: atomic { skip;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto endstate_9
  fi;
state_8:
  if
  :: atomic { skip;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto endstate_9
  fi;
endstate_9:
  0;
state_10:
  if
  :: atomic { writer__1_read__write__control_stop__write?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 1;
              callwriteWork = 0 } -> goto state_3
  :: atomic { reader__2_read__write__control_stop__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_11
  :: atomic { reader__1_read__write__control_stop__read?synch;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto state_11
  fi;
state_11:
  if
  :: atomic { skip;
              call__writeWork = 0;
              callstartwrite = 0;
              callstopwrite = 0;
              callwriteWork = 0 } -> goto endstate_9
  fi
}

init {
  atomic { run writer__1();
    run reader__2();
    run reader__1();
    run read__write__control()
  }
}

/* activereaders0 = 
(IN-TASK READ_WRITE_CONTROL (= ACTIVEREADERS 0)) 
*/
#define activereaders0 (read__write__control[4]@state_11 \
    || read__write__control[4]@state_10 \
    || read__write__control[4]@endstate_9 \
    || read__write__control[4]@state_8 \
    || read__write__control[4]@state_6 \
    || read__write__control[4]@state_3 \
    || read__write__control[4]@state_2 \
    || read__write__control[4]@state_1)

/* writerpresentfalse = 
(IN-TASK READ_WRITE_CONTROL (= WRITERPRESENT NIL)) 
*/
#define writerpresentfalse (read__write__control[4]@state_11 \
    || read__write__control[4]@endstate_9 \
    || read__write__control[4]@state_8 \
    || read__write__control[4]@state_6 \
    || read__write__control[4]@state_5 \
    || read__write__control[4]@state_4 \
    || read__write__control[4]@state_3 \
    || read__write__control[4]@state_2 \
    || read__write__control[4]@state_1)