Java Team3 Benchmark2

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

Category: Social Networks

Benchmark Data

The Trace Part

See marq/java/bench2

The program consists of 6 Java files. The main file Run.java (deterministically) creates a number of social network sites and nice people and makes a certain number of steps. Then an annoying person is added and more steps are made which contain the bad behaviour of this annoying person.

An AspectJ file is provided that prints the events and can be used for monitoring.

To compile the program with instrumentation run

 java -cp "lib/*" org.aspectj.tools.ajc.Main -source 1.7 -d bin -sourceroots bench2

and to execute the program run

 java -cp "lib/*:bin" bench2.Run

The program will produce 5,050,000 events, there is a single kind of event for this property, the send event. The program violates the property.

The Property Part

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 [ count=9 ] -> Failure
                             else 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

This property can be written in first-order LTL as follows

   (forall p1)(forall p2)(
      not eventually (exists s1)(exists s2)(exists s3)( 
          send(p1,p2,s1) and 
               (noreply Until (send(p1,p2,s2) and 
                   (noreply Until send(p1,p2,s3)))
      )
      and not eventually (exists s1,...,s10)(
          send(p1,p2,s1) and 
              (noreply Until send(p1,p2,s2) and ...
              ...
              (noreply Until send(p1,p2,s10))...)
      )
   )

where

   noreply = not (exists s)(send(p2,p1,s))

however it is clear that this would be made more readable with counting quantifiers and aggregate operators.

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.

• The Trace Part seems mixed up with benchmark 1. This benchmark is only about send events, benchmark 1 is about send and ack events. -- Malte, Mufin, 2016-07-04T12