Download Requirements Analysis Tool with Synthesis - RAT

is the short form of the “eventually!” operator. We enter that property into the entry widget of the Property Simulation main window and press the ”Witness” button
to ask for an example trace fulfilling and illustrating the property. We’re presented
with the trace illustrated in Figure 21.
Figure 21: Witness for property G(r 7→ F(a)).
The trace is vacuous because there is no request, but actually there are acknowledges. We see that the property does neither need a request to happen, nor that
there is a request for an acknowledge to occur. Although the example is very simple and we can obtain that information by judging and interpreting the waveforms
we now press the analysis button to show the coverage information illustrated by
Figure 22.
Figure 22: Analysis of trace for property G(r 7→ F(a)).
A check of the analysis reassures our preliminary conclusions. To gain a more interesting trace we request a request to eventually happen as illustrated in Figure 23.
We keep the analysis window opened and ask for a new witness by pressing the
corresponding button in the main window.
We are presented with the trace illustrated in Figure 24. As we are satisfied with
the trace and want a request to happen for future examples we change our property
18 • RATSY Users Manual
RATSY — Requirements Analysis Tool
with Synthesis