Author: niels
Date: Fri May 30 12:04:38 2014
New Revision: 9476
URL: http://svn.gna.org/viewcvs/service-tech?rev=9476&view=rev
Log:
* updated documentation
Added:
trunk/lola2/doc/outputs/output19.txt
Modified:
trunk/lola2/doc/lola.texi
trunk/lola2/doc/outputs/update.sh
Modified: trunk/lola2/doc/lola.texi
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/doc/lola.texi?rev=9476&r1=9475&r2=9476&view=diff
==============================================================================
--- trunk/lola2/doc/lola.texi (original)
+++ trunk/lola2/doc/lola.texi Fri May 30 12:04:38 2014
@@ -1702,11 +1702,11 @@
@end cartouche
@section Markings
-
+@anchor{Markings}
@cindex marking output
@cindex @code{--state} parameter
-Depending on the property and the outcome of the analysis, LoLA can provide a
marking that demonstrates why the property is (not) satisfied. The marking is
printed with the @samp{--state=@var{FILE}} parameter. If no filename
@samp{@var{FILE}} is given, the state is printed on standard output.
+Depending on the property and the outcome of the analysis, LoLA can provide a
marking that demonstrates why the property is (not) satisfied). The marking is
printed with the @samp{--state=@var{FILE}} parameter. If no filename
@samp{@var{FILE}} is given, the state is printed on standard output.
The output lists the names of all marked places, followed by a colon
(@samp{:}) and the number of tokens on the place or @samp{oo} in case the place
is unbounded. Note place names are not necessarily sorted alphabetically and
unmarked places are not printed.
@@ -1715,11 +1715,42 @@
@verbatiminclude outputs/output18.txt
@end smallexample
@end cartouche
+
+The marking can also be printed in @acronym{JSON} format, see @ref{JSON}.
@section Paths
@cindex path output
@cindex @code{--path} parameter
+
+Depending on the property and the outcome of the analysis, LoLA can provide a
+path from the initial marking to a marking that demonstrates why the property
+is (not) satisfied) (see @ref{Markings}). The path is printed with the
+@samp{--path=@var{FILE}} parameter. If no filename @samp{@var{FILE}} is given,
+the path is printed on standard output.
+
+The output lists the transitions. In case of @acronym{CTL}, @acronym{LTL}, or
+boundedness properties, the path may contain cycles. The begin and end of the
+cycles is labeled with @samp{===begin of cycle===} and @samp{===end of
+cycle===}, respectively.
+
+@cartouche
+@smallexample
+@verbatiminclude outputs/output19.txt
+@end smallexample
+@end cartouche
+
+The path can also be printed in @acronym{JSON} format, see @ref{JSON}.
+
+@cindex @code{--pathshape} parameter
+
+Furthermore, the path can be printed in different shapes that can be chosen
+with the @samp{--pathshape=@var{SHAPE}} parameter. With
+@samp{--pathshape=fullrun}, a distributed run is generated. With
+@samp{--pathshape=run}, this distributed run is cropped to only those
+conditions that contribute to reaching the target marking. With
+@samp{--pathshape=event}, an event structure is printed. The result is printed
+in Graphiz format (see @url{http://www.graphviz.org}).
@section JavaScript Object Notations (@acronym{JSON})
@anchor{JSON}
@@ -2049,7 +2080,55 @@
@node Integration guide
@chapter Integration guide
-Niels
+LoLA follows the @acronym{UNIX} principle of ``everything is a file''. Thereby,
+integrating LoLA into other tools boils down to choosing the needed command
+line parameters, providing the input (net, formula) as files, and reading the
+generated output(s). As LoLA allows to read from standard input and write to
+standard output, it can further be integrated without generating files at all.
+
+With the structured @acronym{JSON} output (see @ref{JSON}), it is furthermore
+very easy to extract special portions of the output, for instance using a
+@acronym{JSON} processor like @code{jq} (see
+@url{http://stedolan.github.io/jq/}).
+
+@cartouche
+@smallexample
+$ lola phils10.lola --check=deadlock --quiet --json | jq ".analysis.result,
+.analysis.stats.states"
+true
+29
+@end smallexample
+@end cartouche
+
+As another example, consider the following (very simplistic) Python script that
+passes a net (given as string) to LoLA via standard input and reads the
+@acronym{JSON} output from standard output into a dictionary.
+
+@cartouche
+@smallexample
+#!/usr/bin/env python
+
+from subprocess import Popen, PIPE
+import json
+
+net = """
+PLACE p1, p2;
+MARKING p1;
+TRANSITION t
+CONSUME p1;
+PRODUCE p2;
+"""
+
+lola = Popen(["lola", "--check=deadlock", "--quiet", "--json"], stdin=PIPE,
stdout=PIPE)
+output = lola.communicate(input=net)
+
+result = json.loads(output[0])
+
+net_has_deadlock = result['analysis']['result']
+@end smallexample
+@end cartouche
+
+
Added: trunk/lola2/doc/outputs/output19.txt
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/doc/outputs/output19.txt?rev=9476&view=auto
==============================================================================
--- trunk/lola2/doc/outputs/output19.txt (added)
+++ trunk/lola2/doc/outputs/output19.txt Fri May 30 12:04:38 2014
@@ -0,0 +1,10 @@
+tl.[y=1]
+tl.[y=2]
+tl.[y=3]
+tl.[y=4]
+tl.[y=5]
+tl.[y=6]
+tl.[y=7]
+tl.[y=8]
+tl.[y=9]
+tl.[y=10]
Modified: trunk/lola2/doc/outputs/update.sh
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/doc/outputs/update.sh?rev=9476&r1=9475&r2=9476&view=diff
==============================================================================
--- trunk/lola2/doc/outputs/update.sh (original)
+++ trunk/lola2/doc/outputs/update.sh Fri May 30 12:04:38 2014
@@ -97,3 +97,8 @@
cp $EXAMPLEDIR/phils/phils10.lola output18
create_output output18 "lola --check=deadlock --state=../output18.tmp
phils10.lola"
mv output18.tmp output18.txt
+
+mkdir -p output19
+cp $EXAMPLEDIR/phils/phils10.lola output19
+create_output output19 "lola --check=deadlock --path=../output19.tmp
phils10.lola"
+mv output19.tmp output19.txt
--
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.
