Difference between revisions of "Offline BeepBeep 3 Benchmark2"

Latest revision as of 16:38, 14 June 2016

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 2: Endless bashing

Informal Description

Every Basher must become a Walker when it stops bashing. Bashers dig horizontal tunnels into walls; all these walls are of finite dimensions and hence a Basher that keeps bashing until the end of a level indicates a problem.

Note that it is not sufficient to check that no Bashers remain in the last event of the trace, since:

• A Pingu could be a Basher and then disappear (not allowed)
• A Pingu could change from being a Basher to something other than walker (not allowed either)

Demonstration Traces

This sequence of two events, anywhere in a trace, is illegal:

<message>
  <characters>
    <character>
      <id>0</id>
      <status>BASHER</status>
      ...
    </character>
   ...
   </characters>
</message>

<message>
  <characters>
    <character>
      <id>0</id>
      <status>BLOCKER</status>
      ...
    </character>
   ...
   </characters>
</message>

In the dataset, the traces labelled basher-blocker violate this property.

Formal Specification

This property introduces an additional complexity, as the same constraint applies independently for every Pingu in the trace. A first way of checking it is to "slice" the trace into subtraces, one for each ID. For each such slice, the property then becomes:

G status=BASHER → (status=BASHER U status=WALKER)

A FO-LTL Specification

Without resorting to slices, a specification in LTL-FO+ reads as:

G ∃ x ∊ characters/character/id : /characters/character[id=x]/status = BASHER → (/characters/character[id=x]/status = BASHER U /characters/character[id=x]/status = WALKER)

Note that the notation /character[id=x]/status means: "the value of the status element for the character element whose id has value x".

Clarification Requests