Model directories:

* no-dsm (no DSM at all; DTMC model)
* original (original HS11 algorithm w/ honest households; DTMC model)
* no-punishment (original HS11 algorithm w/ deviating households; SMG model)
* with-punishment ("fixed" algorithm w/ deviating households; SMG model)

Model file name explanation:

mdsm2314.prism - 2 households, 3 day time horizon, 1 deterministic household, 4 jobs
mdsm4344.prism - 4 households, 3 day time horizon, 4 deterministic households, 4 jobs
mdsm2314p.prism - 2 households, 3 day time horizon, 1 deterministic household, 4 jobs, with punishment

In more detail:

- Directory "no-dsm" contains DTMC models of sizes 2 to 7 agents where there is no demand-side management employed (i.e., agent always executes a task if one arrives). Model file mdsmX3X4.prism contains the model of X agents and the property to model-check the value is in the respective mdsmX3X4.props file. The value returned by the model checker can be used to obtain the dotted line from the graph in Figure 2a in [CFK+12] and Figure 4a in [CFK+13b].

- Directory "original" contains DTMC models of sizes 2 to 7 agents where the demand-side management algorithm of [HS11] is employed. Model file mdsmX3X4.prism contains the model of X agents and the property to model-check the value is in the respective mdsmX3X4.props file. The value returned by the model checker can be used to obtain the bold line from the graphs in Figure 2 in [CFK+12] and Figure 4 in [CFK+13b].

- Directory "no-punishment" contains SMG models of sizes 2 to 7 agents where the demand-side management algorithm of [HS11] is modified to allow agent to choose whether it adopts the algorithm or deviates and chooses to execute the task irrespective of the current load. Model file mdsmX304.prism contains the model of X agents and the rPATL properties to model-check the values for different coalition sizes are in the respective mdsmX304.props file. The value returned by the model checker can be used to obtain the value of the horizontal line for the respective model and coalition sizes line from the graph in Figure 2a in [CFK+12] and Figure 4a in [CFK+13b].

- Directory "with-punishment" contains SMG models of sizes 2 to 7 agents where the models from "no-punishment' are modified to allows the distribution manager to cancel a one job per timestep. Model file mdsmX3Y4p.prism contains the model of X agents Y of which are executing the "original" algorithm and the remaining are allowed to deviate. The rPATL property to model-check the value is in the respective mdsmX3Y4.props file. The value returned by the model checker can be used to obtain the value of the horizontal line for the respective model and coalition sizes line from the graph in Figure 2b in [CFK+12] and Figure 4b in [CFK+13b].

PRISM pre-processor (*.pp) files used to generate these models are also provided.

In addition each directory contains a script run-all.sh which will model-check all properties in the directory and output the results into *.res file.

=====================================================================================

[CFK+12]
Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis.
Automatic Verification of Competitive Stochastic Systems.
In Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), volume 7214 of LNCS, pages 315-330, Springer, 2012.
https://www.prismmodelchecker.org/bibitem.php?key=CFK+12

[CFK+13b]
Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis.
Automatic Verification of Competitive Stochastic Systems.
Formal Methods in System Design, 43(1), pages 61-92, Springer, 2013.
https://www.prismmodelchecker.org/bibitem.php?key=CFK+13b

[HS11]
H. Hildmann and F. Saffre.
Influence of variable supply and load flexibility on Demand-Side Management.
In Proc. 8th International Conference on the European Energy Market (EEM'11), pages 63-68, 2011.