/*
 * partial spin model, Timers
 * models only one active timer
 */

mtype = {start, stop, finish}

chan ctl = [0] of {mtype, chan};

proctype user()
{
	chan timer = [0] of {bit};

end:	do
	:: ctl!start(timer) ->
		if
		:: timer?1	/* timer expired */
		:: ctl!stop(timer)
		fi
	:: ctl!stop(timer)	/* stop inactive timer */
	:: ctl!finish(timer) -> break
	od
}
			
proctype timeproc(chan ticks; chan acks)
{
	chan t;
	
end: progress:	do
	:: ctl?start(t) ->
		if
		:: ticks?1 -> acks!1; t!1	/* timed out */
		:: ctl?stop(t)	/* caller stopped it */
		fi
	:: ctl?stop(t)	/* stopped inactive timer */
	:: ticks?1 ->
		acks!1	/* tick, no active timer */
	:: ctl?finish(t) ->
		break
	od;
	ticks?1;
	acks!0
}

proctype tickproc(chan ticks; chan acks)
{
end:	do
	:: ticks!1 ->
		if
		:: acks?0 -> break
		:: acks?1
		fi
	od
}

init
{
	chan ticks = [0] of {bit};
	chan acks = [0] of {bit};

	atomic {
		run tickproc(ticks, acks);
		run timeproc(ticks, acks);
		run user()
	}
}