IETS3 / iets3.opensource

Open Source Parts of IETS3
Apache License 2.0
44 stars 22 forks source link

Fix model checker errors #438

Open lhartl opened 3 years ago

lhartl commented 3 years ago

To be able to use the model checker, the existing model checker errors and warnings should be fixed where possible.

heikob2 commented 3 years ago

Hi, i have a look at the model-checker errors in tests.in.expr.os:

See branch fix/modelchecker-testInExprOs

wsafonov commented 3 years ago

maybe a bug in the TS: shouldn't be type number also be of type any testsuite AlgebraicLanguage::eval()

To me any seems to be a candidate to be a supertype of everything, but right now it's only supertype of join types. Maybe @markusvoelter can give some hints why this has been done this way.

But we clearly have here an issue with deriving a common type for match expressions - in my case it gets a boolean type.

isn't int and real deprecated?

No, they are just simple way of expressing integer and floating-point number types.

IListOneArgOp gives TS-error, if arg is a list and number of entries do not match (with "left" operand).

Looks like a TS bug with the ListWithAllOp that doesn't checks its arg for a list type, instead just generally expecting its type to be a subtype of the base list type which is not correct (due to a possible list size mismatch as you noted)