psf [ -v ] [ -s ] [ -t ] [ -i ] [ -c ] [ -m modulename ]
               [ -o outputfile ] [ -L library-path ] [ filename ...  ]
     psf -l|-x|-X [ -v ] [ -G format ] [ -m modulename ]
               [ -o outputfile ] [ -L library-path ] [ filename ...  ]
     psf -S [ -f ] [ -v ] [ -o outputdirectory ] filename ...


     Psf  compiles the Process Specification language PSF to the Tool Inter-
     face Language TIL.

     Psf searches libraries for PSF modules complementing those in the file-
     names  and  then (optionally) submits the result in the proper order to
     the various phases of the PSF-to-TIL  compiler.   A  full  run  of  psf
     passes  through  the  phases described below.  However, during phases 3
     through 7, psf checks the last modification time of the file to be pro-
     duced  and  if  that  file  is  found to exist and to be newer than the
     file(s) to be compiled, that compilation step is skipped,  except  when
     the  -c option is used, in which case that file is removed and the com-
     pilation step is forced.

     The translation phases are:

     1.  Library searching
         During this phase, psf maintains two lists: a  list  F  of  modules
         found  in  the  files read so far, and a list N of modules that are
         imported by a module on list F but have not yet been  found.   Ini-
         tially,  the  module  name specified with the -m option, if any, is
         placed on list N.  Next, the files named on the  command  line  are
         scanned  and any modules found in those files are placed on list F,
         or moved from N to F, as appropriate.  Next, if N is not empty (and
         the  -S option is not used), psf takes a module name in N, adds the
         suffix .psf (or the suffix specified in the  PSFSUFFIX  environment
         variable, if set) to the module name and searches the library for a
         file with that name.  The library consists of the directories named
         in  the  PSFPATH environment variable (or the current directory, if
         PSFPATH is not set).  If such a  file  is  found,  it  is  read  as
         described  above.   If  no  such file exists, the module remains on
         list N.  This procedure is repeated until it has  been  applied  to
         all  names remaining on list N.  Then, if N is still not empty, psf
         exits with an error message.

     2.  Sorting
         The modules are sorted so that, if module A imports module B,  then
         B  occurs  before A on the list produced in this phase.  If such an
         order can not be found, psf exits with an  error  message.   Other-
         wise,  the  list  is cut off after the module specified with the -m
         option, if any.  This phase is skipped if the -S option is used.

     3.  Splitting
         Each file scanned during phase 1 that contains more than  one  mod-
         ule,  is  split into files containing one module each.  If the file
         four cases:

         (a) A  symbolic  link  exists among the intermediate files with the
             target name.  If this link points to an existing file, then psf
             assumes  that it points to the correct file in the library.  If
             this assumption is incorrect, use the  -i  option.   When  this
             option  is  used, psf removes the symbolic link and defaults to
             case (d), below.

         (b) A file exists with the target name.  If this file is newer than
             the corresponding PSF file, no action is taken, otherwise it is
             removed and psf goes on to try cases (c) and (d).

         (c) The PSF file was found in a library directory and a  file  with
             the  target name exists in the same directory and the -i option
             was not used.  In this case, psf assumes that this file is  the
             intended  translation  and  creates a symbolic link pointing to
             it.  If this assumption is wrong, complain to the person  main-
             taining the library and/or use the -i option.

         (d) If all else fails, psf invokes psf_mtil(1L).

     5.  Compiling MTIL to ITIL
         This  is  analogous to phase 4, except that in case (b) there is an
         extra condition that the ITIL translations  of  the  modules  being
         imported  by  the  one  being considered must not be older than the
         ITIL translation found.  In case (d), psf_itil(1L) is invoked.

     6.  Compiling ITIL to TIL
         This is done by invoking psf_til(1L) unless the output file already
         exists and is not older than the ITIL file being translated.

     7.  Converting sorts to sets
         (Only if the -s option is used.)  The current version of sim(1L) is
         unable to deal with the sum (s in S,  ...  )  construct,  in  cases
         where S is a sort.  To overcome this problem, simpp(1L) is invoked.
         This phase is skipped if the -s option is not used or if the output
         file exists and is not older than the input file.

     8.  Checking the Term Rewrite System
         (Only if the -t option is used.)  Some sets of equations do specify
         an initial algebra, but do not form a usable  Term  Rewrite  System
         when  read  as  rewrite rules.  To flag some (but unfortunately not
         all) such sets, trs_check(1L) is invoked.  This will evoke an error
         message  if  a problem is found.  No files are generated or removed
         in this phase.  This phase is skipped if the -t option is not used.


     -c  Whenever  psf  finds  that  a  file it is about to generate already
         exists, the existing file is removed.  Moreover,  after  successful
         compilation,  all  intermediate  files  are removed.  The directory
         which used to contain those files is also removed, provided it  has
         and remove any symbolic links pointing into the library.

     -l  After  phase  2,  list all modules and the files in which they were
         found in the order determined in phase 2.  Psf exits after  produc-
         ing this listing.

     -L library-path
         Specifies  the libraries to be searched during phase 1, as a colon-
         separated list of directories.  Overrides the  PSFPATH  environment

     -m modulename
         Defines  modulename  to  be  the target module.  The default target
         module is the last module in the ordering established during  phase

     -o outputfile
         Defines  the  name  of  the output file.  The default is module.til
         where module is the target module, unless either the -G or  the  -l
         or  the  -x  or the -X option is used, in which case the default is
         standard output.  However, when the -S option is used, the argument
         of  the -o option is taken to be the name of the directory in which
         the output files are to be generated.  This directory  is  created,
         if necessary.

     -s  Invoke simpp(1L) in translation phase 7.

     -S  Split  mode.  Input files are split into separate files, created in
         the output directory.  The library is ignored.  No further process-
         ing takes place.

     -t  Invoke trs_check(1L) in translation phase 8.

     -v  Verbose  mode.   Print messages on standard output, indicating what
         translation steps are being taken.  Also prints a version number.

     -x  Extraction mode.  Copy all modules in the order determined in phase
         2  to  the  outputfile  specified with the -o option, if any, or to
         standard output otherwise.  psf exits after printing all modules.

     -X  Limited extraction.  Similar to the -x option, but modules found in
         libraries  known  by their absolute path name are not copied.  This
         would typically exclude modules imported  form  various  libraries.
         If  you  want to include modules from your private library into the
         output produced in this mode,  include  a  relative  path  to  that
         library in the PSFPATH environment variable.


     Diagnostics are meant to be self-explanatory.  Most diagnostics are not
     produced by psf itself, but by various translators it invokes.



     PSFBINDIR      Directory  in  which  the  psf_mtil(1L),  mtil_itil(1L),
                    itil_til(1L),  simpp(1L),  and  trs_check(1L) executable
                    images can be found.  Default is /home/psf/bin.

     PSFOPTIONS     Option letters of options to be set by default.  A lead-
                    ing - is optional.

     PSFPATH        Colon-separated  list of directories to be searched dur-
                    ing phase 1.  Default is .   (i.e.  the  current  direc-
                    tory).  Including relative path names other than .  into
                    PSFPATH may lead to unexpected results when used in con-
                    junction with the cd(1) command.

     PSFSUFFIX      Suffix  to be appended to a module name to form the cor-
                    responding file name.  Default is .psf.  Note  that  the
                    PSFSUFFIX must include a period, if such is desired.

     PSFTMPDIR      Directory  in  which  all  intermediate  files are to be
                    stored.  If this directory does not exist,  it  is  cre-
                    ated.   Default is taken from a file named .psfrc in the
                    current directory, if one exists.  If not, it is created
                    and  a  name of the form /tmp/psf?????  is generated and
                    stored into it.  It  is  generally  inadvisable  to  set
                    PSFTMPDIR to an existing directory containing files with
                    names ending in .psf (or  the  value  of  PSFSUFFIX,  if
                    set),  since  those  files  are likely to be overwritten
                    during translation phase  1,  or  removed  when  the  -c
                    option  is used.  Currently, psf refuses to run when the
                    directory determined via the algorithm above appears  on
                    the PSFPATH (v.s.) list.

     TILSUFFIX      Suffix  to be appended to the target module name to form
                    the output file name when the -o  option  is  not  used.
                    Default  is  .til.   Like  PSFSUFFIX,  this  value  must
                    include a dot, if such is desired.


     .psfrc         Contains the name of the directory containing all inter-
                    mediate files, unless the PSFTMPDIR environment variable
                    is set.

     /tmp/psf?????  Default name for the directory containing the intermedi-
                    ate files.


     psf_mtil(1L),   psf_itil(1L),  psf_til(1L),  simpp(1L),  trs_check(1L),
     sim(1L),  trs(1L),  psftc(1L),   asff(1L),   dot(1L),   graphplace(1L),

     dot(1L) is part of the package GraphViz, which can be found on WWW

     does  not check time stamps in cases 4(c) and 5(c).  On the other hand,
     this implies that care must be taken to replace all relevant files when
     updating  a module.  If the person maintaining the library has acciden-
     tally forgotten to update some .mtil or files, use the -i  option  (and


     Hans Mulder (Technical University Eindhoven)
     Bob Diertens (University of Amsterdam)


     If  a  data  operator  named  “|”  exists  and one wishes to include an
     expression involving it as an element of a set, then the operator  sym-
     bol must be inside a pair of parenthesis, i.e.

               sets of s
                 t = { x|y | x in s, y in s}

     won’t work; one has to say:

               sets of s
                 t = { (x|y) | x in s, y in s}

     Phase  5  fails to check that the first argument of the encaps and hide
     operators has the type set of atoms.

     Phase 5 does not always obey the origin rule.  Sometimes  it  fails  to
     identify  sorts  pronounced  equal  by the origin rule and sometimes if
     fails to report an error when the origin rule is violated.

     Phase 5 fails to report an error when the right hand side of a  process
     definition contains an unbound variable.

     Phase  5  fails to report an error when an object is being renamed that
     does not occur in the visible signature of the module being imported.

     One would expect to describe nested parameter  binding  by  using  con-
     structs of the form

               imports a {p bound to b {q bound to c}}.

     Psf  correctly  diagnoses  this as a syntax error.  The official way to
     express nested binding is

               imports a {p bound to b q bound to c}.

     (According to the definition in [BHK], module a  inherits  parameter  q
     from  module  b just in time to have it bound this way.)  This fails to
     work, due to a bug in phase 5.

     Phase 5 fails to report an error when a data module imports  a  process
     Simpp(1L), is always invoked with the -n and -s options.   This  should
     be optional.

     There  is  no  way  to unset options set via the PSFOPTIONS environment

PSF-Toolkit 11 October 1995 psf(L)