Mondok Milán

More checks could be introduced to ensure that variable names, custom enum type names, and enum literals are unique. Also introducing a type for enums should be considered (instead of...

Currently exceptions that are not thrown from DSL visitors (for example mismatching types on two sides of a relational operator) contain no information about which line of the model caused...

This would allow Gamma to use "$" instead of "_" in generated names

Two local variables with the same name (XSTS)

1

Declaring two local variables with the same name inside a transition causes both to appear in the trace output. Example code: ``` choice { local var a: integer = 1;...

`theta-analysis` was modified in a recent PR to depend on concrete solver subprojects instead of the generic `theta-solver` subproject. (See https://github.com/ftsrg/theta/blob/master/subprojects/common/analysis/build.gradle.kts) I believe it would be preferable to adjust to...

IC3

1

This PR adds the IC3 algorithm to Theta. Thank you @dantpu!

MathSAT installation doesn't work on windows

1

The download URL for windows archives was changed with version 5.6.11 (`msvc` was removed from the URL)