Difference between revisions of "Offline Team1 Benchmark2"

From CRV
Jump to: navigation, search
(Created page with "===== 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...")
 
Line 1: Line 1:
 +
Please read the beginning of Benchmark 1 for information about the context of this benchmark and a description of the trace format.
 +
 
===== Informal Description =====
 
===== Informal Description =====
  

Revision as of 15:22, 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".