Extra assumptions in implementation not used

[zirkel]

When the implementation has inputs that are not in the specification, any assumptions on these input variables are not used. For example, in diffusion_par.mmp there is an input variable m:

input int m {m >= 2 && m <= nx && m == ((PID+1)*nx)/NPROCS - (PID*nx)/NPROCS+2};

This m is then used as the extent of an array. The code passes verify, but when used as the impl in compare mode it returns the exception:

Exception in thread "main" edu.udel.cis.vsl.minimp.util.ExecutionException: Execution error encountered at diffusion_par.mmp 32.5--32.6: "m"
Cannot prove that extent 0 of array is nonnegative

[Stephen Siegel]

Need exact information for executing failure scenario (exact command line or JUnit test).

[zirkel]

One command it fails for is:

./tass compare -simplify -reduce=urgent -verbose examples/diffusion/diffusion_seq.mmp examples/diffusion/diffusion_par.mmp -np 3

[Stephen Siegel]

I see the problem. In method OuterPredicate.checkAssumption:

"use non-key assumptions" is set to false when creating initial state of
impl because we just want to compare the key assumptions of the two
models to see if they are equivalent. But this leads to a problem
in constructing the initial state because we get violations
with array bounds. Note the problem only occurs in checking equivalence
of input assumptions, not in the construction of the initial state used
in the search, which is created separately and "use non-key assumptions"
is set to true. A better way to check equivalence needs to be found, in
place of this short-cut.

I'm working on it....

[Stephen Siegel]

Fixed. Wrote new code to check for compatibility and added this to a new utility class. The new code initializes the state for model2 using all assumptions, but then loops through and accumulates the assumptions for the key variables only, and using the resulting predicate to compare against the input assumption of model1.

Corrected obvious missing restriction on epsilon in Diffusion, but compare still fails.

Compare still fails in Laplace.