frac - Fiacre to Time transition systems compilerPart of Tina Toolbox for analysis of Petri nets and Time Petri nets.
Synopsis
Description
Options
Frac Limitations
Examples
See Also
Authors
frac [-help]
[-q | -v] [-o errfile] [-p | -c | -f | -t]
[-flat | -share] [-unsafe] [-O | -g] [-strip] [-arch]
[infile] [outfile]
frac analyzes a Fiacre description and compiles it in a Time Transition System description (extension .tts) suitable for analysis with the Tina tools.
-help Prints a short description of command line flags.
-q | -v Verbosity level (default -q).
Operating mode options:
-p Just parses the fiacre code.
-c Parses and checks the fiacre code, no print nor code generation (default).
-f Parses, checks, and pretty-prints the fiacre code, no code generation.
-t Parses and checks the fiacre code and generates a tts description 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.
-o errorfile Where error messages are written. By default, errors are printed on standard error.
infile The fiacre source. If absent or specified by "-", the fiacre dscription 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 according to the operating mode flag (except if -t since tts descriptions cannot be written on standard output). If both an outfile and some operating mode flag are present, then the format defined by the operating mode flag supersedes that determined by the outfile extension.
file extension output format -------------------------------------------------------------- .fcr fiacre code .tts tts description
Code generation options:
-share | -flat Enables or disables sharing of state components (default enabled). As of version 1.6.0, frac generates by default code allowing the states computed to possibly share some substates. If sharing is enabled, that the decision to share or not follows from some heuristics 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 difficult cases.
-O | -g Optimize (default) or not (-g) the code generated. Optimizations include removal of variables found not to contribute to the state value nd removal of redundant transitions.
Other options:
-strip Forget priority declarations, assert directives and tag annotations from fiacre. frac -f -strip prints a fiacre description strictly conforming to the fiacre language definition and usable in other Fiacre tools (properties and assert directives are features provided by frac but not part of the Fiacre definition).
-arch While compiling a fiacre description into a tts, prints on standard output the architecture tree of the specification (the nodes are the names of components and processes instances).
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").
frac -h frac -f app.fcr [out.fcr] frac app.fcr app.tts
nd(n), sift(n), plan(n), struct(n), ktzio(n), ndrio(n), selt(n), muse(n), pathto(n), play(n), formats(n)
Bernard Berthomieu, with contributions by Rodrigo Saad, Alexandre Hamez and Silvano dal Zilio LAAS/CNRS, 2007-2012, {Bernard.Berthomieu}@laas.fr.
Tina Tools | frac (n) | Version 2.0.0 |