SoyutNet documentation

SoyutNet is a place/transition net (PT net, Petri net) simulator that uses Python’s asyncio task and synchronization utilities as backend. (Soyut means abstract in Turkish.)

This documents gives a brief information on PT nets, summarizes its implementation in SoyutNet and discusses the project’s Goals.

Code repository 🔗

PT nets

Place/transition net is a formal modeling framework for discrete event systems (DES). It also provides a graphical modeling framework to visualize the structure of the model. A graphical example is given below.

An example

In the diagram,

• \(p_1\) and \(p_2\) are called places.

• \(t_1\) is called a transition.

• \(a_1\) and \(a_2\) are arcs connecting transitions and places to each other.

• \(\bullet\) is called a token.

• \(p_1\) is an input place of \(t_1\)

• \(p_2\) is an output place of \(t_1\)

When this model is executed, its flow is

1. \(p_1\) has a token and its output arc is connected to \(t_1\),

2. \(t_1\) is enabled because \(p_1\) has 1 or more tokens,

3. \(t_1\) is fired and it transfers the token from \(p_1\) to \(p_2\).

The final state is:

The model reached its final state according to the rules explained below.

PT net definition and rules

A PT net consists of 5 components

1. \(P=\{p_1, p_2, \dots, p_m\}\) finite set of places

2. \(T=\{t_1, t_2, \dots, t_n\}\) finite set of transitions

3. \(A \subseteq (P \times T) \cup (T \times P)\) set of arcs from P to T and T to P

4. \(W: A \rightarrow \{1, 2, \dots\}\) arc weights

5. \(M_0: P \rightarrow \{0, 1, 2, \dots\}\) initial marking

In the example above,

• \(P=\{p_1, p_2\}\)

• \(T=\{t_1\}\)

• \(A=\{a_1, a_2\}\)

• \(W=\{w(p_1, t_1)=1, w(t_1, p_2)=1\}\)

• \(M_0=\{p_1 = 1, p_2 = 0\}\)

Functions \(w(p_i, t_j)\) and \(w(t_i, p_j)\) denotes the arc weights between transitions and places. After \(t_1\) fires, marking changes and it becomes

\[M_1=\{p_1 = 0, p_2 = 1\}\]

according to the rules below.

1. A transition \(t_i\) is enabled if its all input places have a number of tokens greater than or equal to the weight of the connecting arcs.

   \[\begin{split}M_{in} = \{u_1, u_2, \dots\} ~~~ \textrm{marking of input places of} ~ t_i \\ M_{out} = \{v_1, v_2, \dots\} ~~~ \textrm{marking of output places of} ~ t_i \\\end{split}\]
   \[w(\bar{p}_j, t_i) \leq u_j, ~~~ \textrm{for all input places} ~ \bar{p}_j\]

where \(j\) are the indices of \(t_i\)’s input places and \(M_{in}, M_{out}\) are the current marking of the input and output places (number of tokens in each place).

2. When a transition \(t_i\) is fired, it removes a number of tokens equal to the weights of arcs connecting the input places and transfers a number of tokens equal to the weight of arcs connecting to the output places.

   \[\begin{split}M^{\ast}_{in} = \{u_1-w(\bar{p}_1,t_i), u_2-w(\bar{p}_2, t_i), \dots\} \\ M^{\ast}_{out} = \{v_1+w(t_i,\tilde{p}_1), v_2+w(t_i, \tilde{p}_2), \dots\} \\\end{split}\]

where \(M^{\ast}\) is the new marking of input and output places after \(t_i\) is fired.

Labeled PT net

An extension of PT nets called labeled PT nets which assigns a label to the tokens and arcs.

The transition \(t_1\) expects a specific type of token (represented by ◆) and transforms it to a token with another label (▲).

SoyutNet

SoyutNet implements a slightly modified version of the labeled PT nets. Each place/transition (PT) work asynchronously in their dedicated asyncio.Task and communicates to the other PTs through asyncio.Queue instances in their input/output arcs.

Data structures

Label

An integer value. Its type is label_t = int. It can be the generic label (soyutnet.constants.GENERIC_LABEL) or any positive integer.

ID

An integer value. Its type is id_t = int. It can be the generic ID (soyutnet.constants.GENERIC_ID) or any positive integer.

Token

It is defined as a tuple of a label and an ID.

token: Tuple[label_t, id_t] = (label, id)

Token binding

Tokens are not pure abstract structures. Each token can be binded to a concrete data structure. This can be done via soyutnet.SoyutNet.TokenRegistry.

an_object = an_instantiator()
net = SoyutNet()
treg = net.TokenRegistry()
actual_token = net.Token(label=label, binding=an_object)
treg.register(actual_token) # Registry assigns an auto incrementing ID
id_of_actual_token = actual_token._id

And, the binded object can be retrived somewhere else in the program as below.

binded_object = treg.pop_entry(label, id_of_actual_token).get_binding()

Place

Keeps a Python dictionary of tokens indexed by labels (soyutnet.pt_common.PTCommon._tokens).

token_dictionary: Dict[label_t, list[id_t]] = {
    label_1: [ id_1, id_2 ],
    label_2: [ id_3 ],
    label_3: [ id_4, id_5 ],
}

Arc

Arcs have a weight (default is 1) and one or more labels. And, they keep references to its input and output places/transitions (PTs).

start = pt1 # Weak reference to the input place or transition
end = pt2 # Weak reference to the output place or transition
weight: int = 1
labels: list[label_t] = [ label_1, label_2, ... ]

An arc can accept any token whose label is in its labels list. End points start and end can not both be places or transitions. If one is a place, the other must be a transition.

Arcs use asyncio.Queue instances to wait for and transfer tokens. Their queue’s maximum size is equal the arc’s weight.

Transition

A transition is enabled if all input arc (soyutnet.pt_common.PTCommon._input_arcs) queues (soyutnet.pt_common.Arc._queue) are full. Meaning, input arc queues has the same number of tokens as arc’s weight.

SoyutNet’s additional rule: The sum of a transition’s input arc weights for each label must be equal to the sum of its output arc weights for each label.

As shown in the image below sum of input and output ◆ and ▲ are the same. If this property is not satisfied, SoyutNet model will possibly enter a deadlock.

Note: SoyutNet’s places and transitions accept a callback function named as processor (soyutnet.pt_common.PTCommon._processor). It is called after tokens acquired from input arcs and before sending them through output arcs. SoyutNet’s additional rule can be worked around by a custom processor callback that duplicates or discards input tokens.

Observer records

If a place has an observer attached, the observer keeps track of tokens when an output transition is fired. It records:

• Time instant (for keeping track of the order of firings)

• A tuple of token labels and count of tokens just before the firing

• The identity of transition fired

  records = [
      ( time1, ( (label_1, count_11), (label_2, count_12), ... ), "<name of transition>" ),
      ( time2, ( (label_1, count_21), (label_2, count_22), ... ), "<name of transition>" ),
      ...
  ]
  

The records (soyutnet.observer.ObserverHistoryType) saved in distinct observers can be merged by soyutnet.registry.PTRegistry.get_merged_records() at the end of simulation.

Special place

SoyutNet implements a special type of place called SpecialPlace (soyutnet.place.SpecialPlace). Regular places (soyutnet.place.Place) operates according to the PT net rules. More precisely, places redirect tokens from input arcs to the output arcs by matching token’s and output arc’s labels.

On the other hand, SpecialPlace class constructor accepts two extra optional arguments.

1. producer: It is a callback function which is called to acquire tokens after the default _process_input_arcs (soyutnet.pt_common.PTCommon._process_input_arcs()) is called. This function can be used to produce custom tokens by generating a label and ID. Then, it will be injected into the PT net’s flow.

2. consumer: This callback function is called before the default _process_output_arcs function (soyutnet.pt_common.PTCommon._process_output_arcs()) is called. It can be used as an end point of PT net model. The tokens acquired by this function can be redirected to other utilities.

Graphviz DOT file generation

Version 0.2.0 introduces Graphviz DOT file generation from the SoyutNet’s net structure. DOT language is a special format for defining graph structures that can be parsed by dot command to generate images in several formats.

Example code

The code below implements the first example but arcs have two labels in this case. It means \(t1\) and \(p2\) will accept tokens with both labels.

import sys
import asyncio

import soyutnet
from soyutnet import SoyutNet
from soyutnet.constants import GENERIC_ID, GENERIC_LABEL


def main():
    async def scheduled():
        await asyncio.sleep(1)
        soyutnet.terminate()

    with SoyutNet(extra_routines=[scheduled()]) as net:
        net.DEBUG_ENABLED = True

        LABEL = 1
        initial_tokens = {
            GENERIC_LABEL: [GENERIC_ID],
            LABEL: [1000, 990],
        }
        o1 = net.Observer(verbose=True)
        p1 = net.Place("p1", initial_tokens=initial_tokens, observer=o1)
        o2 = net.Observer(verbose=True)
        p2 = net.Place("p2", observer=o2)
        t1 = net.Transition("t1")
        """Define places and transitions (PTs)"""

        _ = net.Arc(labels=(GENERIC_LABEL, LABEL))
        p1 >> _ >> t1 >> _ >> p2
        """Connect PTs"""

    records = net.registry.get_merged_records()
    graph = net.registry.generate_graph(
        indent="  ", label_names={LABEL: "🤔", GENERIC_LABEL: "🤌"}
    )

    print("\nRecorded events:")
    {net.print(rec) for rec in records}
    print("\nNet graph:")
    print(graph, file=sys.stderr)

    return records, graph


if __name__ == "__main__":
    main()

$ python3 first_example.py 1 # Generates the Graphviz dot file below.
digraph Net {
  subgraph cluster_0 {
    p1_0 [shape="circle",fontsize="20",style="filled",color="#000000",fillcolor="#dddddd",label="",xlabel="p1",height="1",width="1",penwidth=3];
    p2_0 [shape="circle",fontsize="20",style="filled",color="#000000",fillcolor="#dddddd",label="",xlabel="p2",height="1",width="1",penwidth=3];
    t1_0 [shape="box",fontsize="20",style="filled",color="#cccccc",fillcolor="#000000",label="",xlabel="t1",height="0.25",width="1.25",penwidth=3];
    t1_0 -> p2_0 [fontsize="20",label="{🤌,🤔}",minlen="2",penwidth="3"];
    p1_0 -> t1_0 [fontsize="20",label="{🤌,🤔}",minlen="2",penwidth="3"];
  }
  clusterrank=none;
}

$ python first_example.py 2>&1 > /dev/null | dot -Tpng > first_example.png

Outputs:

Goals

SoyutNet implements a modified version of labeled PT nets with an additional rule;

the sum of input arc weights of a transition must be equal to the sum of output arc weights for each label.

Because, SoyutNet assumes that tokens represent real entities with an ID and a label assigned. The ID identifies the token and the label determines how it flows through the network. It also ensures that a token created by a producer arrives at a consumer without duplication or getting discarded as generally expected in a real life application. Producers and consumers should decide to duplicate or discard a token.

The main goal of SoyutNet is to investigate that PT net based formal methods can be used to improve a producer/consumer pipeline.

Docstrings

• SoyutNet
  • soyutnet module
    • SoyutNet
    • _add_int_handlers()
    • _cancel_all_tasks()
    • _int_handler()
    • main()
    • run()
    • terminate()
  • soyutnet.pt_common module
    • Arc
    • PTCommon
    • _loop()
  • soyutnet.place module
    • Place
    • SpecialPlace
  • soyutnet.transition module
    • FiringHistoryType
    • FiringRecordType
    • Transition
  • soyutnet.token module
    • Token
  • soyutnet.observer module
    • ComparativeObserver
    • MergedRecordsType
    • Observer
    • ObserverHistoryType
    • ObserverRecordType
  • soyutnet.registry module
    • DirectoryType
    • PTRegistry
    • PostRegisterCallbackType
    • Registry
    • TokenRegistry
    • _default_post_register_callback()
  • soyutnet.constants module
    • BaseObject
    • GENERIC_ID
    • GENERIC_LABEL
    • INVALID_ID
    • INVALID_LABEL
    • SoyutNetError
    • TokenType
    • TokenWalletType
    • id_t
    • label_t
    • random_identifier()

Examples

• Examples
  • Producer/consumer
  • n-tester
  • Periodic

PT connection examples

• PT connection syntax
  • Graph format
  • Single branch examples
  • Multiple branch examples

Simulations

• PI-controller

• HTTP balancer

• HTTP server

• Timed net

Modules

• soyutnet

Credits

• SoyutNet logo