= Introduction

PTChannel is a plugin for [http://www.renew.de/ Renew] which allows the compilation and simulation of P/T nets with synchronous channels.

== Where to get the Tool

PTChannel is currently not part of the official Renew release. A version of Renew with PTChannel and some examples can be downloaded here:


[http://www.moldt.de/link-for-larger-files/renew4ptchannel.zip renew4ptchannel.zip]



= User Guide
== Getting Started

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

Under Linux / MacOS:


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

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

Under Windows:

{{{
java -p dist;dist/libs -m de.renew.loader gui
}}}

In the git bash the following command must be used instead:

{{{
java -p dist\;dist/libs -m de.renew.loader gui
}}}

In the Powershell of windows (which is also used by Intellij!) the following command must be used:

{{{
java -p "dist\;dist/libs" -m de.renew.loader gui
}}}


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 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 arity ("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.

[[Image(SystemNetGUI.png)]] [[Image(customCompositionGUI.png)]]

== Examples

=== Producer-Consumer synchronizing within one net instance

[[Image(Example1.png)]]

=== Trader and Supplier communicating between multiple net instances

[[Image(Example21.png)]] [[Image(Example22.png)]]