Offline BeepBeep 3 Benchmark3

From CRV
Revision as of 16:36, 14 June 2016 by Giles (Talk | contribs) (Created page with "'''Pingus''' See Benchmark 1 for overview ''List of categories'' == Benchmark Data == === The Trace Part === See Benchmark 1 === The Property Part === Turn around =====...")

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

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:

|x1-x2| < 6 and |y1-y2| < 10

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

  • Find two Pingus with IDs i1 and i2 such that i1 is a Walker and i2 is a Blocker
  • Check that they collide using the formula above
  • If i1'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 (∃ p1 ∊ characters/character : ∃ p2 ∊ characters/character : ∃ i1 ∊ p1/id :
  (p1/status = WALKER ∧ p2/status = BLOCKER ∧
  p1/velocity/x > 0 ∧ |p1/position/x - p2/position/x| < 6 ∧ |p1/position/y - p2/position/y| < 10)
  → (X characters/character[id=i1]/velocity/x < 0))

Intuitively, the first line fetches the XML elements for the two characters and the ID of p1, 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.

Clarification Requests