MODULE main

VAR

ready_to_produce : boolean;
ready_to_deliver : boolean;
buffer_filled : boolean;
buffer_empty : boolean;
ready_to_remove : boolean;
ready_to_consume : boolean;

ASSIGN

init(ready_to_produce) := 1;
next(ready_to_produce) :=
	case
		(ready_to_produce & !ready_to_deliver) : 0;
		(ready_to_deliver & buffer_empty & !ready_to_produce & !buffer_filled) : 1;
	esac;

init(ready_to_deliver) := 0;
next(ready_to_deliver) :=
	case
		(ready_to_deliver & buffer_empty & !ready_to_produce & !buffer_filled): 0;
		(ready_to_produce & !ready_to_deliver) : 1;
	esac;

init(buffer_filled) := 0;
next(buffer_filled) :=
	case
		(buffer_filled & ready_to_remove & !buffer_empty & !ready_to_consume) : 0;
		(ready_to_deliver & buffer_empty & !ready_to_produce & !buffer_filled) : 1;
	esac;

init(buffer_empty) := 1;
next(buffer_empty) :=
	case
		(ready_to_deliver & buffer_empty & !ready_to_produce & !buffer_filled) : 0;
		(buffer_filled & ready_to_remove & !buffer_empty & !ready_to_consume) : 1;
	esac;

init(ready_to_remove) := 1;
next(ready_to_remove) :=
	case
		(buffer_filled & ready_to_remove & !buffer_empty & !ready_to_consume) : 0;
		(ready_to_consume & !ready_to_remove) : 1;
	esac;

init(ready_to_consume) := 0;
next(ready_to_consume) :=
	case
		(ready_to_consume & !ready_to_remove) : 0;
		(buffer_filled & ready_to_remove & !buffer_empty & !ready_to_consume) : 1;
	esac;