Case Studies
- The SIP Protocol
- The PGM Protocol
- Specification documents
- Starting point: the France Telecom modeling
- Some namming an content
conventions for the files modeling PGM. Proposal
by Paris, to be approved.
- Very simple models, with only one loss of one ODATA
- The very
simple model of PGM, starting point for future
studies, in IF+macros, by Paris.
- The very
simple model of PGM with communication delay,
the very simple model in with each communication buffer is
augmented by a fixed delay, in IF+macros, by Paris.
Seem to be bugged...
- The very
simple model of PGM with queues, in IF+macros, by
Paris and Grenoble.
- The very
simple model of PGM with queues, lossy sender, in
IF+macros, by Paris and Grenoble (same code as the very
simple model of PGM with queues, but losses are done by
the sender and not the node)
- The
Sender-Receiver with queues, lossy sender , in IF+macros, by
Paris and Grenoble. (same code as the very simple model of
PGM with queues, lossy sender, without the node)
- Bugs: There where a big bug
on the previous distributed version of the very
simple model of PGM. Download the new online
version 1.4.
- More complex systems, where multiple losses are enabled.
- The multiple
loss PGM, a modeling with queues and arrays that
handle multiple losses, in IF+macros, by Paris and
Grenoble.
- The disturbed
multiple loss PGM, the same as the multiple
loss augmented with a chaotic receiver in
parallel with the normal one, in IF+macros, by Paris and
Grenoble.
- The modeling in
promela by Edinburgh.
- Warning: reset semantics
The semantics of the reset
operator in IF is not the same for all operator. For the
IF tools, it disables a clock, for the TReX, it assigns
values 0. Then, a new operator RAZ
has been introduced. Then, RAZ(X)
as to be replaced by set X:=0
or reset(X) (with a macro
parser, like cpp or m4 or the Search/Replace
function of your editor)