pta

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_add] task1=0 -> (task1'=1);
	[p2_add] task1=0 -> (task1'=2);

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

	// start task 4 (must wait for tasks 1 and 2 to complete)
	[p1_add] task4=0 & task1=3 & task2=3 -> (task4'=1);
	[p2_add] task4=0 & task1=3 & task2=3 -> (task4'=2);
	
	// start task 5 (must wait for task 3 to complete)
	[p1_mult] task5=0 & task3=3 -> (task5'=1);
	[p2_mult] task5=0 & task3=3 -> (task5'=2);
	
	// start task 6 (must wait for tasks 4 and 5 to complete)
	[p1_add] task6=0 & task4=3 & task5=3 -> (task6'=1);
	[p2_add] 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..3]; // 0 inactive, 1 - adding, 2 - multiplying, 3 - done
	c1 : [0..2];
	x1 : clock; // local clock
	
	invariant
        	(p1=1 => x1<=1) &
        	((p1=2 & c1=0) => x1<=2) &
        	((p1=2  & c1>0)=> x1<=1) &
        	(p1=3 => x1<=0)
    	endinvariant

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

	// multi
	[p1_mult] (p1=0) -> (p1'=2) & (x1'=0); // start
	[] (p1=2) & (x1=2) & (c1=0) -> 1/3 : (p1'=3) & (x1'=0) & (c1'=0) + 2/3 : (c1'=1) & (x1'=0);
	[] (p1=2) & (x1=1) & (c1=1) -> 1/2 : (p1'=3) & (x1'=0) & (c1'=0) + 1/2 : (c1'=2) & (x1'=0);
	[p1_done] (p1=2) & (x1=1) & (c1=2) -> (p1'=0) & (x1'=0) & (c1'=0);
	
	// done
	[p1_done] (p1=3) -> (p1'=0);  // finish
	
endmodule

// processor 2 (could be done through renaming after adding constants)
module P2

	p2 : [0..3];
	c2 : [0..2];
	x2 : clock;
	
	invariant
        	((p2=1 & c2=0) => x2<=4) &
        	((p2=1  & c2>0)=> x2<=1) &
        	((p2=2 & c2=0) => x2<=6) &
        	((p2=2  & c2>0)=> x2<=1) &
        	(p2=3 => x2<=0)
    endinvariant

	// addition
	[p2_add] (p2=0) -> (p2'=1) & (x2'=0); // start
	[] (p2=1) & (x2=4) & (c2=0) -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0);
	[] (p2=1) & (x2=1) & (c2=1) -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0);
	[p2_done] (p2=1) & (x2=1) & (c2=2) -> (p2'=0) & (x2'=0) & (c2'=0);

	// multi
	[p2_mult] (p2=0) -> (p2'=2) & (x2'=0); // start
	[] (p2=2) & (x2=6) & (c2=0) -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0);
	[] (p2=2) & (x2=1) & (c2=1) -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0);
	[p2_done] (p2=2) & (x2=1) & (c2=2) -> (p2'=0) & (x2'=0) & (c2'=0);

	// done
	[p2_done] (p2=3) -> (p2'=0);  // finish
	
endmodule

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

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

label "tasks_complete" = (task6=3);