controller.mli

node controller(distance: int) returns (obs, turning: bool; motor1, motor2, motor3, motor4, vel1, vel2, vel3, vel4, cont: int)
	contract 
		var
			rule: bool;
		let
            		rule = not obs & not turning or (turning & (motor1=1 & motor2=2 & motor3=1 & motor4=2));
		tel
			enforce rule
			with (c_move, c_motor1, c_motor2, c_motor3, c_motor4: bool)
		let
			obs = inlined obstacle(distance);
			(turning, cont) = inlined movement(c_move);
			(motor1, vel1) =  inlined motor(c_motor1);
			(motor2, vel2) =  inlined motor(c_motor2);
			(motor3, vel3) =  inlined motor(c_motor3);
			(motor4, vel4) =  inlined motor(c_motor4);
		tel