prism-accumulation/prism-examples/poptas/task_graph/task_graph.prism

// POPTA extension of basic scheduler model from
// G. Norman, D. Parker and J. Sproston
// Model Checking for Probabilistic Timed Automata
// Formal Methods in System Design, 43(2):164-190, 2013
// added when a task is finished the first processor can enter a lower power state
// (consumes less power but longer to next perform tasks as has to warm up first)

popta

// sleep variable of processor 1 is hidden
observables
        task1, task2, task3, task4, task5, task6, p1, p2, x1, x2 //,sleep1
endobservables

const double sleep; // probability P1 sleeps after finishing a task

module scheduler

	// task status: 0 - not started, 1|2 - on processor 1|2, 3 - finished
	task1 : [0..3]; // A+B
	task2 : [0..3]; // CxD
	task3 : [0..3]; // Cx(A+B)
	task4 : [0..3]; // (A+B)+(CxD)
	task5 : [0..3]; // DxCx(A+B)
	task6 : [0..3]; // (DxCx(A+B)) + ((A+B)+(CxD))
	
	// start task 1
	[p1_add1] task1=0 -> (task1'=1);
	[p2_add1] task1=0 -> (task1'=2);

	// start task 2
	[p1_mult2] task2=0 -> (task2'=1);
	[p2_mult2] task2=0 -> (task2'=2);
	
	// start task 3 (must wait for task 1 to complete)
	[p1_mult3] task3=0 & task1=3 -> (task3'=1);
	[p2_mult3] task3=0 & task1=3 -> (task3'=2);

	// start task 4 (must wait for tasks 1 and 2 to complete)
	[p1_add4] task4=0 & task1=3 & task2=3 -> (task4'=1);
	[p2_add4] task4=0 & task1=3 & task2=3 -> (task4'=2);
	
	// start task 5 (must wait for task 3 to complete)
	[p1_mult5] task5=0 & task3=3 -> (task5'=1);
	[p2_mult5] task5=0 & task3=3 -> (task5'=2);
	
	// start task 6 (must wait for tasks 4 and 5 to complete)
	[p1_add6] task6=0 & task4=3 & task5=3 -> (task6'=1);
	[p2_add6] task6=0 & task4=3 & task5=3 -> (task6'=2);
	
	// a task finishes on processor 1
	[p1_done] task1=1 -> (task1'=3);
	[p1_done] task2=1 -> (task2'=3);
	[p1_done] task3=1 -> (task3'=3);
	[p1_done] task4=1 -> (task4'=3);
	[p1_done] task5=1 -> (task5'=3);
	[p1_done] task6=1 -> (task6'=3);

	// a task finishes on processor 2
	[p2_done] task1=2 -> (task1'=3);
	[p2_done] task2=2 -> (task2'=3);
	[p2_done] task3=2 -> (task3'=3);
	[p2_done] task4=2 -> (task4'=3);
	[p2_done] task5=2 -> (task5'=3);
	[p2_done] task6=2 -> (task6'=3);
	
endmodule
	
// processor 1
module P1

	p1 : [0..5]; 
	// 0 - initial location
	// 1 - inactive (idle or sleep)
	// 2,3 - waking (adding and multiplying) 
	// 4 - adding
	// 5 - multiplying
	sleep1 : [0..1]; // when processor is in sleep mode
	x1 : clock; // local clock
	
	invariant
        (p1=0 => x1<=0) &
        (p1=1 => true)  &
        (p1=2 => x1<=4) &
        (p1=3 => x1<=4) &
        (p1=4 => x1<=2) &
        (p1=5 => x1<=3)
    endinvariant

	// initialise
	[start] p1=0 -> 0.5 : (p1'=1) & (sleep1'=0) + 0.5 : (p1'=1) & (sleep1'=1);
	
	// start from sleep state
	[p1_add1]  p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0); // add
	[p1_add4]  p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0); // add
	[p1_add6]  p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0); // add
	[p1_mult2] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0); // multiply
	[p1_mult3] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0); // multiply
	[p1_mult5] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0); // multiply

	// start from idle state
	[p1_add1]  p1=1 & sleep1=0 -> (p1'=4) & (x1'=0); // add
	[p1_add4]  p1=1 & sleep1=0 -> (p1'=4) & (x1'=0); // add
	[p1_add6]  p1=1 & sleep1=0 -> (p1'=4) & (x1'=0); // add
	[p1_mult2] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0); // multiply
	[p1_mult3] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0); // multiply
	[p1_mult5] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0); // multiply

	// wake from sleep
	[p1] p1=2 & x1=4 -> (p1'=4) & (x1'=0); // add
	[p1] p1=3 & x1=4 -> (p1'=5) & (x1'=0); // multiply

	// finish
	[p1_done] p1=4 & x1=2 -> (1-sleep) : (p1'=1) 
							   + sleep : (p1'=1) & (sleep1'=1); // add
	[p1_done] p1=5 & x1=3 -> (1-sleep) : (p1'=1)
							   + sleep : (p1'=1) & (sleep1'=1);  // multiply

endmodule

// processor 2
module P2

	p2 : [0..2]; // 0 - idle, 1 - add, 2 - multiply
	x2 : clock;
	
	invariant
        (p2=1 => x2<=5) &
        (p2=2 => x2<=7)
    endinvariant
	
	// start
	[p2_add1]  p2=0 -> (p2'=1) & (x2'=0); // add
	[p2_add4]  p2=0 -> (p2'=1) & (x2'=0); // add
	[p2_add6]  p2=0 -> (p2'=1) & (x2'=0); // add
	[p2_mult2] p2=0 -> (p2'=2) & (x2'=0); // multiply
	[p2_mult3] p2=0 -> (p2'=2) & (x2'=0); // multiply
	[p2_mult5] p2=0 -> (p2'=2) & (x2'=0); // multiply

	// finish
	[p2_done] p2=1 & x2=5 -> (p2'=0); // add
	[p2_done] p2=2 & x2=7 -> (p2'=0); // multiply

endmodule

// reward structures
// time
rewards "time"
	true : 1;
endrewards

// energy
rewards "energy"

	p1=0 & sleep1=1 : 1/1000;
	p1=0 & sleep1=0 : 10/1000;
	p1>0 : 90/1000;
	p2=0 : 20/1000;
	p2>0 : 30/1000;
	
endrewards

label "tasks_complete" = (task1=3) & (task2=3) & (task3=3) & (task4=3) & (task5=3) & (task6=3);