mpt_verify

MPT_VERIFY Verifies if states enter a given set in a given number of steps

 [flag, N, Vreach] = mpt_verify(sysStruct, X0, Xf, N, U0)
 [flag, N, Vreach] = mpt_verify(controller, X0, Xf, N)

 ---------------------------------------------------------------------------
 DESCRIPTION
 ---------------------------------------------------------------------------
 Checks if states of a dynamical system subject to:
  1. inputs driven by an explicit control law
  2. inputs which belong to a set of admissible inputs U0
 enter a given set Xf, assuming x0 \in X0 in N steps.

 USAGE:
   flag = mpt_verify(sysStruct, X0, Xf, N, U0)
   flag = mpt_verify(controller, X0, Xf, N)

 ---------------------------------------------------------------------------
 INPUT
 ---------------------------------------------------------------------------
 object       - either a sysStruct structure, or an explicit controller
 X0           - set of initial states (a polytope or a polyarray)
 Xf           - target set (a polytope or a polyarray)
 N            - number of steps over which to compute reachable sets
 U0           - set of admissible inputs (polytope object)
 Options.usereachsets 
              - if set to 0 (default is 1), verification question for systems
                described by sysStruct structures will be performed by solving
                an LP/MILP problem. Set this option to true if you want to base
                the verification on reachable sets.

 ---------------------------------------------------------------------------
 OUTPUT                                                                                                    
 ---------------------------------------------------------------------------
 flag        - 1 if Xf is reachable from X0, 0 otherwise
 N           - number of steps in which Xf is reachable from X0 ([] if Xf is
               not reachable)
 Vreach      - V-representation of reachable sets

 see also MPT_REACHSETS, MPT_REACHXU