Support of Simulation - Githubissues

VerifAPS / stvs

StructuredText Verification Studio

http://formal.iti.kit.edu/stvs

GNU General Public License v3.0

9 stars 0 forks source link

Support of Simulation #19

Open wadoon opened 7 years ago

wadoon commented 7 years ago

requested by @mattulbrich

An interactive debugger for Structured Text and generalized test tables.

csicar commented 7 years ago

support the Operations:

ST-Statement-Step-Into (Step-Over, etc. can be
SPS-Cycle
Result of SPS-Cycle-Sumulation is the same as a concrete Table (with added internal State of the SPS)

Breakpoints are not needed since we will store the entire state)

mattulbrich commented 7 years ago

Simulation techonolgy

Interpretation of ST code with concrete values.
Output is a computation sequence which captures all intermediate points of a cycle execution. An element of the sequences comprises:
- pointer into program AST
- variable assignment (state)
Interrupted interpretation / statementwise interpretation is not ncessary
How to deal with non-termination?

Debugging presentation

Given input stimuli (user-provided / concretiser) run the interpretater and store all steps.
The computation sequences can be but need not be stored since they can always be recovered.
Provide step-over, step-into, run-till, conditional breakpoints etc. which are essentially sophisticated searches in the data structures.

Concrete Table manipulation

Counter examples are a possible starting point
Concretisations are a possible starting point.
Constraints can override the content of any thus generated cell. (Concrete values or "real" constraints)