JSON / XML Output

Kind 2 can output its results in two structured formats: JSON and XML. They facilite the processing of Kind 2’s results by external tools. The next sections describe each of these output formats in detail.

JSON format

The JSON output is activated by running Kind 2 with the -json option. Its syntax is fully specified by the JSON schema available in the schemas/kind2-output.json file.

The root element of a JSON output document is either a Log Object if Kind 2 terminates early with an error, or an array of Results Objects if Kind 2 succeeds generating some result. Every Results Object (including Log Object) is identified and distinguished from other Results objects by a property of type string called objectType.

In a successful execution, a Kind2 Options Object specifies the options used by the tool, and any Log message is added to the array as it is written. When Kind 2 is run as an interpreter, the array includes one Execution Object that contains a description of the computed values for the output and state variables. Otherwise, Kind 2 works as a model checker and performs a series of analyses. The beginning of a main analysis is indicated by an AnalysisStart Object, and its end by an AnalysisStop Object. Within these delimiters, a Property Object describes the result for a particular property of the input model under the parameters of the analysis. When the verbose mode is enabled, statistics and progress info of the analysis is also recorded along through Stat and Progress objects.

Similarly to main analyses, when a post-analysis is enabled, the beginning of the post-analysis is indicated by an PostAnalysisStart Object, and its end by an PostAnalysisEnd Object.

Log Object

A Log object records an informative message from the tool. The value of its objectType property is log. The list of properties of a Log object are:

Key

Type

Description

level

string

A level that gives a rough guide of the importance of the message. Can be fatal, error, warn, note, info, debug, or trace.

source

string

The name of the Kind 2 module which wrote the log.

file

string

Associated input file, if any.

line

integer

Associated line in the input file, if any.

column

integer

Associated column in the input file, if any.

value

string

The log message.

Results Objects

A Result object can be one of the following objects: a Log Object, a Kind2 Options Object, an AnalysisStart Object, an AnalysisStop Object, a Property Object, a Stat Object, a Progress Object, a PostAnalysisStart Object, or a PostAnalysisEnd Object.

Kind2 Options Object

A Kind2 options object describes the options used by the tool in the current execution. The value of its objectType property is kind2Options. The list of properties of a Kind2 options object are:

Key

Type

Description

enabled

array

List of Kind 2 module names that are enabled.

timeout

number

The wallclock timeout used for all the analyses.

bmcMax

integer

Maximal number of iterations for BMC and K-induction.

compositional

boolean

Whether compositional analysis is enabled or not.

modular

boolean

Whether modular analysis is enabled or not.

AnalysisStart Object

An AnalysisStart object indicates the beginning of a main analysis. The value of its objectType property is analysisStart. The list of properties of an AnalysisStart object are:

Key

Type

Description

top

string

Name of the current top-level component.

concrete

array

Names of the subcomponents whose implementation is used in the analysis.

abstract

array

Names of the subcomponents whose contract is used in the analysis.

assumptions

array

Array of pairs (name of subcomponent, number of considered invariants).

AnalysisStop Object

An AnalysisStop object indicates the end of a main analysis. The value of its objectType property is analysisStop. No properties are associated.

Property Object

A Property object describes the result for a particular property of the input model. The result should be considered in the context of the analysis in which the property object is contained. The value of its objectType property is property. The list of properties of an AnalysisStart object are:

Key

Type

Description

name

string

Property identifier or description.

scope

string

Name of the component where the property was analyzed.

line

integer

Associated line in the input file, if any.

column

integer

Associated column in the input file, if any.

source

string

Origin of the property. Can be Assumption if it comes from an assumption check, Guarantee if it comes from the check of a guarantee, Ensure if it comes from a check of a require-ensure clause in a contract mode, OneModeActive if it comes from an exhaustiveness check of the state space covered by the modes of a contract, and PropAnnot if it comes from the check of a property annotation.

runtime

object

The runtime of the analysis (in seconds), and whether the timeout expired

k

integer

The value of k in a k-inductive proof, if any.

trueFor

integer

The largest value of k for which the property was proved to be true, if any.

answer

object

The source of the answer, and the result value of the check. The result can be valid, falsifiable, or unknown.

counterExample

object

Counterexample to the property satisfaction (only available when answer is falsifiable). It describes a sequence of values for each stream, and automaton, that leads the system to the violation of the property. It also gives the list of contract modes that are active at each step, if any.

Stat Object

An Stat object provides statistics info about the current analysis. The value of its objectType property is stat. The list of properties of a Stat object are:

Key

Type

Description

source

string

Name of the Kind 2 module which reported the info.

sections

array

List of statSection objects, each of them with a section name and a list of statItem objects. Each statItem has a name, a type, and a value. See schemas/kind2-output.json for further details.

Progress Object

An Progress object reports the current value of k for k-inductive-based analyses. The value of its objectType property is progress. The list of properties of a Progress object are:

Key

Type

Description

source

string

Name of the k-inductive-based analysis.

k

integer

Value for k.

PostAnalysisStart Object

An PostAnalysisStart object indicates the beginning of a post-analysis. The value of its objectType property is postAnalysisStart. The list of properties of an PostAnalysisStart object are:

Key

Type

Description

name

string

Name of the post-analysis

The post-analyses currently available are Test Generation (testgen), Proof Certificates (certification), Contract Generation (contractgen), Compilation to Rust (rustgen), Invariant Logging (invlog), Invariant Printing (invprint), and Inductive Validity Core (ivc).

PostAnalysisEnd Object

An PostAnalysisEnd object indicates the end of a post-analysis. The value of its objectType property is postAnalysisEnd. No properties are associated.

Execution Object

An Execution object describes the sequences of values for the output and state variables of an input model computed from its simulation (see the interpreter mode). The value of its objectType property is execution. It only has one object property called trace which follows the same format than property counterExample in Property Object.

ModelElementSet Object

A ModelElementSet object describes a set of model elements (a model element can be an equation, a node call, an assumption, a guarantee, etc). It is used to describe a core that we can get from an Inductive Validity Core (ivc) or Minimal Cut Set (mcs) analysis. The result should be considered in the context of the analysis or post-analysis in which the ModelElementSet object is contained. The value of its objectType property is modelElementSet.

Key

Type

Description

class

string

Class of the core. Can be must, must complement, ivc, ivc complement, mcs or mcs complement.

size

integer

Number of model elements in the core.

property

string

The property associated with the core. If all properties are considered, this field is missing.

runtime

object

The runtime for computing the core (in seconds).

nodes

array

For each node, contains an object that enumerates the model elements of the node that are part of the core.

counterExample

object

Counterexample to the property satisfaction (only when relevant, that is, when class is mcs or mcs complement). See the property object for more info.

XML format

The XML output is activated by running Kind 2 with the -xml option. Its syntax is fully specified by the XML schema available in the schemas/kind2-output.xsd file.

The root element of a XML output document is either a Log Element if Kind 2 terminates early with an error, or a Results Element if Kind 2 succeeds generating some result.

Log Element

A Log element is a simple element that records an informative message from the tool. The list of attributes of a Log element are:

Attribute

Base Type

Description

class

xs:string

A level that gives a rough guide of the importance of the message. Can be fatal, error, warn, note, info, debug, or trace.

source

xs:string

The name of the Kind 2 module which wrote the log.

line

xs:integer

Associated line in the input file, if any.

column

xs:integer

Associated column in the input file, if any.

Results Element

A Results element is a sequence of zero or more of the following elements: a Log Element, an AnalysisStart Element, an AnalysisStop Element, a Property Element, a Stat Element, a Progress Element, a PostAnalysisStart Element, a PostAnalysisEnd Element, or an Execution Element.

The list of attributes of a Results element are:

Attribute

Base Type

Description

enabled

xs:string

List of comma-separated Kind 2 enabled module names.

timeout

xs:decimal

The wallclock timeout used for all the analyses.

bmc_max

xs:integer

Maximal number of iterations for BMC and K-induction.

compositional

xs:boolean

Whether compositional analysis is enabled or not.

modular

xs:boolean

Whether modular analysis is enabled or not.

AnalysisStart Element

An AnalysisStart element is an empty element that indicates the beginning of a main analysis. The list of attributes of an AnalysisStart element are:

Attribute

Base Type

Description

top

xs:string

Name of the current top-level component.

concrete

xs:string

Names of the subcomponents whose implementation is used in the analysis (comma-separated list).

abstract

xs:string

Names of the subcomponents whose contract is used in the analysis (comma-separated list).

assumptions

xs:string

Comma-separated list of pairs (subcomponent name, number of considered invariants).

AnalysisStop Element

An AnalysisStop element is an empty element that indicates the end of a main analysis. No attributes.

Property Element

A Property element describes the result for a particular property of the input model. The result should be considered in the context of the analysis in which the property element is contained. The list of attributes of a Property element are:

Attribute

Base Type

Description

name

xs:string

Property identifier or description.

scope

xs:string

Name of the component where the property was analyzed.

file

xs:string

Associated input file, if any.

line

xs:integer

Associated line in the input file, if any.

column

xs:integer

Associated column in the input file, if any.

source

xs:string

Origin of the property. Can be Assumption if it comes from an assumption check, Guarantee if it comes from the check of a guarantee, Ensure if it comes from a check of an ensure clause in a contract mode, OneModeActive if it comes from an exhaustiveness check of the state space covered by the modes of a contract, and PropAnnot if it comes from the check of a property annotation.

A Property element contains one Answer element, which includes the result for the property check (valid, falsifiable, or unknown), and identifies the Kind 2 module responsible for the answer. If the result is valid, or falsifiable, it also contains a Runtime element, which reports the runtime of the analysis (in seconds), and whether the timeout expired or not. If the result is valid, a K element gives the value of k for which the property was proved valid. If the result is falsifiable, a Counterexample element describes a sequence of values for each stream, and automaton, that leads the system to the violation of the property. It also gives the list of contract modes that are active at each step, if any. If the result is unknown, the Property element may contain a TrueFor element specifying the largest value of k for which the property was proved to be true.

Stat Element

An Stat element provides statistics info about the current analysis. It has only one attribute of type xs:string, source, which is the name of the Kind 2 module which reported the piece of information. Its content consists in one or more Section elements. Each section has one name element, and one or more item elements. Each item element has one name element, and either a value element or a valuelist element. A valuelist has one or more value elements, and each value element has a type attribute (currently int or float), and its content is the actual value.

Progress Element

A Progress element is a simple element that reports the current value of k for a k-inductive-based analysis. It has only one attribute of type xs:string, source, which is the name of the k-inductive-based analysis.

PostAnalysisStart Element

An PostAnalysisStart element is an empty element that indicates the beginning of a post-analysis. It has only one attribute of type xs:string, the name of the post-analysis. The post-analyses currently available are Test Generation (testgen), Proof Certificates (certification), Contract Generation (contractgen), Compilation to Rust (rustgen), Invariant Logging (invlog), Invariant Printing (invprint), and Inductive Validity Core (ivc).

PostAnalysisEnd Element

An PostAnalysisEnd element is an empty element that indicates the end of a post-analysis. No attributes.

Execution Element

An Execution element describes the sequences of values for the output and state variables of an input model computed from the simulation of its execustion (see the interpreter mode).

ModelElementSet Element

A ModelElementSet element describes a set of model elements (a model element can be an equation, a node call, an assumption, a guarantee, etc). It is used to describe a core that we can get from an Inductive Validity Core (ivc) or Minimal Cut Set (mcs) analysis. The result should be considered in the context of the analysis or post-analysis in which the ModelElementSet element is contained. The list of attributes of a ModelElementSet element are:

Attribute

Base Type

Description

class

string

Class of the core. Can be must, must complement, ivc, ivc complement, mcs or mcs complement.

size

integer

Number of model elements in the core.

property

string

The property associated with the core. If all properties are considered, this attribute is missing.

A ModelElementSet element contains one Runtime element, which indicates the runtime for computing the core. It also contains a sequence of Node elements, each one enumerating the model elements in that node that are part of the core. When relevant, it can also contain a Counterexample element (see the Property element for more info).