README
¶
A Go library for parsing Petri nets
Nets
Nets is a Go library for parsing Petri nets, and Time Petri nets, written using the textual description format of the Tina toolbox. The format is defined in the section on the .net format described in the manual pages for Tina.
The library provides an exported type for dealing with Petri nets that can be useful to build new tools. We also provide methods to marshall a Net into a .net file or a PNML file for Place/Transition nets.
Installation
go get github.com/dalzilio/nets
Usage
You can find some examples of code in the *_test.go files and some example of
.net files in directory testdata. The main function, Parse, returns a
Net struct from an io.Reader.
package main
import (
"fmt"
"os"
"github.com/dalzilio/nets"
)
func main() {
file, _ := os.Open("testdata/sokoban_3.net")
net, err := nets.Parse(file)
if err != nil {
log.Fatal("parsing error: ", err)
}
fmt.Printf("net %s has %d transitions\n", net.Name, len(net.Tr))
// Output:
// net Sokoban has 452 transitions
}
Dependencies
The library has no dependencies outside of the standard Go library. It uses Go modules and has been tested with Go 1.16.
License
This software is distributed under the GNU Affero GPL v3. A copy of the license agreement is found in the LICENSE file.
Authors
- Silvano DAL ZILIO - LAAS/CNRS
Documentation
¶
Overview ¶
Package nets defines a concrete type for Time Petri Nets and provides a Parser for building Nets from the textual description format used in the Tina toolbox (see below).
The net format ¶
We support a very general subset of the description format for Time Petri nets found in the Tina man pages (see http://projects.laas.fr/tina/manuals/formats.html). We explain some of our restrictions below. All the files successfully parsed or printed using the library are valid .net file
A net is described by a series of declarations of places, transitions, priorities and/or notes, and an optional naming declaration for the net. The net described is the superposition of these declarations. The grammar of .net declarations is the following, in which nonterminals are bracketed by < .. >, terminals are in upper case or quoted. Spaces, carriage return and tabs act as separators.
Labels may be (optionally) assigned to places and transitions, but we do not support the use of a "lb" declaration, for labels, that was only kept for backward compatibility. We also do not support stopwatches and reset arcs.
Grammar
.net ::= (<trdesc>|<pldesc>|<lbdesc>|<prdesc>|<ntdesc>|<netdesc>)*
netdesc ::= ’net’ <net>
trdesc ::= ’tr’ <transition> {":" <label>} {<interval>} {<tinput> -> <toutput>}
pldesc ::= ’pl’ <place> {":" <label>} {(<marking>)} {<pinput> -> <poutput>}
ntdesc ::= ’nt’ <note> (’0’|’1’) <annotation>
prdesc ::= ’pr’ (<transition>)+ ("<"|">") (<transition>)+
interval ::= (’[’|’]’)INT’,’INT(’[’|’]’) | (’[’|’]’)INT’,’w[’
tinput ::= <place>{<arc>}
toutput ::= <place>{<normal_arc>}
pinput ::= <transition>{<normal_arc>}
poutput ::= <transition>{arc}
arc ::= <normal_arc> | <test_arc> | <inhibitor_arc> |
<stopwatch_arc> | <stopwatch-inhibitor_arc>
normal_arc ::= ’*’<weight>
test_arc ::= ’?’<weight>
inhibitor_arc ::= ’?-’<weight>
weight, marking ::= INT{’K’|’M’}
net, place, transition,
label, note, annotation ::= ANAME | ’{’QNAME’}’
INT ::= unsigned integer
ANAME ::= alphanumeric name, see Notes below
QNAME ::= arbitrary name, see Notes below
Notes ¶
Two forms are admitted for net, place and transition names:
ANAME : any non empty string of letters, digits, primes (’) and underscores (_)
’{’QNAME’}’ : any chain between braces, and in which the three characters "{,}, or \" are escaped with a \
Empty lines and lines beginning with ’#’ are considered comments.
In any closed temporal interval [eft,lft], one must have eft <= lft.
Weight is optional for normal arcs, but mandatory for test and inhibitor arcs.
By default: transitions have temporal interval [0,w[; normal arcs have weight 1; places have marking 0; and transitions have the empty label "{}"
When several labels are assigned to some node, only the last assigned is kept.
When a transition is associated with several timing intervals, we keep the intersection of all the intervals (the result must not be empty).
It is also possible to list transitions associated with a place, in a pl declaration. Arcs defined in this way are added to the respective transitions.
Simple example of .net file ¶
This is a simple example of .net file. Note that it is possible to have several declarations for the same object (place or transition); the end result is the fusion of all these declarations.
tr t1 p1 p2*2 -> p3 p4 p5 tr t2 [0,2] p4 -> p2 tr t3 : a p5 -> p2 tr t3 p3 -> p3 tr t4 [0,3] p3 -> p1 pl p1 (1) pl p2 (2)
Example (Basic) ¶
This example shows the basic usage of the package: Parse a .net file and output the result on the standard output. Since the net has priorities, we also compute the transitive closure of its priority relation (a call to PrioClosure). Note that we print the number of places and transitions of the net, as a comment, but that we strip the original comments found in the file.
package main
import (
"fmt"
"log"
"os"
"github.com/dalzilio/nets"
)
func main() {
file, err := os.Open("testdata/demo.net")
if err != nil {
log.Fatal("error opening file:", err)
}
defer file.Close()
net, err := nets.Parse(file)
if err != nil {
log.Fatal("parsing error: ", err)
}
if err := net.PrioClosure(); err != nil {
log.Fatal("error with priorities: ", err)
}
fmt.Printf("%s", net)
}
Output: # # net demo # 4 places, 7 transitions # pl p0 pl p1 pl p4 : b pl p2 (1) tr t1 [0,1] p0 -> p1 tr t0 : a ]2,3[ p0*3 -> p1 p4 tr t3 p2 -> tr t5 : {\{a\}} p4 -> p0 tr t4 -> p4 tr t6 p4?1 -> tr t2 : {b s} [0,0] p1?-4000 -> pr t1 > t0 pr t3 > t1 t0 t2 pr t6 > t1 t0 t2
Example (CountTransitions) ¶
This example shows how to use the result of parsing a .net file to find the number of transitions in a net.
package main
import (
"fmt"
"log"
"os"
"github.com/dalzilio/nets"
)
func main() {
file, _ := os.Open("testdata/sokoban_3.net")
net, err := nets.Parse(file)
if err != nil {
log.Fatal("parsing error: ", err)
}
fmt.Printf("net %s has %d transitions\n", net.Name, len(net.Tr))
}
Output: net Sokoban has 452 transitions
Example (Pnml) ¶
This example shows how to output a Net into a PNML Place/Transition file.
package main
import (
"log"
"os"
"github.com/dalzilio/nets"
)
func main() {
file, _ := os.Open("testdata/abp.net")
net, err := nets.Parse(file)
if err != nil {
log.Fatal("parsing error: ", err)
}
_ = net.Pnml(os.Stdout)
}
Index ¶
Examples ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func BCompare ¶ added in v1.4.0
BCompare returns an integer comparing two bounds. The result will be 0 if a and b are equal, negative if a < b, and positive otherwise. We return the difference between the bounds values, with some exceptions. We always return +1 when b a infinite or when a and b have same values, but a is open whereas b is closed. For intance, the bound [1,.. is considered strictly greater than ]1,.. with our choice. We return -1 in the symetric cases.
func BIsPositive ¶ added in v1.4.0
BIsPositive returns true if b1 is greater or equal to 0.
Types ¶
type Atom ¶
Atom is a pair of a place index (an index in slice Pl) and a multiplicity (we never store places with a null multiplicity). We assume that markings and arc weights should fit into a 32 bits integer and we make no attempt to check if these values overflow.
type Bound ¶
Bound is the type of bounds in a time interval.
func BSubstract ¶ added in v1.4.0
BSubstract computes the diference, b1 - b2, between its time bounds parameters. We return an infinite bound when b2 is infinite.
func (Bound) PrintLowerBound ¶ added in v1.4.0
PrintLowerBound returns a textual representation of a time interval bound used as a lower bound constraint, such as "4 <" or "5 ≤". We return the string "∞" if b is infinite (which should not happen in practice).
func (Bound) PrintUpperBound ¶ added in v1.4.0
PrintUpperBound is the dual of PrintLowerBound and returns a representation of a time interval bound used as a lower bound constraint, such as "< 4" or "≤ 5". We return the string "< ∞" if b is infinite.
type Handle ¶ added in v1.4.0
Handle is a unique identifier for a Marking. Basically this is the canonical, interned version (using go unique package) of a string representation of a Marking.
type Marking ¶
type Marking []Atom
Marking is the type of Petri net markings. It is a slice of Atoms (places index and multiplicities) sorted in increasing order by places. We may use negative multiplicities, for instance to encode the Delta in a Petri net transition.
Conventions
- Items are of the form {key, multiplicity}
- Items with weight 0 do not appear in multisets (default weight);
- Items are ordered in increasing order of keys.
func (Marking) AddToPlace ¶ added in v1.4.0
AddToPlace returns a new Marking obtained from m by adding mult tokens to place pl.
type Net ¶
type Net struct {
Name string // Name of the net.
Pl []string // List of places names.
Tr []string // List of transitions names.
Tlabel []string // List of transition labels. We use the empty string when no labels.
Plabel []string // List of place labels.
Time []TimeInterval // List of (static) timing constraints for each transition.
Cond []Marking // Each transition has a list of conditions.
Inhib []Marking // Each transition has inhibition conditions (possibly with capacities).
Pre []Marking // The Pre (input places) condition for each transition (only useful with read arcs in TPN).
Delta []Marking // The delta (Post - Pre) for each transition.
Initial Marking // Initial marking of places.
Prio [][]int // the slice Prio[i] lists all transitions with less priority than Tr[i] (the slice is sorted).
}
Net is the concrete type of Time Petri Nets. We support labels on both transitions and places. The semantics of nets is as follows. Our choice differs from the traditional semantics of TPN (based on Pre- and Post-conditions), because we want to uniformly support inhibitor-arcs and capacities.
• COND: In a condition, Cond[k], an atom (p, m) entails that if transition Tr[k] is enabled at marking M then M.Get(p) >= m. Therefore Tr[k] is enabled at M when Compare(M, Cond[k]) >= 0 (for the pointwise comparison).
• INHIB: In a dual way, in the inhibition condition Inhib[k], if transition Tr[k] is enabled at marking M then M.Get(p) < Inhib[k].Get(p) or Inhib[k].Get(p) == 0.
• PRE: The value of Pre[k] models the arcs from an "input" place to transition Tr[k]. In a TPN, the value of Tr[k].Get(p) gives the tokens "losts" from the input plac p. This is useful when we need to check if a (timed) transition is re-initialized. Transition Tr[k2] is not re-initialized at marking M, after firing Tr[k1], if Compare(Add(M, Pre[k2]), Cond[k1]) >= 0 (using pointwise operations).
• DELTA: An atom (p, m) in Delta[k] indicates that if Tr[k] fires then the marking of place p must increase by m (in this case m can be negative). Hence if we fire Tr[k] at marking M, the result is Add(M, Delta[k]).
func Parse ¶
Parse returns a pointer to a Net structure from a textual representation of a TPN. We return a nil pointer and an error if there was a problem while reading the specification.
func (*Net) AllEnabled ¶ added in v1.4.0
AllEnabled returns the set of transitions (as an ordered slice of transition index) enabled for marking m.
func (*Net) IsEnabled ¶ added in v1.4.0
IsEnabled checks if transition t in the net is enabled for marking m, meaning m is greater than the precondition for t (in net.Cond) and also less than the inhibition/capacity constraints given in net.Inhib.
func (*Net) Pnml ¶
Pnml marshall a Net into a P/T net in PNML format and writes the output on an io.Writer. Because of limitations in the PNML format, we return an error if the net has inhibitor arcs. We also drop timing information on transitions and replace read arcs with "tests"; meaning a pair of input/output arcs.
This method is only useful if you create or modify an object of type Net. It is preferable to use the `ndrio` program to transform a .net file into a PNML P/T file.
We combine names and labels for the naming of places and transitions in the PNML file but we build the id by adding a prefix ('pl_' for places and 'tr_' for transitions), because it is possible to use the same name as a place and as a transition in a .net file.
func (*Net) PrioClosure ¶ added in v1.3.0
PrioClosure updates the priority relation by computing its transitive closure. We return an error if we have circular dependencies between transitions.
type TimeInterval ¶
type TimeInterval struct {
Left, Right Bound
}
TimeInterval is the type of time intervals.
func (*TimeInterval) String ¶
func (i *TimeInterval) String() string
func (*TimeInterval) Trivial ¶ added in v1.4.0
func (i *TimeInterval) Trivial() bool
Trivial is true if the time interval i is of the form [0, w[ or if the interval is un-initialized (meaning the left part of the interval is of kind BINFTY)
Source Files
Directories