.TH selt n "Version 4.0.0" "Tina Tools"

.SH NAME
selt  \- SE\-LTL model checker

Part of Tina Toolbox for analysis of Petri nets and Time Petri nets.

.SH SYNOPSIS

.B selt
[\-\f2h\f1elp] 

.B selt
[\-prelude ltlfile] [\-ltl2nc | \-spin | \-ltl2ba | \-spot]
     [\-q | \-v] [\-b | \-c | \-p | \-s | \-g] [\-S scnfile] [\-wp n]
     ktzfile [\-f formula | formfile] [outfile] [errorfile]

.B selt
[\-prelude ltlfile] [\-ltl2nc | \-spin | \-ltl2ba | \-spot]
     [\-q | \-v] [\-b | \-c | \-p | \-s | \-g] [\-S scnfile] [\-wp n]
     \-script formfile ktzfile [outfile] [errorfile]

.SH DESCRIPTION

selt model-checks state-event LTL formulas on a kripke transition system
given in ktz format.

If some  formula is specified (by  flag -f or by  providing formfile),
then  the result  of  evaluation  of  the formula  is  printed
according to the output mode and verbosity flags, and selt exits.

If  no  formula file is  specified,  then  selt  starts an  interactive
session, evaluating commands entered by the user on standard input (see
"selt se-ltl language and commands" below).


.SH OPTIONS

.TP
\-\f2h\f1elp
Recalls options.


.TP
.B Ktz input:

.TP
ktzfile
The kripke transition system on which formula are model-checked, in
ktz format (extension \&.ktz).

.TP
\-wp (0|1|2)
This flag removes (0), preserves (1),  or forces at each state (2) the
temporal divergence  property possibly present in the  kts file (see
tina's -wp flag for details).

.TP
\-script
For using selt as a script interpreter:
The first file is then a file of selt declarations and the second is a ktzfile,
Evaluation of property declarations is silent and, with boolean output, formulas are printed before their truth values.

.TP
.B LTL input:

.TP
\-f formula
Passes to selt the formula to be verified.

.TP
formfile
Specifies a file holding the formulas to be verified. Must have extension \&.ltl

.TP
\-prelude ltlfile
Specifies a  file containing selt  commands to be evaluated  on entry,
before  any formula  provided by  -f, by  formfile,  or interactively.
This  flag is  useful to  load  SE-LTL libraries.   ltlfile must  have
extension .ltl

.TP
.B LTL to Buchi automata converter options:

.TP
default  option
If none of the following options is passed, selt will use the converter
the name of which is found in the environment variable LTL2BA, if set,
or ltl2nc otherwise (ltl2nc is bundled with tina, for all targets).


.TP
\-ltl2nc
Convert  ltl formula  to buchi  automata  using ltl2nc  (ltl to  never
claim), a stripped down version of spin-6.2.3 only implementing option
-f.  ltl2nc binaries are bundled with tina distributions.

.TP
\-spin
Convert ltl formula to buchi automata using spin (any version).
spin must be installed at your site from the sources or binaries
available from (http://spinroot.com).

.TP
\-ltl2ba
Convert ltl formula to buchi automata using Oddoux/Gastin ltl2ba.
Typically yields smaller automata than the above,
fits most purposes and easy to compile.
ltl2ba must be installed at your site, from the sources available
at (http://www.lsv.fr/~gastin/ltl2ba). Pre-compiled binaries of
ltl2ba V1.0 for some targets may be available at
(http://www.laas.fr/tina/software2.php).

.TP
\-spot
Convert ltl formula to buchi automata using ltl2tgba from the SPOT
model checking library.
ltl2tgba must be installed at your site, from
the sources available at (http://spot.lrde.epita.fr).
This is certainly the fastest converter available, and that yielding
the smallest automata, but compilation may be challenging on some targets.

.TP
.B Verbosity level:

.TP
\-v
prints banner and evaluation times for LTL commands (default).

.TP
\-q 
No  banner  nor times  are  printed. This  flag  is  useful for  batch
operation.


.TP
.B Output mode flags:

.TP
\-b
When  evaluating  a formula,  just  prints  its  truth value,  without
counter example.

.TP
\-c
When  a formula  evaluates  to  FALSE, prints  in  addition a  counter
example in condensed form (default).

.TP
\-p
When  a formula  evaluates  to  FALSE, prints  in  addition a  counter
example in full form.

.TP
\-s
When  a formula  evaluates  to  FALSE, prints  in  addition a  counter
example in the scn formmat of the nd stepper.

.TP
\-g
When a formula  evaluates to FALSE, does not  print a counter example,
but builds the  full graph obtained as the  synchronization of the kts
and of the  bucchi automaton translating the negation  of the formula,
instead, in ktz form (to be provided).


.TP
.B Other flags:

.TP
\-S  scnfile
When a  formula evaluates to FALSE,  writes a counter  example in \&.scn
format of in file scnfile (creating the file if it does not exist, and
overwriting  it otherwise).   This flag  is useful  to  replay counter
examples  in  the  nd  stepper  when  modelchecking  an  existing  ktz
description and a  description of the net the \&.ktz file describes the
behavior  of  is available  (see  "interacting  with  the nd  stepper"
below).


.TP
.B Output destination:

.TP
outfile
Where results are written. The output format is determined by the file
type, according  to the  table below. If  absent or specified  by "-",
then results are written on standard output in the format specified by
the output flag. If both an  outfile and some output flag are present,
then the format defined by  the output flag supersedes that determined
by the outfile extension.

.nf
file extension		output format
--------------------------------------------------------------
\&.scn			nd stepper \&.scn format
\&.ktz			\&.ktz format
any other		textual output
.fi


.TP
.B Errors destination:

.TP
errorfile
Where error messages are written. By default, errors are printed on standard error.



.SH INTERACTING WITH THE ND STEPPER

For  model-checking  Petri nets  or  Time  Petri  nets, tool  selt  is
interfaced with the nd editor of the Tina toolbox.

When  the \&.ktz  of  the behavior  of  some net  is  not available,  or
rebuilding  it  is  cheap,  SE-LTL   properties  of  the  net  can  be
model-checked as  follows: load  the net into  nd, then build  the ktz
description  of its behavior  (using the  reachability tool,  with the
default output  mode and  construction), then invoke  the modelchecker
from the menu  in the ktz window, and finally  select "stepper" in the
nd tools menu.  Any counter example computed by the model-checker will
then be loaded automatically into the stepper, for replay.

When the \&.ktz of the behavior  of some net is available and rebuilding
it is expensive, then invoke selt with option -S. The file passed with
-S will always hold the  last counter example built. In parallel, load
the net description into nd and select "stepper" in the nd tools menu.
For replaying a counter example, load the \&.scn file specified with -S.



.SH SELT SE-LTL LANGUAGE AND COMMANDS

Selt implements a version of the SE-LTL linear time temporal logic as described in paper:

S.  Chaki, E.  M. Clarke,  J. Ouaknine,  N. Sharygina,  and  N. Sinha,
"State/Event-based   Software  Model   Checking",   4th  International
Conference on Integrated Formal  Methods (IFM'04), Springer LNCS 2999,
pages 128--147, April 2004.

For building  Buchi automata from  LTL files, the recommended  tool is
ltl2ba (see above option -ltl2ba for details), a tool described in the
paper:

P. Gastin  and D.  Oddoux, "Fast LTL  to Buchi  Automata Translation",
13th Conference Computer-Aided  Verification (CAV'2001), Springer LNCS
2102, pages 53--65, July 2001.

.SH 1. \f2Lexical matters\f1:

- A identifier is either:

Any  place   or  transition  identifier  allowed  in \&.net  or \&.ndr
descriptions, that  is: any  sequence of letters,  digits, underscores
"_" and primes  "'", or any sequence of  characters enclosed in braces
in which "{", "}" (except the outer ones) and "\\" are prefixed by "\\"

Any sequence of symbols from the list ~ ` ! @ # $ % ^ & * - + = : ? | \ /   < > [ ];

A qualified identifier: an identifier prefixed by S., E. or L.

e.g.   hello, _p4'_, 123, >=<, or {variable x45}, are legal identifiers.

- The commands are: op, infix, prefix, forget, verb, output, source, quit, assert.
Command names  may not be used  as operator or  variable names.

- When  analyzing  identifiers,  the  scanner  advances  as  right  as
possible.  So, in a juxtaposition  of identifiers, two symbolic or two
alphanumeric unbraced identifiers,  or e.g. an alphanumeric identifier
and a  command name, must  be separated by  a space.  But no  space is
necessary  between  identifiers  of   different  kinds  or  between  a
parenthesis (or ";") and an identifier.

- justaposition bind  tighter than infixes and associate  to the left,
infixes and prefixes associate to the  right. That is, if f is a 3-ary
operator in functional notation, [],  <>, -, are prefixes, and /\\, \\/,
are infixes:

.nf
			[] p1 => <> - p3 /\\ f u v w
  parses as	([] p1) => ((<> (- p3)) /\\ (f u v wp))
			
			f - <> p1 (f p0 p1 (p4 /\\ p5)) \\/ f u v w
  parses as	(f (- <> p1) (f p0 p1 (p4 /\\ p5))) \\/ (f u v w)

  and		f - <> p1 f p0 p1 p4 \\/ f u v w
  parses as 	(f (- <> p1) f p0 p1 p4) \\/ (f u v w)
  which is ill-typed
.fi

- infixes  have precedence in  0..5 (see  below). Infixes  with higher
precedence bind tighter than those with lower precedence.


.SH 2. \f2The initial environment\f1:

It is made up of (pushed in that order):

- The  atomic  state  and  event  propositions. They  have  the  names
captured in the .ktz file,  i.e. those of the places and transitions
of the Petri net if the \&.ktz file was generated by tina.

- Then, the logic and arithmetic primitives, constituted of:

.nf
   constants:	T (true), F (false),
		dead (deadlock property)
		div (temporal divergence property)
		sub (state is partially known)

   prefixes:	[] (always), <> (eventually), () (next),
   		- (logic negation), ~(arithmetic negation)

   infixes:	U (until), V (release), of precedence 0
   		=> (implies), <=> (equivalent), of precedence 1
		/\\ (and), \\/ (or), of precedence 2
		<=, >=, =, le, lt, ge, gt, of precedence 3
		+, of precedence 4
		*, of precedence 5
.fi
		
- Then the user defined operators.

Since the syntactic classes of atomic state propositions, atomic event
propositions, logic primitives,  integer,  and user defined operators,
overlap,  we must have  some way  of disambiguating  identifiers.  For
this:

- unqualified identifiers are bound to  the command with than name, if
any, or otherwise to the last pushed environment entry with that name.

- identifiers  qualified by  S (e.g.  S.p1)  are bound  to the  atomic
state proposition with that name with the qualifier removed (e.g. p1);

- identifiers  qualified by  E (e.g.  E.t1)  are bound  to the  atomic
event proposition with that name with the qualifier removed (e.g. t1);

- identifiers  qualified by  L  (e.g.  L./\\) are  bound  to the  logic
primitive with that name with the qualifier removed (e.g. /\\);

So, atomic  propositions (found  in the ktz  file) sharing  their name
with some atomic propositions in a different group (state or event) or
with some command  (e.g. op), or some logical  primitive (e.g.  -), or
the name  of which  is an integer  (e.g.  3),  must be referred  to in
formulas by their qualified form (e.g.  S.op, E.-, or S.3);


.SH 3. \f2Fixity\f1:

Identifiers declared  infix (binary  logic primitives or  user defined
operators declared by "infix") must be used in infix notation;

Identifiers declared  prefix (unary  logic primitives or  user defined
operators declared by "prefix") must  be used in prefix notation (in a
juxtaposition  of  identifiers, prefix  operators  associate with  the
right expression);

Other operators  or primitives accessed by their  qualified names must
be used in functional notation.   E.g. if a1, a2, a3 are parenthesized
expressions, and f has arity 3, then:

.nf
	a1 /\\ a2 and L./\\ a1 a2 are legal (and equivalent)
    but a1 L./\\ a2 is ill-typed

	f - a1 a2 a3 is legal (parses as ((f (- a1)) a2) a3)
    but f L.- a1 a2 a3 T is ill-typed (parses as (((f L.-) a1) a2) a3)
.fi

.SH 4. \f2Commands and effects\f1:

Commands must terminate with ";".  In formula files, the final ";" may
be  omitted (EOF  plays that  role). The  effects of  commands  are as
follows ("exp" is any ltl expression, x, y, f, xi are identifiers):

.nf
exp;
	evaluates LTL expression exp;

assert exp "whentrue" "whenfalse";
       evaluates exp then prints string whentrue (resp. whenfalse) if
       exp holds (resp. does not) instead of the default message TRUE
       (resp. FALSE).

op f x1 ... xn = exp;
	declares an  operator f  or arity n  (n >=  0), to be  used in
	functional notation;

infix [n] x f y = exp;
	declares a binary operator f in infix notation. n is an
	optional integer in 0..5 specifying precedence.

prefix f x = exp;
	declares a unary operator f in prefix notation;

forget f1 ... fn;
	Removed items names f1 ...  fn from the environment, and their
	fixity information;

source [file | "file"];
	reads at toplevel the contents of file. The file name is
	optionally surrounded  by string quotes (this  is necessary if
	the name includes spaces);

verb [true | false | debug];
	verbosity level. Tne initial  setting follows from the command
	line flags -v | -q (default -v);

	true  (default):  prints   the  banner,  prompts,  results  of
	commands, and evaluation times;

	false:  just   prints  the   results  of  evaluation   of  LTL
	expressions (useful in batch mode);

	debug: may print extra information (mainly for developper);

output [proof | fullproof | quiet | stepper | graph]
	specify   effects   and   results   of  evaluations   of   LTL
	expressions.  The  command  line  flags  -c, -p,  -b,  -s,  -g
	specifies the initial setting (default -c);

	proof  (default): evaluations  return  TRUE, or  FALSE with  a
	counter example in condensed form;

	fullproof: evaluations  return TRUE,  or FALSE with  a counter
	example in full form (may be very large);

	quiet: evaluations just return  TRUE or FALSE, without counter
	examples.

	stepper: as output fullproof  except the counter example is in
	stepper format (typically used in batch mode);

	graph: not implemented yet

quit	
	leaves selt (also ^D on Unix targets).
.fi

.SH 5. \f2Example commands\f1:

.nf
p1;			(eqv. p1 lt 0 \\/ p1 gt 0)
- p1;   		(eqv. p1 = 0)
p1 /\\ p2 >= 2;		(eqv. p1 /\\ (p2 >= 2))
infix x sup y = x >= y + 1;	(declares arithmetic operator sup, in infix form)
p1+p2;
p1+p2 > p3;
p1*p2 = 0;
infix y follows x = [] (x => <>y);  
      		(declares logical operator "follows", in infix form)
(t3 \\/ p5) follows (t1 /\\ p1>=p2);
    		(eqv. [] ((t1 /\\ (p1>=p2)) => <> (t3 \\/ p5)));
.fi



.SH EXAMPLES

.nf
selt abp.ktz -f "[] (t1 => <> t3)" -q -b
selt abp.ktz -p
.fi


.SH SEE ALSO

nd(n), tina(n), plan(n), struct(n), ktzio(n), ndrio(n), tedd(n), sift(n), muse(n), pathto(n), scan(n), play(n), walk(n), reduce(n), formats(n), stan(n)

.SH AUTHORS
Bernard Berthomieu, with contributions by Francois Vernadat, Pierre-Olivier Ribet,
LAAS/CNRS,  2000-2026, {Bernard.Berthomieu|Francois.Vernadat}@laas.fr.

