Difference between revisions of "Offline Team1 Benchmark3"
(Created page with "Please read the beginning of Benchmark 1 for information about the context of this benchmark and a description of the trace format. ===== Informal Description ===== A Walker...") |
(No difference)
|
Latest revision as of 15:23, 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.
Contents
Informal Description
A Walker encountering a Blocker must turn around and keep on walking.
Demonstration Traces
The following trace fragment shows in the first event a Walker (ID 0) colliding with a Blocker (ID 1), and in the second, the same Walker that keeps on walking in its original direction.
<message> <characters> <character> <id>0</id> <status>WALKER</status> <position> <x>100</x> <y>60</y> </position> <velocity> <x>0.5</x> <y>0.5</y> </velocity> </character> <character> <id>1</id> <status>BLOCKER</status> <position> <x>104</x> <y>61</y> </position> <velocity> <x>0</x> <y>0</y> </velocity> </character> ... </characters> </message> <message> <characters> <character> <id>0</id> <status>WALKER</status> ... <velocity> <x>0.5</x> <y>0.5</y> </velocity> </character> ... </characters> </message>
In the dataset, the traces labelled rebel-walker
violate this property.
Formal Specification
The complexity added to this property is that one cannot resort to "slices" of a single Pingu, as we need to correlate in each event the x-y positions of two Pingus.
In this dataset, two Pingus collide if:
|x1-x2| < 6 and |y1-y2| < 10
where (xi,yi) are the x-y coordinates of Pingu i. One must therefore:
- Find two Pingus with IDs i1 and i2 such that i1 is a Walker and i2 is a Blocker
- Check that they collide using the formula above
- If i1's x-velocity in the current event is positive, it should be negative in the next event, and vice versa
A FO-LTL Specification
To simplify, in LTL-FO+, we can break the specification in two cases: one for the Walker going to the right (x-velocity positive), and the other for the Walker going to the left. Here is the first of these cases:
G (∃ p1 ∊ characters/character : ∃ p2 ∊ characters/character : ∃ i1 ∊ p1/id :
(p1/status = WALKER ∧ p2/status = BLOCKER ∧
p1/velocity/x > 0 ∧ |p1/position/x - p2/position/x| < 6 ∧ |p1/position/y - p2/position/y| < 10)
→ (X characters/character[id=i1]/velocity/x < 0))
Intuitively, the first line fetches the XML elements for the two characters and the ID of p1, the second line checks that they are respecively a Walker and a Blocker, the third checks that they collide, and the last checks that in the next event, the velocity of the walker has changed its sign.
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.