Difference between revisions of "Java Team3 Benchmark2"

Revision as of 21:57, 2 June 2016

AnnoyingFriend. The setting is that of people sending messages to each other on social networks

Category: Social Networks

Benchmark Data

The Trace Part

<< Information about Java program to follow >>

The Property Part

See the rules for the necessary descriptions

Informal Description

The context of this property is a monitoring system that observes people's interactions with a number of social networks. It has been observed that if person A attempts to contact person B on at least three different social networking sites without any response from person B then person B finds person A annoying. Furthermore, if there are 10 such messages across any number of sites, person A is annoying person B.

This property detects annoying people with the intention that some action is taken e.g. blocking further contact or sending them a message telling them that they are annoying.

There is a single observed event: send(personA,personB,site) records that personA sent personB a message on that site. All objects can be identified as references (i.e. using == in Java).

The property is that for every two people A and B, person A does not send person B three consecutive messages on different sites without a response. Note that, symmetrically, this should also hold for B and A. A response is a message from B to A on any site i.e. not just one of the sites that A contacted B on.

Demonstration Traces

The following traces should be accepted

   send(A,B,facebook).send(A,B,myspace)
   send(A,B,facebook).send(A,B,myspace).send(A,B,facebook)
   send(A,B,facebook).send(A,B,myspace).send(B,A,twitter).send(A,B, linkedin)
   

Other than the anachronism of somebody using myspace, all three traces are okay as (i) the limits are not reached, (ii) sending to facebook twice is okay here as the total is 3, and (iii) B contacts A before the limits are reached.

The following three traces should be rejected

   send(A,B,facebook).send(A,B,myspace).send(A,B,twitter)
   send(A,B,s).send(A,B,s).send(A,B,s).send(A,B,s).send(A,B,s).send(A,B,s).send(A,B,s).send(A,B,s).send(A,B,s).send(A,B,s)
   send(B,A,facebook).send(A,B,facebook).send(A,B,myspace).send(A,B,twitter)

In the first bad trace person A sends a message to person B three times across different sites. In the second bad trace person A sends a message to person B consecutively ten times. The third trace is bad as even though B sends a message to A at the start, there are then three consecutive messages from A to B across different sites.

Formal Specification

A QEA for this property can be given as follows

   qea(AnnoyingFriend){
       Forall(p1,p2)
   
       accept skip(NoSends){
           send(p1,p2,site1) -> OneSend do [ count=1 ]
       }
       accept skip(OneSend){
           send(p1,p2,site2) if [ site1 != site2 ] -> TwoSend do [ count=count+1 ]
                             else -> OneSend do [ count=count+1]
           send(p2,p1,site) -> NoSends
      }
      accept skip(TwoSend){
           send(p1,p2,site3) if [ site1!=site3 and site2!=site3] -> Failure
                             else if [ count=9 ] -> Failure
                             else -> TwoSend do [ count=count+1 ]
            send(p2,p1,site) -> NoSends
     }    
   }

Note that the site variables are unquantified. The semantics is that they match against the value in the trace and that binding is remembered (until it is overwritten). In the same way the count variable is added to the binding and updated as the trace is processed. The values of these unquantified variables are local to each combination of quantified variables.

A FO-LTL Specification

<< To be completed >>

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.