SYNOPSIS
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 ...
DESCRIPTION
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.
OPTIONS
-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
variable.
-m modulename
Defines modulename to be the target module. The default target
module is the last module in the ordering established during phase
2.
-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
Diagnostics are meant to be self-explanatory. Most diagnostics are not
produced by psf itself, but by various translators it invokes.
EXIT STATUS
ENVIRONMENT
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.
FILES
.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.
SEE ALSO
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),
daVinci(1L).
dot(1L) is part of the package GraphViz, which can be found on WWW
<URL:http://www.research.att.com/orgs/ssr/book/reuse/>.
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
complain).
AUTHORS
Hans Mulder (Technical University Eindhoven)
Bob Diertens (University of Amsterdam)
BUGS
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
module.
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
variable.
PSF-Toolkit 11 October 1995 psf(L)