Variables declared VAR should be accessible in a specification

[csicar]

Even though they are only "internal" variables, they should be trackable in a specification (for internal testing reasons perhaps) like the counter variable in your example.

I would suggest they are treated similar to OUTPUT variables.

There might be (in a future version) a configuration switch which en/disables the feature.

Commit: 62f6b311b97f394dd3cfc3b0b99bd7aa0deb1c3c

copy of original issue

[csicar]

VAR could be used as Assumptions and Assertions. At the moment only assertion is used

[csicar]

variables can only be defined at the top-level
these types are possible:

VAR
name: type

VAR_INOUT
name: type

It should be possible to addVar and Var_inout as Input or as Output Variables.

For GeTeTa-Interface:
export Variables as Input or as Output variable, depending on if it is an assumption or an assertion

[csicar]

in ChangeVariable use Dropdown with Values "INOUT as Input", "INOUT as OUTPUT" etc.

[csicar]

make sure local VAR can be added two times to the spec-table

[csicar]

https://github.com/VerifAPS/stvs/tree/local-var-support

[csicar]

wrong behaviour when counterexample is avaiable