Problem with function example

[leuschel]

make LargeFunction LANGUAGE=java DIRECTORY=benchmarks/model_checking/ProB/micro java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/micro/LargeFunction.mch cp benchmarks/model_checking/ProB/micro/*.java . javac -cp .:btypes.jar LargeFunction.java LargeFunction.java:66: error: incompatible types: BRelation<BInteger,BInteger> cannot be converted to BRelation<BTuple<BInteger,BInteger>,BInteger> BRelation<BTuple<BInteger, BInteger>, BInteger> _ic_set_0 = new BRelation<BInteger, BInteger>(); ^ LargeFunction.java:69: error: no suitable constructor found for BRelation(BTuple<BInteger,BInteger>) _ic_set_0 = _ic_set_0.union(new BRelation<BTuple<BInteger, BInteger>, BInteger>(new BTuple<>(_ic_y_1, _ic_x_1.plus(_ic_y_1).modulo(n)))); ^ constructor BRelation.BRelation(PersistentHashMap) is not applicable (argument mismatch; cannot infer type arguments for BTuple<> reason: no instance(s) of type variable(s) S,T exist so that BTuple<S,T> conforms to PersistentHashMap) constructor BRelation.BRelation(BTuple<BTuple<BInteger,BInteger>,BInteger>...) is not applicable (varargs mismatch; cannot infer type arguments for BTuple<> reason: inference variable S has incompatible bounds equality constraints: BTuple<BInteger,BInteger> lower bounds: BInteger) where S,T are type-variables: S extends Object declared in class BTuple T extends Object declared in class BTuple 2 errors make: *** [LargeFunction] Error 1

[leuschel]

Example is

MACHINE LargeFunction
CONSTANTS n, fun
PROPERTIES n=100 &
 fun = %(x,y).(x:0..n & y:0..n | (x+y) mod n)
VARIABLES x
INVARIANT
 x: 0..n
INITIALISATION
  x:= 1
OPERATIONS
  //incx = x:= (x+1) mod n;
  setf = BEGIN x:= fun(x,x) END
END

[favu100]

This issue is fixed for Java now (there is still the same bug for C++)

[favu100]

This issue is solved now