View source for Offline BeepBeep 3 Benchmark2

'''Pingus''' See Benchmark 1 for overview

''List of categories''

== Benchmark Data ==

=== The Trace Part ===

See Benchmark 1

=== The Property Part ===

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:

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

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

In the dataset, the traces labelled <code>basher-blocker</code> 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:

<b>G</b> status=BASHER &rarr; (status=BASHER <b>U</b> status=WALKER)

===== A FO-LTL Specification =====

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

<b>G</b> &exist; x ∊ characters/character/id : /characters/character[id=x]/status = BASHER &rarr; (/characters/character[id=x]/status = BASHER <b>U</b> /characters/character[id=x]/status = WALKER)

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

== Clarification Requests ==