Offline BeepBeep 3 Benchmark3

Pingus See Benchmark 1 for overview

List of categories

Benchmark Data

The Trace Part

See Benchmark 1

The Property Part

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.