VIATRA2/Benchmarks/Petri-net Simulation Benchmark

From Eclipsepedia

Jump to: navigation, search

Contents

The Petri net simulation benchmark

Benchmark description

The Petri-net benchmark suite is defined to capture the problem of visual language simulation with dynamic operational semantics.

This suite summarizes typical domain specific language simulation with the following characteristics: (i) mostly static graph structure, (ii) relatively small and local model manipulations, and (iii) typical as-long-as-possible (ALAP) execution mode. This benchmark focuses on the effective reusability of already matched elements as typical firing of a transition only involves a small part of the net. While an incremental pattern matcher can track the changes of the Petri net and updates only the involved sub-matchings, non-incremental local search based approaches will have to restart the matching from scratch after the net changed.

For a more detailed test specification, see the following article:

Bergmann G.,Horváth Á., Ráth I., Varró D.: A Benchmark Evaluation of Incremental Pattern Matching in Graph Transformation.
In: Proc. of the 4th International Conference on Graph Transformation (ICGT'08), Leicester,
UK, September 2008 

Metamodeling

In order to have a adoptable suite we tried to define the metamodel as simple as possible and therefor used only entities and relations. For latter and more complex Petri-nets we also allowed inhibitor arcs also along with transition priority but the current suite uses only simple transitions, arcs and places.

entity('PN')
{
entity('metamodel')->""
{
  entity('PetriNet')
  {
    relation('places','PetriNet','Place');
    relation('transitions','PetriNet','Transition');
 
    entity('Arc_Weight')->"1";
    entity('Place')
     {
       entity('Place_Capacity')->"";
       entity('Token');
       relation('InhibitorArc','Place','Transition');
       relation('InhibitorArc'.'weight','Place'.'InhibitorArc','Arc_Weight');
       relation('OutArc','Place','Transition');
       relation('OutArc'.'weight','Place'.'OutArc','Arc_Weight');
       relation('capacity','Place','Place'.'Place_Capacity');
       relation('tokens','Place','Place'.'Token');
     }
    entity('Transition')
     {
       entity('Transition_Priority');
       relation('Transition'.'InArc','Transition','Place');
       relation('Transition'.'InArc'.'weight','Transition'.'InArc','Arc_Weight');
       relation('Transition'.'priority','Transition','Transition'.'Transition_Priority');
     }
  }
}
}

Initial model

In the Petri net test set, we selected “regular” Petri nets as test cases, which are generated automatically. Here regular means that the number of places and transitions are approximately equal (where their exact ratio is around 1.1). Furthermore, the net has only a low number of tokens, and thus, there are only a few fireable transitions in each marking.

To generate the elements of the test set we used six reduction operations (in the inverse direction to increase the size of the net) which are described in [2] as means to preserve safety and liveness properties of the net. These operations are combined with a weighted random operation selection. This allows fine parametrization of the number of transitions and places with an average fan-out of 3-5 incoming and outgoing edges. In all test cases, the generation started from the Petri net depicted in Fig 1.
Fig. 1.: Petri net
(which is trivially a live net) and the final test graphs are also available in PNML format from TODO.

The Petri-net generator is also available in the source zip. Feel free to use it to define new more complex Petri-nets.

Pattern and rule library

For checking that the firing enabledness condition for a Petri net transition we use the graph pattern isTransitionFireable. Its flattened version (when it is not constructed form other patterns) is the following (see also in Fig 2.
Fig. 2.: TransitionFireable pattern
):
pattern TransitionFireable_flattened(Transition) =
{
	'PetriNet'.'Transition'(Transition);
	neg pattern notFireable_flattened(Transition) =
	{
		'PetriNet'.'Place'(Place);
		'PetriNet'.'Transition'(Transition);
		'PetriNet'.'Place'.'OutArc'(OutArc, Place, Transition);
		neg pattern placeToken(Place) =
		{
			'PetriNet'.'Place'(Place); 
			'PetriNet'.'Place'.'Token'(Token);
			'PetriNet'.'Place'.'tokens'(X, Place, Token);
		}
	}
	or 
	{
		'PetriNet'.'Place'(Place);
		'PetriNet'.'Transition'(Transition);
		'PetriNet'.'Place'.'InhibitorArc'(OutArc, Place, Transition);
		'PetriNet'.'Place'.'Token'(Token);
		'PetriNet'.'Place'.'tokens'(X, Place, Token);
	}
}

The pattern uses nested negative application conditions to express that a Transition is enabled if every input Place instance connected to the Transition instance has at least one Token instance associated and no inhibitor input Place instance contains tokens. In this case, embedded NACs are used to express universal quantification with double negation of existence.

And for the Token manipulation we used the Add~ and RemoveTokens gt rules depicted in Fig 3.
Fig. 3.: Add/RemoveTokens gt rules
with the following vtcl source code:
// Removes a token from the place 'Place'.
gtrule removeToken(in Place) =
{
	precondition find placeWithToken(Place, Token)
	postcondition find placeWithoutToken(Place,Token)
}
 
// Adds a token to the place 'Place'.
gtrule addToken2(in Place) =
{
	precondition find place(Place)
	postcondition find placeWithToken(Place, Token)
}
 
pattern placeWithToken(Place, Token) =
{
	'PetriNet'.'Place'(Place);
	'PetriNet'.'Place'.'Token'(Token) in Place;
	'PetriNet'.'Place'.'tokens'(X, Place, Token);
}
 
pattern place(Place) =
{
	'PetriNet'.'Place'(Place);
}
 
pattern placeWithoutToken(Place,Token) =
{
	'PetriNet'.'Place'(Place);
}


Measurement results

TODO

Downloadables