ddefb

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

ddefb

#include <AFMotor.h>
#include "controller_controller.c"
#include "car.c"

AF_DCMotor motor1(1);
AF_DCMotor motor2(2);
AF_DCMotor motor3(3);
AF_DCMotor motor4(4);

int obs_sensor;

ddefb

$(SIGALI) < $(CONTRACT_PROG)_z3z/$(CONTRACT_NODE).z3z > /dev/null

ddefb

$./controller_sim

ddefb

SIM_PROG=car
SIM_NODE=controller
CONTRACT_NODE=controller

CONTRACT_PROG=$(SIM_PROG)

CC=gcc
HEPTC=heptc
HEPTS=hepts

ddefb

$(HEPTC) -target c -target z3z -s $(SIM_NODE) $(CONTRACT_PROG).ept

ddefb

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

ddefb

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

ddefb

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;

ddefb

source("jualib.R")

THINGSBOARD_SERVER = 'ip'
user = "username"
pass = "password"
station_name = "station_name"
keys = c('var_1', 'var_2', 'var_3')
start = "2000-01-01"
end = "2018-12-31"