search

utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
52 stars 31 forks source link

Integers no longer supported in expressions #81

Closed alaarman closed 7 years ago

alaarman commented 8 years ago

The type that SpinS gives to the referenced slot in the below expression is a "byte". The type checker now requires "numeric"

$ pins2lts-sym/prom2lts-sym X.509.prm.spins -i "TC_0.d==1" prom2lts-sym: Exploration order is bfs-prev prom2lts-sym: Saturation strategy is none prom2lts-sym: Guided search strategy is unguided prom2lts-sym: Attractor strategy is default prom2lts-sym: Precompiled SpinS module initialized prom2lts-sym: opening X.509.prm.spins prom2lts-sym: state vector length is 97; there are 58 groups prom2lts-sym, \ error **: Expression with type "numeric" can only be used if the language front-end defines it: "1"

Meijuh commented 7 years ago

This issue is not valid anymore. It is resolved.

alaarman commented 7 years ago

This is fixed in Next?

Meijuh commented 7 years ago

Yes (in)equality checks are now supported due to this line: https://github.com/utwente-fmt/ltsmin/blob/next/src/ltsmin-lib/ltsmin-type-system.h#L106.