setup_boing.m

% Setup function for the boing demonstration
%
% Syntax:
%   "setup_boing"
%
% Description:
%   "setup" sets various model and verification parameters for the
%   boing demonstration.  In this demo, parameters are set as variables in
%   the Matlab base workspace and specified in the model using the
%   variable names.
% 
%   Boing is a model of a bouncing ball.  See the readme.txt file 
%   in the boing directory for a complete description of (and getting started guide for)
%   the boing example.
% 
%
% See Also:
%   global_var,boing_param


% declare global variables in base work space
evalin('base','global_var');

% declare global variables here
global_var

%Define hyperplanes for the regions in the boing example

%Define hyperplane " floor".  This hyperplane represents the floor that the ball strikes.
%The velocity is reset when the ball strikes the floor.
floor=linearcon([],[], [0 1 0],1);
assignin('base','floor',floor);

%Define hyperplane " hole". It corresponds to the region to be avoided.  When the system is
%in the 'hole' region and is at or below the level of the floor, the ball falls into the hole 
%(i.e. the system fails).
hole=linearcon([],[], [1 0 0;-1 0 0],[3;-2.5]);
assignin('base','hole',hole);

%Define hyperplane "right_wall".  When the ball hits this hyperplane, the simulation is over
%and the system satisfies the specification (not falling in the hole).
right_wall=linearcon([],[], [-1 0 0],-4);
assignin('base','right_wall',right_wall);

% Define Analysis Region.  This is the entire region (three dimensional) of the state space that
%will be considered during the analysis.  If the system leaves the analysis region, analysis will 
%stop.
boing_AR=linearcon([],[], [1 0 0;-1 0 0; 0 1 0; 0 -1 0;0 0 1;0 0 -1],[5;1;12;1;12;12]);
assignin('base','boing_AR',boing_AR);


% Define Parameter region.  This is the variation allowed for the value of wind resistance that
%will be considered during the analysis.  For details how v impacts the dynamics, please see
%file boingfunc_nonlinear.m .

boing_PAR=linearcon([],[], [1;-1],[.5;-.1]);
assignin('base','boing_PAR',boing_PAR);

% Define initial condition for the continuous space.  This is the entire set of initial conditions
% for which verification will be performed.  Also, the vertices of this region may be simulated automatically
% using the 'explore' function. 
boing_ICS={linearcon([],[], [1 0 0;-1 0 0; 0 1 0; 0 -1 0;0 0 1;0 0 -1],[.1;.1;2.5;-2.4;.1;.1])};
assignin('base','boing_ICS',boing_ICS);

global initial_hybrid_set;
initial_hybrid_set.BlockName{1} = 'fsm';
initial_hybrid_set.StateName{1} = 'idle1';
initial_hybrid_set.X0 =boing_ICS;


GLOBAL_SYSTEM = 'boing';
GLOBAL_APARAM = 'boing_param';
GLOBAL_SPEC={};

%The specification for this system is as follows:  "Is it always true that the system never enters the hole
%while at the same time never leaves the analysis region?". 

%The CTL expression below is commented out because the spec is automatically generated by CheckMate
%(because of the Stateflow state named 'avoid').  The line below should serve as a template for 
%manually adding user-defined CTL specifications.
%GLOBAL_SPEC{1} = '(AG  ~fsm== avoid) & (AG ~out_of_bound)';