migrate project

parent 8ca56b70
*.aux
*.bbl
*.blg
*.dvi
*.fdb_latexmk
*.fls
*.log
*.out
*.pdf
*.run.xml
*.synctex.gz
$pdf_mode = 1;
$clean_ext = "bbl";
$pdflatex = 'lualatex %O --shell-escape %S -synctex=1';
Version history for the LLNCS LaTeX2e class
date filename version action/reason/acknowledgements
----------------------------------------------------------------------------
29.5.96 letter.txt beta naming problems (subject index file)
thanks to Dr. Martin Held, Salzburg, AT
subjindx.ind renamed to subjidx.ind as required
by llncs.dem
history.txt introducing this file
30.5.96 llncs.cls incompatibility with new article.cls of
1995/12/20 v1.3q Standard LaTeX document class,
\if@openbib is no longer defined,
reported by Ralf Heckmann and Graham Gough
solution by David Carlisle
10.6.96 llncs.cls problems with fragile commands in \author field
reported by Michael Gschwind, TU Wien
25.7.96 llncs.cls revision a corrects:
wrong size of text area, floats not \small,
some LaTeX generated texts
reported by Michael Sperber, Uni Tuebingen
16.4.97 all files 2.1 leaving beta state,
raising version counter to 2.1
8.6.97 llncs.cls 2.1a revision a corrects:
unbreakable citation lists, reported by
Sergio Antoy of Portland State University
11.12.97 llncs.cls 2.2 "general" headings centered; two new elements
for the article header: \email and \homedir;
complete revision of special environments:
\newtheorem replaced with \spnewtheorem,
introduced the theopargself environment;
two column parts made with multicol package;
add ons to work with the hyperref package
07.01.98 llncs.cls 2.2 changed \email to simply switch to \tt
25.03.98 llncs.cls 2.3 new class option "oribibl" to suppress
changes to the thebibliograpy environment
and retain pure LaTeX codes - useful
for most BibTeX applications
16.04.98 llncs.cls 2.3 if option "oribibl" is given, extend the
thebibliograpy hook with "\small", suggested
by Clemens Ballarin, University of Cambridge
20.11.98 llncs.cls 2.4 pagestyle "titlepage" - useful for
compilation of whole LNCS volumes
12.01.99 llncs.cls 2.5 counters of orthogonal numbered special
environments are reset each new contribution
27.04.99 llncs.cls 2.6 new command \thisbottomragged for the
actual page; indention of the footnote
made variable with \fnindent (default 1em);
new command \url that copys its argument
2.03.00 llncs.cls 2.7 \figurename and \tablename made compatible
to babel, suggested by Jo Hereth, TU Darmstadt;
definition of \url moved \AtBeginDocument
(allows for url package of Donald Arseneau),
suggested by Manfred Hauswirth, TU of Vienna;
\large for part entries in the TOC
16.04.00 llncs.cls 2.8 new option "orivec" to preserve the original
vector definition, read "arrow" accent
17.01.01 llncs.cls 2.9 hardwired texts made polyglot,
available languages: english (default),
french, german - all are "babel-proof"
20.06.01 splncs.bst public release of a BibTeX style for LNCS,
nobly provided by Jason Noble
14.08.01 llncs.cls 2.10 TOC: authors flushleft,
entries without hyphenation; suggested
by Wiro Niessen, Imaging Center - Utrecht
23.01.02 llncs.cls 2.11 fixed footnote number confusion with
\thanks, numbered institutes, and normal
footnote entries; error reported by
Saverio Cittadini, Istituto Tecnico
Industriale "Tito Sarrocchi" - Siena
28.01.02 llncs.cls 2.12 fixed footnote fix; error reported by
Chris Mesterharm, CS Dept. Rutgers - NJ
28.01.02 llncs.cls 2.13 fixed the fix (programmer needs vacation)
17.08.04 llncs.cls 2.14 TOC: authors indented, smart \and handling
for the TOC suggested by Thomas Gabel
University of Osnabrueck
07.03.06 splncs.bst fix for BibTeX entries without year; patch
provided by Jerry James, Utah State University
14.06.06 splncs_srt.bst a sorting BibTeX style for LNCS, feature
provided by Tobias Heindel, FMI Uni-Stuttgart
16.10.06 llncs.dem 2.3 removed affiliations from \tocauthor demo
11.12.07 llncs.doc note on online visibility of given e-mail address
15.06.09 splncs03.bst new BibTeX style compliant with the current
requirements, provided by Maurizio "Titto"
Patrignani of Universita' Roma Tre
30.03.10 llncs.cls 2.15 fixed broken hyperref interoperability;
patch provided by Sven Koehler,
Hamburg University of Technology
15.04.10 llncs.cls 2.16 fixed hyperref warning for informatory TOC entries;
introduced \keywords command - finally;
blank removed from \keywordname, flaw reported
by Armin B. Wagner, IGW TU Vienna
15.04.10 llncs.cls 2.17 fixed missing switch "openright" used by \backmatter;
flaw reported by Tobias Pape, University of Potsdam
27.09.13 llncs.cls 2.18 fixed "ngerman" incompatibility; solution provided
by Bastian Pfleging, University of Stuttgart
04.09.17 llncs.cls 2.19 introduced \orcidID command
10.03.18 llncs.cls 2.20 adjusted \doi according to CrossRef requirements;
TOC: removed affiliation numbers
splncs04.bst added doi field;
bold journal numbers
samplepaper.tex new sample paper
llncsdoc.pdf new LaTeX class documentation
This diff is collapsed.
Dear LLNCS user,
The files in this directory belong to the LaTeX2e package for
Lecture Notes in Computer Science (LNCS) of Springer-Verlag.
It consists of the following files:
readme.txt this file
history.txt the version history of the package
llncs.cls the LaTeX2e document class
samplepaper.tex a sample paper
fig1.eps a figure used in the sample paper
llncsdoc.pdf the documentation of the class (PDF version)
splncs04.bst current LNCS BibTeX style with alphabetic sorting
This diff is collapsed.
\documentclass[runningheads,envcountsect,envcountsame,a4paper]{lncs/llncs}
\usepackage[a4paper,textwidth=12.6cm,textheight=20.5cm,heightrounded,hratio=1:1,vratio=3:5]{geometry}
\usepackage{fontspec}
\usepackage{luatexbase}
\usepackage{microtype}
\usepackage{textcomp}
\usepackage{graphicx}
\usepackage[bookmarksdepth=2,pdfauthor={Pascal Hein, Mario Fiestelmann, Stephanie Kinderreich},pdfsubject={A MontiCore Modelling Language for the Analysis of Petri Nets}]{hyperref}
\pdfvariable minorversion=7
\usepackage{listings}
\usepackage{xcolor}
\renewcommand\UrlFont{\color{blue}\rmfamily}
\usepackage{float}
\newfloat{lstfloat}{htb}{lop}
\floatname{lstfloat}{Listing}
\def\lstfloatautorefname{Listing}
\lstdefinestyle{petrinet}{
keywordstyle=[2]{\color{blue}\bfseries},
otherkeywords={<-,->},
morekeywords={petrinet,assert,place,transition,initial},
morekeywords=[2]{<-,->}
}
\lstdefinestyle{mcgrammar}{
morekeywords={grammar,extends,scope,interface,astrule,method,enum,implements,symbol,abstract}
}
\lstset{frame=single,numbers=left,basicstyle=\scriptsize,literate={"}{\textquotedbl}1,escapeinside={/@}{@/}}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{subcaption}
\usepackage{tikz}
\usetikzlibrary{arrows,shapes,snakes,automata,backgrounds,petri,positioning}
\tikzset{node distance=1.3cm,>=stealth',bend angle=45,auto}
\tikzstyle{place}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=6mm]
\tikzstyle{transition}=[rectangle,thick,draw=black!75,
fill=black!20,minimum width=8mm,inner ysep=2pt]
\tikzstyle{treenode}=[rectangle,thick,draw=blue!75,fill=blue!20,minimum size=6mm]
\usepackage{tikz-uml}
\newcommand\rdot{{}^\bullet}
\hyphenation{co-ve-ra-bi-li-ty}
\begin{document}
\title{\emph{petrinets4analysis}: A Petri Net Modeling and Analysis Language Developed with MontiCore\thanks{Practical Project for the lecture ``Software Language Engineering'' by Prof.\ Dr.\ B.\ Rumpe. The authors are grateful to Imke Drave for her supervision of the project.}}
\titlerunning{\emph{petrinets4analysis}: Petri Net Modeling with MontiCore}
%\title{A MontiCore Modelling Language for the Analysis of Petri Nets\thanks{Practical Project for the lecture ``Software Language Engineering'' by Prof.\ Dr.\ B.\ Rumpe. The authors are grateful to Imke Drave for her supervision of the project.}}
%\titlerunning{Abbreviated paper title}
\author{Pascal Hein \and
Mario Fiestelmann \and
Stephanie Kinderreich}
\authorrunning{P. Hein, M. Fiestelmann, S. Kinderreich}
\institute{RWTH Aachen Unversity, Aachen, Germany \\ \email{\normalfont\{pascal.hein, mario.fiestelmann, stephanie.kinderreich\}@rwth-aachen.de}}
\maketitle
\input{src/tex/P1.abstract}
\input{src/tex/01.intro}
\input{src/tex/02.background}
\input{src/tex/03.language}
\input{src/tex/04.implementation}
\input{src/tex/05.conclusion}
\bibliography{src/bib/Literatur.bib}
\bibliographystyle{lncs/splncs04}
\end{document}
@article{murata1989petri,
title={{Petri Nets: Properties, Analysis and Applications}},
author={Murata, Tadao},
journal={Proceedings of the IEEE},
volume={77},
number={4},
pages={541--580},
year={1989},
publisher={IEEE}
}
@book{desel2005free,
title={{Free Choice Petri Nets}},
author={Desel, Jörg and Esparza, Javier},
volume={40},
year={2005},
publisher={{Cambridge University Press}}
}
@book{rumpe2017monticore,
title={{MontiCore 5 Language Workbench. Edition 2017}},
author={Rumpe, Bernhard and H{\"o}lldobler, Katrin},
year={2017},
publisher={{Shaker Verlag}}
}
@article{dickson1913finiteness,
ISSN = {00029327, 10806377},
URL = {http://www.jstor.org/stable/2370405},
author = {Leonard Eugene Dickson},
journal = {American Journal of Mathematics},
number = {4},
pages = {413--422},
publisher = {Johns Hopkins University Press},
title = {Finiteness of the Odd Perfect and Primitive Abundant Numbers with $n$ Distinct Prime Factors},
volume = {35},
year = {1913}
}
@article{commoner1971marked,
title={{Marked Directed Graphs}},
author={Commoner, Frederic and Holt, Anatol W. and Even, Shimon and Pnueli, Amir},
journal={Journal of Computer and System Sciences},
volume={5},
number={5},
pages={511--523},
year={1971},
publisher={Academic Press}
}
@techreport{varpaaniemi1995prod,
title={{PROD Reference Manual}},
author={Varpaaniemi, Kimmo and Halme, Jaakko and Hiekkanen, Kari and Pyssysalo, Tino},
year={1995},
institution={Helsinki University of Technology},
number={B13},
}
@article{barros2007use,
title={{On the Use of Programming Languages for Textual Specification of Petri Net Models}},
author={Barros, João Paulo and Gomes, Luís},
journal={Petri Net Newsletter (Newsletter of the Special Interest Group on Petri Nets and Related System Models},
year={2007}
}
@inproceedings{matcovschi2003petri,
title={{Petri Net Toolbox for MATLAB}},
author={Matcovschi, Mihaela-Hanako and Mahulea, Cristian and Pastravanu, Octavian},
booktitle={11th IEEE Mediterranean Conference on Control and Automation MED'03},
year={2003}
}
@article{chaouiya2007petri,
title={{Petri Net Modelling of Biological Networks}},
author={Chaouiya, Claudine},
journal={Briefings in bioinformatics},
volume={8},
number={4},
pages={210--219},
year={2007},
publisher={Oxford University Press}
}
@inproceedings{yakovlev1996petri,
title={{Petri Nets and Digital Hardware Design}},
author={Yakovlev, Alexandre V and Koelmans, Albert M},
booktitle={Advanced Course on Petri Nets},
pages={154--236},
year={1996},
organization={Springer}
}
@article{parr1995antlr,
title={{ANTLR: A Predicated-$LL(k)$ Parser Generator}},
author={Parr, Terence J. and Quong, Russell W.},
journal={Software: Practice and Experience},
volume={25},
number={7},
pages={789--810},
year={1995},
publisher={Wiley Online Library}
}
@article{gansner2000open,
title={{An open graph visualization system and its applications to software engineering}},
author={Gansner, Emden R and North, Stephen C},
journal={Software: Practice and Experience},
volume={30},
number={11},
pages={1203--1233},
year={2000},
publisher={Wiley Online Library}
}
@inproceedings{kemper1992efficient,
title={{An Efficient Polynomial-Time Algorithm to Decide Liveness and Boundedness of Free-Choice Nets}},
author={Kemper, Peter and Bause, Falko},
booktitle={International Conference on Application and Theory of Petri Nets},
pages={263--278},
year={1992},
organization={Springer}
}
@book{schindler2012werkzeuginfrastruktur,
title={{Eine Werkzeuginfrastruktur zur Agilen Entwicklung mit der UML/P}},
author={Schindler, Martin},
volume={11},
year={2012},
publisher={RWTH Aachen University, Germany}
}
@article{karsai2014design,
title={{Design Guidelines for Domain Specific Languages}},
author={Karsai, Gabor and Krahn, Holger and Pinkernell, Claas and Rumpe, Bernhard and Schindler, Martin and V{\"o}lkel, Steven},
journal={arXiv preprint arXiv:1409.2378},
year={2014}
}
@book{diestel1996graphentheorie,
title={{Graphentheorie (Elektronische Ausgabe 2006)}},
author={Diestel, Reinhard},
journal={Springer-Verlag Heidelberg},
volume={2000},
pages={2006},
year={1996}
}
@book{zimmermann2007stochastic,
title={{Stochastic Discrete Event Systems}},
author={Zimmermann, Armin},
year={2007},
publisher={Springer}
}
\ No newline at end of file
% TeX root = ../../paper.tex
\section{Introduction}
% Die Logos sind veraltet und duerfen zurzeit nicht verwendet werden!
% Auf Seite \pageref{Logo} in Abbildung \ref{Logo} befindet sich das SE Logo.
Petri nets are a well-established and powerful language frequently used for modeling asynchronous or non-deterministic processes in software as well as in industrial settings, e.g.\ the design of integrated computing modules~\cite{yakovlev1996petri}. Furthermore, other application domains such as biology and chemistry also make use of these models~\cite{chaouiya2007petri}. In particular, mathematical theories can be applied to ensure conformance with design criteria. Their main use in development processes is visualization and documentation~\cite{schindler2012werkzeuginfrastruktur}\cite[p.~79]{zimmermann2007stochastic} instead of a primary design tool.
Based on the MontiCore Language Workbench~\cite{rumpe2017monticore}, we propose the textual modeling language \emph{petrinets4analysis}: In conjunction with an analysis toolkit, it enables the use of petri nets as core elements of the design process. This allows the automatic and continuous verification of models as they evolve, in particular to detect modeling errors as early as possible. Thereby, in the future, use for code generation is imaginable. With restricted and intuitive syntax, \emph{petrinets4analysis} is a domain-specific language (DSL) that is easily usable also by domain experts without knowledge of programming~\cite{karsai2014design}.
Suppose, for instance, that a simple embedded device is described by the petri net in Figure~\ref{fig:intro:example}. This petri net allows the device to create objects whenever idle, and write them to the disk once finished. Objects on the disk can be deleted afterwards. This device's disk could easily overflow! (The net is \emph{unbounded}, which we define formally in Section~\ref{sec:background:properties}.) In more complex nets, errors like this might be harder to detect. We provide our tool with the source code in Listing~\ref{lst:intro:example} which is the textual description in the \emph{petrinets4analysis} language, describing places (l. 4-6) and transitions (l. 8-16) of the net. Due to the assertion of boundedness (l. 2), our toolkit would alert the user to her modeling mistake; a simple change leads to the correction in Figure~\ref{fig:intro:example2} where a reservoir of ``disk space'' limits the number of objects written.
\begin{figure}[htb]
\centering
\begin{minipage}{0.45\textwidth}
\begin{tikzpicture}
\node [place,label=above:memory] (mem) {};
\node [place,tokens=1,below of=mem,label=below:idle] (idle) {};
\node [transition,left of=mem,label=right:create,rotate=90] (create) {}
edge[pre,bend right=45] (idle) edge[post] (mem);
\node [place,right=2cm of mem,label=above:disk] (disk) {};
\node [transition,right of=mem,label=right:write,rotate=90] (write) {}
edge[pre] (mem) edge[post,bend left=45] (idle) edge[post] (disk);
\node [transition,right of=disk,label=right:delete,rotate=90] (del) {}
edge[pre] (disk);
\end{tikzpicture}
\caption{A simple, unbounded petri net. For a more detailed explanation, we refer to Section~\ref{sec:background}.}\label{fig:intro:example}
\end{minipage}
\hfill
\begin{minipage}{0.45\textwidth}
\begin{tikzpicture}
\node [place,label=above:memory] (mem) {};
\node [place,tokens=1,below of=mem,label=below:idle] (idle) {};
\node [transition,left of=mem,label=right:create,rotate=90] (create) {}
edge[pre,bend right=45] (idle) edge[post] (mem);
\node [place,right=2cm of mem,label=above:disk] (disk) {};
\node [place,below of=disk,tokens=3,label=below:disk space] (space) {};
\node [transition,right of=mem,label=right:write,rotate=90] (write) {}
edge[pre] (mem) edge[post,bend left=40] (idle) edge[post] (disk) edge[pre,bend right=40] (space);
\node [transition,right of=disk,label=right:delete,rotate=90] (del) {}
edge[pre] (disk) edge[post,bend left=45] (space);
\end{tikzpicture}
\caption{A place has been added to the petri net in Figure~\ref{fig:intro:example} to make it bounded.}\label{fig:intro:example2}
\end{minipage}
\end{figure}
\begin{lstfloat}
\centering
\begin{lstlisting}[style=petrinet]
petrinet Processing {
assert bounded; // checks the net for boundedness
// an error is thrown, because it is unbounded
place memory;
place idle initial 1; // places are slots where tokens are stored
place disk; // at start of execution, "idle" contains 1 token
transition create: // transitions move tokens between places
1 <- idle // this edge removes one token from "idle"
1 -> memory // and one token is put into "memory"
transition write:
1 <- memory
1 -> disk
1 -> idle
transition delete:
1 <- disk
}
\end{lstlisting}
\caption{petrinets4analysis code for the model in Figure~\ref{fig:intro:example}}\label{lst:intro:example}
\end{lstfloat}
After reviewing theoretical foundations in Section~\ref{sec:background}, we describe our language design in Section~\ref{sec:language} and discuss selected implementation details in Section~\ref{sec:implementation}.
\subsubsection{Related Work}
Clearly, both textual descriptions for modeling artifacts---including petri nets---and their analysis are not new. For instance, Barros and Gomes~\cite{barros2007use} discuss the merits of defining a new language versus adding syntax to an existing one. They propose an extension of Ruby syntax to support composition, addition, and refinement. Similarly, Varpaaniemi et al.~\cite{varpaaniemi1995prod} describe a specification language for Pr/T nets (similar in nature to petri nets) on top of the C language preprocessor, which in turn generates a reachability analysis tool.
With these approaches, developers have access to the power of the underlying language (e.g. C), allowing the use of existing macros, expressions, libraries and development environments. On the other hand, specifically designed languages may be easier for domain experts to learn and apply due to their restricted and intuitive syntax~\cite{karsai2014design}. Through the use of MontiCore~\cite{rumpe2017monticore}, we are able to design such a language without the overhead of creating a parser and infrastructure from scratch, one of the drawbacks identified by Barros and Gomes~\cite{barros2007use}.
MontiCore has been used previously to design other DSLs for modeling processes. In particular, UML/P~\cite{schindler2012werkzeuginfrastruktur} is a powerful formalization of the popular Unified Modeling Language that can be used both for verification and code generation, also targeting the modeling and design phases. Our work expands on this idea by targeting petri nets, hence covering another artifact type.
On the other hand, Matcovschi et al.~\cite{matcovschi2003petri} provide a toolbox for the MATLAB environment that implements many behavioral and structural analyses for graphical petri net models. Its focus is not on language design but on ease of use for designing and analyzing nets through a graphical interface. However, models can easily become too large for graphical editors, while textual representations are more easily built from multiple components~\cite{barros2007use}.
While the capabilities of \emph{petrinets4analysis} are severely restricted in comparison with state-of-the-art tools, it serves as a proof of concept for intuitive domain-specific, textual modeling languages which can more easily be integrated into a development process. Our main focus is on the use of the MontiCore Language Workbench~\cite{rumpe2017monticore} to design such a language with minimal effort, and hence its increased maintainability and extensibility.
This diff is collapsed.
% TeX root = ../../paper.tex
\section{Language}\label{sec:language}
The \emph{petrinets4analysis} language is defined on a syntactical level (in particular, the parser) and on a semantic level, both aided by MontiCore generation capabilities. In this section, we discuss implementation choices for both of these.
\subsection{Grammar Design}
The syntactic foundation of a textual software language is a context-free grammar which defines all valid keywords and permissible input values as well as syntactic sugar (e.g. punctuation and bracketing), and their static arrangement~\cite{rumpe2017monticore}. We define a grammar for the MontiCore Language Workbench that specifies the syntax of the \emph{petrinets4analysis} language, which produces Java classes for the abstract syntax tree (AST) as well as additional infrastructure (cf. Section~\ref{sec:implementation}). The desired modeling elements are
\begin{itemize}
\item structural features: places, transitions and edges between them
\item behavioral annotations: initial markings, i.e. token counts in places, and weights on edges
\item presupposition of analytical conditions that ensure conformance with certain behavioral properties (e.g. boundedness, cf. Section \ref{sec:background:properties})
\end{itemize}
Consequently, the \texttt{Petrinet} grammar in Listing \ref{lst:language:grammar} defines the structure of the \emph{petrinets4analysis} language. It contains non-terminals for the most important elements to represent the required modeling capabilities. Places (l.~\ref{grammar:place}), transitions (l.~\ref{grammar:transition}) and edges (l.~\ref{grammar:edgestart}-\ref{grammar:edgeend}) are represented by the non-terminals of the corresponding name.
\begin{lstfloat}
\centering
\begin{lstlisting}[style=mcgrammar]
grammar Petrinet extends de.monticore.literals.Literals {
scope Petrinet = "petrinet" Name "{"
Assertion*
(Place | Transition)*
"}";
Assertion = "assert" Requirement ";";
interface Requirement;/@\label{grammar:requirement}@/
astrule Requirement =
method Optional<Boolean> verify(ASTPetrinet petrinet) { };
GlobalRequirement implements Requirement = GlobalFeature;/@\label{grammar:globalreq}@/
enum GlobalFeature = "bounded" | "safe";
SubclassRequirement implements Requirement = Subclass;
enum Subclass = "state_machine" | "marked_graph" | "free_choice"
| "extended_free_choice" | "asymmetric_choice";
Liveness implements Requirement =
LivenessLevel ("(" ("*" | (TransitionReference || ",")+) ")")?;
enum LivenessLevel = "l0live" | "l1live";
TransitionReference = transition:Name@Transition;/@\label{grammar:liveend}@/
symbol Place = "place" Name ("initial" initial:IntLiteral)? ";";/@\label{grammar:place}@/
astrule Place = outEdge:FromEdge* inEdge:ToEdge*;/@\label{grammar:placeast}@/
symbol Transition = "transition" Name ":" (FromEdge | ToEdge)*;/@\label{grammar:transition}@/
abstract Edge = count:IntLiteral place:Name@Place;/@\label{grammar:edgestart}@/
FromEdge extends Edge = count:IntLiteral "<-" place:Name@Place;
ToEdge extends Edge = count:IntLiteral "->" place:Name@Place;/@\label{grammar:edgeend}@/
}
\end{lstlisting}
\caption{The \emph{petrinets4analysis} MontiCore grammar}\label{lst:language:grammar}
\end{lstfloat}
Analytical preconditions can be imposed by the \texttt{Assertion} non-terminal, which itself contains a \texttt{Requirement} interface (l.~\ref{grammar:requirement}). As in object-oriented programming languages, interface non-terminals in MontiCore grammars have to be implemented by concrete types that expose certain methods. Here, implementing non-terminals correspond to criteria expected of the model, and they must implement a method for their verification. This interface pattern makes the language extensible to more criteria. Our \texttt{Liveness}, \texttt{GlobalFeature} (for boundedness or safeness) and \texttt{SubclassRequirement} (l.~\ref{grammar:globalreq}-\ref{grammar:liveend}) non-terminals implement this interface and can thus be used in models of the language.
Another design detail of the grammar is the segmentation of edges into \texttt{FromEdge} and \texttt{ToEdge}. It would be possible to formalize edges as one non-terminal, where the two different directions (defined by \texttt{<-} and \texttt{->}) are only differentiated by a Boolean attribute. However, for analysis purposes it is convenient to access these sets separately (including derived properties, such as their size). Modeling the grammar with a Boolean attribute that distinguishes the edges would mean to search through all existing edges and check the Boolean attribute each time the application accesses any kind of edge. Our approach ensures that incoming and outgoing edges are saved separately, leveraging the methods generated by MontiCore.
While \texttt{Transition} non-terminals contain edges naturally as part of the AST, places have no reference to them. However, analysis implementations must be able to access incoming and outgoing edges of a place; we add them manually---again utilizing MontiCore to define these lists' interfaces through an \texttt{astrule} for the \texttt{Place} non-terminal.
\subsection{Well-formedness of Models}\label{sec:lang:semantics}
The grammar ensures syntactic correctness of textual petri net definitions, but additionally, models must be well-formed. This can be verified via context conditions (cocos) in MontiCore. Cocos are handwritten Java classes implementing a specific visitor pattern that check the internal representation of defined models for contextual inconsistencies~\cite{rumpe2017monticore}. For the petri net language, we define the following rules:
\begin{itemize}
\item Place and transition names must be unique.
\item Edges in one transition must be unique.
\item Assertions must appear uniquely.
\item Place and transition names must exist if they are referred to in the model.
\item A model has to satisfy all assertions stated in the model definition.
\end{itemize}
With the first four conditions the correct parsing and interpretation of the models is guaranteed, since there is no possibility for ambiguities or usage of non-existing objects. Furthermore, the last coco delivers a mechanism to reject petri nets which claim conformance with properties (e.g. boundedness, liveness) but do not satisfy them: with this mechanism, continuous verification within the modeling process is made possible.
This diff is collapsed.
% TeX root = ../../paper.tex
\section{Conclusion}
Petri nets are a popular tool for modeling, visualizing and analyzing processes, especially in asynchronous or non-deterministic settings. With the textual modeling language \emph{petrinets4analysis}, we support the use of petri nets in the design process enabled by the automatic and continuous verification of models. This helps to detect modeling errors as early as possible. Moreover, the restricted and intuitive syntax of our DSL has the advantage that it can also be used by non-programmers~\cite{karsai2014design}.
We implement methods for analyzing the petri nets regarding properties like liveness or boundedness through evaluation of the coverability tree, as well as transformations which reduce the complexity of petri nets by eliminating places or transitions and hence decrease computation time for subsequent tasks.
With the help of visitors, the tool can output petri nets in different formats: we produce both a syntactically correct model of the \emph{petrinets4analysis} language following common formatting guidelines, as well as a graph representation in the \emph{Dot} language~\cite{gansner2000open} for further processing and visualisation.
The MontiCore Language Workbench~\cite{rumpe2017monticore} on which the \emph{petrinets4analysis} tool is based allows us to design the language and toolkit with minimal effort. From a context-free grammar defining the syntax for petri net models, we obtain a parser as well as Java code and infrastructure for AST processing and contextual verification through cocos. While similar (and more powerful) tools for petri net processing exist, our tool proves the efficiency of using a language workbench such as MontiCore, resulting in a small handwritten codebase of language-specific additions, a fact that greatly benefits maintainability and extensibility.
% TeX root = ../../paper.tex
\begin{abstract}
In modeling and design, both textual and visual artifacts have long been used~\cite{schindler2012werkzeuginfrastruktur}. Petri nets are a powerful tool used for asynchronous or non-deterministic processes in software development, industrial engineering~\cite{yakovlev1996petri} and other domains~\cite{chaouiya2007petri}. With powerful analysis toolkits they can be used not only for visualization but also to support modeling and verification~\cite{barros2007use}.
We propose a textual modeling language, \emph{petrinets4analysis}, based on the MontiCore Language Workbench~\cite{rumpe2017monticore}, which affords the use of petri nets as a primary modeling artifact. Our domain specific language (DSL) is usable by programmers and non-programmers alike, and the corresponding analysis toolkit allows access to transformations, model checking, and printing functionality. Due to the powerful language generation by MontiCore based on a simple context-free grammar, only a small hand-written codebase is needed, enhancing maintainability and extensibility.
Our work demonstrates the use of language workbenches to create a modeling DSL and the accompanying benefits, and can easily be expanded upon to include more advanced analysis techniques or transformations.
% 1.) Introduction. In one sentence, what’s the topic? Phrase it in a
% way that your reader will understand. If you’re writing a PhD thesis,
% your readers are the examiners – assume they are familiar with the
% general field of research, so you need to tell them specifically what
% topic your thesis addresses. Same advice works for scientific papers –
% the readers are the peer reviewers, and eventually others in your
% field interested in your research, so again they know the background
% work, but want to know specifically what topic your paper covers.
%
%
% 2.) State the problem you tackle. What’s the key research question?
% Again, in one sentence. (Note: For a more general essay, I’d adjust
% this slightly to state the central question that you want to address)
% Remember, your first sentence introduced the overall topic, so now you
% can build on that, and focus on one key question within that topic. If
% you can’t summarize your thesis/paper/essay in one key question, then
% you don’t yet understand what you’re trying to write about. Keep
% working at this step until you have a single, concise (and
% understandable) question.
%
% 3.) Summarize (in one sentence) why nobody else has adequately
% answered the research question yet. For a PhD thesis, you’ll have an
% entire chapter, covering what’s been done previously in the
% literature. Here you have to boil that down to one sentence. But
% remember, the trick is not to try and cover all the various ways in
% which people have tried and failed; the trick is to explain that
% there’s this one particular approach that nobody else tried yet (hint:
% it’s the thing that your research does). But here you’re phrasing it
% in such a way that it’s clear it’s a gap in the literature. So use a
% phrase such as “previous work has failed to address…”. (if you’re
% writing a more general essay, you still need to summarize the source