Difference between revisions of "Offline Team1 Benchmark2"

From CRV
Jump to: navigation, search
 
Line 52: Line 52:
  
 
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".
 
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 ==
 +
 +
This is a space where other teams can ask for clarifications and the submitting team can answer. When a team requests a clarification, the team should be mentioned in the request and the request timestamped. The team submitting the benchmark should ensure they watch this page so that they get notifications of questions.

Latest revision as of 15:24, 14 July 2016

Please read the beginning of Benchmark 1 for information about the context of this benchmark and a description of the trace format.

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

This is a space where other teams can ask for clarifications and the submitting team can answer. When a team requests a clarification, the team should be mentioned in the request and the request timestamped. The team submitting the benchmark should ensure they watch this page so that they get notifications of questions.