car.mli

node obstacle(dist: int) returns (obs: bool)
let 
	automaton
		state OBSTACLE do
			obs = true;
			unless (dist > 45) then NO_OBSTACLE
		state NO_OBSTACLE do
			obs = false;
			unless (dist <= 45) then OBSTACLE
	end
tel

node motor(c: bool) returns (mode, velocity: int)
let 
	automaton
        	state FORWARD do
            		mode = 1;
            		velocity = 255;
            		unless not c then BACKWARD
        	state BACKWARD do
            		mode = 2;
            		velocity = 255;
            		unless c then FORWARD
    	end
tel

node movement(c: bool) returns (turning: bool; ombc:int)
	var last mbc:int = 0; 
let
	ombc = mbc;
	automaton
		state MOVING do
			mbc = 0;
			turning = false;			
			unless not c then STURNING
		state STURNING do
			mbc = 0;
			turning = true;
			until not c then TURNING | c then MOVING
		state TURNING do
			mbc = last mbc + 1;
			turning = true;
			unless c & (12 = last mbc) then STURNING
	end
tel

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=1 & motor3=2 & 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