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 | -hp | -strip]
            [-q | -v] [-p | -c | -4mf24mcr | -4mt24mts | -hippo]
            [-flat | -share] [-unsafe] [-O | -g] [-4mj24mson]
            [infile] [outfile] [-o errfile]



1mDESCRIPTION0m
       frac  analyzes a Fiacre description and compiles it into a Time Transi-
       tion System description (extension .tts) suitable for analysis with the
       Tina tools or into a hippo description (extension .hippo) suitable  for
       deployment with the Hippo runtime engine.


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


       -hp    Enables hippo experimental extensions of  the  fiacre  language:
              tasks and events (implicit is outfile has extension hippo).


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


       -strip Parses  but  forgets all fiacre language extensions supported by
              frac, including properties features, probes, observers and hippo
              extensions.  frac -f -strip prints a fiacre description strictly
              conforming to the fiacre language definition and usable in other
              Fiacre tools; properties, observer and hippo features  are  pro-
              vided 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.


       -hippo Parses and checks the fiacre code and generates a hippo descrip-
              tion suitable for the Hippo runtime engine (in development).


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




       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
              .hippo         hippo 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,   Silvano   dal  Zilio  and  Pierre-Emmanuel  Hladik  LAAS/CNRS,
       2007-2020, {Bernard.Berthomieu}@laas.fr.



Tina Tools                       Version 2.6.0                         4mfrac24m(n)
