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.
Incremental JSON format
The incremental JSON output is activated by running Kind 2 with the -ijson
option. It contains the same Results Objects as the regular JSON
output, but prints them as a sequence of independent JSON objects rather than as
elements of a single enclosing array.
With the -json option, the output is not a complete, parsable JSON document
until Kind 2 terminates and closes the root array. The -ijson option emits
each object as a complete JSON value as soon as it becomes available. This allows
external tools to process Kind 2’s output incrementally without waiting for the
entire analysis to finish.
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 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),
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
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),
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).