Difference between revisions of "Offline BeepBeep 3 Benchmark1"

Revision as of 08:21, 28 May 2016

Name of benchmark Synthetic execution traces of the video game Pingus, used for runtime verification. All details regarding these traces can be found in the paper Automated Bug Finding in Video Games: A Case Study for Runtime Monitoring. We highly recommend you scan that paper first.

List of categories

Benchmark Data

Pingus is a clone of Psygnosis’ Lemmings game series made by Ingo Ruhnke. It regularly counts among the highest quality open source games available and was once ranked in the Top 10 Linux games by CNN. The game is divided into more than 70 levels, each of which being populated with various kinds of obstacles, walls, and gaps. Between 10 and 100 autonomous, penguin-like characters (the Pingus) progressively enter the level from a trapdoor and start walking across the area. A Pingu keeps walking in the same direction until it either reaches a wall (in which case it turns around) or falls into a gap (and dies, if it falls from too high).

The goal of the game is to have a minimum percentage of the incoming Pingus safely reach the exit door. To this end, the player can give special abilities to certain Pingus, allowing them to modify the landscape in order to create a walkable path to the goal. For example, some Pingus can become Bashers and dig into the ground; others can become Builders and construct a staircase to reach over a gap. Other abilities modify the behaviour of other Pingus: hence the Blocker stands in the way and makes any Pingu that reaches it turn around as if it encountered a wall.

The Trace Part

The dataset is made of 20 traces consisting of a simulated execution of the game; each of these traces contains from 5 to 95 Pingus walking in the game field at the same time. You can download the trace files from DataHub (click on the button "Go to resource").

All traces are in XML format. Each event of the trace has the following structure:

<message>
 <characters>
  <character>
   <id>0</id>
   <status>WALKER</status>
   <position>
    <x>62</x>
    <y>0</y>
   </position>
   <velocity>
    <x>1</x>
    <y>0</y>
   </velocity>
  </character>
  ...
 </characters>
</message>

The event is contained in a message element, which contains a single characters element. Within this element, there are multiple character elements, corresponding to the properties of a single Pingu on the game field. Each Pingu has a unique ID, a position (x-y) and a velocity vector (x-y). In addition, each Pingu has a status, which can be "walker" (normal state), or any of these special abilities: "blocker", "floater", "basher", "blower", "faller".

IDs are unique within each individual message element, but obviously, they repeat from one event to the next. Some Pingus, however, may disappear at some point in the trace if they die, so the number of character elements is not fixed for the entire trace. Within each message, IDs do not appear in any particular order: this depends on the iterator on game elements provided by the game itself. We cannot assume either that IDs start at 0 or that they form a continuous sequence.

Since Pingus' game loop runs at about 160 Hz, message elements correspond to snapshots of the game's state roughly 0.08 seconds apart. Therefore, processing the trace in real time requires handling at least that many events per second.

The Property Part

See the rules for the necessary descriptions of what should be included in the following sections

Informal Description

Demonstration Traces

Formal Specification

A FO-LTL Specification

Clarification Requests

This is a space where other teams can ask for clarifications and the submitting team can answer. When a team requests a clarification, the team should be mentioned in the request and the request timestamped. The team submitting the benchmark should ensure they watch this page so that they get notifications of questions.