2.1, Figure 6.3). Exploration executes the model program indirectly, by
invoking the methods of this object.
The LibraryModelProgram class is derived from the ModelProgram base class.We
now provide a simplified description of this class, which omits many details. The
names and members (etc.) of the types and methods in this simplified description
are not the same as in the actual library. To avoid confusion with the actual modeling
library, we call the class ModelProgramSimple here. It uses these types (which are
also not exactly the same as the ones in the actual modeling library):
State The state of a model program, represented by a dictionary that associates
each state variable name with its value.
Action The invocation of an action, including the action method name and all of
its arguments.
Transition A state transition, with constructor Transition(State current,
Action a, State next)
Our ModelProgramSimple class provides these properties and methods:
State InitialState Property that returns the model program??™s initial state
Set
GetActions(State s) Method that returns the set of actions that
are enabled in state s.
State GetTargetState(State s, Action a) Method that returns the next state
reached by executing action a in the current state s.
104 Exploring and Analyzing Finite Model Programs
ModelProgramSimple m = ModelName.Factory.
Pages:
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157