Avantssar's CL-Atse. Input type: Specification file: (UTF-8)

Options for CL-Atse:
%% Hello, this is the WebCassis services provider, nice to meet you.
%% Running : /var/lib/tomcat6/webapps/WebCassis/BIN/cl-atse --help [limit 10s]

      European Project AVANTSSAR's
       &European Project AVISPA's
    ___           __  _____  __   ___   
   |    |        |  |   |   |    |      
   |    |    --- |--|   |    --  |--    
   |___ |___     |  |   |    __| |___   

    Version 2.5-19 (2012-octobre-11)    

Usage  :  cl-atse [options] [-f file] [files]

  [files]  Name of the IF/ASLANv1 files to process (default is standard input)
           Note : HLPSL files allowed if hlpsl2if is available. Multiple files allowed.
  -f file  Name of a specification file to process. Same as [files].
  -u       Do not take term types into account.
  -o       Write the attack to file.atk
  -v       Print more output informations, in the avispa O.F. (same as '--of if+').

Expert/Long options :

  --nb n    (int) Maximum number of iterations per ASLan transition rule. (default is 3 for IF, 1 for ASLAN).
            WARNING: This option must be manually increased if no attack is found. No heuristic for a max. bound.
            With --lvl 2 : this corresponds to nb. of role iterations, or loops at ASlan++ level;
            With --lvl 0 : this is the nb. of times each transition can be run in any attack trace.
  --free    Uses a free pairing symbol (default for the typed model).
  --assoc   Uses an associative pairing symbol (default for the untyped model).
  --typed   Use term types as defined in the spec. (default).
  --untyped Do not take term types into account.
  --short   Perform breath-first search (minimal attack).
  --of str  Select the output format and it's level of verbosity. Default is 'if', choices are :
     aslan  Standard output format from the Avantssar project, very concise;
     if     Standard output format from the Avispa project, with step details;
     if+    Same as 'if' but also shows the protocol specification as it was understood;
     if++   Same as 'if+' but show things exactly as they were analysed (after simpl.);
     if-    Shows a quick view of the attack trace, if one is found;
     brief  Shows an even more concise view of the attack trace and analysis result.
  --out     (string) Write the attack to some specific file
  --dir d   (string) Output directory to use with -out
  --ns      Do not simplify the input file (complete trace).
  --opt     Try to replace hashing by tokens. (slower or faster dep. on protocol) (Default for IF).
  --noopt   Do not try to replace hashing by tokens. (slower or faster dep. on protocol) (Default for ASLAN).
  --verbose Print more output informations, in the avispa O.F. (same as '--of if+').
  --noexec  Do not Analyse, i.e. only write the specification the way it was understood.
  --col n   (int) Number of column in the output (default 80, disabled with -1).
  --bench   Benchmark output format (very concise).
  --aslan   Expect AVANTSSAR's ASLAN in input and tries to follow ASLAN in output.
  --if      Expect AVISPA's IF as input; Not default anymore since AVANTSSAR.
  --lvl n   (int) Level of protocol rebuilding: 0 for none; 2 for full processing (default).
  --store   When an attack is found, store the current state in a .state file.
  --split   Create a directory with the spec's name and fill it with >100 sub state files,
            so that many different instances of cl-atse can analyse them in parallel.
  --hc str  Choses a strategy for Horn clauses deductions. Default is btd+, choices are :
     btd    Backward TopDown strategy, i.e. backward strategy with depth-first recursivity;
     blr    Backward LeftRight strategy, i.e. backward strategy with breadth-first recursivity;
     btd+   Backward TopDown plus heuristical choice of the fact to descend into first.
  --not_hc  Extend tests for negtive constraints w.r.t Horn Clauses.
  --sets    Follows the Aslan semantic by treating all facts as objets in a set (not multiset).
            By default, all facts (and contains) are in multisets, i.e. without any rule 'fact.fact = fact'.

Debugging options :

  --max n   (int) Forced activation of -lvl 0 if this number of steps is reached (default 80).
  --vv      Print even more output and term informations (debug). Same as '--of if++'.
  --tab     Write the correspondence table (debug).
  --par     Write the parser output (debug).
  --heavy   Extend the search for unforgeable atoms during simplification.
  --debug   Write debuging informations for Read.ml (debug).
  --split   Use the --split option on hlpsl2if for hlpsl input file.
  --states  Shows all internal system states of the analysis.
  --trace   Use -trace "Short trace" to follow one particular trace.
  --reverse Inverse the order of protocol steps in the read_aslan module.
  --unforgeable Computes a list of unforgeable terms before analysis.

Miscellaneous options :

  --version Print the version number.
  --licence Print the CL-Atse's disclaimer (licence).
  -help  Display this list of options
  --help  Display this list of options

%% Job terminated successfully.