Author: niels
Date: Fri May 23 15:11:34 2014
New Revision: 9446
URL: http://svn.gna.org/viewcvs/service-tech?rev=9446&view=rev
Log:
* more updates and examples
Added:
trunk/lola2/doc/outputs/output16.txt
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=9446&r1=9445&r2=9446&view=diff
==============================================================================
--- trunk/lola2/doc/lola.texi (original)
+++ trunk/lola2/doc/lola.texi Fri May 23 15:11:34 2014
@@ -1098,17 +1098,11 @@
@section Unsupported properties
-@c @b{Boundedness}
-@c While @math{k}-boundedness for a given @math{k} can be checked, boundedness
as such
-@c (i.e. the existence of a @math{k} such that a place or the net is
@math{k}-bounded)
-@c is not supported in the current release. Support for this property is
scheduled
-@c for an upcoming release.
-
-@b{Home states}
-A marking is a home state if it is reachable from every reachable marking. For
-a given marking, this can be checked as a liveness of a state predicate where
-the predicate describes the candidate marking. However, the question whether
-the net has home markings cannot be answered with this release.
+@b{Home states}.
+A marking is a @i{home state} if it is reachable from every reachable marking.
+For a given marking, this can be checked as a liveness of a state predicate
+where the predicate describes the candidate marking. However, the question
+whether the net has home markings cannot be answered with this release.
@section General recommendations
@@ -1138,75 +1132,106 @@
can get a witness path, its length, and whether or not state space
exploration is exhaustive.
-You select the search strategy using the command line option
@samp{--search=SEARCH} where @samp{SEARCH} is one of the values @samp{depth},
@samp{breadth},
-@samp{sweep}, or @samp{findpath}.
+You select the search strategy using the command line option
+@samp{--search=@var{SEARCH}} where @samp{@var{SEARCH}} is one of the values
+@samp{depth}, @samp{sweep}, @samp{findpath}, or @samp{cover}. If now value is
+given, @samp{depth} is used as default search strategy.
@section Available values
+@subsection Depth first search (@samp{--search=depth}, default)
+
@cindex @samp{--search=depth} parameter
-@b{Depth first search, @samp{--search=depth}} (default value).
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
necessarily
-the shortest possible witnesses.
-
-@cindex @samp{--search=breadth} parameter
-
-@b{Breadth first search, @samp{--search=breadth}}. LoLA explores the state
-space in breadth first order. Internally, this is organized as a depth-first
-search with increasing depth limits. This means that there is some
-computational overhead compared to depth first search. On the other hand,
-witness paths are as short as possible. Breadth first search is available
-only if LoLA can reduce the given property to a simple reachability query.
-For complex temporal logic formulae, LoLA applies depth-first search anyway.
+the exhaustive strategies. Witness paths can be produced but are not
+necessarily the shortest possible witnesses.
+
+@c @subsection Breadth first search
+@c
+@c @cindex @samp{--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
+@c search with increasing depth limits. This means that there is some
+@c computational overhead compared to depth first search. On the other hand,
+@c witness paths are as short as possible. Breadth first search is available
+@c only if LoLA can reduce the given property to a simple reachability query.
+@c For complex temporal logic formulae, LoLA applies depth-first search anyway.
+
+@subsection Sweep-line method (@samp{--search=sweep})
@cindex @samp{--search=sweep} parameter
-@b{The sweep-line method,@samp{--search=sweep}}. The sweep-line method
-depends on a progress measure assigned to states and explores states in
-ascending progress order. States with progress value smaller than the
-current explored ones are removed from memory. Thus, the sweep-line method
-requires less space than depth-first or breadth-first search. If states
-are reached that have potentially been removed before, they are stored
permanently, and their successors are explored (in subsequent ``rounds'').
Hence, the state space is explored
-exhaustively. LoLA computes the required progress measure automatically.
-Self-defined measures are not supported. The sweep-line method is only
available
-if the given property can be reduced to a simple reachability problem.
-Otherwise, LoLA applies depth-first search anyway. Using the
-sweep-line method, no witness path can be produced. Since some markings may
-be visited after prior removal, the numbers of visited markings and fired
-transitions is generally larger than with depth-first search (but peak
-memory usage can be smaller).
+The sweep-line method depends on a progress measure assigned to states and
+explores states in ascending progress order. States with progress value smaller
+than the current explored ones are removed from memory. Thus, the sweep-line
+method requires less space than depth-first or breadth-first search. If states
+are reached that have potentially been removed before, they are stored
+permanently, and their successors are explored (in subsequent ``rounds'').
+Hence, the state space is explored exhaustively.
+
+LoLA computes the required progress measure automatically. Self-defined
+measures are not supported. The sweep-line method is only available if the
+given property can be reduced to a simple reachability problem. Otherwise, LoLA
+applies depth-first search anyway. Using the sweep-line method, no witness path
+can be produced. Since some markings may be visited after prior removal, the
+numbers of visited markings and fired transitions is generally larger than with
+depth-first search (but peak memory usage can be smaller).
@itemize
@item Karsten Wolf. @b{Automated Generation of a Progress Measure for the
Sweep-Line Method.} @i{@acronym{STTT}}, 8(3):195-203, June 2006.
@end itemize
+@cartouche
+@smallexample
+@include outputs/output16.txt
+@end smallexample
+@end cartouche
+
+
+@subsection Memoryless search (@samp{--search=findpath})
+
@cindex @samp{--search=findpath} parameter
-
-@b{Memoryless search, @samp{--search=findpath}}
-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 paths produced by this method may contain cycles and are not
-necessarily the shortest possible witness paths. Search is not exhaustive.
-If a certain depth is exceeded, search resets to the initial state and
-explores another path (transitions are randomly selected). The depth at
-which LoLA resets to the initial state can be controlled using the
-@samp{--depthlimit=DEPTH} command line option where @samp{DEPTH} is any integer
-greater than 1. The default depth limit is one million. With another
-command line option, @samp{--retrylimit=RETRIES}, you can force LoLA to
-terminate after @samp{RETRIES} resets to the initial marking. In the result
-part, LoLA pretends that the desired marking has not been found (which may
-be wrong since search is not exhaustive). If @samp{RETRIES} is set to 0,
-LoLA goes on forever, exploring an unlimited number of paths each having length
-@samp{DEPTH} (unless the desired state is found). This search strategy is
available only if the given property can be transformed into a simple
reachability query. Otherwise, LoLA performs depth-first search anyway.
+@cindex @samp{--depthlimit} parameter
+@cindex @samp{--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
+paths produced by this method may contain cycles and are not necessarily the
+shortest possible witness paths. The search is not exhaustive.
+
+If a certain depth is exceeded, search resets to the initial state and explores
+another path (transitions are randomly selected). The depth at which LoLA
+resets to the initial state can be controlled using the
+@samp{--depthlimit=@var{DEPTH}} command line option where @samp{@var{DEPTH}} is
+any integer greater than 1. The default depth limit is one million.
+
+With another command line option, @samp{--retrylimit=@var{RETRIES}}, you can
+force LoLA to terminate after @samp{@var{RETRIES}} resets to the initial
+marking. In the result part, LoLA pretends that the desired marking has not
+been found (which may be wrong since search is not exhaustive). If
+@samp{@var{RETRIES}} is set to 0, LoLA goes on forever, exploring an unlimited
+number of paths each having length @samp{@var{DEPTH}} (unless the desired state
+is found). This search strategy is available only if the given property can be
+transformed into a simple reachability query. Otherwise, LoLA performs
+depth-first search anyway.
@itemize
@item Karsten Schmidt. @b{LoLA wird Pfadfinder.} @i{In 6. Workshop Algorithmen
und Werkzeuge f@"ur Petrinetze (AWPN'99), Frankfurt, Germany}, October 11.-12.,
1999, volume 26 of CEUR Workshop Proceedings, pages 48-53, October 1999.
CEUR-WS.org.
@end itemize
+@cartouche
+@smallexample
+@include outputs/output15.txt
+@end smallexample
+@end cartouche
+
+@subsection Coverability graph (@samp{--search=cover})
+
@cindex @samp{--search=cover} parameter
-@b{Coverability graph} [TODO]
+[TODO]
@section Setting resource limits
Added: trunk/lola2/doc/outputs/output16.txt
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/doc/outputs/output16.txt?rev=9446&view=auto
==============================================================================
--- trunk/lola2/doc/outputs/output16.txt (added)
+++ trunk/lola2/doc/outputs/output16.txt Fri May 23 15:11:34 2014
@@ -0,0 +1,14 @@
+$ lola --check=deadlock --search=sweep phils10.lola
+lola: reading net from phils10.lola
+...
+lola: calculating the progress measure
+lola: checking for deadlocks (--check=deadlock)
+...
+lola: using sweepline method (--search=sweepline)
+lola: transition progress range [-3,1], transients in [-3,1]
+lola: using 200 bytes per marking, including 0 wasted bytes
+lola: using 120 bytes per marking, with 0 unused bits
+lola: 82 persistent markings, 27 transient markings (max)
+lola: result: yes
+lola: The net has a deadlock.
+lola: 109 markings, 410 edges
--
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.
