QCT Query Language

QVtrace uses a standard logical predicate language to query the design using constraints. Constraints are formal conditions that the design is expected to meet. These conditions can be a direct translation of the requirement specifications, or “unit tests” as the system design grows, or simple sanity checks for parameter bounds and specific scenarios. During analysis, QVtrace determines if the model is consistent, or inconsistent, with each constraint.


Expressing constraints

Once a design has been loaded into QVtrace, constraints can be manually typed into the query window, or imported from a text file with the '.qct' extension.

Each constraint must represent a condition that can be evaluated as either true or false. It is good practice to terminate each constraint with a semicolon.

Example: (Input1 >= 0) impl (Output == Input1);
   (Input1 < 0) impl (Output == -Input1);

Variables
Properties can reference variables present in the model by explicitly calling the variable names.  The general format for referencing variables is:

subsystemName.variableName{time}

where ‘variableName’ references an input or output within a system or subsystem, and ‘subsystemName is optional for cases where variableName is present in more than one subsystem.

Example: to reference the 'standby' input of the 'manager' subsystem, one writes "manager.standby".

Constants
Explicit integer and real numbers can be used as constants within a query property.  

Example: to state that ‘input0’ should be larger than 5, one writes ‘"input0 > 5”.

Boolean constants are not supported. There is no difference between just stating a boolean expression and stating the boolean expression is true.

Example: ‘"In1 == true” and “In1” are equivalent expressions.

Time Dependence

The value of a node at a particular time step can be referenced either absolutely, relatively, or universally. The following table details how variableName can be referenced at different time steps in QCT properties:

Reference	Relationship	Description	Example
variableName	Relative	variableName at the current time step. Equivalent to variableName{t}.	Stating that Input0 should be greater than 10 at the current time step can be written ‘Input0 > 10’ or ‘Input0{t} > 10’
variableName{t}	Relative	variableName at the current time step.	Input0 at time point 3 would be referenced using 'Input0{3}'
variableName{t-1}	Relative	variableName at the previous time step.*	Stating that Output2 should change each time step could be stated as: 'Output2{t} != Output2{t-1}
variableName{t-n}	Relative	variableName at n time steps prior to the current time step.*	referencing output 2 should change each time step could be stated thus: 'Out2{t} != Out2{t-1}'
variableName{0}	Absolute	variableName at the initial condition or 0th time step.
variableName{n}	Absolute	variableName at the nth time step, where n is an integer.	Input0 at time step 3 would be referenced using 'Input0{3}'
variableName{all}	Universal	variableName at every evaluated time step (property should always hold).	If In1 is false at time step 0, then Out1 is always true can be expressed as: '(In1{0} == true) impl (Out1{all} == true)'
variableName{never}	Universal	variableName at every evaluated time step (property should never hold).	If In1 is false at time step 0, then Out1 is always true with: '(In1{0} == true) impl (Out{never} == false)'

*Note that QVtrace uses the convention that relative time references are made to time steps prior to the current time, ’t’. Referencing time steps ahead of the current time is not supported. For example, the property that a variable remains unchanged from one step to the next  should be properly stated as “variableName{t}==variableName{t-1}”, however “variableName{t+1}==variableName{t}” is not acceptable.