Tutorial - SpaceEx


This tutorial shows you how to get started with the SpaceEx reachability analysis software. In it, we analyze a simplified model of a car combined with a trajectory tracking controller.

Installation instructions for the SpaceEx virtual machine can be found here.
A more thorough introduction to the SpaceEx software can be found here.
This tool has been integrated into the CPS-VO and can be launched from inside its group here.

Deriving the Model

Cars are highly complex, non-linear systems. As such, any model for which we may design a controller must significantly simplify a vehicle's actual dynamics. We often like to use a four-state dynamic bicycle model of a car which can accomodate the effects of air-drag and tire-friction on a moving vehicle. However, at low velocites, we can further simplify our model and only consider it's kinematics. This kinematic bicycle model of a car (shown below) is sufficient for designing trajectory-tracking controllers for low speed manuvers such as parking and in-town driving.

Here is a diagram of our car model, followed by its kinematic equations of motion:

Here x is the position of the center of mass of the car and v is its velocity. Theta is angle of the car with respect to the x-axis on a coorinate plane. Delta represents the steering angle of the front wheel with respect to the center-line of the car. The scalar variables v and u are respectively the velocity and the steering rate inputs.

As SpaceEx can only analyze linear or affine system models, we will have the make some simplifying assumptions in order to be able to perform any analysis.

The easiest way to to this is to assume that the steering angle will never deviate much from zero, in which case we can use a small angle approximation which simplifies our system to the following set of equations.

Another assumption that we will make is that the trajectory we want to track is a line emanating from the origin and travelling right along the positive portion of the x-axis. This will further simplify our modeling, as we will not have to explicitly specify a function defining the desired trajectory of our system.

As for the controller, we will implement a proportional derivative controller which attempts to drive our system towards the x-axis and then maintain a constant trajectory along it.

Modeling in the GUI

Before computing the reachable set for our system, we must first specify our system and controller using the SpaceEx model editor. After opening the editor, you will see a screen similar to the one below.

The first thing we want to do is to create a new model and base component. Click the purple icon in the top left corner of editor to create a new model. This creates a generic model that we can populate with components. Next, select the circular icon below it to add a new base component. Name it "car." Also save your project with a name such as "tutorial."

Create a new variable x by right clicking anywhere in the central pane of the editor and selecting "New variable" from the dropdown menu. In the rightmost region of the editor, a set of input options will appear allowing us to rename the variable as well as modify some other attributes. For the purposes of this tutorial, all we need to need to do is rename the variable to x.

Create three additional variables and label them y, theta, delta, u, and v.

We also need to create a constant parameter for the L in our third equation. Right click and select "New Constant" to create it.

In addition, we're going to want to set v to be a constant value as it makes the control problem simpler. Select v in the column of variables in the main box. A list of settings will appear in the rightmost box. In the dynamics section, select the "const" radio button. The tab representing v will turn green and now represents a constant parameter of the model location.

Now we can add state equations to our model. Click the location block so that it's customization options appear in the rightmost pane. In the "flow" box, input the equations shown in the image below. Note that you can only specify equations of the form x' == a1 * x1 + a2 * x2 + a3 * x3 + ... . Divisions are not allowed.

Since in a physical car, there is a maximum speed with which we can actuate a steering wheel. We can also add a constraint on delta in the "invariant" box.

At this point, our set of equations to too big to fit inside the box representing our model location. Click it and drag the small square in its bottom-right corner to resize the box.

Now we need to create base components to represent a clock and a controller. The clock is just a single state equation with a constant of one. The controller is just a proportional controller which attempts to force the car to travel along the x axis in a straight line. The specifics are not important and any other controller which can be written as a set of affine equations will work. Again, note that in this case we are going to assume that the velocty of the car is a constant non-zero value.

Below are pictures showing the parameters and state equations for the clock and controller.

We now combine our three basic components by creating a network component. Click on the other button in the top left corner under Model Explorer. Label this component "system."

Right click in the open area of the main pane. Go to "Add Bind" and then select "car" from the list of options. This adds the basic node to the system. We see that the param list becomes populated with all the parameters of the car component.

In the right pane, we see that the constant parameters v and "Linv" are set to the "link" radio button. Switch both over to "value" and set them to the values shown in the image below.

Add the controller component, updating the constant parameters k1, k2, and k3, to the values shown in the figure below.

Add the clock block.

Note that variables in each block with identical names become connected in the network component. Their values will remain coupled when we simulate our system. In this case, since our controller has no flow equations but only an invariant, the variable u of the controller is dependent on the states in the car model which, in turn, is influenced by the input u.

Save the entire SpaceEx model file one more time. We're now ready to use the web interface to analyze our model.

Analyze Using the Web Interface

Now that we have created a model file, it's time to analyze our system using the web interface. In case you haven't already, follow the linked directions above to set up the virtual machine server. If successfull you should see an IP adrress in the VM terminal. Open up a browser and go to that address. You will be taken to the home page of the web interface which looks something like the image below

Click on "Run Model" in the top-left corner in order to be taken to model selection page of the web interface.

Load our model by clicking on the "Browse..." button and navigating to the "tutorial.xml" file that we created earlier.

Specify an initial state or a set of initial states for you system by selecting the "Specification" tab in the left pane. Enter equalities in the the "Initial states" box, separating each by an "&." As we will see later, the user can set variables to specific values or specify a range of values for each variable.

Go to the "Options" tab. For this tutorial, the only thing we care about is the local time horizon. Adjust this value to 15 seconds. The other settings let the user customize the type of set representations that SpaceEx uses in its analysis core.

Finally go to the "Output" tab to specify which variables SpaceEx will plot. In our case, we are interested in the evolution of x and y over time, t. Add each of these variables to the "Output variables" box, separating each with a comma. SpaceEx will plot a 2-dimensional graph for every possible pair of variables that are specified. In addition, if the user wants to output a PDF of the plots, they can check the "Generate PDF file" box in the left pane.

Press the "Start" button at the bottom of the left pane to run SpaceEx. Not much happens. Since we set each variable's initial value to zero, each varible remains at zero except for x which increases at a constant rate over time.

If we go back to the "Specification" tab and set the initial value of y to 0.1, we now see that our controlled system stabilizes to y == 0 over time and SpaceEx computes a safe region containing this trajectory.

This result is more pronounced if we set y to be equal to 1.

We can get a more useful result if we define a range of initial states using inequalites. In the figure below, we constrain the initial values of y and theta to fall inside [0.8, 1.2] and [-0.1, 0.1] respectively. Runnning the analysis core again, we see that SpaceEx has computed a bounding region for the set of all possible trajectories generated by the set of initial conditions.

That's the end of the tutorial. Users can further refine their simulation by specifying forbidden states in the "Specification" tab. The are also several useful parameters to experiment with in the "Options" and "Advanced" tabs. Please refer to the documentation, linked above, and the SpaceEx website for instructions on how to incorporate these features.