Introduction

PTChannel is a plugin which allows the compilation and simulation of P/T channels with synchronous channels.

It is available for Modular Renew, currently being developed in the branch modular/ptchannel and not part of any distribution package.

A version of Renew with PTChannel  and some examples can be downloaded here: renew4ptchannel.zip

User Guide Getting Started

(For Linux - other operating systems see Starting modular Renew)

After downloading and extracting the file, one might start Renew with PTChannel using the follwing command:

$ java -p renew4ptchannel:renew4ptchannel/libs -m de.renew.loader gui

If the directory has been renamed (e.g. to "dist"), substitute "renew4ptchannel" accordingly.

To use the formalism in Renew, select it under Simulation/Formalism?. For communication within one net instance, select the Single P/T Net with Channel Compiler.

If partitioning into multiple net instances is required, select the P/T Net in Net Compiler.

Construct a viable P/T net with synchronous channels and start the simulation under Simulation/Run? Simulation or Simulation/Simulation? Net Step.

If the P/T Net in Net Compiler is selected, the user needs to set hyperparameters for the construction of a system net that handles communication before the simulation can start.

P/T Nets with Synchronous Channels

The PTChannel plugin extends Renew by a new Petri net formalism, which in turn extends P/T nets by synchronous channels.

A detailed explanation and definition of P/T nets with synchronous channels can be found in the theses Voß22, Kühnemund21, and the paper Voß+22.

As a quick overview:

P/T-nets with synchronous channels (PTC-nets) are a superset of ordinary P/T-nets. In P/T nets with channels, transitions may be inscribed with up- or downlinks. Up-/Downlinks accept two types of parameters for bi-directional information exchange: Integers and Variables. Integers indicate how many "black tokens" get transferred between transitions Variables can be bound to these integers and used as arc inscriptions Modularizing and partitioning nets is possible. Resulting net instances can communicate via channels. Communication is organized via a system net. Inter-Net communication is possible through uplinks only.

Viable User Input

PTC-nets follow a specific syntax. Since it is an extension to ordinary P/T-nets, it follows the syntax for P/T-nets and all viable P/T nets are also viable in the PTC-net formalism.

The only difference are transition inscriptions, which are not allowed in P/T-nets but possible in PTC-nets.

If two transitions shall communicate via a channel, one transition must be inscribed with a downlink (indicated by the keyword this, e.g. this:sync()) and the other transition must be inscribed with an equally named uplink (e.g. :sync()).

It is possible and intended to inscribe multiple transitions with the same up- or downlink. In that case, a transition has multiple possible communication partners.

Additionally, transition channels may carry parameters in the form of variables and integers (e.g. this:sync(x, 2) and :sync(1, y)). Note that only transitions with the same digits ("Stelligkeit") may communicate. Also, if an integer is at position i in the parameter tuple, the communication partner needs a variable at the same position i.

Arcs connected to communicating transitions may be inscribed with its variables (e.g. x ).

Under Examples, one may find a viable P/T channel net for the producer-consumer scheme.

Inter-Net Communication

A system net is used to enable the synchronization of different net instances with selected P/T Net in Net Compiler.

The following hyperparameters need to be set by a user, which are used to create a syntactically correct system net automatically:

Which and how many net instances shall be created from the templates? Which synchronizations shall be possible in the net?

Modelers can select these settings in a GUI, that automatically opens whenever the simulation of a syntactically correct PTC-net is started. The GUI for a Sender-Receiver example can be seen in the next figure, together with the panel to manually create synchronization options.