Offline BeepBeep 3 Benchmark3

Pingus See Benchmark 1 for overview

List of categories

Benchmark Data

The Trace Part

See Benchmark 1

The Property Part

The paper on Pingus (see link at top of the page) describes many properties one can verify on the execution of the game. For the purpose of this benchmark, we picked three of them.

Property 3: Turn around

Informal Description

A Walker encountering a Blocker must turn around and keep on walking.

Demonstration Traces

The following trace fragment shows in the first event a Walker (ID 0) colliding with a Blocker (ID 1), and in the second, the same Walker that keeps on walking in its original direction.

<message>
  <characters>
    <character>
      <id>0</id>
      <status>WALKER</status>
      <position>
        <x>100</x>
        <y>60</y>
      </position>
      <velocity>
        <x>0.5</x>
        <y>0.5</y>
      </velocity>
    </character>
    <character>
      <id>1</id>
      <status>BLOCKER</status>
      <position>
        <x>104</x>
        <y>61</y>
      </position>
      <velocity>
        <x>0</x>
        <y>0</y>
      </velocity>
    </character>
   ...
   </characters>
</message>

<message>
  <characters>
    <character>
      <id>0</id>
      <status>WALKER</status>
      ...
      <velocity>
        <x>0.5</x>
        <y>0.5</y>
      </velocity>
    </character>
   ...
   </characters>
</message>

In the dataset, the traces labelled rebel-walker violate this property.

Formal Specification

The complexity added to this property is that one cannot resort to "slices" of a single Pingu, as we need to correlate in each event the x-y positions of two Pingus.

In this dataset, two Pingus collide if:

|x₁-x₂| < 6 and |y₁-y₂| < 10

where (x_i,y_i) are the x-y coordinates of Pingu i. One must therefore:

• Find two Pingus with IDs i₁ and i₂ such that i₁ is a Walker and i₂ is a Blocker
• Check that they collide using the formula above
• If i₁'s x-velocity in the current event is positive, it should be negative in the next event, and vice versa

A FO-LTL Specification

To simplify, in LTL-FO+, we can break the specification in two cases: one for the Walker going to the right (x-velocity positive), and the other for the Walker going to the left. Here is the first of these cases:

G (∃ p₁ ∊ characters/character : ∃ p₂ ∊ characters/character : ∃ i₁ ∊ p₁/id :
  (p₁/status = WALKER ∧ p₂/status = BLOCKER ∧
  p₁/velocity/x > 0 ∧ |p₁/position/x - p₂/position/x| < 6 ∧ |p₁/position/y - p₂/position/y| < 10)
  → (X characters/character[id=i₁]/velocity/x < 0))

Intuitively, the first line fetches the XML elements for the two characters and the ID of p₁, the second line checks that they are respecively a Walker and a Blocker, the third checks that they collide, and the last checks that in the next event, the velocity of the walker has changed its sign.