AGREE System Stall

[cong-liu-2000]

Propositional formula (antecedent  consequent) is often used to specify sub-component requirements or contracts in AGREE. If the same antecedent is used in multiple AGREE guarantee statements, the consequents could be in conflict. This results in the antecedent to be always false. And if the value of the antecedent is a function of the underlying Lustre clock, it could stop the whole system from progressing in time. This will cause the system-level guarantee statements beyond a certain time horizon to be trivially true.
In the example below, the top-level system consists of only one sub-system A. A has a local Boolean variable Complete. Due to the two guarantee statements in A, Complete is always false. Complete is also referenced at the top-level. The assignment states that it should be true if and only if clock1 reaches 3. Since Complete is always false, clock1 can never reach 3. This makes the guarantee statement ("output range1") trivially true. Note that this does not just stops clock1. It actually stops the whole system from progressing in time. clock2 is independent of clock1. The guarantee ("output range2") is also proved to be true. This suggests that the whole system stops at “tick” 2. Any guarantee statement beyond the time becomes trivially true.
Proposed fix:

1. Generate “Stuck-At” warning if a system variable (not const) holds a constant value.
2. Generate “System stall” warning if the system cannot progress in time.

package SystemStall
public
with Base_Types;

system A
	features
		Input: in data port Base_Types::Integer;
		Output: out data port Base_Types::Integer;			
	annex agree {** 
		eq Complete : bool;
		guarantee "Complete implies positive output " : Complete => Output > 0;
		guarantee "Complete implies negative output " : Complete => Output < 0;
	**};	
end A ; 
   
system top_level
	features
		Input: in data port Base_Types::Integer;
		Output: out data port Base_Types::Integer;
	annex agree {**
		eq clock1 : int = prev(clock1 + 1, 0);
		eq clock2 : int = prev(clock2 + 1, 0);		 
		eq A_sub_Complete : bool = (clock1 = 3);
		guarantee "output range1" : (clock1 = 4) => (Output > 10);			
		guarantee "output range2" : (clock2 = 4) => (Output > 10);
	**};	
end top_level;

system implementation top_level.Impl
	subcomponents
		A_sub : system A ; 
	connections
		IN_TO_A : port Input -> A_sub.Input;
		A_TO_Output : port A_sub.Output -> Output; 
	annex agree {**	
		assign A_sub_Complete = A_sub.Complete;
	**};	
end top_level.Impl;		

end SystemStall;

[kfhoech]

Can you better describe what you mean by "system stall?" Getting stuck at a step in time may make sense in terms of a simulation or execution. But, it really doesn't fit with model checking. What would the criterion be for a variable to be considered as "stuck"?

You are correct that there is a contradiction in the given model. First, note that system A contains two guarantee statements that are contradictory if the local variable Complete is true. Accordingly, the only possible realization of such a system is when Complete is universally false. In that case, the antecedents of the guarantee expressions are false and the guarantees themselves are trivially true. However, this alone is not the source of the contradiction. The contradiction occurs when an implementation of the top-level system attempts to force the subcomponent system A to be non-realizable. Accordingly, the component composition is not consistent. If the model is inconsistent then the Assume-Guarantee contract analysis cannot be trusted.

AGREE includes a check for such a condition. In investigating this issue, it was discovered that the model checker invariant generation was turned off for the consistency checks making AGREE unable to determine whether the composition was consistent. This has been fixed in the code base and will be in the next release.

Also, the combination of the equation statement

eq A_sub_Complete : bool = (clock1 = 3);

and

assign A_Sub_Complete = A_sub.Complete;

is illegal because multiple assignments are being made to the same variable. The AGREE validator missed checking for a combination of assign and eq statements. This has been corrected in the validator code base and also will be in the next release.

Thanks for helping to improve AGREE!

[cong-liu-2000]

Replace:
eq A_sub_Complete : bool = (clock1 = 3);
with:
eq A_sub_a : bool;
assume "clock1" : A_sub_a = (clock1 = 3);
will have the same results.

[cong-liu-2000]

By "system stall", I mean the underlying Lustre model only admit traces that have a bounded length. In the example, the upper bound is 3. In other words, there is no counter-example that has a length of more than 3.

[cong-liu-2000]

The criterion for a variable to be considered as "stuck" could be implemented as an AGREE contract. In the example, this could be: guarantee "A_sub_Complete stuck at 0" : not A_sub_Complete;
I imagine this kind of contracts should be checked before verifying the actual functional contracts. It will generate a warning message to user saying some variable is stuck at false. Do you want to continue?

[kfhoech]

Given the definition for "system stall" to mean that traces cannot be longer than the length at which the model becomes "stuck," note that the reason the traces cannot be longer is that the model becomes inconsistent at that step. No analysis at that step or beyond is possible because the logic is self contradictory. Thus, there are no valid traces longer than that limit. Again, this is not because the analysis is somehow stuck; it's because the model becomes inconsistent at that step.

As for replacing the right hand side of the eq statement for A_sub_Complete with an assumption, this is a misuse of assumptions to drive behavior. Basically, it's using the combination of an assumption and an assignment on the top level component to drive a local variable in an encapsulated component. This essentially forms a hidden input to the encapsulated component. It is, perhaps, a little better in that application of inductive validity cores to the consistency result shows the assumption as part of the contradictory logic. (Note: AGREE still uses the historic term "Set of Support" for IVC.)

For the inferring the automated guarantee

guarantee "A_sub_Complete stuck at 0" : not A_sub_Complete;

this seems strange. Why would one define the local variable A_sub_Complete and make an assumption on its value only to subsequently guarantee it's always false? It's only because the user knows that in some future implementation the variable will be used to drive inconsistent behavior in some implementation subcomponent. Under what heuristic could the analysis postulate such guarantees? Perhaps it is better stated as lemma on the implementation. But two things are wrong with this: First, the lemma fails to detect the inconsistency because there is no valid trace to the inconsistent state whereupon the lemma is falsified. Second, how does the analysis even know to postulate such a lemma? It's only because of the inconsistency between the assumption on the value of A_sub_complete, the hidden input to sub_A, and the potential contradiction in the guarantees on the composited systemA. Under what heuristic could it be inferred?

Finally, the existing consistency checks, as weak as they are, adequately cover this case. And, they cover it in a more general manner.