next_inactive up previous


Synet : A Synthesizer of Distributable Bounded Petri-Nets from Finite Automata
Version 2.0b

Benoît Caillaud

Introduction

Synet is a software package synthesizing bounded Petri-nets, based on the algorithms described in [1,3,4,2]. It also comprizes a new synthesis algorithm based on the computation of extremal rays of polyhedral cones.

A PDF version of this document is also available.

Description of the software package

The package contains several executables and a library:

synet
A tool synthesizing distributable bounded Petri-nets. It uses the Polyhedral library of IRISA or the CPLEX linear programming library of Ilog.
psynet
This is a version of the tool that doesn't require the CPLEX commercial library.
osynet
Native code version of synet, produced with the ocamlopt compiler. Requires the CPLEX library.
qsynet
Native code version of psynet, produced with the ocamlopt compiler. Does not require the CPLEX library.
ocamlsynet
Objective Caml toplevel environment containing all the synet modules. Can be used to develop customized versions of the tool. The CPLEX library is required.
synet.cma
An Objective Caml library containing the various software modules of the tool. The library is provided wih a set of .cmi files which are required at link-time.
synet.cmxa
Same as above, but in native code version.

A couple of utilities are also provided:

distribute
Transforms a distributable Petri-net into an equivalent Petri-net with communication places and transitions.
reachability
Computes the reachability graph of a bounded Petri-net.
draw-net
A Petri-net drawing tool using the ATT Graphviz package.
draw-aut|
An automaton drawing tool using the ATT Graphviz package.

Copyright notice

The Synet package has been first developped in 1996 and 1997 by Benoît Caillaud and Eric Badouel at IRISA, Rennes, France. It has been improved in 1999 by Benoît Caillaud, with the implementation of a new synthesis algorithm based on the computation of extremal rays of polyhedral cones.

The current version of the tool should be considered as a preliminary prototype rather than a stable and robust tool. Therefore it is not freely available and researchers that are willing to use this tool should contact the author (Benoit.Caillaud@irisa.fr).

Requirements

The software requires :

  1. The O'Caml environment version 2.02 or newer.
  2. The libnum rational arithmetic library (distributed with Objective Caml).
  3. GCC version 2.7.2.1 or newer.
  4. The Polyhedral library of Irisa, now maintained by D. Wilde (http://www.ee.byu.edu/~wilde/polyhedra.html).
  5. The GNU make command (sometimes called gmake).
  6. The Graphviz graph visualization software distributed by ATT (http://www.research.att.com/sw/tools/graphviz/).
  7. The CPLEX linear programming library developped by Ilog. This library is not compulsory, however it is strongly recommended.

Compilation and installation

SYNET is known to compile correctly on Sparc/Solaris and Intel-486/Linux systems. However it should compile correctly on most POSIX compliant systems. A port to Windows NT is under way.

How to compile

Two environment variables must be defined:

USE_ CPLEX
Must be set is CPLEX is to be used.
CPLEX_ DIR
If CPLEX is used, this must contain the location of the CPLEX library.

If the default make command is GNU-make:

[balta]bc: make

Otherwise:

[balta]bc: gmake

Installation of the binaries

[balta]bc: cp synet psynet ocamlsynet distribute \
    reachability draw_aut draw_net $BINDIR

Where $BINDIR is the directory where the executables are to be placed.

Command-line syntax

 synet [<options>] <.aut-file-name>

 synet [<options>] -l <.aut-file-name>

 synet [<options>] -d <.dis-file-name> <.aut-file-name> 

 synet [<options>] -r [-d <.dis-file-name>] <.aut-file-name>

Where:

All other possible options are:

Usage: synet { <options> } <filename>
  where <options> ::= <option> { <options> }
        <option>  ::= -d <filename>
                    | -l
                    | -n
                    | -i
                    | -p
                    | -x
                    | -o <filename>
                    | -v <integer>
                    | -q
                    | -e <filename>
                    | -w
                    | -r
                    | -c <filename>
                    | -z <filename>

-d filename
The synthesis is constrained by a mapping of events over a set of processors given in .dis format.
-l
Synthesis modulo equality of languages.
-n
Suppresses minimisation of synthesized nets.
-i
Impure nets are synthesized (-r implies -i).
-p
(b)Only pure nets are synthesized.
-x
The net is visualized using the Graphviz package.
-o filename
The net is stored in file <filename> in .net format.
-v integer
Verbose (debug) mode. Displays the revision number of the tool and some statistics.
-q
Quiet mode: nothing is printed.
-e filename
(a)The synthesized net takes into account the constraints of an environment.
-w
Statistics about the Simplex algorithm are printed at the end.
-r
New algorithm based on the computation of extremal raoys of polyhedral cones.
-c filename
solves only the separation problems listed in file <filename>. This file should contain a list of pairs of states and events of the automaton enclosed by two parenthesis.
-z filename
solves only the separation problems consisting in the transitions of the automaton A' given as parameter which origin state is a state of the automaton A and which destination state is not a state of A. This option is similar to option -c.

The symbol (a)means that the option is not yet implemented. (b)indicates that this option is assumed by default.

Syntax of input and output files

Common definitions

Terminal symbols <nat>, <string> and <ident> respectively represent natural integers, character strings and identifiers in OCaml syntax.

<state-id>     ::= <nat> | <string> | <ident>
<event-id>     ::= <nat> | <string> | <ident>
<location-id>  ::= <nat> | <string> | <ident>
<place-id>     ::= <nat> | <string> | <ident>

Syntax of .aut files

This file format extends the .aut format of Open/Caesar[5] and Aldebaran.

<.aut>       ::= des(<nat>,<nat>,<nat>) <trans-list>
<trans-list> ::= | <trans> <trans-list>
<trans>      ::= ( <state-id> , <event-id> , <state-id> )

Because of a bug in aldebaran that has never been corrected, users are strongly advised to declare initial state as state 0.

Syntax of .dis files

<.dis>         ::= <mapping-list>
<mapping-list> ::= | <mapping> <mapping-list>
<mapping>      ::= ( <event-id> , <location-id> )

Every event of the automaton must have a unique mapping.

Syntax of .cut files

<.cut>         ::= <essp-list>
<essp-list>    ::= | <essp> <essp-list>
<essp>         ::= ( <state-id> , <event-id> )

Every event-state separation problem (essp) must be an essp of the automaton.

Syntax of .net files

<.net>           ::= <statement-list>
<statement-list> ::= | <statement> <statement-list>
<statement>      ::= <location> | <transition> | <place> | <flow>
<location>       ::= location <location-id>
<transition>     ::= transition <event-id> {:: <location-id>} 
<place>          ::= place <place-id> {:= <nat>} {:: <location-id>}
<flow>           ::= flow <place-id> -- { <nat> | # } -> <event-id>
                   | flow <place-id> <- { <nat> } -- <event-id>

Flow arcs of the form flow p - # -> t are inhibitor arcs. They are generated by the distribute command.

A tiny example

File a.aut defines in the Aldebaran syntax a simple but easy to understand automaton:

des(0,7,6)
(0,a,1)
(0,c,2)
(1,b,5)
(1,c,3)
(2,a,3)
(3,d,4)
(5,t,0)

File a.dis contains a location mapping of the events of automaton a.aut over two processes: A and B.

(a,A)
(b,B)
(c,B)
(d,A)
(t,A)

SYNET produces the following output:

localhost[1]% synet -r -o a.net -d a.dis a.aut 
The transition system is separated.
Synthesized net:
  +a-d-t::A
  +c-d::A
  -a+t:=1::A
  +b-t::A
  +a-b::B
  -c-b+t:=1::B
localhost[2]% 

An the Petri net is saved in file a.net:

location B
location A
transition t :: A
transition d :: A
transition b :: B
transition c :: B
transition a :: A
place x_5 := 1 :: B
place x_4 :: B
place x_3 :: A
place x_2 := 1 :: A
place x_1 :: A
place x_0 :: A
flow x_5 ---> b
flow x_5 ---> c
flow x_4 ---> b
flow x_3 ---> t
flow x_2 ---> a
flow x_1 ---> d
flow x_0 ---> t
flow x_0 ---> d
flow x_5 <--- t
flow x_4 <--- a
flow x_3 <--- b
flow x_2 <--- t
flow x_1 <--- c
flow x_0 <--- a

Both the automaton and the Petri can be visualized:

localhost[3]% draw_aut a.aut
--- a.aut ---

localhost[4]% draw_net a.net
localhost[5]% 

The command draw_aut displays the following window:



96


And draw_net displays:



99


The synthesized Petri-net can be directly visualized: synet -r -x -d a.dis a.aut.

Case Study : The INRES Protocol

This section details an application of distributable Petri net synthesis. A correct by construction implementation of a simple transport level communication protocol, the INRES protocol [6], is synthesized using the algorithms presented in the previous sections. For the sake of clarity, the method is first detailed on a simplified version of the protocol, and then applied on the full protocol, however with an increased complexity. The example illustrates a new methodology for distributed program synthesis, based on the algorithms for distributable Petri net synthesis presented briefly in the previous sections and in greater details in [2].


A Simplified Protocol

In this section, we consider a simplified version of the INRES communication protocol [6]. The specification of service of the INRES protocol is given below:

localhost[6]% draw_aut inres-serv.aut



111


For the sake of the exposition, we consider the simplified service described below:

localhost[7]% cat prot.dis
(s,A)
(r,B)
(d,B)
(a,A)
localhost[8]% draw_aut prot.aut



116


The simplified protocol defines the transmission of data between two users user-A and user-B linked to respective protocol entities A and B. Event s means that entity A is given by user-A some data to transmit; event r means that entity B delivers some data to user-B; event d is a disconnection request (located on B); event a is the notification of the disconnection (located on A). With this protocol, data exchanges (words in (sr)*) may take place until a disconnection is requested.

We aim at synthesizing a distributed implementation of this protocol: two processes A and B, communicating with one another through a reliable communication medium. Events s and a are located on process A, while events r and d are located on B. This is defined by the location map l: l(s)=l(a)=A and l(r)=l(d)=B.

We wish to use distributable Petri net synthesis to produce a Petri net implementation of the communication protocol: thus, for every place p of the net, the flow relation F must satisfy: F(p,s)=F(p,a)=0 or F(p,r)=F(p,d)=0.

Unfortunately the automaton specifying the service (shown above) is not isomorphic to the marking graph of any distributable Petri net: event a and state 2 cannot be separated, as it is shown below:

localhost[9]% synet -x -r -d prot.dis prot.aut
Event-state separation failures:
  Event a and state 2 are not separated.
Synthesized net:
  -s+r:=1::A
  +d-a::A
  +a::A
  +s-r::B
  -d/r:=1::B



154


However this can be alleviated by refining the automaton into a weakly bisimilar automaton which is actually the marking graph of a distribuable Petri net. In [7], is advocated an event splitting heuristics for refining non separated automata into separated automata. In our case, the two occurrences of s may be replaced by s1 and s2, and similarly for d, leading to three different refinements. However, none of the refined automata is separated with respect to the restricted set of localizable regions, compatible with the distribution constraints. Even though in the non distributed case event splitting is a systematic method for refining automata into separated automata, it is potentially useless in the distributed case.

As an alternative resort, refinement can be done by inserting silent transitions while keeping weak bisimilarity. In our case, the adequate refinement step consists in replacing transition (3,a,4) by two transitions: (3,t,4) and (4,a,5) (see the automaton below), with silent event t located on process B.

localhost[10]% cat prot_r.dis
(s,A)
(r,B)
(d,B)
(a,A)
(t,B)
localhost[11]% draw_aut prot_r.aut 



170


The refined automaton is then isomorphic to the reachable marking graph of the Petri net shown below. Places and transitions are sorted according to their locations: A on the left and B on the right.

localhost[12]% synet -x -r -d prot_r.dis prot_r.aut 
The transition system is separated.
Synthesized net:
  -s+r:=1::A
  +t-a::A
  +s-r-t::B
  +d-t::B
  -d/r:=1::B



177


The distributable Petri net is then expanded into the Petri net shown below by making communications between processes explicit:

localhost[13]% distribute prot_r.net prot_rd.net
localhost[14]% draw_net prot_rd.net



182183


By distributing its reachable state graph as indicated in [2], with an abstraction from event t and with minimization, one obtains the automata shown below:

localhost[13]% draw_aut prot_rd_A.aut
localhost[14]% draw_net prot_rd_B.aut



190191


It follows from the method that this distributed implementation is behaviorally correct.

The full protocol

As in the previous section, the same method can be used to deal with the full INRES protocol, however with an increased complexity. The protocol to be realized consists in two processes A and B communicating through an asynchronous communication network. The automaton below gives the expected behaviour (specification of service) of the distributed protocol:



197


Events Conreq, Conconf, Datreq and Disind are located on process A, while events Conind, Disreq, Conresp and Datind are located on process B.

It should be noticed that the specification of service of the INRES protocol is not co-deterministic : there are three transitions labelled Disind entering the initial state. However, splitting the occurrences of Disind is not sufficient to secure realizability in a distributed Petri net. A further refinement step has to take place : The specification should be refined into an equivalent one modulo weak bisimulation, shown below. This is done by both event splitting and insertion of a silent transition. Finding the proper location of insertion of the silent transition is guided by intuition solely. In this latter automaton, events Conreq, Conconf, Datreq and Disind1 through Disind4 are located on A ; events Conind, Disreq1, Disreq2, Conresp, Datind and t are located on B.



225


The automaton is realized in the distributable Petri net shown below:



228229


This Petri net yields the communicating automata given below, a correct by construction implementation of the INRES service:



233234


Bibliography

1
E. Badouel, L. Bernardinello, and P. Darondeau.
Polynomial algorithms for the synthesis of bounded nets.
In P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, editors, TAPSOFT'95: Theory and Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 364-378, Aarhus, Denmark, May 1995.

2
E. Badouel, P. Darondeau, and P. Caillaud.
Distributing finite automata through petri net synthesis.
Journal on Foundamental Aspects of Computer Science, 2001.
to appear.

3
E. Badouel and P. Darondondeau.
On the synthesis of general petri nets.
publication interne PI-1061, IRISA, novembre 1996.

4
B. Caillaud.
Application des techniques de synthèse de réseaux de petri bornés à la répartition d'automates réactifs.
In Deuxième congrès sur la modélisation des systèmes réactifs (MSR'99), Cachan, France, mars 1999.

5
H. Garavel.
The Open/Caesar Reference Manual.
VERIMAG, March 1995.

6
D. Hogrefe.
OSI-formal specification case study: the INRES protocol and service.
Technical Report 91-012, University of Bern, 1991.

7
A. Yakovlev.
Designing control logic for counterflow pipeline processor using petri nets.
Formal Methods in System Design, 12:39-71, 1998.

About this document ...

Synet : A Synthesizer of Distributable Bounded Petri-Nets from Finite Automata
Version 2.0b

This document was generated using the LaTeX2HTML translator Version 99.2beta8 (1.43)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -split 0 synet

The translation was initiated by Benoit Caillaud on 2002-03-15


next_inactive up previous
Benoit Caillaud 2002-03-15