TeSSLa Petri-Net Library

module PetriNetStructure

Module containing functions and type definitions for modelling a Petri net in the TeSSLa language Functions for monitoring of the network can be found in module PetriNetMonitoring

Usage:

The petri net

               1
             --------p1
    1       /
p0-------|t0|
            \    2
             --------p2

can be modelled in the following way:

import PetriNetStructure

in: t0: Events[Int]

def petriNet =
addPlace("p0", 5, Some(10), true,
addPlace("p1", 6, Some(8), false,
addPlace("p2", 0, None, true,
addTransition("t0", Set.add(Set.empty,("p0", 1)), Set.add(Set.add(Set.empty,("p1", 1)),("p2", 2)), t0,
emptyNet))))

Thereby place p0 has initial capacity of 5, maximum capacity of 10 and uses fifo principle. Place p1 has initial capacity of 6, maximum capacity of 8 and uses lifo principle. Place p2 has initial capacity of 0, no maximum capacity and uses fifo principle.

ANCHOR Type PetriNet

PetriNet

Type for attributes of a place in the Petri net. Consisting of

• places: Map relating place names and attributes
• transitions: Map relating transition names and connected places with (pot. negative) weights and trigger streams

Objects of this type can be generated with help of the functions in this module

ANCHOR Type Place

Place

Type for names of places in the Petri net (alias of String)

ANCHOR Type PlaceAtt

PlaceAtt

Type for attributes of a place in the Petri net. Consisting of

• init: Integer indicating the initial number of markings in the place
• max: Option[Int] indicating the maximal capacity of a place in the net. None if there is no maximal capacity
• fifo: Boolean indicating whether place follows fifo (first in first out) policy (otherwise lifo, last in first out policy is followed)

ANCHOR Type Transition

Transition

Type for names of transitions in the Petri net (alias of String)

ANCHOR addPlace

addPlace(name: Place, initial: Int, max: Option[Int], fifo: Bool, pn: PetriNet): PetriNet

Function for adding a new place to a Petri net.

• name: The place name (has to be unique)
• initial: The initial markings in the place
• max: The maximal capacity of the place (optional)
• fifo: Boolean indicating whether the net follows first in first out (true) or last in last out (false) policy
• pn: The petri net to which the place should be added
• Returns a petri net with the additional place

	def addPlace(name: Place, initial: Int, max: Option[Int], fifo: Bool, pn: PetriNet) : PetriNet = {
		def newPlaces = Map.add(pn.places, name, {init = initial, max = max,  fifo = fifo})
		{
			places = newPlaces,
			transitions = pn.transitions
		}
	}

ANCHOR addTransition

addTransition(name: Transition, from: Set[(Place, Int)], to: Set[(Place, Int)], trigger: Events[Int], pn: PetriNet): PetriNet

Function for adding a new transition to a Petri net.

• name: The transition name (has to be unique)
• from: Set of place name/token number tuples of incoming edges
• to: Set of place name/token number tuples of incoming edges
• trigger: A stream with events that indicate how often a transition is fired
• pn: The petri net to which the transition should be added
• Returns a petri net with the additional transition

	def addTransition(name: Transition, from: Set[(Place, Int)], to: Set[(Place, Int)], trigger: Events[Int], pn: PetriNet) : PetriNet = {
		def completeTransitions = Set.union(Set.map(from, (el) => (el._1,-el._2)), to)
		def newTransitions = Map.add(pn.transitions, name, {conn: completeTransitions, trig: trigger})
		{
			places = pn.places,
			transitions = newTransitions
		}
	}

ANCHOR emptyNet

emptyNet: PetriNet

Constant for an empty Petri net

	def emptyNet : PetriNet = {places = Map.empty, transitions = Map.empty}