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 |
---|---|---|
|
|
A level that gives a rough guide of the importance of the message. Can be |
|
|
The name of the Kind 2 module which wrote the log. |
|
|
Associated input file, if any. |
|
|
Associated line in the input file, if any. |
|
|
Associated column in the input file, if any. |
|
|
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 |
---|---|---|
|
|
List of Kind 2 module names that are enabled. |
|
|
The wallclock timeout used for all the analyses. |
|
|
Maximal number of iterations for BMC and K-induction. |
|
|
Whether compositional analysis is enabled or not. |
|
|
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 |
---|---|---|
|
|
Name of the current top-level component. |
|
|
Names of the subcomponents whose implementation is used in the analysis. |
|
|
Names of the subcomponents whose contract is used in the analysis. |
|
|
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 |
---|---|---|
|
|
Property identifier or description. |
|
|
Name of the component where the property was analyzed. |
|
|
Associated line in the input file, if any. |
|
|
Associated column in the input file, if any. |
|
|
Origin of the property. Can be |
|
|
The runtime of the analysis (in seconds), and whether the timeout expired |
|
|
The value of |
|
|
The largest value of |
|
|
The |
|
|
Counterexample to the property satisfaction (only available when |
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 |
---|---|---|
|
|
Name of the Kind 2 module which reported the info. |
|
|
List of |
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 |
---|---|---|
|
|
Name of the k-inductive-based analysis. |
|
|
Value for |
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 of the post-analysis |
The post-analyses currently available are Test Generation (testgen
),
Proof Certificates (certification
),
Contract Generation (contractgen
),
Compilation to Rust (rustgen
),
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 of the core. Can be |
|
|
Number of model elements in the core. |
|
|
The property associated with the core. If all properties are considered, this field is missing. |
|
|
The runtime for computing the core (in seconds). |
|
|
For each node, contains an object that enumerates the model elements of the node that are part of the core. |
|
|
Counterexample to the property satisfaction (only when relevant, that is, when class is |
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 |
---|---|---|
|
|
A level that gives a rough guide of the importance of the message. Can be |
|
|
The name of the Kind 2 module which wrote the log. |
|
|
Associated line in the input file, if any. |
|
|
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 |
---|---|---|
|
|
List of comma-separated Kind 2 enabled module names. |
|
|
The wallclock timeout used for all the analyses. |
|
|
Maximal number of iterations for BMC and K-induction. |
|
|
Whether compositional analysis is enabled or not. |
|
|
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 |
---|---|---|
|
|
Name of the current top-level component. |
|
|
Names of the subcomponents whose implementation is used in the analysis (comma-separated list). |
|
|
Names of the subcomponents whose contract is used in the analysis (comma-separated list). |
|
|
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 |
---|---|---|
|
|
Property identifier or description. |
|
|
Name of the component where the property was analyzed. |
|
|
Associated input file, if any. |
|
|
Associated line in the input file, if any. |
|
|
Associated column in the input file, if any. |
|
|
Origin of the property. Can be |
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
),
Compilation to Rust (rustgen
),
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 of the core. Can be |
|
|
Number of model elements in the core. |
|
|
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).