-- SMV for problem: rw21 MODULE main VAR writer__1 : { s1 , s2 , s3 , s4 , s5 }; call__writeWork : boolean; callstartwrite : boolean; callstopwrite : boolean; callwriteWork : boolean; reader__2 : { s1 , s2 }; reader__1 : { s1 , s2 }; read__write__control : { s1 , s2 , s3 , s4 , s5 , s6 , s8 , s9 , s10 , s11 }; INIT ( ( writer__1 = s1 ) & ( call__writeWork = 0 ) & ( callstartwrite = 0 ) & ( callstopwrite = 0 ) & ( callwriteWork = 0 ) & ( reader__2 = s1 ) & ( reader__1 = s1 ) & ( read__write__control = s1 ) ) TRANS ( ( ( writer__1 = s2 ) & ( next(writer__1) = s3 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 1 ) & unchanged_except_writer__1 ) | ( ( writer__1 = s3 ) & ( next(writer__1) = s4 ) & ( next(call__writeWork) = 1 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_writer__1 ) | ( ( writer__1 = s4 ) & ( next(writer__1) = s5 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_writer__1 ) | ( ( ( read__write__control = s1 ) & ( next(read__write__control) = s2 ) & ( writer__1 = s1 ) & ( next(writer__1) = s2 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 1 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_writer__1 ) ) | ( ( ( read__write__control = s2 ) & ( next(read__write__control) = s3 ) & ( writer__1 = s5 ) & ( next(writer__1) = s1 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 1 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_writer__1 ) ) | ( ( ( read__write__control = s3 ) & ( next(read__write__control) = s3 ) & ( writer__1 = s5 ) & ( next(writer__1) = s1 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 1 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_writer__1 ) ) | ( ( ( read__write__control = s3 ) & ( next(read__write__control) = s10 ) & ( writer__1 = s1 ) & ( next(writer__1) = s2 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 1 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_writer__1 ) ) | ( ( ( read__write__control = s3 ) & ( next(read__write__control) = s8 ) & ( reader__2 = s2 ) & ( next(reader__2) = s1 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__2 ) ) | ( ( ( read__write__control = s3 ) & ( next(read__write__control) = s8 ) & ( reader__1 = s2 ) & ( next(reader__1) = s1 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__1 ) ) | ( ( ( read__write__control = s3 ) & ( next(read__write__control) = s4 ) & ( reader__2 = s1 ) & ( next(reader__2) = s2 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__2 ) ) | ( ( ( read__write__control = s3 ) & ( next(read__write__control) = s4 ) & ( reader__1 = s1 ) & ( next(reader__1) = s2 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__1 ) ) | ( ( ( read__write__control = s4 ) & ( next(read__write__control) = s4 ) & ( writer__1 = s5 ) & ( next(writer__1) = s1 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 1 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_writer__1 ) ) | ( ( ( read__write__control = s4 ) & ( next(read__write__control) = s3 ) & ( reader__2 = s2 ) & ( next(reader__2) = s1 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__2 ) ) | ( ( ( read__write__control = s4 ) & ( next(read__write__control) = s3 ) & ( reader__1 = s2 ) & ( next(reader__1) = s1 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__1 ) ) | ( ( ( read__write__control = s4 ) & ( next(read__write__control) = s5 ) & ( reader__2 = s1 ) & ( next(reader__2) = s2 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__2 ) ) | ( ( ( read__write__control = s4 ) & ( next(read__write__control) = s5 ) & ( reader__1 = s1 ) & ( next(reader__1) = s2 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__1 ) ) | ( ( ( read__write__control = s5 ) & ( next(read__write__control) = s5 ) & ( writer__1 = s5 ) & ( next(writer__1) = s1 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 1 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_writer__1 ) ) | ( ( ( read__write__control = s5 ) & ( next(read__write__control) = s4 ) & ( reader__2 = s2 ) & ( next(reader__2) = s1 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__2 ) ) | ( ( ( read__write__control = s5 ) & ( next(read__write__control) = s4 ) & ( reader__1 = s2 ) & ( next(reader__1) = s1 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__1 ) ) | ( ( ( read__write__control = s5 ) & ( next(read__write__control) = s6 ) & ( reader__2 = s1 ) & ( next(reader__2) = s2 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__2 ) ) | ( ( ( read__write__control = s5 ) & ( next(read__write__control) = s6 ) & ( reader__1 = s1 ) & ( next(reader__1) = s2 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__1 ) ) | ( ( read__write__control = s6 ) & ( next(read__write__control) = s9 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control ) | ( ( read__write__control = s8 ) & ( next(read__write__control) = s9 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control ) | ( ( ( read__write__control = s10 ) & ( next(read__write__control) = s3 ) & ( writer__1 = s5 ) & ( next(writer__1) = s1 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 1 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_writer__1 ) ) | ( ( ( read__write__control = s10 ) & ( next(read__write__control) = s11 ) & ( reader__2 = s2 ) & ( next(reader__2) = s1 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__2 ) ) | ( ( ( read__write__control = s10 ) & ( next(read__write__control) = s11 ) & ( reader__1 = s2 ) & ( next(reader__1) = s1 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control_reader__1 ) ) | ( ( read__write__control = s11 ) & ( next(read__write__control) = s9 ) & ( next(call__writeWork) = 0 ) & ( next(callstartwrite) = 0 ) & ( next(callstopwrite) = 0 ) & ( next(callwriteWork) = 0 ) & unchanged_except_read__write__control ) ) DEFINE Idle := 0; writer__1_enabled := ( ( ( writer__1 = s5 ) & ( ( ( read__write__control = s10 ) | ( read__write__control = s5 ) | ( read__write__control = s4 ) | ( read__write__control = s3 ) | ( read__write__control = s2 ) ) ) ) | ( ( writer__1 = s4 ) & ( 1 ) ) | ( ( writer__1 = s3 ) & ( 1 ) ) | ( ( writer__1 = s2 ) & ( 1 ) ) | ( ( writer__1 = s1 ) & ( ( ( read__write__control = s3 ) | ( read__write__control = s1 ) ) ) ) ) ; reader__2_enabled := ( ( ( reader__2 = s2 ) & ( ( ( read__write__control = s10 ) | ( read__write__control = s5 ) | ( read__write__control = s4 ) | ( read__write__control = s3 ) ) ) ) | ( ( reader__2 = s1 ) & ( ( ( read__write__control = s5 ) | ( read__write__control = s4 ) | ( read__write__control = s3 ) ) ) ) ) ; reader__1_enabled := ( ( ( reader__1 = s2 ) & ( ( ( read__write__control = s10 ) | ( read__write__control = s5 ) | ( read__write__control = s4 ) | ( read__write__control = s3 ) ) ) ) | ( ( reader__1 = s1 ) & ( ( ( read__write__control = s5 ) | ( read__write__control = s4 ) | ( read__write__control = s3 ) ) ) ) ) ; read__write__control_enabled := ( ( ( read__write__control = s11 ) & ( 1 ) ) | ( ( read__write__control = s10 ) & ( ( ( reader__1 = s2 ) ) | ( ( reader__2 = s2 ) ) | ( ( writer__1 = s5 ) ) ) ) | ( ( read__write__control = s8 ) & ( 1 ) ) | ( ( read__write__control = s6 ) & ( 1 ) ) | ( ( read__write__control = s5 ) & ( ( ( reader__1 = s1 ) ) | ( ( reader__2 = s1 ) ) | ( ( reader__1 = s2 ) ) | ( ( reader__2 = s2 ) ) | ( ( writer__1 = s5 ) ) ) ) | ( ( read__write__control = s4 ) & ( ( ( reader__1 = s1 ) ) | ( ( reader__2 = s1 ) ) | ( ( reader__1 = s2 ) ) | ( ( reader__2 = s2 ) ) | ( ( writer__1 = s5 ) ) ) ) | ( ( read__write__control = s3 ) & ( ( ( reader__1 = s1 ) ) | ( ( reader__2 = s1 ) ) | ( ( reader__1 = s2 ) ) | ( ( reader__2 = s2 ) ) | ( ( writer__1 = s1 ) ) | ( ( writer__1 = s5 ) ) ) ) | ( ( read__write__control = s2 ) & ( ( ( writer__1 = s5 ) ) ) ) | ( ( read__write__control = s1 ) & ( ( ( writer__1 = s1 ) ) ) ) ) ; unchanged_except_read__write__control := ( ( writer__1 = next(writer__1) ) & ( reader__2 = next(reader__2) ) & ( reader__1 = next(reader__1) ) ) ; unchanged_except_read__write__control_reader__1 := ( ( writer__1 = next(writer__1) ) & ( reader__2 = next(reader__2) ) ) ; unchanged_except_read__write__control_reader__2 := ( ( writer__1 = next(writer__1) ) & ( reader__1 = next(reader__1) ) ) ; unchanged_except_read__write__control_writer__1 := ( ( reader__2 = next(reader__2) ) & ( reader__1 = next(reader__1) ) ) ; unchanged_except_writer__1 := ( ( reader__2 = next(reader__2) ) & ( reader__1 = next(reader__1) ) & ( read__write__control = next(read__write__control) ) ) ; -- -- (IN-TASK READ_WRITE_CONTROL (= ACTIVEREADERS 0)) activereaders0 := ( ( read__write__control = s11 ) | ( read__write__control = s10 ) | ( read__write__control = s9 ) | ( read__write__control = s8 ) | ( read__write__control = s6 ) | ( read__write__control = s3 ) | ( read__write__control = s2 ) | ( read__write__control = s1 ) ); -- -- (IN-TASK READ_WRITE_CONTROL (= WRITERPRESENT NIL)) writerpresentfalse := ( ( read__write__control = s11 ) | ( read__write__control = s9 ) | ( read__write__control = s8 ) | ( read__write__control = s6 ) | ( read__write__control = s5 ) | ( read__write__control = s4 ) | ( read__write__control = s3 ) | ( read__write__control = s2 ) | ( read__write__control = s1 ) ); -- -- (AFTER "internal(writer_1;call_writeWork)") call__writeWork_def := ( ( next(writer__1) = s4 ) ); -- -- (AFTER "call(writer_1;read_write_control.start_write)") callstartwrite_def := ( ( next(writer__1) = s2 ) ); -- -- (AFTER "call(writer_1;read_write_control.stop_write)") callstopwrite_def := ( ( next(writer__1) = s1 ) ); -- -- (AFTER "internal(writer_1;callwritework)") callwriteWork_def := ( ( next(writer__1) = s3 ) );