NYCS: Naples hYbrid Controller Synthesis

Syntax of the Configuration File

The configuration file tells NYCS what to do with the model, by setting a number of options in XML. The most relevant tags are the following:

<nycs type="config" > ... </nycs>: this tag must embrace the whole configuration file.
<component id="..." > ... </component>: this tag identifies the name of the LHG the options apply to. The option "id" will contain the name. The following tags will be contained within this one.
<scenario name="..." />: this option is mandatory and "name" must be one of the following string values:
- safety control: the tool computes the controllability region w.r.t. a safety goal, specified by the "safe" option (see below).
- reachability control: the tool computes the controllability region w.r.t. a reachability goal, specified by the "reach" option (see below).
<safe> list of regions <safe /> : the safe area for the safety control scenario. It can be a distinct non-convex polyhedron for each location. Each region is specified as follows:
- <region loc="..." > non-convex polyhedron <region />: the polyhedron is attributed to the location specified by "loc". If no "loc" is specified, then the polyhedron is attributed to all locations.
<reach> list of regions <reach /> : the target area for the reachability control scenario. It can be a distinct non-convex polyhedron for each location. Regions follow the same syntax as for the above "safe" tag.
<max iterations="..." />: limits the maximum number of iterations that the algorithms can perform.
<timeout seconds="..." />: stops the computation after the timeout specified in "seconds".

Advanced options (usually unnecessary):

<outer-operator name="..." />: for safety scenario: "rwa" or "sor"; for reachability scenario: "rwa via rwa", "rwa via sor", "sor via rwa", or "sor via sor"

<inner-operator name="..." />: for outer operator "rwa", "rwa via rwa", and "sor via rwa":

basic,	slow (for reference)
maps,	fast (default)
smooth-basic,	smooth trajectories, slow implementation
smooth,	smooth trajectories, fast implementation

for outer operator "sor", "sor via sor", and "rwa via sor":

basic,	slow dual implementation (for reference)
global,	dual implementation
local,	fast dual implementation (default for reachability)
local_recycle,	fast dual implementation (default for safety, incompatible with reachability)

<over level="..." />: type of over-approximation for the reachability scenario; must be either "large" or "small" (default); there is usually no reason to depart from the default, as it is faster.

Config file example

Example of a config file:

<nycs type="config">                         
<component id="TNC">                  
  <scenario name="safety control" />             
  <max iterations="10" />
  <timeout seconds="10000" />   
  <over level="small">
  <outer-operator name="rwa" />                          
  <inner-operator name="maps" />     
  <verbosity level="debug" />                    
  <safe>                                          
    <region> !(x >= 0 & x <= 2 & y >= 0 & y <= 1) & !( x >= 2 & x <= 4 & y >= -1 & y <= 0 ) & !( x >= -2 & x <= 0 & y >= 1 & y <= 2 )</region>                         
  </safe>
</component>
</nycs>