//
// Database with REDundancy for bluemoon Prism package
// Budde & D'Argenio, 2015
//
//{-
// Concept of the database computing system with redundancy:
// 
// 2 Types of Processors        (Pi, i=0..1)
// 2 Types of disk Controllers  (Cj, j=0..1)
// 6 Disk clusters              (Dk, k=0..5)
//
// For redundancy 'RED'=2,3,..., there are RED components of each type
// of Processor and Controller, and RED+2 Disks on each disk cluster.
// Processors, Controllers and Disks break down with different rates.
// A processor of type i breaking down causes one processor of the other
// type to break as well, with certain rate.
// A single repairman chooses randomly among broken components, and
// fixes them up (one at a time) with one of two possible speed rates.
//
// Initial state: all components in the system are operatinoal.
// Reference events: any system transition.
// Rare event: system failure caused by RED simultaneously broken Processors
//             or Controllers of the same type, or RED broken Disks on the
//             same disk cluster.
//-}

ctmc

// -- The following values were extracted from José Villén-Altamirano,
// -- "Importance functions for RESTART simulation of highly-dependable
// -- systems", Simulation, Vol. 83, Issue 12, December 2007, pp. 821-828.

// -- Redundancy level, viz. how many breaks produce a system failure
const int RED;

// -- Processors
global P1: [0..RED] init RED;
global P2: [0..RED] init RED;
const double PF = 2000;   // -- Processors' mean time to failure (in hours)
const double IPF = 0.01;  // -- Processors' inter-type failure rate
// -- Controllers
global C1: [0..RED] init RED;
global C2: [0..RED] init RED;
const double CF = 2000;  // -- Controllers' mean time to failure (in hours)
// -- Disk clusters
global D1: [0..RED+2] init RED+2;
global D2: [0..RED+2] init RED+2;
global D3: [0..RED+2] init RED+2;
global D4: [0..RED+2] init RED+2;
global D5: [0..RED+2] init RED+2;
global D6: [0..RED+2] init RED+2;
const double DF = 6000;  // -- Disks' mean time to failure (in hours)
// -- Repairman rates
const double R1 = 1.0;
const double R2 = 0.5;

const bool _TIME_ = true;

module Processors
	[] P1 > 0 -> (P1/PF)*(1-IPF): (P1'=P1-1)
	           + (P1/PF)*(  IPF): (P1'=P1-1)&(P2'=P2-1);
	[] P2 > 0 -> (P2/PF)*(1-IPF): (P2'=P2-1)
	           + (P2/PF)*(  IPF): (P2'=P2-1)&(P1'=P1-1);
endmodule

module Controllers
	[] C1>0 -> C1/CF: (C1'=C1-1);
	[] C2>0 -> C2/CF: (C2'=C2-1);
endmodule

module DiskClusters
	[] D1>0 -> D1/DF: (D1'=D1-1);
	[] D2>0 -> D2/DF: (D2'=D2-1);
	[] D3>0 -> D3/DF: (D3'=D3-1);
	[] D4>0 -> D4/DF: (D4'=D4-1);
	[] D5>0 -> D5/DF: (D5'=D5-1);
	[] D6>0 -> D6/DF: (D6'=D6-1);
endmodule

// -- Number of failed components in the system
formula NFails = (2*RED-P1-P2)
               + (2*RED-C1-C2)
               + (6*(RED+2)-D1-D2-D3-D4-D5-D6);
// -- Operational Components in the minimal cutset
formula minOC = min(P1, P2, 
                    C1, C2, 
                    D1-2, D2-2, D3-2, D4-2, D5-2, D6-2);

module Repairman
	f: bool init false;
	// -- Type 1 failures on processors ...
	[] !f & P1<RED -> 0.5 * R1 * (RED-P1)/NFails: (P1'=P1+1)
	                + 0.5 * R1 * (RED-P1)/NFails: (P1'=P1+1) & (f'=!f);
	[] !f & P2<RED -> 0.5 * R1 * (RED-P2)/NFails: (P2'=P2+1)
	                + 0.5 * R1 * (RED-P2)/NFails: (P2'=P2+1) & (f'=!f);
	// -- ... on controllers ...
	[] !f & C1<RED -> 0.5 * R1 * (RED-C1)/NFails: (C1'=C1+1)
	                + 0.5 * R1 * (RED-C1)/NFails: (C1'=C1+1) & (f'=!f);
	[] !f & C2<RED -> 0.5 * R1 * (RED-C2)/NFails: (C2'=C2+1)
	                + 0.5 * R1 * (RED-C2)/NFails: (C2'=C2+1) & (f'=!f);
	// -- ... and on disks.
	[] !f & D1<RED+2 -> 0.5 * R1 * (RED+2-D1)/NFails: (D1'=D1+1)
	                  + 0.5 * R1 * (RED+2-D1)/NFails: (D1'=D1+1) & (f'=!f);
	[] !f & D2<RED+2 -> 0.5 * R1 * (RED+2-D2)/NFails: (D2'=D2+1)
	                  + 0.5 * R1 * (RED+2-D2)/NFails: (D2'=D2+1) & (f'=!f);
	[] !f & D3<RED+2 -> 0.5 * R1 * (RED+2-D3)/NFails: (D3'=D3+1)
	                  + 0.5 * R1 * (RED+2-D3)/NFails: (D3'=D3+1) & (f'=!f);
	[] !f & D4<RED+2 -> 0.5 * R1 * (RED+2-D4)/NFails: (D4'=D4+1)
	                  + 0.5 * R1 * (RED+2-D4)/NFails: (D4'=D4+1) & (f'=!f);
	[] !f & D5<RED+2 -> 0.5 * R1 * (RED+2-D5)/NFails: (D5'=D5+1)
	                  + 0.5 * R1 * (RED+2-D5)/NFails: (D5'=D5+1) & (f'=!f);
	[] !f & D6<RED+2 -> 0.5 * R1 * (RED+2-D6)/NFails: (D6'=D6+1)
	                  + 0.5 * R1 * (RED+2-D6)/NFails: (D6'=D6+1) & (f'=!f);
	// -- Type 2 failures on processors ...
	[] f & P1<RED -> 0.5 * R2 * (RED-P1)/NFails: (P1'=P1+1)
	               + 0.5 * R2 * (RED-P1)/NFails: (P1'=P1+1) & (f'=!f);
	[] f & P2<RED -> 0.5 * R2 * (RED-P2)/NFails: (P2'=P2+1)
	               + 0.5 * R2 * (RED-P2)/NFails: (P2'=P2+1) & (f'=!f);
	// -- ... on controllers ...
	[] f & C1<RED -> 0.5 * R2 * (RED-C1)/NFails: (C1'=C1+1)
	               + 0.5 * R2 * (RED-C1)/NFails: (C1'=C1+1) & (f'=!f);
	[] f & C2<RED -> 0.5 * R2 * (RED-C2)/NFails: (C2'=C2+1)
	               + 0.5 * R2 * (RED-C2)/NFails: (C2'=C2+1) & (f'=!f);
	// -- ... and on disks.
	[] f & D1<RED+2 -> 0.5 * R2 * (RED+2-D1)/NFails: (D1'=D1+1)
	                 + 0.5 * R2 * (RED+2-D1)/NFails: (D1'=D1+1) & (f'=!f);
	[] f & D2<RED+2 -> 0.5 * R2 * (RED+2-D2)/NFails: (D2'=D2+1)
	                 + 0.5 * R2 * (RED+2-D2)/NFails: (D2'=D2+1) & (f'=!f);
	[] f & D3<RED+2 -> 0.5 * R2 * (RED+2-D3)/NFails: (D3'=D3+1)
	                 + 0.5 * R2 * (RED+2-D3)/NFails: (D3'=D3+1) & (f'=!f);
	[] f & D4<RED+2 -> 0.5 * R2 * (RED+2-D4)/NFails: (D4'=D4+1)
	                 + 0.5 * R2 * (RED+2-D4)/NFails: (D4'=D4+1) & (f'=!f);
	[] f & D5<RED+2 -> 0.5 * R2 * (RED+2-D5)/NFails: (D5'=D5+1)
	                 + 0.5 * R2 * (RED+2-D5)/NFails: (D5'=D5+1) & (f'=!f);
	[] f & D6<RED+2 -> 0.5 * R2 * (RED+2-D6)/NFails: (D6'=D6+1)
	                 + 0.5 * R2 * (RED+2-D6)/NFails: (D6'=D6+1) & (f'=!f);
endmodule
	

label "reference" = _TIME_;
label "goal" = (P1=0) | (P2=0)
             | (C1=0) | (C2=0)
             | (D1<=2) | (D2<=2) | (D3<=2) | (D4<=2) | (D5<=2) | (D6<=2);