---

Manual Reference Pages  - frac (n)

---

NAME

frac - Fiacre to Time transition systems compiler

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

CONTENTS

Synopsis
Description
Options
Frac Limitations
Examples
See Also
Authors

frac [-help]
[-pr | -obs | -hp | -strip]
[-q | -v] [-p | -c | -fcr | -tts | -hippo]
[-flat | -share] [-unsafe] [-O | -g] [-json]
[infile] [outfile] [-o errfile]

frac analyzes a Fiacre description and compiles it into a Time Transition 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.

-help Prints a short description of command line flags.
Input language options:
-pr	Enables properties extensions of the fiacre language: property declarations, assert directives and tag annotations (implicit is outfile has extension tts).
-pr	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 provided by frac but are not part of the Fiacre definition.
Output options:
-q	Quiet operation (default).
-f	Verbose operation.
-p	Just parses the fiacre input.
-c	Parses and checks the fiacre input, no output generated (default).
-fcr	Parses, checks, and pretty-prints the fiacre code, no code generation.
-tts	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.
-hippo	Parses and checks the fiacre code and generates a hippo description suitable for the Hippo runtime engine (in development).
-json	While compiling a fiacre description into a tts, emits a description of the architecture of the fiacre specification (components, types, variables, transitions) in json format.
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, 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 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.
Files options:
infile	The fiacre source. If absent or specified by "-", the fiacre description 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 .tts                    tts description .hippo          hippo description
-o errorfile
	Where error messages are written. By default, errors are printed on standard error.

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