Twitlanger – Maude Interpreter for Twitlang

An interpreter for Twitter interactions modeling language

Summary

Online social networks are widespread means to enact interactive collaboration among people by, e.g., planning events, diffusing information, and enabling discussions. Twitter provides one of the most illustrative example of how people can effectively interact without resorting to traditional communication media. For example, the platform has acted as a unique medium for reliable communication in emergency or for organizing cooperative mass actions. This use of Twitter in a cooperative, possibly critical, setting calls for a more precise awareness of the dynamics regulating message spreading. To this aim, we designed Twitlang, a formal language to model interactions among Twitter accounts. The operational semantics associated to the language allows users to clearly and precisely determine the effects of actions performed by Twitter accounts, such as post, retweet, reply to or delete tweets. The language has been implemented in the form of a Maude interpreter, Twitlanger, which takes a language term as an input and, automatically or interactively, explores the computations arising from the term. By relying on this interpreter, automatic verification of communication properties of Twitter accounts can be carried out via the analysis tools provided by the Maude framework.

Documents

Rocco De Nicola, Alessandro Maggi, Marinella Petrocchi, Angelo Spognardi, and Francesco Tiezzi. Twitlang(er): interactions modeling language (and interpreter) for Twitter. Technical Report, IMT, 2015.

Download

The current version of the tool can be found here.

Requirements

Usage

The archive contains the Maude implementation of the interpreter. In order to use the command-line interpreter it is necessary to launch Maude, and to load the file containing the Twitlanger specification:

maude twitlanger.maude

A few examples are already defined and can be evaluated using aliases without the need to type the full specification manually. Consider, for instance, the following specification:

--- Example 1
eq example1 = !(um1 || ug1) .

eq um1 = Mickey : empty : empty : none : 
         (tweet('Hello,x) . (search( predP7(Goofy) , z )@ Mickey) . delete(x) . nil) .

eq ug1 = Goofy : empty : empty : Mickey : 
         ((search( predP7(Mickey) , z' )@ Goofy) . reply(z','Hello,void,y) . nil) .

In this simple specification the overall network is composed by two users: Mickey and Goofy. Initially they do not have any message stored in their timelines and notification lists.
Mickey’s behavior consist of tweeting “Hello”, waiting to receive Goofy’s reply and finally deleting his own original tweet.
Goofy, who is following Mickey, finds the tweet and then replies to it writing “Hello” as well.

Using Maude’s search command we can then generate the state-space comprised of all the possible evolutions of this initial state (together with the respective trace):

Maude> search example1 =>* T:Twitter .

Obtaining:

Solution 1 (state 0)
states: 1 rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)
T:Twitter --> 
!(1,
( Goofy
 : empty
 : empty
 : Mickey
 : (find(predP7(Mickey),z')@ Goofy) . reply(z', 'Hello, void, y) . nil)
 ||
 Mickey
 : empty
 : empty
 : emptyul
 : tweet('Hello, x) . (find(predP7(Goofy),z)@ Mickey) . delete(x) . nil)

Solution 2 (state 1)
states: 2 rewrites: 26 in 0ms cpu (0ms real) (~ rewrites/second)
T:Twitter --> 
!(2,
{< 1 null null 'Hello none none Mickey >}
( Goofy
 : < 1 null null 'Hello none none Mickey >
 : empty
 : Mickey
 : (find(predP7(Mickey),z')@ Goofy) . reply(z', 'Hello, void, y) . nil)
 ||
 Mickey
 : < 1 null null 'Hello none none Mickey >
 : empty
 : emptyul
 : (find(predP7(Goofy),z)@ Mickey) . delete(1) . nil)

Solution 3 (state 2)
states: 3 rewrites: 99 in 0ms cpu (0ms real) (~ rewrites/second)
T:Twitter --> 
!(2,
{< 1 null null 'Hello none none Mickey >}
{(Goofy :Nfound(< 1 null null 'Hello none none Mickey >))}
( Goofy
 : < 1 null null 'Hello none none Mickey >
 : empty
 : Mickey
 : reply(< 1 null null 'Hello none none Mickey >, 'Hello, void, y) .
 nil)
 ||
 Mickey
 : < 1 null null 'Hello none none Mickey >
 : empty
 : emptyul
 : (find(predP7(Goofy),z)@ Mickey) . delete(1) . nil)

Solution 4 (state 3)
states: 4 rewrites: 194 in 0ms cpu (0ms real) (~ rewrites/second)
T:Twitter --> 
!(3,
{< 1 null null 'Hello none none Mickey >}
{(Goofy :Nfound(< 1 null null 'Hello none none Mickey >))}
{< 2 null 1 (@ Mickey 'Hello) Mickey none Goofy >}
( Goofy
 : < 1 null null 'Hello none none Mickey > ; < 2 null 1 (@ Mickey
 'Hello) Mickey none Goofy >
 : empty
 : Mickey
 : nil)
 ||
 Mickey
 : < 1 null null 'Hello none none Mickey >
 : < 2 null 1 (@ Mickey 'Hello) Mickey none Goofy >
 : emptyul
 : (find(predP7(Goofy),z)@ Mickey) . delete(1) . nil)

Solution 5 (state 4)
states: 5 rewrites: 340 in 0ms cpu (0ms real) (~ rewrites/second)
T:Twitter --> 
!(3,
{< 1 null null 'Hello none none Mickey >}
{(Goofy :Nfound(< 1 null null 'Hello none none Mickey >))}
{< 2 null 1 (@ Mickey 'Hello) Mickey none Goofy >}
{(Mickey :Nfound(< 2 null 1 (@ Mickey 'Hello) Mickey none Goofy >))}
( Goofy
 : < 1 null null 'Hello none none Mickey > ; < 2 null 1 (@ Mickey
 'Hello) Mickey none Goofy >
 : empty
 : Mickey
 : nil)
 ||
 Mickey
 : < 1 null null 'Hello none none Mickey >
 : < 2 null 1 (@ Mickey 'Hello) Mickey none Goofy >
 : emptyul
 : delete(1) . nil)

Solution 6 (state 5)
states: 6 rewrites: 404 in 0ms cpu (0ms real) (~ rewrites/second)
T:Twitter --> 
!(3,
{< 1 null null 'Hello none none Mickey >}
{(Goofy :Nfound(< 1 null null 'Hello none none Mickey >))}
{< 2 null 1 (@ Mickey 'Hello) Mickey none Goofy >}
{(Mickey :Nfound(< 2 null 1 (@ Mickey 'Hello) Mickey none Goofy >))}
{(Mickey :Ndelete(1))}
( Goofy
 : < 2 null 1 (@ Mickey 'Hello) Mickey none Goofy >
 : empty
 : Mickey
 : nil)
 ||
 Mickey
 : empty
 : < 2 null 1 (@ Mickey 'Hello) Mickey none Goofy >
 : emptyul
 : nil)

No more solutions.
states: 6 rewrites: 410 in 0ms cpu (1ms real) (~ rewrites/second)

The solutions provided by the interpreter have the following structure:

!(id_counter,
{network_label_1}
{network_label_2}
...
{network_label_N}
( user_1 
 : timeline_1 
 : notification_list_1 
 : following_list_1 
 : behavior_1 ) 
 ||
( user_2 
 : timeline_2 
 : notification_list_2 
 : following_list_2 
 : behavior_2 ) 
 || ...
 user_M 
 : timeline_M 
 : notification_list_M 
 : following_list_M 
 : behavior_M )

The last solution represents a state that cannot further evolve, and indeed both users’ behaviours in our example have been reduced to the inert “nil” behaviour.

By providing different target system structures in the search command it is possible to evaluate specific solutions that comply to the given requirements. Moreover it is possible to define additional constraints that the solutions have to verify by using the such that clause.

As an example, the following command can be used to find all the solutions in which user Mickey has an empty timeline:

Maude> search example1 =>* T:Twitter such that (getTimeline(getUser(Mickey,T:Twitter)) == empty) .

Obtaining:

Solution 1 (state 0)
states: 1 rewrites: 8 in 0ms cpu (0ms real) (~ rewrites/second)
T:Twitter --> 
!(1,
( Goofy
 : empty
 : empty
 : Mickey
 : (find(predP7(Mickey),z')@ Goofy) . reply(z', 'Hello, void, y) . nil)
 ||
 Mickey
 : empty
 : empty
 : emptyul
 : tweet('Hello, x) . (find(predP7(Goofy),z)@ Mickey) . delete(x) . nil)

Solution 2 (state 5)
states: 6 rewrites: 434 in 0ms cpu (0ms real) (~ rewrites/second)
T:Twitter --> 
!(3,
{< 1 null null 'Hello none none Mickey >}
{(Goofy :Nfound(< 1 null null 'Hello none none Mickey >))}
{< 2 null 1 (@ Mickey 'Hello) Mickey none Goofy >}
{(Mickey :Nfound(< 2 null 1 (@ Mickey 'Hello) Mickey none Goofy >))}
{(Mickey :Ndelete(1))}
( Goofy
 : < 2 null 1 (@ Mickey 'Hello) Mickey none Goofy >
 : empty
 : Mickey
 : nil)
 ||
 Mickey
 : empty
 : < 2 null 1 (@ Mickey 'Hello) Mickey none Goofy >
 : emptyul
 : nil)

No more solutions.
states: 6 rewrites: 440 in 0ms cpu (1ms real) (~ rewrites/second)

A few utility operators are available to support conditional clauses definition, such as:

  • getUser(U:User,T:Twitter) retrieves the tuple (Network) representing the user. It can be used in conjunction with property getters:
    • getTimeline(N:Network)
    • getNotList(N:Network)
    • getFollowList(N:Network)
    • getBehavior(N:Network)
  • the same getters are overloaded and can be used directly to get the property of a specific user in Twitter:
    • getTimeline(U:User,T:Twitter)
    • getNotList(U:User,T:Twitter)
    • getFollowList(U:User,T:Twitter)
    • getBehavior(U:User,T:Twitter)
  • expand(U:User,N:Nat,T:Twitter) retrieves all the messages that a user can reach by following message links (ids) up to a given depth N (testing for presence of a message in a set of messages can be performed via the mixfix operator in, e.g. “M in MList”)

Integration with the Maude LTL Model Checker

To use Twitlanger in conjunction with the LTL Model Checker provided by Maude, type in the Maude interactive console the following command:

Maude> load twitcheck .

(NB: make sure to have the files twitcheck.maude and model-checker.maude in the same directory)

Once the module is loaded, you can ask the model checker to verify the formula form over the initial state init using the command:

Maude> reduce modelCheck(init,form) .

A number of state predicates are already defined and can be used in LTL formulas:

  • tweetSent(P:Predicate)
    given a predicate P over messages, this property holds in any state reached after a tweet matching P has been sent;
  • tweetFound(P:Predicate,U:User)
    given a predicate P over messages and a username U, this property holds in any state reached after a tweet matching P has been found (via action find) by U;
  • tweetInTimeline(P:Predicate,U:User), tweetInNList(P:Predicate,U:User), tweet@User(P:Predicate,U:User)
    given a predicate P over messages and a username U, these three properties hold in any state where a tweet matching P is present respectively in U’s timeline, notification list, or either of them;
  • tweet@Users(P:Predicate,UL:UserList)
    given a predicate P over messages and a list of usernames UL, this property holds in any state where a tweet matching P is present – either in the timeline or the notification list – in all the accounts whose usernames are in UL.

An extended case study within the academic domain is incorporated into Twitlanger.
It involves 7 Twitter users: University, Director, Office, Professor, StudentA, StudentB and TwtCloud (an account representing all the Twitter accounts external to the domain but following University).

To generate an initial state for the network, you can use the operation:

op case-study : Behavior Behavior Behavior Behavior Behavior Behavior Behavior -> Twitter .

The behaviours will be associated respectively to the following accounts: TwtCloud, University, Director, Office, Professor, StudentA, StudentB.

A number of predefined behaviour identifiers are already provided in the execution context, and can be used to test some relevant scenarios.

For example the initial state

case-study(nil,nil,nil,nil,'Bp1,nil,nil)

describes a scenario in which Professor sends a tweet about an exam.

To check whether both StudentA and StudentB receive the tweet, we can invoke the model checker to evaluate the given formula:

Maude> reduce modelCheck(case-study(nil,nil,nil,nil,'Bp1,nil,nil),tweetSent(predP4(tweet-exam)) |->
          (tweet@Users(predP4(tweet-exam),(StudentA ;; StudentB)) ) ) .

The result will be a counterexample:

result ModelCheckResult: counterexample({
!(1,
( University
 : empty
 : empty
 : Director
 : nil)
 ||
( Director
 : empty
 : empty
 : Office
 : nil)
 ||
( Office
 : empty
 : empty
 : Director ;; Professor
 : nil)
 ||
( Professor
 : empty
 : empty
 : Office ;; Director
 : 'Bp1)
 ||
( StudentA
 : empty
 : empty
 : Office
 : nil)
 ||
( StudentB
 : empty
 : empty
 : Office ;; Professor
 : nil)
 ||
 TwtCloud
 : empty
 : empty
 : University
 : nil),unlabeled}, {
!(2,
{< 1 null null (# 'exam 'will 'take 'place 'in 'classroom 'A5) none none
 Professor >}
( University
 : empty
 : empty
 : Director
 : nil)
 ||
( Director
 : empty
 : empty
 : Office
 : nil)
 ||
( Office
 : < 1 null null (# 'exam 'will 'take 'place 'in 'classroom 'A5) none
 none Professor >
 : empty
 : Director ;; Professor
 : nil)
 ||
( Professor
 : < 1 null null (# 'exam 'will 'take 'place 'in 'classroom 'A5) none
 none Professor >
 : empty
 : Office ;; Director
 : nil)
 ||
( StudentA
 : empty
 : empty
 : Office
 : nil)
 ||
( StudentB
 : < 1 null null (# 'exam 'will 'take 'place 'in 'classroom 'A5) none
 none Professor >
 : empty
 : Office ;; Professor
 : nil)
 ||
 TwtCloud
 : empty
 : empty
 : University
 : nil),deadlock})

This indicates that the formula does not hold, and the reason is trivially that StudentA does not follow Professor, thus does not receive the message.

Since we are assuming all students in the University are following the Office account, we could modify the initial state to represent the fact that Office is going to retweet all tweets with hashtag “exam”:

case-study(nil,nil,nil,'Bo,'Bp1,nil,nil)

Invoking the model checker again against this initial state will now yield:

result Bool: true

which means the property is satisfied.

About

For suggestions, remarks, bugs or requests please do not hesitate to contact any of us.

  • alessandro.maggi@imtlucca.it
  • angelo.spognardi@iit.cnr.it
  • marinella.petrocchi@iit.cnr.it
  • francesco.tiezzi@imtlucca.it