/*
	 * Formula As Typed: []  (callstartwrite -> <> (callstartread1 || callstartread2))
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !([]  (callstartwrite -> <> (callstartread1 || callstartread2)))
	 * (formalizing violations of the original)
	 */

never {    /* !([]  (callstartwrite -> <> (callstartread1 || callstartread2))) */
T0_init:
	if
	:: (1) -> goto T0_init
	:: (! ((callstartread1)) && ! ((callstartread2)) && (callstartwrite)) -> goto accept_S4
	fi;
accept_S4:
	if
	:: (! ((callstartread1)) && ! ((callstartread2))) -> goto T0_S4
	fi;
T0_S4:
	if
	:: (! ((callstartread1)) && ! ((callstartread2))) -> goto accept_S4
	fi;
accept_all:
	skip
}