ddefb

$./controller_sim

ddefb

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

ddefb

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

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

SIM_PROG=car
SIM_NODE=controller
CONTRACT_NODE=controller

CONTRACT_PROG=$(SIM_PROG)

CC=gcc
HEPTC=heptc
HEPTS=hepts

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

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"

ddefb

#include <AFMotor.h>
#include "controller_controller.h"
#include "robo.h"

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

int obs_sensor;

ddefb

void setup() {
    Serial.begin(9600);
  
    Robo__controller_reset(&mem);
  
    pinMode(A0, OUTPUT);
    pinMode(A1, INPUT);
    digitalWrite(A0, LOW);
}

ddefb

double read_obstacle(){
  
    digitalWrite(A0, HIGH);
    delayMicroseconds(15);
    digitalWrite(A0, LOW);
    uint32_t pulse_time = pulseIn(A1, HIGH);     
    double distance = 0.01715 * pulse_time;
  
    return distance;
}