asa-ga4.pml

mtype { LOAD_TASK, TASK_READY, TASK_COMPLETE, HELO_CLIENT, START_CAPABILITY, CAPABILITY_INPUT, CAPABILITY_OUTPUT, CAPABILITY_COMPLETE };
mtype { READY, COMPLETE };
chan taskBus = [128] of { mtype };

active proctype TaskClient() {
	taskBus ! LOAD_TASK;
	if
		:: taskBus ? TASK_READY -> 
			taskBus ? HELO_CLIENT;
		:: taskBus ? HELO_CLIENT ->
			taskBus ? TASK_READY;
			assert(0);
	fi;
	taskBus ! START_CAPABILITY;
	taskBus ! CAPABILITY_INPUT;
	taskBus ? CAPABILITY_OUTPUT;
	taskBus ? CAPABILITY_COMPLETE;
	taskBus ? TASK_COMPLETE;
}

active proctype TaskManager() {
	chan observer = [0] of {mtype};
	do
	::
		taskBus ? LOAD_TASK;
		run TaskExecutor(observer);
		observer ? READY;
		observer ? COMPLETE;
		taskBus ! TASK_COMPLETE;
	od;
}

proctype TaskExecutor(chan observer) {
	run ScriptTaskStrategy(observer)
}

proctype ScriptTaskStrategy(chan observer) {
	observer ! READY;
	run Capability();
	observer ! COMPLETE;
}

proctype Capability() {
	taskBus ! HELO_CLIENT;
	taskBus ? START_CAPABILITY;
	taskBus ? CAPABILITY_INPUT;
	taskBus ! CAPABILITY_OUTPUT;
	taskBus ! CAPABILITY_COMPLETE;
}