
NAME
     selt  - SE-LTL model checker

     Part of Tina Toolbox for analysis of  Petri  nets  and  Time
     Petri nets (see also nd, tina, plan, struct, ndrio, ktzio).


SYNOPSIS
     selt [-help]
     selt ktzfile [-f formula | formfile] [-prelude ltlfile]
           [-q | -v] [-b | -c | -p | -s | -g] [-S scnfile] [-wp n]
           [outfile]


DESCRIPTION
     selt model-checks state-event LTL formulas on a kripke tran-
     sition 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  formulafile 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).


OPTIONS
     -help Recalls options.

     Ktz input:

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

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

     LTL input:

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

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

     -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

     Verbosity level:

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

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

     Output mode flags:

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

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

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

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

     -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).

     Other flags:

     -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  other-
          wise).   This flag  is useful  to  replay counter exam-
          ples  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).

     Output destination:

     outfile
          Where results are written. The output format is  deter-
          mined by the file type, according  to the  table below.
          If  absent or specified  by "-", then results are writ-
          ten  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  exten-
          sion.

          file extension      output format
          --------------------------------------------------------------
           .scn               nd stepper .scn format
           .ktz               .ktz format
           any other          textual output


FILES
     File net.txt,  ndr.txt, tpn.txt, TPN.rng in  directory  for-
     mats  specify  the  syntax of  .net,  .ndr,  .tpn and  .pnml
     net description  files, respectively.  File  formats/scn.txt
     file specifies the .scn format.


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


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   proper-
     ties  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 model-
     checker 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  automati-
     cally 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.



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, selt  relies on
     ltl2ba,  a  tool    described  in   the   paper  below   and
     available  at http://www.liafa.jussieu.fr/~oddoux/ltl2ba

     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.


1. Lexical matters:

     - 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 A. or L.

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

     - The commands are: op, infix, prefix, forget, verb, output,
     source.   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:

                    [] 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

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


2. The initial environment:

     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:

        constants:  T (true), F (false),
                    dead (deadlock property)
                    div (temporal divergence property)
        prefixes:   [] (always), <> (eventually), () (next), - (negation)
        infixes:    /\ (and), \/ (or), => (implies), <=> (equivalent),
                    U (until), V (release), of precedence 0
                    <=, >=, =, of precedence 1,
                    +, of precedence 2
                    *, of precedence 3

     - Then the user defined operators.

     Since the  syntactic classes of atomic  proposition, 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  A (e.g.  A.p1)  are bound  to the  atomic
     proposition with that name with the qualifier removed (e.g. p1);

     - 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 command  (e.g. op) or with 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. A.op, A.-, or A.3);


3. Fixity:

     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:

          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)


4. Commands and effects:

     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):

     exp;
          evaluates LTL expression exp;

     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..3 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).


5. Example commands:

     p1;                 (eqv. p1 >= 1)

     - p1;               (eqv. p1 = 0)

     p1 /\ p2 >= 2;      (eqv. p1 /\ (p2 >= 2))

     op x > y = x >= y + 1;

          (declares arithmetic operator >, in infix form)

     p1+p2;              (eqv. p1+p2 >= 0, eqv. p1 \/ p2)

     p1+p2 > p3;

     p1*p2 = 0;

     infix y follows x = [] (x => <>y);

          (declares logocal operator "follows:, in infix form)

     (t3 \/ p5) follows (t1 /\ p1>=p2);

          (eqv. [] ((t1 /\ (p1>=p2)) => <> (t3 \/ p5)));


FILES
     Files scn.txt and  ktz.scn in directory formats specify  the
     syntax  of  scenario  .scn  files and .ktz transition system
     files, respectively.


SEE ALSO
     nd, tina, plan, struct, ndrio, ktzio


AUTHORS
     Bernard Berthomieu, Pierre-Olivier Ribet,  LAAS/CNRS,  2000-
     2005, Bernard.Berthomieu@laas.fr.

