Author: niels
Date: Fri May 23 16:16:13 2014
New Revision: 9447
URL: http://svn.gna.org/viewcvs/service-tech?rev=9447&view=rev
Log:
* more documentation on the JSON part
Modified:
trunk/lola2/doc/lola.texi
Modified: trunk/lola2/doc/lola.texi
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/doc/lola.texi?rev=9447&r1=9446&r2=9447&view=diff
==============================================================================
--- trunk/lola2/doc/lola.texi (original)
+++ trunk/lola2/doc/lola.texi Fri May 23 16:16:13 2014
@@ -1677,32 +1677,149 @@
@section @acronym{JSON}
-With the command line parameter @samp{--json}, LoLA outputs a @acronym{JSON}
representation of its output to the standard output or a given filename (e.g.,
@samp{--json=output.json}). The result is a @acronym{JSON} object whose entries
are as follows:
+With the command line parameter @samp{--json}, LoLA outputs a @acronym{JSON}
+representation of its output to the standard output or a given filename (e.g.,
+@samp{--json=output.json}). The result is a @acronym{JSON} object whose entries
+are as follows:
@table @asis
@item @code{analysis} [object]
+
+This object collects information on the performed analysis.
+
@item @code{analysis.type} [string]
+
+The type of the analysis (the parameter given with @samp{--check}).
+
@item @code{analysis.stats} [object]
+
+This object collects information on the constructed state space.
+
@item @code{analysis.stats.edges} [number]
+
+The number of fired transitions.
+
@item @code{analysis.stats.states} [number]
+
+The calculated markings. Note that in case of some search strategies, not all
+of these markings are actually stored.
+
@item @code{analysis.result} [boolean]
+
+The result of the analysis. In case no result was found (e.g. due to reaching
+of a resource limit), this entry is missing. In case the result is unknown
+(e.g. using a Bloom store where no witness was found), the result is
+@samp{null}.
+
@item @code{analysis.formula} [object]
+
+This object collects information on the formula in case the analysis type is
@samp{modelchecking}.
+
@item @code{analysis.formula.atomic_propositons} [number]
+
+The number of atomic propositions occurring in the formula.
+
+@item @code{analysis.formula.parsed} [string]
+
+The formula as interpreted by the parser before processing. Note this string
+may be different from the original input, because the parser may add brackets
+and spaces.
+
+@item @code{analysis.formula.parsed_size} [number]
+
+The length of the formula before processing. This value is mostly valuable in
+case of very long formulae to make a prediction about the estimated duration of
+processing.
+
+@item @code{analysis.formula.place_mentioned} [number]
+
+The total number of places mentioned in the formula.
+
+@item @code{analysis.formula.place_unique} [number]
+
+The unique number of places mentioned in the formula. As most reduction
+techniques especially perform well when only a part of the net is affected,
+this number gives a good hint in how ``local'' the property is.
+
+@item @code{analysis.formula.processed} [string]
+
+The formula as interpreted by the parser after processing. Processing tries to
+remove redundancies and unfolds more complex properties (e.g. @samp{FIREABLE})
+or operators (e.g. @samp{<->}) to simpler ones. Note that the outmost temporal
+operator may be removed in case reachability or invariance formulae are checked
+-- in this case, the formula only contains the state predicate to check. See
+@ref{Supported Properties} fore more information.
+
+@item @code{analysis.formula.processed_size} [number]
+
+The length of the formula after processing.
+
@item @code{analysis.formula.type} [string]
+The type of the formula. LoLA tries to find the most special type to choose the
+most efficient algorithm. Therefore, formulae like `EF \math{P}' are not
+checked using @acronym{CTL} routines, but rather using more efficient
+reachability algorithms.
+
@item @code{call} [object]
+
+This object collects information on the call and caller of LoLA.
+
@item @code{call.architecture} [number]
+
+The datapath width of the architecture in bits. This number is useful to check
+whether the compiler version of LoLA can make use of more than 4 gigabytes of
+memory (in this case, 64 bit are required).
+
@item @code{call.assertions} [boolean]
+
+Whether assertions are checked at runtime. This setting should only be used to
+debug LoLA. Make sure you configured LoLA with @samp{./configure
+--enable-optimizations}. See @ref{Bootstrapping LoLA} for more information.
+
@item @code{call.build_system} [string]
+
+An identifier of the build system used to compile LoLA, including the kernel
+name, kernal version, architecture, and vendor.
+
@item @code{call.optimizations} [boolean]
+
+Whether optimizations were used at compile time. This setting should only be
+switched off to debug LoLA. Make sure you configured LoLA with
+@samp{./configure --enable-optimizations}. See @ref{Bootstrapping LoLA} for
+more information.
+
@item @code{call.package_version} [string]
+
+The version number of LoLA.
+
@item @code{call.parameters} [array]
+
+An array containing the used command line parameters.
+
@item @code{call.svn_version} [string]
+
+If LoLA was compiled from the original source code repository, this entry
+contains the revision number of the compiled source code.
+
@item @code{call.hostname} [string]
+The hostname of the caller.
+
@item @code{limits} [object]
+
+This object contains the set limits of the execution.
+
@item @code{limits.markings} [number]
+
+The maximal number of markings to be constructed (set with the
+@samp{--markinglimit} parameter). The value is @samp{null} in case no limit is
+provided.
+
@item @code{limits.time} [number]
+
+The maximal runtime of LoLA in seconds (set with the @samp{--timelimit}
+parameter). The value is @samp{null} in case no limit is provided.
@item @code{net} [object]
@item @code{net.conflict_sets} [number]
--
You received this e-mail, because you subscribed the mailing list
"service-tech-commits" which will forward you any e-mail addressed to
[email protected]. If you want to unsubscribe or make any changes to
your subscription, please go to
https://mail.gna.org/listinfo/service-tech-commits.
