4mfrac24m(n)                                                                4mfrac24m(n)

1mNAME0m
       frac - Fiacre to Time transition systems compiler

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


1mSYNOPSIS0m
       1mfrac 22m[-4mh24melp]
            [-pr | -obs | -strip]
            [-q | -v] [-p | -c | -4mf24mcr | -4mt24mts]
            [-flat | -share] [-unsafe] [-O | -g] [-4mj24mson]
            [-selt] [-muse] [-scan] [infile] [outfile] [-o errfile]



1mDESCRIPTION0m
       frac analyzes a Fiacre description and compiles it in a Time Transition
       System description (extension .tts) suitable for analysis with the Tina
       tools.


1mOPTIONS0m
       -4mh24melp Prints a short description of command line flags.



       1mInput language options:0m


       -pr    Enables  properties  extensions of the fiacre language: property
              declarations, assert directives and tag annotations (implicit is
              outfile has extension tts).


       -obs   Enables probes and observers fiacre extensions (for developers).


       -strip Parses but forgets all fiacre language extensions  supported  by
              frac, including properties features, probes and observers.  frac
              -f -strip prints a fiacre description strictly conforming to the
              fiacre  language  definition  and  usable in other Fiacre tools;
              properties, probes and observer features are  provided  by  frac
              but are not part of the Fiacre definition.



       1mOutput options:0m


       -q     Quiet operation (default).


       -f     Verbose operation.


       -p     Just parses the fiacre input.


       -c     Parses  and  checks  the  fiacre input, no output generated (de-
              fault).


       -4mf24mcr   Parses, checks, and pretty-prints the fiacre code, no code  gen-
              eration.


       -4mt24mts   Parses  and  checks the fiacre code and generates a tts descrip-
              tion suitable for analysis by the Tina tools (after compilation,
              see below).

              A tts description is a directory (file.tts) containing at least:
              - file.net, containing the description of a Priority
                Time Petri net;
              - file.c, containing a description of the data processing
                synchronized with the net, and obeying the Tina TTS API.

              For analysis by Tina, file file.tts/file.c mut be compiled  into
              a  shared  library  (extension .so on Linux/Unix, .dylib on Mac,
              .dll on Windows).  The frac distributions include a Makefile for
              this task. The code generated requires gcc as C compiler.


       -4mj24mson  While compiling a fiacre description into a  tts,  emits  a  de-
              scription  of the architecture of the fiacre specification (com-
              ponents, types, variables, transitions) in json format.


       1mVerification options:0m


       -t     Generate .ltl file for checking SE-LTL properties with tool selt
              (default).  (check Release Notes for details).


       -se    Generate in addition a .mmc file for checking mu-calculus  prop-
              erties  with  tool  muse  (as of version 2.8.0).  (check Release
              Notes for details).


       -n     Generate in addition a .rch file for checking reachability prop-
              erties with toolscan (as  of  version  2.8.0).   (check  Release
              Notes for details).


       1mCode generation options:0m


       -share | -flat
              Enables  or  disables  sharing  of state components (default en-
              abled). As of version 1.6.0, frac generates by default code  al-
              lowing the states computed to possibly share some substates.  If
              sharing  is  enabled,  then the decision to share or not follows
              from some heuristic decisions by frac.


       -unsafe
              Fiacre allows to write share variables everywhere, at  the  risk
              of  write  interferences.   Frac applies a conservative check to
              prevent concurrent assignements of shared variables and  rejects
              programs  not  passing  this test. Flag -unsafe transforms these
              interference failures into simple warnings for handling the dif-
              ficult cases.


       -O | -g
              Optimize  (default) or  not  (-g) the   code  generated.   Opti-
              mizations  include   removal  of   variables found  not to  con-
              tribute to  the state value nd removal of redundant transitions.




       1mFiles options:0m


       infile The fiacre source. If absent or specified by "-", the fiacre de-
              scription is read on standard  input.


       outfile
              Output destination. The output format is determined by the  file
              type,  according   to  the  table below. If  absent or specified
              by "-", then the results are written on standard output  accord-
              ing  to the operating mode flag (except if -t since tts descrip-
              tions cannot be written on standard output). If both an  outfile
              and some operating mode flag are present, then  the  format  de-
              fined  by  the operating mode flag supersedes that determined by
              the outfile extension.

              file extension      output format
              --------------------------------------------------------------
              .fcr           fiacre
              .tts           tts description


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



1mFRAC LIMITATIONS0m
       The following limitations of frac currently hold:

       - the main process/component should be closed (no parameters
         allowed);
       - while statements may not contain "to" statements and must
         be deterministic (no "any" nor "select" statements);
       - init statements must be deterministic;
       - any input communication offer should match some output
         offer (no "open inputs").


1mEXAMPLES0m
       frac -h
       frac -f app.fcr [out.fcr]
       frac app.fcr app.tts



1mSEE ALSO0m
       nd(n),  sift(n),  plan(n),  struct(n),  ktzio(n),  ndrio(n),   selt(n),
       muse(n), pathto(n), play(n), formats(n)



1mAUTHORS0m
       Bernard Berthomieu, with contributions by Rodrigo Saad, Alexandre Hamez
       and       Silvano       dal      Zilio      LAAS/CNRS,       2007-2020,
       {Bernard.Berthomieu}@laas.fr.



Tina Tools                       Version 2.6.0                         4mfrac24m(n)
