search

VerifAPS / stvs

StructuredText Verification Studio
http://formal.iti.kit.edu/stvs
GNU General Public License v3.0
9 stars 0 forks source link

Variables declared VAR should be accessible in a specification #5

Open csicar opened 7 years ago

csicar commented 7 years ago

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 commented 7 years ago

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

csicar commented 7 years ago

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 commented 7 years ago

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

csicar commented 7 years ago

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

csicar commented 7 years ago

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

csicar commented 7 years ago

wrong behaviour when counterexample is avaiable