Type checker does not catch double-bounded invariants

[RasmusRendal]

Copy of UPPAALModelChecker/UPPAAL-Meta#88

The following system:

where timer is a clock and tau is a double, should be caught by the typechecker, since invariants can only be bounded by integers, not by doubles.

Instead, it is caught at runtime, such that an error only occured when we are in the actual state.

We may or may not want to wait with doing this check until we implement #10, since we do allow double-bounded invariants in SMC.

invalidinvariant.xml.gz

[mikucionisaau]

I think such checks should be part of the TypeChecker, i.e. the parser should mostly check the grammar and the semantics should be checked by the later tooling. In this (more general) context, the floating point constraints are still meaningful in SMC/Monte-Carlo simulations, thus such expressions cannot be ruled out at this point.

There is also a similar issue with constraints in queries, where the following is accepted and should not: E<> timer >= 3.14 -- i.e. the query is about symbolic analysis and floating point numbers cannot be accepted. But still, it should be part of later checks.