Difference between revisions of "Offline BeepBeep 3 Benchmark2"
(Created page with "'''Pingus''' See Benchmark 1 for overview ''List of categories'' == Benchmark Data == === The Trace Part === See Benchmark 1 === The Property Part === Endless bashing =...") |
(→The Property Part) |
||
Line 11: | Line 11: | ||
=== The Property Part === | === The Property Part === | ||
− | Endless bashing | + | 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 ===== | ===== Informal Description ===== |
Latest revision as of 16:38, 14 June 2016
Pingus See Benchmark 1 for overview
List of categories
Contents
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".