AGREE generates incorrect type assertions for subrange types.

[kfhoech]

This issue is related to Issue 13 and Issue 76.

Consider the following model:

package Scratch_Pkg
public

	with Base_Types;
	with Data_Model;

	data Score extends Base_Types::Integer
		properties
			Data_Model::Integer_Range => 0 .. 10;
	end Score;

	system Scratch
		features
			i : in data port Score;
			o : out data port Score;
		annex agree {**
			eq z : int [0, 10];

			guarantee "Z non negative" : z >= 0;
			guarantee "Output equals z" : o = z;
		**};
	end Scratch;

	system implementation Scratch.Impl
		annex agree {**
			assign z = i + 3;
			assign o = z;
		**};
	end Scratch.Impl;

end Scratch_Pkg;

Notably, this model, according to AGREE, meets the all contracts, passes consistency checks and realizability check. However, note that the input is unconstrained, causing conflict between the implementation assignment and the range constraint on 'z'. The problem is that AGREE blindly adds an assertion constraining the range of 'z' which conceptually back propagates a constraint on the input. How do we change this? Should there be some means of checking that the assignment to 'z' meets its range? Also, would addition of the range constrained variables in JLustre be a better way to go?

[kfhoech]

A better way to go is likely to check the ranges as assumptions and guarantees. For each input that its range meets the subrange type predicate. And, for each output add a check that it meets its type predicate.

The model discussed in the original issue description would then (if the added checks are written AGREE) appear as:

package Scratch_Pkg
public

	with Base_Types;
	with Data_Model;

	data Score extends Base_Types::Integer
		properties
			Data_Model::Integer_Range => 0 .. 10;
	end Score;

	system Scratch
		features
			i : in data port Score;
			o : out data port Score;
		annex agree {**
			-- Type predicates to be generated from the Integer_Range property
			assume "Input 'i' type precicate" : 0 <= i and i <= 10;
			guarantee "Output 'o' type predicate" : 0 <= o and o <= 10;

			eq z : int ; -- [0, 10];
			assume "Local 'z' type predicate" : 0 <= z and z <= 10;

			guarantee "Z non negative" : z >= 0;
			guarantee "Output equals z" : o = z;
		**};
	end Scratch;

	system implementation Scratch.Impl
		annex agree {**
			assign z = i + 3;
			lemma "Local 'z' type predicate" : 0 <= z and z <= 10;
			assign o = z;
		**};
	end Scratch.Impl;

end Scratch_Pkg;

Of course the tool should generate the checks behind the scene and should not need to appear in the AGREE model.

There are two problems with this approach that need to be resolved:

1. The local variable 'z' introduced in the system type contract is essentially an input. For this, in the assume-guarantee contract analysis, an assertion is generated. However, the local variable has a value assigned in the implementation, generating a further assertion that the value of 'z' is offset from the value of the input 'i' by three. However, these assertions are now in conflict: the range of 'i' and 'z' cannot be the same if there is an offset between them. The problem is how to detect this conflict.

2. If there is a composition of models where each has inputs and outputs that are connected such that each element takes input from the other, then the assume-guarantee contracts are mutually dependent and the the type predicate contracts cannot be established.

[kfhoech]

After discussing this with @mwwhalen the following is deemed to be the safest course forward:

The subrange declaration on local variables is dangerous in that local variables can be properly used in only one two ways in a model. The models given in this issue description deliberately use the local variable in both ways, creating a contradiction. First, it can be used to abstractly model behavior which results in a variable with value constrained to a subrange. In this case a proper expression of the subrange predicate is an assumption. And, the user must not thereafter introduce an assignment to that variable. Second, the variable can be used as the LHS of an assignment of a computed value. In this case the proper expression for the range is a guarantee (or lemma) safely checking range of the value. Since the present form of the subrange as applied to a local variable supports only the first use and silently introduces a range assertion, it is deemed to be a dangerous in that subsequent assignment may introduce a contradiction as done in the given model.

But, what would be the disadvantage of changing the generated predicate from an assertion to a guarantee in both cases? Suppose we have the following model:

package Scratch_Pkg
public

	with Base_Types;
	with Data_Model;

	data Score extends Base_Types::Integer
		properties
			Data_Model::Integer_Range => 0 .. 10;
	end Score;

	system Scratch
		features
			i : in data port Score;
			o : out data port Score;
		annex agree {**
			eq z : int [0, 10];

			guarantee "Output equals z" : o = z;
		**};
	end Scratch;

	system implementation Scratch.Impl
		annex agree {**
			assign z = i + 3;
			assign o = z;
		**};
	end Scratch.Impl;

end Scratch_Pkg;

Where the subrange can be specified as sugar on the 'eq' statement means guarantee that the value of 'z' meets the type predicate. Thus, if we were to write in AGREE what this means:

package Scratch_Pkg
public

	with Base_Types;
	with Data_Model;

	data Score extends Base_Types::Integer
		properties
			Data_Model::Integer_Range => 0 .. 10;
	end Score;

	system Scratch
		features
			i : in data port Score;
			o : out data port Score;
		annex agree {**
			-- Type predicates to be generated from the Integer_Range property
			assume "Input 'i' type predicate" : 0 <= i and i <= 10;
			guarantee "Output 'o' type predicate" : 0 <= o and o <= 10;

			eq z : int ;
			-- Type predicate to be generated from the subrange on 'z'
			guarantee "Local 'z' type predicate" : 0 <= z and z <= 10;

			guarantee "Output equals z" : o = z;
		**};
	end Scratch;

	system implementation Scratch.Impl
		annex agree {**
			assign z = i + 3;
			assign o = z;
		**};
	end Scratch.Impl;

end Scratch_Pkg;

When we consider the type contract for 'Scratch' the exported value for 'z' is constrained by the contract to the given range and given the corresponding guarantee of equality between the output and 'z', the output is likewise constrained. When checking the assume-guarantee contract, the analysis is able to detect the contradiction between the guarantee of the type predicate on 'z' and the 'assign' statement with 'z' as LHS.

If we do away with the subrange declaration in the 'eq' statements and suggest to the user that in cases where the introduced local variable can be constrained with an assumption (or assertion if in an implementation), then the user is ever at peril of introducing a contradiction in a later implementation.

Accordingly, the decision taken is to change the generated range predicates from assertions to obligations (guarantees). The generated obligations are always safe. And it has the benefits of not changing the grammar (and accordingly breaking legacy models) and of helping the user avoid introducing contradictions in later implementations.

Finally, handling of systems where there is a circular dependency is actually more general problem with the definition of the model. If this were to exist in a real system, the system would need to be (borrowing a term from control theory) non-causal. This is clearly impossible, indicating there is actually a problem with the model. To break the circular loop and make the system causal the correct modification is the addition of unit delays.

[kfhoech]

Resolved by Pull Request 101.