Author: niels
Date: Wed May 28 16:30:44 2014
New Revision: 9472
URL: http://svn.gna.org/viewcvs/service-tech?rev=9472&view=rev
Log:
* updated documentation
Added:
trunk/lola2/doc/outputs/output17.txt
trunk/lola2/doc/outputs/output18.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=9472&r1=9471&r2=9472&view=diff
==============================================================================
--- trunk/lola2/doc/lola.texi (original)
+++ trunk/lola2/doc/lola.texi Wed May 28 16:30:44 2014
@@ -476,7 +476,7 @@
As first step, you may want to get to know LoLA and execute
-@cindex @samp{--help} parameter
+@cindex @code{--help} parameter
@cartouche
@smallexample
@@ -486,7 +486,7 @@
to display information about the command line parameters of LoLA. This gives
you a brief overview of the most important parameters of LoLA. With
-@cindex @samp{--detailed-help} parameter
+@cindex @code{--detailed-help} parameter
@cartouche
@smallexample
@@ -1141,7 +1141,7 @@
@subsection Depth first search (@samp{--search=depth}, default)
-@cindex @samp{--search=depth} parameter
+@cindex @code{--search=depth} parameter
LoLA explores the state space in depth first order. This is the fastest among
the exhaustive strategies. Witness paths can be produced but are not
@@ -1149,7 +1149,7 @@
@c @subsection Breadth first search
@c
-@c @cindex @samp{--search=breadth} parameter
+@c @cindex @code{--search=breadth} parameter
@c
@c @b{Breadth first search, @samp{--search=breadth}}. LoLA explores the state
@c space in breadth first order. Internally, this is organized as a depth-first
@@ -1161,7 +1161,7 @@
@subsection Sweep-line method (@samp{--search=sweep})
-@cindex @samp{--search=sweep} parameter
+@cindex @code{--search=sweep} parameter
The sweep-line method depends on a progress measure assigned to states and
explores states in ascending progress order. States with progress value smaller
@@ -1192,9 +1192,9 @@
@subsection Memoryless search (@samp{--search=findpath})
-@cindex @samp{--search=findpath} parameter
-@cindex @samp{--depthlimit} parameter
-@cindex @samp{--retrylimit} parameter
+@cindex @code{--search=findpath} parameter
+@cindex @code{--depthlimit} parameter
+@cindex @code{--retrylimit} parameter
LoLA explores the state space without recording visited states at all. It stops
if, by chance, a state witnessing the given property is encountered. Witness
@@ -1229,7 +1229,7 @@
@subsection Coverability graph (@samp{--search=cover})
-@cindex @samp{--search=cover} parameter
+@cindex @code{--search=cover} parameter
[TODO]
@@ -1514,28 +1514,34 @@
@b{Compression by place invariants}.
-A place invariant is a mapping that assigns a @i{weight} to each place such
that all reachable markings get the same weighted token sum. Invariants
-correspond to solutions @i{x} of the linear System of equations @i{Cx=0}
-where @i{C} is the incidence matrix of the Petri nets. Having such a place
-invariant, the number of tokens on one place @i{p} with nonzero weight is fully
-determined by the number of tokens on the remaining places and the constant
-overall weight (which can be calculated for the initial marking). In other
-words, if two markings do not differ on any place except @i{p}, they are
-equal on @i{p} as well. We call @i{p} an @i{insignificant} place. Since a
-Petri net may have several place invariants, more than one place may be
-insignificant. During preprocessing, LoLA analyzes the linear dependencies
-in the incidence matrix and comes up with a factoring of the place set into
-significant and insignificant places. When compression by place invariants is
-active, LoLA only ships significant places to the resulting bit vector.
-Typically, compression by place invariants reduces the length of the resulting
-bit vector to 30-70 percent of the original size. Since experience tells that
-preprocessing does not require much run time, its use is
-strongly recommended. For efficiency reasons, LoLA only determines @i{whether}
a place is insignificant but not how. That is, LoLA does not fully explore
place invariants and does not store them permanently. For this reason, bit
vectors
-in the store, although uniquely characterizing a marking, cannot be used
-to restore a full marking for later use. If such functionality is ever
-useful (in future releases), switching off compression by capacities may make
sense. During preprocessing, LoLA reports the number of significant places.
-This way, the user can easily experience the compression ration through
-place invariants.
+
+@anchor{Compression by place invariants}
+
+A place invariant is a mapping that assigns a @i{weight} to each place such
+that all reachable markings get the same weighted token sum. Invariants
+correspond to solutions @i{x} of the linear System of equations @i{Cx=0} where
+@i{C} is the incidence matrix of the Petri nets. Having such a place invariant,
+the number of tokens on one place @i{p} with nonzero weight is fully determined
+by the number of tokens on the remaining places and the constant overall weight
+(which can be calculated for the initial marking). In other words, if two
+markings do not differ on any place except @i{p}, they are equal on @i{p} as
+well. We call @i{p} an @i{insignificant} place. Since a Petri net may have
+several place invariants, more than one place may be insignificant. During
+preprocessing, LoLA analyzes the linear dependencies in the incidence matrix
+and comes up with a factoring of the place set into significant and
+insignificant places. When compression by place invariants is active, LoLA only
+ships significant places to the resulting bit vector. Typically, compression by
+place invariants reduces the length of the resulting bit vector to 30-70
+percent of the original size. Since experience tells that preprocessing does
+not require much run time, its use is strongly recommended. For efficiency
+reasons, LoLA only determines @i{whether} a place is insignificant but not how.
+That is, LoLA does not fully explore place invariants and does not store them
+permanently. For this reason, bit vectors in the store, although uniquely
+characterizing a marking, cannot be used to restore a full marking for later
+use. If such functionality is ever useful (in future releases), switching off
+compression by capacities may make sense. During preprocessing, LoLA reports
+the number of significant places. This way, the user can easily experience the
+compression ration through place invariants.
@itemize
@item Karsten Schmidt. @b{Using Petri Net Invariants in State Space
Construction.} @i{In Hubert Garavel and John Hatcliff, editors, Tools and
Algorithms for the Construction and Analysis of Systems (TACAS 2003), 9th
International Conference, Part of ETAPS 2003, Warsaw, Poland}, volume 2619 of
Lecture Notes in Computer Science, pages 473-488, April 2003. Springer-Verlag.
@@ -1564,6 +1570,7 @@
@end itemize
@section Store
+@anchor{Store}
During state space exploration, LoLA maintains a store. A store contains
information on whether or not a marking (i.e. an encoded bit sequence)
@@ -1670,12 +1677,40 @@
@node Output formats
@chapter Output formats
-Niels
-
-Resultat, Pfade, Markierung, strukturiert, Status/Statistik
-
-
-@section @acronym{JSON}
+@cindex @code{--quiet} parameter
+
+LoLA will output runtime information on standard error. This output is purely
informational and may change in future versions. If you want to process
information, we advice using the @acronym{JSON} output, see @ref{JSON}.
+
+You can silence all output but the result and the number of calculated
markings using the @samp{--quiet} parameter.
+
+@cartouche
+@smallexample
+@verbatiminclude outputs/output17.txt
+@end smallexample
+@end cartouche
+
+@section 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.
+
+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.
+
+@cartouche
+@smallexample
+@verbatiminclude outputs/output18.txt
+@end smallexample
+@end cartouche
+
+@section Paths
+
+@cindex path output
+@cindex @code{--path} parameter
+
+@section JavaScript Object Notations (@acronym{JSON})
+@anchor{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.,
@@ -1826,25 +1861,67 @@
parameter). The value is @samp{null} in case no limit is provided.
@item @code{net} [object]
+
+An object collecting information on the input net.
+
@item @code{net.conflict_sets} [number]
+
+The number of conflict sets. A conflict set contains those transitions that
are in conflict. These sets are explicitly stored to speed up the firing of
transitions.
+
@item @code{net.filename} [string]
+
+The filename of the input net.
+
@item @code{net.places} [number]
+
+The number of place of the input net.
+
@item @code{net.places_significant} [number]
+
+The number of significant places of the input net, see @ref{Compression by
place invariants,,Compression by place invariants}.
+
@item @code{net.transitions} [number]
+The number of transitions of the input net.
+
@item @code{path} [array]
+An array of transition names expressing a witness/counterexample path for the
given property (e.g., a path from the initial marking to a deadlock state). In
case of @acronym{CTL}, @acronym{LTL}, or boundedness properties, the path may
contain cycles. In this case, the path array contains sub-array expressing
these cycles.
+
+Note: To include this entry, use the @samp{--jsoninclude=path} parameter.
+
@item @code{state} [object]
+An object expressing a witness/counterexample marking for the given property.
The marking is given as mapping from place names to integers.
+
+Note: To include this entry, use the @samp{--jsoninclude=state} parameter.
+
@item @code{store} [object]
+
+An object collecting information on the used marking store, see @ref{Storage
concepts}.
+
@item @code{store.bucketing} [number]
+
+The number of buckets if bucketing is used; can be set with
@samp{--bucketing@var{=BUCKETS}}.
+
@item @code{store.encoder} [string]
+
+The used state encoder, see @ref{Encoding,,Encoding}.
+
@item @code{store.threads} [number]
+
+The number of threads used; can be set with @samp{--threads=@var{THREADS}}.
+
@item @code{store.search} [string]
+
+The used search strategy, see @ref{Search strategies}.
+
@item @code{store.type} [string]
+
+The used store, see @ref{Store,,Store}.
+
@end table
-The entries @samp{path} and @samp{state} need to be explicitly enabled using
the @samp{--jsoninclude} parameter.
@subsection Example
@@ -1872,8 +1949,8 @@
@section Syntax errors [#01]
-@cindex @code{syntax error -- aborting [#01]}
-@cindex @code{see manual for a documentation of this error}
+@cindex @code{syntax error -- aborting [#01]} message
+@cindex @code{see manual for a documentation of this error} message
@table @code
@item syntax error, unexpected @i{x}, expecting @i{y}
@@ -1888,7 +1965,7 @@
@section Command line errors [#02]
-@cindex @code{command line error -- aborting [#02]}
+@cindex @code{command line error -- aborting [#02]} message
These errors indicate that the given command line parameters are wrong, for
instance that a required argument is missing or that a combination of arguments
@@ -1925,7 +2002,7 @@
@section File input/output errors [#03]
-@cindex @code{file input/output error -- aborting [#03]}
+@cindex @code{file input/output error -- aborting [#03]} message
@table @code
@item could not close @i{purpose} file @i{filename}
@@ -1940,7 +2017,7 @@
@section Thread error [#04]
-@cindex @code{thread error -- aborting [#04]}
+@cindex @code{thread error -- aborting [#04]} message
@table @code
@item thread could not be created
Added: trunk/lola2/doc/outputs/output17.txt
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/doc/outputs/output17.txt?rev=9472&view=auto
==============================================================================
--- trunk/lola2/doc/outputs/output17.txt (added)
+++ trunk/lola2/doc/outputs/output17.txt Wed May 28 16:30:44 2014
@@ -0,0 +1,4 @@
+$ lola --check=deadlock --quiet phils10.lola
+lola: result: yes
+lola: The net has a deadlock.
+lola: 29 markings, 37 edges
Added: trunk/lola2/doc/outputs/output18.txt
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/doc/outputs/output18.txt?rev=9472&view=auto
==============================================================================
--- trunk/lola2/doc/outputs/output18.txt (added)
+++ trunk/lola2/doc/outputs/output18.txt Wed May 28 16:30:44 2014
@@ -0,0 +1,10 @@
+hl.1 : 1
+hl.2 : 1
+hl.3 : 1
+hl.4 : 1
+hl.5 : 1
+hl.6 : 1
+hl.7 : 1
+hl.8 : 1
+hl.9 : 1
+hl.10 : 1
Modified: trunk/lola2/doc/outputs/update.sh
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/doc/outputs/update.sh?rev=9472&r1=9471&r2=9472&view=diff
==============================================================================
--- trunk/lola2/doc/outputs/update.sh (original)
+++ trunk/lola2/doc/outputs/update.sh Wed May 28 16:30:44 2014
@@ -88,3 +88,12 @@
mkdir -p output16
cp $EXAMPLEDIR/phils/phils10.lola output16
create_output output16 "lola --check=deadlock --search=sweep phils10.lola"
+
+mkdir -p output17
+cp $EXAMPLEDIR/phils/phils10.lola output17
+create_output output17 "lola --check=deadlock --quiet phils10.lola"
+
+mkdir -p output18
+cp $EXAMPLEDIR/phils/phils10.lola output18
+create_output output18 "lola --check=deadlock --state=../output18.tmp
phils10.lola"
+mv output18.tmp output18.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.
