Synthesis for
LEGO Mindstorms NXT and EV3 Robots

Overview

Spectra Tools provides several different means to execute and simulate the synthesized controller, concrete or symbolic. First, code generation from concrete controllers. The concrete controller is directly translated to a simple implementation of a state machine. We currently have application-specific Java code generation tailored to run on Lego NXT robots. Second, an execution API for symbolic controllers. The symbolic controller is loaded and iteratively called, at runtime, with the current inputs from the environment, to provide the next outputs (assignment to system variables). This runtime environment requires a BDD library, however its use is limited to single calls to extract a satisfying assignment. Our students have used it to execute their Lego robots where the actual execution runs on a Raspberry Pi.

Over the last three years (in 2015 and in 2017), small teams of 3rd year Computer Science undergraduate students from Tel Aviv University, have used Spectra and Spectra Tools in two semester long project classes we have taught, to develop about 10 different autonomous Lego robots, which the students actually built and run.

Robots of SYNTECH15

Robots of SYNTECH17

Available materials