Management and Representation of State
The way that T-VEC manages state information is to treat state variables as both inputs and outputs of the system. For example, in Simulink, state information is maintained by certain blocks like unitDelay, discrete integrator, and others. Each of these blocks maintains both a current cycle's output value and also state value that is used as its part of its input during the next cycle. Fir example:
The output of the unitDelay block for cycle N is the input to the unitDelay block from cycle N-1. So, in a sense, there are 2 inputs to the diagram (above) for the current execution/simulation cycle. There is the "temperature" input and also the input to the unitDelay block from the previous cycle. The diagram has also 2 outputs, the primary output and the state variable value that will be used as the input to the next cycle. In addition, each of these types of blocks include an initial condition value.
This is the value that is used as the "previous cycle's" value during the first execution cycle (i.e. at T=0). To produce test vectors, the tools translate the Simulink model into a T-VEC specification of the semantics of the model. In the T-VEC specification, the state information is represented as both an input parameter and as an output parameter of the T-VEC subsystem associated with the Simulink diagram. As part of this translation process, each logical slice (aka DCPs (Domain Convergence Paths)) through the diagram is identified and captured. Each DCP path includes a Functional Relationship (i.e., output computation) and Constraint Relationship (describing when the Functional Relationship is the valid definition of the output value). T-VEC then takes each DCP path, solves the constraint equations simultaneously (including linear and non-linear constraints relationships and floating point types) to identify the input values that will make the Constraint Relationship TRUE, then those selected input values are used with the Functional Relationship to compute the expected output value(s) for that DCP path. So, each state variable is "solved" for any other input variable. As a default, T-VEC produces test vectors for both the T=0 cycle, where the state variables are set to there initial condition values, and also for T>0 where the state variable values are chosen (solved for) in a way that contributes to a TRUE evaluation of the Constraint Relationship.