Over specific runs on erroneously triggered in certain cases

[phdmakk]

The check for over specific runs on clauses is erroneously triggered in certain cases.

Considering the example below, if the last called function is over-specific on its own then the calling is flagged as over-specific as well (incorrectly). Additionally, this applies only if it is the last otherwise the calling one is not flagged. Finally, there has to be at least one level in between.

module Issue1m {

	type port P1 message {
		inout integer;
	}
	
	type component C1 {
		var integer vc_III;
	}

	type component C2 {
		var integer vc_I;
		port P1 PP;
	}

	function f_F1 () runs on C2 {
		f_F1_1();
		f_F2();
		f_F2_1(); 
		//if the last one is over specific 
		//then the calling is flagged as over-specific as well (incorrectly)
		// - if it is not the last then the calling one is not flagged
		// - there has to be at least one level in between
	}

	function f_F2 () runs on C2 {
		//second level reference
                f_F3();
	}
	function f_F3 () runs on C2 {
		PP.send(1);
	}

	function f_F1_1 () runs on C1 {
		//reference to an element of another component
                vc_III := 1;
	}
	function f_F2_1 () runs on C1 {
		//no reference
	}
}