(defpredicate "callwriteWork" (after "internal(writer_1;callwritework)"))
(defpredicate "callstopwrite" (after "call(writer_1;read_write_control.stop_write)"))
(defpredicate "callstartwrite" (after "call(writer_1;read_write_control.start_write)"))
(defpredicate "callstartread2" (after "call(reader_2;read_write_control.start_read)"))
(defpredicate "callstartread1" (after "call(reader_1;read_write_control.start_read)"))

(defpredicate "writerpresentfalse" (in-task read_write_control (= writerpresent nil)))
(defpredicate "activereaders0" (in-task read_write_control (= activereaders 0)))