We present the command line tool SYNOPS. It allows the term-based construction of partial languages consisting of different kinds of causal structures representing runs of a concurrent system: labeled directed acyclic graphs (LDAGs), labeled partial orders (LPOs), labeled stratified directed acyclic graphs (LSDAGs) and labeled stratified order structures (LSOs). It implements region based algorithms for the synthesis of place/transition nets and general inhibitor nets from behavioural specifications given by such partial languages.
Synthesis of Petri nets from behavioral descriptions has been a successful line of
research since the 1990s. There is a rich body of nontrivial theoretical results and
there are important applications in industry, in particular in hardware design
[
The synthesis problem is the problem to construct, for a given behavioral specification, a Petri net such that the behavior of this net coincides with the specified behavior (if such a net exists). There are many different methods which are presented in literature to solve this problem for different classes of Petri nets. They differ mainly in the Petri net class and the model for the behavioral specification considered. On the other hand, all these methods are based on one common theoretical concept, the notion of a region of the given behavioral specification.
In this paper, we present a new tool for the region based synthesis of Petri nets from behavioral specifications given by so called partial languages. A partial language is a set of finite causal structures, where a causal structure represents causal relationships between events of a finite run of a concurrent system. If the concurrent system is given by a Petri net, events represent transition occurrences. Expressible causal relationships are for example direct and indirect causal dependency, concurrency and synchronicity of events. The tool supports different kinds of causal structures, describing different semantics of different Petri net classes and having different expressiveness and interpretation: – Labelled acyclic graphs (LDAG): LDAGS represent runs underlying process nets of place/transition-nets. They are used to specify all direct causal dependencies caused by token flow between transitions occurrences. – Labelled partial orders (LPO): LPOs represent non-sequential runs of place/transition-nets. They are used to specify all ”earlier than”-relations (which we call indirect causal dependencies) between transitions occurrences. Unrelated events are called concurrent. LPOs are transtively closed LDAGs. – LDAGs extended by synchronicity (LSDAG): LSDAGs represent runs underlying process nets of general inhibitor nets according to the a-priorisemantics. They are DAGs extended by ”not later than”-relations between events. A cycle of ”not later than”-relations between events represents a synchronous step of events, i.e. it is possible to distinguish between concurrency and synchronicity. – Labelled stratified order structures (LSO): LSOs represent non-sequential runs of general inhibitor nets according to the a-priori-semantics. LSOs are transitively closed LSDAGs.
This means, by a partial language the set of runs of a Petri net for different
Petri net classes and different net semantics can be specified. It depends on the
application area, which Petri net class and which kind of causal structures are
appropriate or available for solving a concrete synthesis problem. In [
Infinite behaviour can be represented by an infinite set of finite runs, i.e. an infinite partial language (where one finite run can be the prefix of another finite run).
The tool allows to construct finite partial languages (allowing to specify
finite behaviour) of the mentioned types via command line using a term-based
notation. This term based notation allows to compose runs from a set of basic
runs by several composition operators (sequential and parallel composition and
iteration). For the synthesis of nets the tool implements algorithms based on a
technique using so called token flows developed in the project SYNOPS [
The paper is organized as follows. In section 2 we briefly recall some basic mechanism of region-based synthesis. In section 3 we present some new technical developments for the synthesis of place/transition nets from finite sets of LPOs. In section 4 we describe the architcture and the components of the tool. In particular we describe how to specify finite sets of LPOs, LDAGs, LSDAGs and LSOs via command line. In section 5 we present some case studies involving the implemented algorithm for the synthesis of place/transition nets from finite sets of LPOs. In section 6 we briefly compare the tool to other synthesis tools. In section 7 we give a brief outlook onto current and further developments and in section 8 we give some hints for downloading and testing the tool. In this section, we denote the set of runs of a net N by L(N ). L(N ) is called the language generated by N . We formally consider the following synthesis problem w.r.t. different Petri net classes and different types of partial languages:
That means, we search for an exact solution of the problem. Such an exact solution may not exist, i.e. not each language L is a net language.
The classical idea of region-based synthesis is as follows: First consider the net N having an empty set of places and set of transitions T . This net generates each run in L (i.e. L ⊆ L(N )), because there are no places restricting transition occurrences. But it generates much more runs. Since we are interested in an exact solution, we restrict L(N ) by adding places.
There are places p, which restrict the set of runs too much in the sense that L \ L(N ) 6= ∅, if p is added to N . Such places are called non-feasible (w.r.t. L). We only add so called feasible places p satisfying L ⊆ L(N ), if p is added to N (Figure 1). The idea of region-based synthesis is to add all feasible places to N . The resulting net Nsat is called the saturated feasible net. On the one hand, Nsat has by construction the following very nice property: L(Nsat) is the smallest net language satisfying L ⊆ L(Nsat). This is clear, since L(Nsat) could only be further restricted by adding non-feasible places. This property directly implies that there is an exact solution of the synthesis problem if and only if Nsat is such an exact solution. Moreover, if there is no exact solution, Nsat is the best approximation to such a solution ”from above”.
On the other hand, this result is only of theoretical value, since the set of feasible places is in general infinite (Figure 2). Therefore, for a practical solution, a finite subset of the set of all feasible places is defined, such that the net Nfin defined by this finite subset fulfills L(Nfin) = L(Nsat). Such a net Nfin is called finite representation of Nsat. In order to construct such a finite representation, in an intermediate step a feasible place is defined through a so called region of the given language L.
The described approach is common to all known region-based synthesis
methods (see Figure 3) and can be applied to all kinds of partial languages. In
particular, this approach can be applied to different notions of regions (of a partial
language) and of finite representations Nfin. There are two types of definitions of
regions and two types of definitions of finite representations, covering all known
region-based synthesis methods [
Experiments in the first phase of the project SYNOPS showed that the so
called separation representation produces Petri nets which are simpler and more
compact, especially having less places [
For computing the separation representation, first all so called wrong
continuations of L are constructed. The set of wrong continuations represents the
behaviour which is not specified. Briefly, a wrong continuation consists of a
prefix of some specified run together with a follower step of transition occurrences
extending a specified run by one additional event. Figure 4 shows examples of
wrong continuations. For every wrong continuation, the synthesis algorithm tries
to compute a place prohibiting the wrong continuation (for details on how to
compute such a place we refer to [
The synthesized Petri net depends on the considered order of wrong continuations, since places often prohibit more than one wrong continuation. It is advantageous to compute such places first, which prohibit much wrong continuations. Therefore several new methods were implemented for constructing an appropriate order of wrong continuations. In the next Section 3 some technical details of the implemented synthesis algorithm are described. 3
In this section we briefly introduce wrong continuations formally and describe some newly developed ideas optimizing the synthesis procedure.
A multiset over a set T is a function m : T → N. A step T is a multiset over T . Addition + on multisets is defined by (m + m0)(a) = m(a) + m0(a). We write Pa∈T m(a)a to denote a multi-set m. The relation ≤ between multiset is defined through m ≤ m0 ⇐⇒ ∀a ∈ T (m(a) ≤ m0(a)). An LPO over a set T is a tuple (V, <, l) where V is the finite set of events, <⊆ V × V is a partial order, and l : V → T is a labelling function. For W ⊆ V we define the multiset l(W )(a) = |{v ∈ W | l(v) = a}|. An LPO (W, <, l) is a prefix of an LPO (V, <, l) if W ⊆ V and (w ∈ W ) ∧ (v < w) ⇒ (v ∈ W ). A step sequence w = α1 . . . αn can be represented by an LPO, where each step αi corresponds to a set of pairwise unordered events and events from different steps are ordered according to the step sequence. A step sequence σ is a step linearization of an LPO (V, <, l), if the partial order representing σ contains <. For example, the step sequences a(b + c)a(b + c), ab(a + c)(b + c) and aba(b + 2c) are step linearizations of the LPO shown in Figure 5.
Throughout this section, let L be a prefix closed partial language of LPOs. We denote Lstep the set of all step-linearizations of LPOs in L. Since lpo ∈ L is a run of a net N if and only if each step linearization of lpo is a step execution of N , wrong continuations are defined formally as step sequences which extend elements from Lstep by one event as follows: Definition 1 (Wrong Continuation). Let σ = α1 . . . αn−1αn ∈ Lstep and t ∈ T such that wσ,t = α1 . . . αn−1(αn + t) 6∈ Lstep, where αn is allowed to be the empty step. Then wσ,t is called wrong continuation of L.
We call α1 . . . αn−1 the prefix and αn + t the follower step of the wrong continuation.
To prohibit a wrong continuation, one needs to find a feasible place p such that after occurrence of its prefix there are not enough tokens to fire its follower step. A prefix α1 . . . αn−1 of a wrong continuation stepwise linearizes a prefix of an LPO in L. A follower step of such a LPO-prefix can constructed by taking a subset of its direct successor in the LPO and add an event with a new label. This means, a wrong continuation can be represented on the level of LPOs, where wrong continuations having the same follower step and whose prefixes stepwise linearize the same LPO-prefix need not be distinguished. For example a(b + c)a(b + c)a, aba(2b + c) and aba(a + c) are wrong continuations of the LPO shown in Figure 5. Their representations on the level ofs LPOs are shown in Figure 4 (from left to right).
Since the follower marking after the occurrence of a prefix of a wrong continuation only depends on the number of occurrences of each transition (but not on their ordering), the following statement holds: Proposition 1. Let wσ,t = α1 . . . αn−1(αn + t) be a wrong continuation and σ0 = α10 . . . αm0−1αn ∈ Lstep satisfying α1 + . . . + αn−1 = α10 + . . . + αm0−1. Then wσ,t can be prohibited it and only if wσ0,t can be prohibited.
That means in particular, for storing the set of all wrong continuations it is enough to construct all pairs (l(W ), l(S)), where (W, <, l) is a prefix of some LPO in L and S is a subset of direct successors of (W, <, l) extended by an additional event. For example, the wrong continuation a(b + c)a(b + c)a is stored in the form (2a + 2b + 2c, a). Moreover, the follower steps of wrong continuations with equivalent prefixes need to be merged.
We now define an order on the set of wrong continuations.
Definition 2 (More restrictive wrong Continuation). A wrong continuation wσ,t is more restrictive than a wrong continuation wσ0,t0 , if the following holds: If wσ,t is not a step execution of a place/transition net N , then wσ0,t0 is not a step execution of N .
If it is possible to forbid a wrong continuation, then automatically all less restrictive wrong continuations are forbidden, too. This means, if one considers more restrictive wrong continuations first, then less places are computed and runtime is faster.
If two wrong continuations have equivalent prefixes and the follower step of the first is included in the follower step of the second, then the first wrong continuation is more restrictive than the second one, since its follower step needs less tokens. For example a(b + c)a(2b) is more restrictive than a(b + c)a(2b + c) in this sense.
Proposition 2. Let wσ,t = α1 . . . αn−1(αn+t) and wσ00,t0 = α10 . . . αm0−1(αm0+t0) be wrong continuations of L satisfying α1 + . . . + αn−1 = α10 + . . . + αm0−1 and (αn + t) ≤ (αm0 + t0). Then wσ,t is more restrictive than wσ0,t0 .
If the last step of a wrong continuation is sequenzialized by several terminal steps of a second wrong continuation, then the second wrong continuation is more restrictive than the first one, since a step is not enabled, if a sequentialization of the step is not enabled in a marking. For example a(b + c)aa is more restrictive than a(b + c)(2a) in this sense.
Proposition 3. Let wσ,t = α1 . . . αn−1(αn+t) and wσ0,t0 = α10 . . . αm0−1(αm0+t0) be wrong continuations of L satisfying α1 + . . . + αn−1 + (αn + t) = α10 + . . . + αm0−1 + (αm0 + t0) and α1 + . . . + αn−1 ≥ α10 + . . . + αm0−1. Then wσ,t is more restrictive than wσ0,t0 .
According to these oberservations, wrong continuations are ordered in the following way: Wrong continuations with longer prefixes are considered first and if two wrong continuations have equal prefix, then the wrong continuation with the shorter follower step is considered first. 4.1
Overview The SYNOPS tool is implemented strictly following advanced object oriented paradigms using a classical 3-tier-architecture: - The client tier is realized as a command line interface (CLI). In the meanwhile we also provide a graphical user interface (GUI) which additionally visualizes Petri net synthesis results. The CLI (resp. GUI) and the middle tier are loosly coupled, such that an easy and fast change is possible. - The middle tier (SynCore) encapsulates data types for the supported kinds of runs, sets of such runs and Petri nets and basic operations for creating, manipulating and destroying such objects. It can only be accessed via a facade (SynShell). - Sets of runs and synthesized Petri nets are stored in text files. For Petri nets the PNML-standard is used, such that synthesis results can be visualized by many Petri net editors. For storing sets of runs we use a simple self-created text format which lists runs, events and edges. A run consists of a finite set of events labelled by action names and a finite set of directed edges between events. A run can be represented through the four different causal structures previously mentioned.
The object of interest are sets of runs, since synthesis algorithms are operating on such sets. Every event has an ID which is unique within a run. Every run has an ID which is unique within a set of runs. Sets have global unique IDs. This way, each object can be identified by a combination of IDs in the usual way. For example, the identifier set1.lpo5.event3 represents the event with ID event3 in the run with ID lpo5 belonging to the set with ID set1.
There are several useful operations for manipulation of these data structures,
for example operations testing consistency properties of runs specified by the
user (such as cycle-freeness), operations computing the transitive closure of runs
specified by the user, operations computing all prefixes of a run (based on a
modified version of the algorithm of Warshall [
A Petri net consists of places, transitions and two kinds of edges between places and transitions (flow edges and inhibitor edges). Places have a unique ID, a name, a number of tokens and a maximum capacity of tokens (which can be infinity). Transitions have a unique ID and a name. Edges have a weight. This way several low level Petri net classes can be represented such as place/transition nets and inhibitor nets. Moreover, there are several restrictions available such as a bound of 1 for arc weights in order to represent elementary Petri nets. Such restrictions are realized by overwriting methods in specialized classes. This modular construction makes it easy to extend the framework by other net classes in future. 4.3
Synthesis algorithms So far, there is only one synthesis algorithm implemented in the download version of the tool: The algorithm syn-tf-sep computes place/transition nets from finite sets of LPOs using the separation representation of the set of token flow regions. 4.4
Command line interface CLI The CLI allows easy construction of long runs and sets of runs using a term-based notation. Currently, each command may only contain one operation. Complicated terms are constructed stepwise command by command.
A set (of runs) is opened by ’set ID’. After opening a set, runs of the set can be specified. Runs can only be specified within a set. Finally, a set is closed by ’tes’.
A run is opened by ’dag ID’ (for LDAGs), ’lpo ID’ (for LPOs), ’sdag ID’ (for LSDAGs) or ’lso ID’ (for LSOs). After opening a run, events and edges of the run can be specified. Events and edges can only be specified within a run. A run is closed by ’gad’, ’opl’, ’gads’ or ’osl’. After closing a run, consistency of the user input is checked. Moreover, in case of LPOs and LSOs, the transitive closure is constructed (that means, it is not necessary to specify all transitive edges). Finally, all prefixes of the run are computed, preparing the synthesis computation.
An event is specified by ’event ID LABEL’. An edge in a LDAG or an LPO between two events with IDs e1 and e2 is specified by ’et e1 e2’. A ”not later than” edge is specified by ’nlt e1 e2’. Using these operations, simple runs can be constructed such as LPO lpo1 shown in Figure 7. Figure 8 shows the syntax for specifying lpo1.
- If run1 and run2 are runs, then by ’append ID run1 run2’ the sequential composition of run1 and run2 is stored in a run with ID ID. Sequential composition means, that from each event in run1 to each event in run2 an LPO-edge is drawn. - If run1 and run2 are runs, then by ’compose ID run1 run2’ the parallel composition of run1 and run2 is stored in a run with ID ID. Parallel composition means, that between event in run1 and run2 there are no edges. - If run is a run, then by ’iterate ID run N’ the run is N times sequentially composed with itself (iterated) and the result is stored in a run with ID ID.
Using these operations, longer runs can be construced such as LPO lpo2 shown in Figure 7. Figure 9 shows the syntax for specifying lpo2.
It is also possible to apply sequential composition and iteration only partially w.r.t. a so called interface. An interface specifies explicitly, which events of the 1 set set1 2 lpo a 3 event a a 4 opl 5 lpo b 6 event b b 7 opl 8 iterate lpo1 b 3 9 compose lpo2 a lpo1 10 tes previous run are in direct causal dependency with which events of the subsequent run. Only between such events an edge is drawn. An interface is specified as an option of the operations append and iterate of the form ’-interface EDGELIST’, where an edge in EDGELIST between events with IDs e1 and e2 is specified by ’e1 < e2’ and edges are separated by a space. An interface can be used to specify LPO lpo3 shown in Figure 7. Figure 10 shows the syntax for specifying lpo3.
It is possible to use a run specified in a certain set within another set by using its fully qualified ID. The same holds for events.
A run or a set of runs with ID ID can be stored by ’save ID FILE’ at location FILE. A run or set of runs stored at location FILE can be be loaded by ’load FILE’. A run can be loaded only within an opened set of runs.
At each stage of the input, by ’state all’ all objects constructed so far are printed in form of text. The notation used here is the same as in the case of saving objects. If the GUI is used, by ’plot ID’ the run with ID ID is visualized.
A synthesis algorithm ALG can be applied to a set of runs with ID ID by ’ALG ID [OPTIONS]’. The synthesized Petri net is stored in PNML format, such that it can be visualized by Petri net editors. If the GUI is used instead of the CLI, the Petri net is also visualized. The user is noticed, if the synthesized net is an exact solution or not. If the algorithms uses the separation representation and the net is not an exact solution, all wrong continuations which could not be prohibited are returned as a tuple (pref ix, step), where pref ix and step are given by their Parikh-vector (counting the number of transition occurrences in the prefix and in the follower step). As already mentioned, only the algorithm syn-tf-sep is available in the download version. This algorithm has no options, so far.
The program is exited by ’exit’. 4.5
Storing Petri nets and sets of runs
Synthesized Petri nets are stored in the Petri Net Markup Language (PNML)
[
For testing compactness, we constructed several simple Petri nets with different initial markings having a finite set of runs, synthesized a net from this set of runs and compared the result with the initial net. Figure 12 shows two of the considered Petri nets with parametrized initial marking allowing different numbers of iterations. The complete set of considered sets of runs can be downloaded with the tool. In all cases the synthesized net and the initial net coincided.
For testing performance we considered the following examples used in [
Algorithm basis computes place/transition nets from finite sets of LPOs using
the basis representation of the set of token flow regions. Algorithm classic
computes place/transition nets from finite sets of LPOs using the separation
representation of the set of transition regions of the step language corresponding
to the set of LPOs. It turned out in [
Our experimental results show, that algorithm syn-tf-sep computes as small nets as algorithm classic, since it also uses the separation representation. Concerning performance on the other side, algorithm syn-tf-sep performes much better than algorithm classic and little worse than algorithm basis for the test series lpo6,n (for example runtimes 13 ms for the LPO-set {lpo6,2} and 132 ms for {lpo6,3}). Concerning the test series with combinations of lpo1 - lpo5, it performs as fast as algorithm classic (for example runtimes 5 ms for the LPO-set {lpo1, lpo2} and 6 ms for {lpo1, lpo2, lpo3, lpo4, lpo5}). Altogether, it is able to cope with nondeterminism and concurrency (since we ran the algorithms basis and classic several years ago on another system at another institut as syn-tf-sep, it does not make sense to compare absolute runtimes).
Currently we are working on a more efficient implementation concerning concurrency. In particular, it is possible to significantly reduce the number of prefixes, which need to be computed, by considering a more compact representation of iterations (which is currently implemented in the context of infinite iterations, see Section 7). 6
Up to our best knowledge, the only tool which also supports synthesis from
partial languages is the graphical Petri net editor VIPTOOL [
There is is another tool-supported line of research considering transition
systems instead of languages as behavioral specification. The tool [
One application of synthesis algorithms is process mining. There is a big
tool frame work called PROM [
Currently, an analoguous algorithm is implemented for the synthesis of general
inhibitor nets from finite sets of LSOs [
The presented set of operations is currently extended by the following operations allowing fast generation of large sets of runs: Alternative composition of runs, sequential composition, parallel composition and iteration of sets of runs, and standard operations on sets (of runs) like union, intersection, difference.
In order to increase usability, we plan to implement shortcuts for all operations (such a ’a<b’ instead of ’et a b’ or ’lpo1 a<b’ instead of ’append lpo1 a b’) and the possibility to use more than one operation in a command (such as ’lpo1 a<(b|c)’ instead of the sequence ’compose lpo0 b c’ and ’append lpo1 a lpo0’).
Further steps are: Adapting the algorithms to restriced net classes such as elementary nets and workflow nets and to the use of additional information such as predefined places or undesired runs. 8
The tool can be downloaded from the project webpage [