Other work related to multiplexing is discussed
in Campbell et al. (2005b).
Part V
Appendices
A Modeling Library
Reference
A model program created from C# source consists of actions and variables defined
by the types declared in a single namespace. The namespace name is the model
program name. For example:
namespace MyModelProgram
{
static class Contract
{
static bool MyStateVariable1 = true;
[Action]
static void Reset() { /* ... */ }
}
class Client : LabeledInstance
{
bool isEntered = false;
// ...
}
}
The model program named MyModelProgram has two state variables, MyState-
Variable1 and isEntered, as well as one action named Reset. The isEntered state
variable can be seen as a field map of Client object IDs to Boolean values, since it
has a value for each instance of the class.
The tools require you to provide a factory method as a command-line argument.
The factory method should be a static public method with return type ModelProgram.
For example,
281
282 Modeling Library Reference
namespace MyModelProgram
{
public static class Factory
{
public static ModelProgram Create()
{
return new LibraryModelProgram(typeof(Factory).Assembly,
"MyModelProgram");
}
}
}
The Create method in this example instantiates a ModelProgram object from the
definitions for the MyModelProgram namespace found in the current assembly.
Pages:
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369