% @ofmc(NO)
% TESTED FEATURES: LTL goals
% EXPECTED OUTCOME: Unsafe
specification LTLFinally_Unsafe
channel_model CCM

entity Env
{
	symbols
		prop, tick1, tick2, tick3 : fact;

	breakpoints { prop, tick1, tick2, tick3 }
	body {
		tick1;
		tick2;
		tick3;
	}

	goals
		g : <>(prop);
}