toy2d_with_w.cfg

#-----------------------------------------------------------------------
# File: toy2d_with_w.cfg
#-----------------------------------------------------------------------

# Brief description: This code is written for the "networks of discrete-time stochastic control/switched systems" meeting the following two purposes: 
# In the first part of the code, we build finite MDPs as finite abstractions of the given systems. In the second part, we synthesize controllers for the constructed finite MDPs satisfying some high-level specifications. 
# The stochasticity inside the model should be additive noise.
# This code is able to build finite MDPs for the "general setting" of discrete-time nonlinear stochastic control/switched systems, but synthesize controllers for some class of specifications (safety and reachability).
# This code also accepts the effects of other subsystems as disturbances with bounded intervals. If one is interested in working on the interconnected system (without disturbances), the disturbance should be implemented as zero.
# This configuration file utilizes the kernel GB_FP to build a finite MDP together with synthesize a controller for a road traffic network.

#-----------------------------------------------------------------------
# Project Data
#-----------------------------------------------------------------------
# (Project name) is essential. It will be used for names of output files.
project_name = "toy2d_with_w";

#-----------------------------------------------------------------------
# Output Memory Model
#-----------------------------------------------------------------------
# The (data) tells the tool which memory model should be used when saving results
# use the values : raw | bits | bitmap | bdd
data = "raw";
save_transitions = "true";
save_controller = "true";

#-----------------------------------------------------------------------
# State/Input/Disturbance Sets
#-----------------------------------------------------------------------
# The user is asked to provide the range of the state, input and disturbance intervals.
# The lower and upper bounds of the sets are respectively indicated by "lb" and "ub". The disceretization parameters are also designated by "eta".
states{
	dim = "2";
	eta = "  0.5,  0.5";
	lb  = "-10.0,-10.0";
	ub  = " 10.0, 10.0";
}

inputs{
	dim = "2";
	eta = " 0.2, 0.2";
	lb  = "-1.0,-1.0";
	ub  = " 1.0, 1.0";
}

disturbances{
	dim = "1";
	eta = " 0.2";
	lb  = "-1.0";
	ub  = " 1.0";
}


#----------------0-------------------------------------------------------
# System-Post Dynamics
#-----------------------------------------------------------------------
# The user is required to provide the desired dynamics.
# The additive noise inside the dynamics is not needed to be implemented. Instead, the covariance matrix of the noises will be later asked to be implemented.
# Your post variables should start with (xx) followed by the index of the dimension (starting from 0 not 1).
# Maximum number of dimensions is (states.dim)
# you are allowed to use:
#  - array indexing to access states in x (e.g., x0 as the first state variable)
#  - array indexing to access inputs in u (e.g., u0 as the first input variable)
#  - array indexing to access disturbances in u (e.g., w0 as the first distrubance variable)
#  - any math function from: https://www.khronos.org/registry/OpenCL/sdk/1.0/docs/man/xhtml/mathFunctions.html
post_dynamics{
	xx0 = "x0 + 10*u0*cos(u1) + w0";
    xx1 = "x1 + 10*u0*sin(u1) + w0";
}

#-----------------------------------------------------------------------
# Information of the Noises
#-----------------------------------------------------------------------
# The user is also asked to provide the inverse and the determinant of the covariance matrix of the noises. 
# The original covariance matrix should be positive semi-definite.
# The cutting probability should be a value below th max value of the PDF and used to cut the probability below
# it and cosider any values below it as zero.
noise {
	inv_covariance_matrix = "1.3333,1.3333";
	det_covariance_matrix = "0.5625";
	cutting_probability = "1e-3";
}

#-----------------------------------------------------------------------
# Specifications
#-----------------------------------------------------------------------
# This code is able to synthesize controllers for the "safety and reachability" pecifications.
# type = safe | reach
# If the property of interest is "safety", the user is asked to provide the range of the safe set.
specs {
	type = "safe";
	time_steps = "8";
}