This is a bit more difficult because we can??™t
simply observe them.We must infer them from the behavior; in particular, from the
sample traces we wrote. (In this example we don??™t have access to any source code
or documentation.)
The state variables in a model program serve just three purposes: first, to determine
what runs are possible by selecting the actions that are enabled in each state; second,
to determine the data that appear during runs by storing the arguments and return
values of the actions; and third, to support safety and liveness analyses by describing
the safe states and accepting states.
We select these state variables: The page variable indicates which kind of page is
displayed, Topics or Messages. The style variable indicates the appearance of the
entries on the topics page, WithText or TitlesOnly. The sort variable indicates the
sort order of the topics page when titles only are shown: ByFirst or ByMostRecent.
Stored information that determines the sequencing of actions is called control
state; other stored information is data state. All of our state variables store control
state. For this example we chose a high level of data abstraction where we ignore
the page contents (the titles and messages). Our actions have no arguments or return
values. Therefore this model program has no data state, apart from what is already
stored in the control state.
Pages:
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107