Specifying Control Requirements

The control requirements supported by the toolbox is of the form of reachavoidstay specifications i.e. starting in init reach and stay in goal while never entering avoid.

The toolbox supports specifying goal, init, and avoid sets as unions of polytopes or alternatly directly as locations of the discrete abstraction.

Specifying Requirements

%The polytopes a constructed as with the pahs polytopes. This example uses a simplex.
p1.vertices{[1;1],[0;0],[0;1]}
p1=makesimplex(p1)

%The first init polytope is specified in both modes 1 and 2
req.init{1}.modes=[1 2];
req.init{1}.poly=p1;

%The avoid set is only in mode 2
req.avoid{1}.modes=2;
req.avoid{1}.poly=p2;
req.avoid{2}.modes=2;
req.avoid{2}.poly=p3;

%The goal set specified in both modes
req.goal{1}.modes=2;
req.goal{1}.poly=p4;

%The PAHS the requirements are made on
pahs=demopahs();

%Convert the requirements to specifications on the discrete abstraction
spec=req2spec(pahs,req);

%It is possible to add specifications on the discrete abstraction.
%Instead of polytopes the locations of the pahs/discrete abstraction
%are specified directly directly.
spec.avoid{end+1}.modes=1;
spec.avoid{end}.loc=3;