search

favu100 / b2program

READ-ONLY MIRROR of https://gitlab.cs.uni-duesseldorf.de/general/stups/b2program; DO NOT PUSH
5 stars 3 forks source link

Fix type errors #11

Open favu100 opened 2 years ago

favu100 commented 2 years ago

java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/tictac.mch cp benchmarks/model_checking/ProB/Other/*.java . javac -cp .:btypes.jar tictac.java tictac.java:127: error: incompatible types: no instance(s) of type variable(s) S,T exist so that BRelation<S,T> conforms to BSet<BTuple<BInteger,BInteger>> return square.checkDomain(BRelation.cartesianProduct(BSet.interval(new BInteger(1), new BInteger(3)), BSet.interval(new BInteger(1), new BInteger(3)))).and(square.checkRange(BSet.interval(new BInteger(0), new BInteger(1)))).and(square.isFunction()).and(square.isPartial(BRelation.cartesianProduct(BSet.interval(new BInteger(1), new BInteger(3)), BSet.interval(new BInteger(1), new BInteger(3))))).booleanValue(); ...

$ time make SetLaws LANGUAGE=java DIRECTORY=benchmarks/model_checking/ProB/Other java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/SetLaws.mch cp benchmarks/model_checking/ProB/Other/*.java . javac -cp .:btypes.jar SetLaws.java SetLaws.java:560: error: incompatible types: BSet cannot be converted to BSet<BSet> for(BSet _ic_ss_1 : SS.pow().difference(SS)) { ^ Note: Some messages have been simplified; recompile with -Xdiags:verbose to get full output 1 error make: *** [SetLaws] Error 1

favu100 commented 2 years ago

java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/EqualityLaws.mch cp benchmarks/model_checking/ProB/Other/*.java . javac -cp .:btypes.jar EqualityLaws.java EqualityLaws.java:279: error: illegal start of type return new BSet<BSet>(new BSet()).unequal(new BSet<BSet>()).booleanValue(); ^ ...

favu100 commented 2 years ago

java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/EqualityLaws.mch cp benchmarks/model_checking/ProB/Other/*.java . javac -cp .:btypes.jar EqualityLaws.java EqualityLaws.java:279: error: illegal start of type return new BSet(new BSet()).unequal(new BSet()).booleanValue(); ^ ...

The latter is fixed now

favu100 commented 2 years ago

The universal and existential quantifiers seem to be the problem for the invariant violation

For C++, there are other problems

favu100 commented 2 years ago 
$ time make SetLaws LANGUAGE=java DIRECTORY=benchmarks/model_checking/ProB/Other
java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/SetLaws.mch
cp benchmarks/model_checking/ProB/Other/*.java .
javac -cp .:btypes.jar SetLaws.java
SetLaws.java:560: error: incompatible types: BSet cannot be converted to BSet<BSet>
for(BSet _ic_ss_1 : SS.pow().difference(SS)) {

is fixed now. However, there are still invariant violations (similar to C++).

This issue is caused by conditionalPredicate in the quantified predicate template: quantified_predicate

favu100 commented 2 years ago 
java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/tictac.mch
cp benchmarks/model_checking/ProB/Other/*.java .
javac -cp .:btypes.jar tictac.java
tictac.java:127: error: incompatible types: no instance(s) of type variable(s) S,T exist so that BRelation<S,T> conforms to BSet<BTuple<BInteger,BInteger>>
return square.checkDomain(BRelation.cartesianProduct(BSet.interval(new BInteger(1), new BInteger(3)), BSet.interval(new BInteger(1), new BInteger(3)))).and(square.checkRange(BSet.interval(new BInteger(0), new BInteger(1)))).and(square.isFunction()).and(square.isPartial(BRelation.cartesianProduct(BSet.interval(new BInteger(1), new BInteger(3)), BSet.interval(new BInteger(1), new BInteger(3))))).booleanValue();
...

Check domain and check range should be implemented for both types: BSet and BRelation

favu100 commented 2 years ago 
$ time make SetLaws LANGUAGE=java DIRECTORY=benchmarks/model_checking/ProB/Other
java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/SetLaws.mch
cp benchmarks/model_checking/ProB/Other/*.java .
javac -cp .:btypes.jar SetLaws.java
SetLaws.java:560: error: incompatible types: BSet cannot be converted to BSet<BSet>
for(BSet _ic_ss_1 : SS.pow().difference(SS)) {

is fixed now. However, there are still invariant violations (similar to C++).

This issue is caused by conditionalPredicate in the quantified predicate template: quantified_predicate

This issue should be fixed for Java now. Still, the C++ implementation for strictSubset seems to be wrong.

Edit: This issue is now solved for C++ as well

favu100 commented 2 years ago 
java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/tictac.mch
cp benchmarks/model_checking/ProB/Other/*.java .
javac -cp .:btypes.jar tictac.java
tictac.java:127: error: incompatible types: no instance(s) of type variable(s) S,T exist so that BRelation<S,T> conforms to BSet<BTuple<BInteger,BInteger>>
return square.checkDomain(BRelation.cartesianProduct(BSet.interval(new BInteger(1), new BInteger(3)), BSet.interval(new BInteger(1), new BInteger(3)))).and(square.checkRange(BSet.interval(new BInteger(0), new BInteger(1)))).and(square.isFunction()).and(square.isPartial(BRelation.cartesianProduct(BSet.interval(new BInteger(1), new BInteger(3)), BSet.interval(new BInteger(1), new BInteger(3))))).booleanValue();
...

Check domain and check range should be implemented for both types: BSet and BRelation

So this is the last issue to be fixed. isPartial is also affected

favu100 commented 2 years ago 
java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/tictac.mch
cp benchmarks/model_checking/ProB/Other/*.java .
javac -cp .:btypes.jar tictac.java
tictac.java:127: error: incompatible types: no instance(s) of type variable(s) S,T exist so that BRelation<S,T> conforms to BSet<BTuple<BInteger,BInteger>>
return square.checkDomain(BRelation.cartesianProduct(BSet.interval(new BInteger(1), new BInteger(3)), BSet.interval(new BInteger(1), new BInteger(3)))).and(square.checkRange(BSet.interval(new BInteger(0), new BInteger(1)))).and(square.isFunction()).and(square.isPartial(BRelation.cartesianProduct(BSet.interval(new BInteger(1), new BInteger(3)), BSet.interval(new BInteger(1), new BInteger(3))))).booleanValue();
...

Check domain and check range should be implemented for both types: BSet and BRelation

So this is the last issue to be fixed. isPartial is also affected

This issue is now also fixed for Java (but not yet for C++)

favu100 commented 2 years ago

The last bug is also fixed now

favu100 commented 2 years ago

Another type error has been discovered:

BoolLaws_SetCompr.java:359: error: method cartesianProduct in class BRelation<S#2,T#2> cannot be applied to given types; return _ic_set_20.equal(BRelation.cartesianProduct(BRelation.cartesianProduct(BUtils.BOOL, BUtils.BOOL), BUtils.BOOL)).booleanValue(); ^ required: BSet<S#1>,BSet<T#1> found: BRelation<BBoolean,BBoolean>,BSet reason: cannot infer type-variable(s) S#1,T#1 (argument mismatch; no instance(s) of type variable(s) S#1,T#1 exist so that BRelation<S#1,T#1> conforms to BSet<S#1>) where S#1,T#1,S#2,T#2 are type-variables: S#1 extends Object declared in method <S#1,T#1>cartesianProduct(BSet<S#1>,BSet<T#1>) T#1 extends Object declared in method <S#1,T#1>cartesianProduct(BSet<S#1>,BSet<T#1>) S#2 extends Object declared in class BRelation T#2 extends Object declared in class BRelation BoolLaws_SetCompr.java:375: error: method cartesianProduct in class BRelation<S#2,T#2> cannot be applied to given types; return _ic_set_21.equal(BRelation.cartesianProduct(BRelation.cartesianProduct(BUtils.BOOL, BUtils.BOOL), BUtils.BOOL)).booleanValue(); ^ required: BSet<S#1>,BSet<T#1> found: BRelation<BBoolean,BBoolean>,BSet reason: cannot infer type-variable(s) S#1,T#1 (argument mismatch; no instance(s) of type variable(s) S#1,T#1 exist so that BRelation<S#1,T#1> conforms to BSet<S#1>) where S#1,T#1,S#2,T#2 are type-variables: S#1 extends Object declared in method <S#1,T#1>cartesianProduct(BSet<S#1>,BSet<T#1>) T#1 extends Object declared in method <S#1,T#1>cartesianProduct(BSet<S#1>,BSet<T#1>) S#2 extends Object declared in class BRelation T#2 extends Object declared in class BRelation 2 errors

favu100 commented 2 years ago

This issue is solved now

favu100 commented 2 years ago

Run SetLaws, RelLaws, and FunLaws etc. Files with RelLaws and FunLaws could still have some errors