02265: Advanced Topics in Software Engineering (f15)

This assignment is about formalising Place/Transition nets and their behaviour in mathematics and to write a plugin for generating the state space of a Petri net (assuming that they are 1-bounded, and providing an error message if it turnes out during the state space generation that this assumption is violated).

1. Formalise the concept of Place/Transition nets (with arc-weights). Note that parts of that was done in the lecture already (syntax); the firing rule needs to be adjusted:
   1. Formalise the syntax of Petri nets (which are there in the meta model of Petri nets) in mathematical terms.
   2. Formalise the states of a Petri net (in Petri nets often called marking) in mathematics (here we still assume that there can be any number of tokens on a place).
   3. Formalise when a transition is "enabled" in a state, and what its successor state is when the transition fires (this is called the "firing rule" of a Petri net).

       

2. Extend the Petri net editor from Assignment 1 by a popop action that generates all the reachable states (possibly also the transitions between them). In order to be sure that there are only finitely many states, we assume now that there is always at most one token on each place (this is called 1-boundedness).

    

   The output (displayed in a dialog window) should be the number of states and a list of states, from which a firing of a transition would violate the above 1-boundedness condition.

   1. Define a data structure for representing the states of the Petri, which properly implements a hash function and the equals method accordingly. It might be a good idea to distinguish one special marking, which indicates the violation of 1- boundedness.
   2. Define a function that, for a given marking, calculates all enabled transitions.
   3. Define a function that calculates the successor marking, for a given marking and a transition.
   4. With the above functions, implement the systematic generation of the state space. Make sure that you never add the "same" state twice.
   5. Implement a popup action that, from a Petri net in the graphical editor for Petri nets from Assignment 1, starts the generation of the state space and, in the end, shows the required information (see above) in a dialog.