These are files for the PRISM models and experiments reported in Model-checking Information Diffusion in Social Networks with PRISM submitted to PRIMA 2019. The files are organised into four directories each (apart from random_networks) of which contains its own readme. model_1 contains files associated with the Continuous Time Markov Chain model of the classic SIS model of information diffusion (Model 1 in the paper) model_2 contains files associated with the Agent View of the SIS model (Model 2 in the paper) model_3_4 contains files associated with the Threshold Influence models (Models 3 and 4 in the paper). random_networks contains the json files associated with the random networks generated to test the applicability of the "gets there first effect". The contents of the individual readmes also appears below: model_1 ======= Classic SIS model. *.gra files are data points as plotted in PRISM's internal format. *.png files are images generated using PRISM from the .gra files. si.pm is a PRISM continuous time Markov Chain model for the SI model of information diffusion in social networks for 20 agents sis.pm is a PRISM continuous time Markov Chain model for the SIS model of information diffusionin social networks for 20 agents. In each case results for different numbers of agents were obtained by altering the number the max_agents constant int he file. properties.props is a PRISM properties file containing three properties: 1. R{"infected"} =? [I=T] 2. P=? [ F <= T infected=20] 3. P=? [ F infected=20] 1. Returns the expected number of infected agents at time T 2. Returns the probability that 20 agents (all agents in the two models) will be infected at time T 3. Returns the probability that all agents will be infected at some point. experiment1a.* Plots property 2 for values of T between 0 and 5,000 and values of mu between 0 and 1 for sis.pm experiment1b.* is the same experiment but with T capped at 100,000. experiment1c.* Plots property 3 for values of mu between 0 and 1. experiment1d.* Plots property 3 for a mu of 1 and as the number of agents in the model varies. experiment1e.* Plots property 1 for values of T between 0 and 20 and values of mu between 0 and 1. model_2 ======= SIS Model taking the Agent View *.gra files are data points as plotted in PRISM's internal format. *.png files are images generated using PRISM from the .gra files. all_agents.pm is a template file to all quick generation of specfic network instances (by deleteing lines). It represents a fully connected network of 10 agents in which no agent believes phi or not phi. sis_experiment2.pm is generated from all_agents. It is fully connected network in which at the start one agent (alice) believes phi and one (bob) believese not phi sis_network_10_1.pm is generated from all_agent. It represents a random network generated as described in the paper. In its current configuration agent gwen (8 connections) intially believes phi and agent frank (2 connections) initially believes not phi. All agents believe neither phi nor not phi. These initial starting conditions can be varied by editing _status and _anti_status for each agent (initialising with 1 indicated belief). properties.props contains PRISM properties. experiment2.png/.gra the result of running sis_experiment2 with R{"infection"}=? [ I=T ] (expected infection at time T) with T between 1 and 20, incrementing by 1. experiment3.png/.gra the result of sis_network_10_1 with messages between 1 and 40, incremeting by 2 and with either 2-connected agents/6-conneceted agents/8-connected+2-connected agents at start. ScreenShot-experiment3-n+m.png files are a screenshot of the probabilities generated by PRISM that at some point all agents in the network are infected by phi where n indicates the connectivity of the agent that initially believes phi and m indicates the connectivity of the agent that initially believes not phi. These are for sis_network_10_1. timings contains files related to tracking the time taken to build a model and perform model checking for model 2. model_2/timings =============== SIS Model taking the Agent View: Timing Information Nagents.pm are files containing a fully connected network version of model 2 for N agents. generate_model_sis.pl is a perl file that will generate a fully connected version for model 2 for some number of agents supplied as an argument. properties.prop contains a PRISM property (that the network is fully infected at time 10) times.dat contains the data from running prism in three columns - the first is the number of agents, the second is the time taken in seconds to build the model and the third is the time taken in seconds for model checking. times.p is an input file for gnuplot used to chart the data in times.dat model_3_4 ========= Influence Threshold based model taking an Agent View *.gra files are data points as plotted in PRISM's internal format. *.png files are images generated using PRISM from the .gra files. all_agents.pm is a template file for Model 3 for quick generation of specfic network instances (by deleteing lines). It represents a fully connected network of 10 agents in which no agent believes phi. all_agents_anti.pm is a template file for Model 4 for quick generation of specfic network instances (by deleteing lines). It represents a fully connected network of 10 agents in which no agent believes either phi or not phi. inflence_experiment4 - fully connected network, phi starts with one agent. influence_experiment5 - using nettverk_10_1 (see model 2), phi starts with one agent. influence_anti_experiment6 - fully connected network with phi and not phi influence_anti_experiment7 - using nettverk_10_1 (see model_2)) with phi and not phi properties.props contains PRISM properties. experiment4.png/.gra the results of running influence_experiment4 with R{"infection"}=? [ I=T ] (expected infection at time T) with T between 1 and 20. experiment5.png/.gra the results of influence_experiment5 with T between 1 and 40, with either 2-connected agents/6-conneceted agents/8-connected+2-connected agents at start. experiment6.png/.gra the results of running influence_anti_experiment6 with R{"infection"}=? [ I=T ] (expected infection at time T) with T between 1 and 40. experiment7.png/.gra the results of influence_anti_experiment7 with T between 1 and 40, with either 2-connected agents/6-conneceted agents/8-connected+2-connected agents at start. timings contains files related to tracking the time taken to build a model and perform model checking for model 4. model_3_4/timings ================= Influence Threshold Model taking the Agent View: Timing Information Nagents.pm are files containing a fully connected network version of model 4 for N agents. generate_model.pl is a perl file that will generate a fully connected version for model 4 for some number of agents supplied as an argument. properties.prop contains a PRISM property (that the network is fully infected at time 10) times.dat contains the data from running prism in three columns - the first is the number of agents, the second is the time taken in seconds to build the model and the third is the time taken in seconds for model checking. times.p is an input file for gnuplot used to chart the data in times.dat