Abstract Petri Net Notation can be used for describing different types of nets in a common notation. The notation is suitable for specifying Place/Transition nets, coloured Petri nets, generalized stochastic Petri nets and hierarchical Petri nets. However, the algorithms offered by the Kit work on 1-safe Petri nets and therefore the Kit only supports the following subset of APNN:
(For full details on APNN see here).

Start symbol: net

  net ::= \beginnet {id} element \endnet

element ::=	place element
	| transition element
	| arc element
	| ;

  id ::= string

place ::=	\place{id}{ name partition init }
	| \place{id}{ \like{ string } }

name ::=	\name{ string }
	| ;

  partition ::= \partition{ integer }

init ::=	\init{ 1 }
	| \init{ 0 }
	| ;

  transition ::= \transition{id}{ name }

  arc ::= \arc{id}{ \from{id} \to{id} }

Now we want to specify Dekker's mutex algorithm in APNN notation. First we look at Dekker's mutex algorithm modelled as 1-safe Petri net:

Places P9 through P14 denote different values of the variables. For example, if process 1 fires transition T1, then the value of variable flag1 should be set to 1 afterwards. Moreover, we know that the value of flag1 is 0 before the execution of T1. To model this behaviour correctly, we have to draw edges from P9 to T1 and from T1 to P10. Transition T2 should be fired only if process 1 stays in state P2 (it is marked) and if the value of variable flag2 is 0 before execution of T2. So we have to draw an edge from P13 to T2. Also, we must draw an edge from T2 to P13 because the value of flag2 will not change during execution of T2.

For the sake of clarity all the edges connecting places P9 through P14 with transitions in the processes are omitted. See here for the Petri net with all edges.

In APNN this Petri net looks like the following:

The program begins with the keyword \beginnet followed by a name enclosed in braces and ends with the keyword \endnet. Between these lines one can define places, transitions, and arcs in any order. Places can get additional information like name, partition and initial value. For example, place P1 is named idle1 and holds one token initially. Place P5 is defined like P2 and therefore named trying1, too. Transitions can be named in the same way. The names of places and transitions need not be unique, but the identifiers (P1, P2, T1 etc) must be. Arcs can be defined easily. For example, arc A1 leads from place P1 to transition T1, and arc A3 leads from transition T1 to place P2.

\beginnet{dekker}

\place{P1}{\name{idle1} \partition{1} \init{1}}
\place{P2}{\name{trying1} \partition{1}}
\place{P3}{\name{incs1} \partition{1}}
\place{P4}{\name{} \partition{1}}
\place{P5}{\like{P2}}
\place{P6}{\like{P2}}
\place{P7}{\like{P2}}
\place{P8}{\like{P2}}

\place{P9}{\name{flag1=0} \partition{2} \init{1}}
\place{P10}{\name{flag1=1} \partition{2}}
\place{P11}{\name{turn=1} \partition{3} \init{1}}
\place{P12}{\name{turn=2} \partition{3}}
\place{P13}{\name{flag2=0} \partition{4} \init{1}}
\place{P14}{\name{flag2=1} \partition{4}}

\place{P15}{\name{idle2} \partition{5} \init{1}}
\place{P16}{\name{trying2} \partition{5}}
\place{P17}{\name{incs2} \partition{5}}
\place{P18}{\name{} \partition{5}}
\place{P19}{\like{P16}}
\place{P20}{\like{P16}}
\place{P21}{\like{P16}}
\place{P22}{\like{P16}}

\transition{T1}{\name{flag1:=1}}
\transition{T2}{\name{flag2=0}}
\transition{T3}{\name{turn:=2}}
\transition{T4}{\name{turn:=2}}
\transition{T5}{\name{flag1:=0}}
\transition{T6}{\name{flag2=1}}
\transition{T7}{\name{turn=1}}
\transition{T8}{\name{turn=2}}
\transition{T9}{\name{flag1:=0}}
\transition{T10}{\name{turn=2}}
\transition{T11}{\name{turn=1}}
\transition{T12}{\name{flag1:=1}}

\transition{T13}{\name{flag2:=1}}
\transition{T14}{\name{flag1=0}}
\transition{T15}{\name{turn:=1}}
\transition{T16}{\name{turn:=1}}
\transition{T17}{\name{flag2:=0}}
\transition{T18}{\name{flag1=1}}
\transition{T19}{\name{turn=2}}
\transition{T20}{\name{turn=1}}
\transition{T21}{\name{flag2:=0}}
\transition{T22}{\name{turn=1}}
\transition{T23}{\name{turn=2}}
\transition{T24}{\name{flag2:=1}}

\arc{A1}{\from{P1} \to{T1}}
\arc{A2}{\from{P9} \to{T1}}
\arc{A3}{\from{T1} \to{P2}}
\arc{A4}{\from{T1} \to{P10}}

\arc{A5}{\from{P2} \to{T2}}
\arc{A6}{\from{P13} \to{T2}}
\arc{A7}{\from{T2} \to{P3}}
\arc{A8}{\from{T2} \to{P13}}

\arc{A9}{\from{P3} \to{T3}}
\arc{A10}{\from{P11} \to{T3}}
\arc{A11}{\from{T3} \to{P4}}
\arc{A12}{\from{T3} \to{P12}}

\arc{A13}{\from{P3} \to{T4}}
\arc{A14}{\from{P12} \to{T4}}
\arc{A15}{\from{T4} \to{P4}}
\arc{A16}{\from{T4} \to{P12}}

\arc{A17}{\from{P4} \to{T5}}
\arc{A18}{\from{P10} \to{T5}}
\arc{A19}{\from{T5} \to{P1}}
\arc{A20}{\from{T5} \to{P9}}

\arc{A21}{\from{P2} \to{T6}}
\arc{A22}{\from{P14} \to{T6}}
\arc{A23}{\from{T6} \to{P5}}
\arc{A24}{\from{T6} \to{P14}}

\arc{A25}{\from{P5} \to{T7}}
\arc{A26}{\from{P11} \to{T7}}
\arc{A27}{\from{T7} \to{P2}}
\arc{A28}{\from{T7} \to{P11}}

\arc{A29}{\from{P5} \to{T8}}
\arc{A30}{\from{P12} \to{T8}}
\arc{A31}{\from{T8} \to{P6}}
\arc{A32}{\from{T8} \to{P12}}

\arc{A33}{\from{P6} \to{T9}}
\arc{A34}{\from{P10} \to{T9}}
\arc{A35}{\from{T9} \to{P7}}
\arc{A36}{\from{T9} \to{P9}}

\arc{A37}{\from{P7} \to{T10}}
\arc{A38}{\from{P12} \to{T10}}
\arc{A39}{\from{T10} \to{P7}}
\arc{A40}{\from{T10} \to{P12}}

\arc{A41}{\from{P7} \to{T11}}
\arc{A42}{\from{P11} \to{T11}}
\arc{A43}{\from{T11} \to{P8}}
\arc{A44}{\from{T11} \to{P11}}

\arc{A45}{\from{P8} \to{T12}}
\arc{A46}{\from{P9} \to{T12}}
\arc{A47}{\from{T12} \to{P2}}
\arc{A48}{\from{T12} \to{P10}}

\arc{A49}{\from{P15} \to{T13}}
\arc{A50}{\from{P13} \to{T13}}
\arc{A51}{\from{T13} \to{P16}}
\arc{A52}{\from{T13} \to{P14}}

\arc{A53}{\from{P16} \to{T14}}
\arc{A54}{\from{P9} \to{T14}}
\arc{A55}{\from{T14} \to{P17}}
\arc{A56}{\from{T14} \to{P9}}

\arc{A57}{\from{P17} \to{T15}}
\arc{A58}{\from{P12} \to{T15}}
\arc{A59}{\from{T15} \to{P18}}
\arc{A60}{\from{T15} \to{P11}}

\arc{A61}{\from{P17} \to{T16}}
\arc{A62}{\from{P11} \to{T16}}
\arc{A63}{\from{T16} \to{P18}}
\arc{A64}{\from{T16} \to{P11}}

\arc{A65}{\from{P18} \to{T17}}
\arc{A66}{\from{P14} \to{T17}}
\arc{A67}{\from{T17} \to{P15}}
\arc{A68}{\from{T17} \to{P13}}

\arc{A69}{\from{P16} \to{T18}}
\arc{A70}{\from{P10} \to{T18}}
\arc{A71}{\from{T18} \to{P19}}
\arc{A72}{\from{T18} \to{P10}}

\arc{A73}{\from{P19} \to{T19}}
\arc{A74}{\from{P12} \to{T19}}
\arc{A75}{\from{T19} \to{P16}}
\arc{A76}{\from{T19} \to{P12}}

\arc{A77}{\from{P19} \to{T20}}
\arc{A78}{\from{P11} \to{T20}}
\arc{A79}{\from{T20} \to{P20}}
\arc{A80}{\from{T20} \to{P11}}

\arc{A81}{\from{P20} \to{T21}}
\arc{A82}{\from{P14} \to{T21}}
\arc{A83}{\from{T21} \to{P21}}
\arc{A84}{\from{T21} \to{P13}}

\arc{A85}{\from{P21} \to{T22}}
\arc{A86}{\from{P11} \to{T22}}
\arc{A87}{\from{T22} \to{P21}}
\arc{A88}{\from{T22} \to{P11}}

\arc{A89}{\from{P21} \to{T23}}
\arc{A90}{\from{P12} \to{T23}}
\arc{A91}{\from{T23} \to{P22}}
\arc{A92}{\from{T23} \to{P12}}

\arc{A93}{\from{P22} \to{T24}}
\arc{A94}{\from{P13} \to{T24}}
\arc{A95}{\from{T24} \to{P16}}
\arc{A96}{\from{T24} \to{P14}}

\endnet

Atomic propositions in formulae

Atomic propositions can consist of ...

• Place identifiers
  A place identifier can be an atomic proposition, for example P1, P2, P3.
   
• Place names
  One can use the name of a place as atomic proposition, for example "incs1".

Names must be typed in quotes.