// basic task graph model from
// Bouyer, Fahrenberg, Larsen and Markey
// Quantitative analysis of real-time systems using priced timed automata
// Communications of the ACM, 54(9):78–87, 2011

pta // model is a PTA

// probability P3 fails
const double p;

module scheduler

	task1 : [0..4]; // A+B
	task2 : [0..4]; // CxD
	task3 : [0..4]; // Cx(A+B)
	task4 : [0..4]; // (A+B)+(CxD)
	task5 : [0..4]; // DxCx(A+B)
	task6 : [0..4]; // (DxCx(A+B)) + ((A+B)+(CxD))

	// task status: 
	// 0 - not started
	// 1 - running on processor 1
	// 2 - running on processor 2
	// 3 - running on processor 3
	// 4 - task complete
	
	// start task 1
	[p1_add] task1=0 -> (task1'=1);
	[p2_add] task1=0 -> (task1'=2);
	[p3_add] task1=0 -> (task1'=3);

	// start task 2
	[p1_mult] task2=0 -> (task2'=1);
	[p2_mult] task2=0 -> (task2'=2);
	[p3_mult] task2=0 -> (task2'=3);
	
	// start task 3 (must wait for task 1 to complete)
	[p1_mult] task3=0 & task1=4 -> (task3'=1);
	[p2_mult] task3=0 & task1=4 -> (task3'=2);
	[p3_mult] task3=0 & task1=4 -> (task3'=3);

	// start task 4 (must wait for tasks 1 and 2 to complete)
	[p1_add] task4=0 & task1=4 & task2=4 -> (task4'=1);
	[p2_add] task4=0 & task1=4 & task2=4 -> (task4'=2);
	[p3_add] task4=0 & task1=4 & task2=4 -> (task4'=3);
	
	// start task 5 (must wait for task 3 to complete)
	[p1_mult] task5=0 & task3=4 -> (task5'=1);
	[p2_mult] task5=0 & task3=4 -> (task5'=2);
	[p3_mult] task5=0 & task3=4 -> (task5'=3);
	
	// start task 6 (must wait for tasks 4 and 5 to complete)
	[p1_add] task6=0 & task4=4 & task5=4 -> (task6'=1);
	[p2_add] task6=0 & task4=4 & task5=4 -> (task6'=2);
	[p3_add] task6=0 & task4=4 & task5=4 -> (task6'=3);
	
	// a task finishes on processor 1
	[p1_done] task1=1 -> (task1'=4);
	[p1_done] task2=1 -> (task2'=4);
	[p1_done] task3=1 -> (task3'=4);
	[p1_done] task4=1 -> (task4'=4);
	[p1_done] task5=1 -> (task5'=4);
	[p1_done] task6=1 -> (task6'=4);

	// a task finishes on processor 2
	[p2_done] task1=2 -> (task1'=4);
	[p2_done] task2=2 -> (task2'=4);
	[p2_done] task3=2 -> (task3'=4);
	[p2_done] task4=2 -> (task4'=4);
	[p2_done] task5=2 -> (task5'=4);
	[p2_done] task6=2 -> (task6'=4);

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

	p1 : [0..2];
	// 0 - idle
	// 1 - add
	// 2 - multiply
	
	x1 : clock; // local clock
	
	invariant
        (p1=1 => x1<=2) &
        (p1=2 => x1<=3)
    endinvariant

	// addition
	[p1_add] p1=0 -> (p1'=1) & (x1'=0); // start
	[p1_done] p1=1 & x1=2 -> (p1'=0) & (x1'=0); // finish

	// multiplication
	[p1_mult] p1=0 -> (p1'=2) & (x1'=0); // start
	[p1_done] p1=2 & x1=3 -> (p1'=0) & (x1'=0);  // finish

endmodule

// processor 2
module P2

	p2 : [0..2];
	// 0 - idle
	// 1 - add
	// 2 - multiply
	
	x2 : clock; // local clock
	
	invariant
        (p2=1 => x2<=5) &
        (p2=2 => x2<=7)
    endinvariant

	// addition
	[p2_add] p2=0 -> (p2'=1) & (x2'=0); // start
	[p2_done] p2=1 & x2=5 -> (p2'=0) & (x2'=0); // finish

	// multiplication
	[p2_mult] p2=0 -> (p2'=2) & (x2'=0); // start
	[p2_done] p2=2 & x2=7 -> (p2'=0) & (x2'=0);  // finish

endmodule

// processor 3 (faster than processor 2 but can fail)
module P3

	p3 : [0..3];
	// 0 - idle
	// 1 - add
	// 2 - multiply
	fail3 : [0..1]; // failed to complete task
	
	x3 : clock; // local clock
	
	invariant
        (p3=1 => x3<=3) &
        (p3=2 => x3<=5) &
        (p3=3 => x3<=0)
    endinvariant

	// addition
	[p3_add] p3=0 -> (p3'=1) & (x3'=0); // start
	[] p3=1 & x3=3 -> p : (fail3'=1) & (p3'=3) & (x3'=0)  // fail
	                + (1-p) : (fail3'=0) & (p3'=3) & (x3'=0); // finish

	// multiplication
	[p3_mult] p3=0 -> (p3'=2) & (x3'=0); // start
	[] p3=2 & x3=5 -> p : (fail3'=1) & (p3'=3) & (x3'=0) // fail
	                + (1-p) : (fail3'=0) & (p3'=3) & (x3'=0); // finish

	[p3_fail] p3=3 & fail3=1 -> (p3'=0) & (x3'=0) & (fail3'=0); // failed
	[p3_done] p3=3 & fail3=0 -> (p3'=0) & (x3'=0) & (fail3'=0); // completed

endmodule

// reward structure: elapsed time
rewards "time"
	true : 1;
endrewards

// reward structures: energy consumption
rewards "energy"
	p1=0 : 10/1000;
	p1>0 : 90/1000;
	p2=0 : 20/1000;
	p2>0 : 30/1000;
endrewards

// target state (all tasks complete)
label "tasks_complete" = (task6=4);