For example, you might use a bag to model reference counting. In reference
counting, operations track whether an element may be deleted based on the number
of references.
static class ReferenceCounting
{
static Bag
references = Bag.EmptyBag;
static Set allocated = Set.EmptySet;
[Action]
static void AddReference(string obj)
{
references = references.Add(obj);
allocated = allocated.Add(obj);
}
static bool RemoveReferenceEnabled(string obj)
{
return references.Contains(obj);
}
[Action]
static void RemoveReference(string obj)
{
references = references.Remove(obj);
}
static bool DeleteObjectEnabled(string obj)
{
return allocated.Contains(obj) && !references.Contains(obj);
}
168 Modeling Systems with Structured State
[Action]
static void DeleteObject(string obj)
{
references = references.Remove(obj);
}
}
If you were to explore this model program you would notice that the following
two traces result in the same end state:
Trace 1 Trace 2
AddReference("objA") AddReference("objA")
RemoveReference("objA") AddReference("objA")
AddReference("objA") RemoveReference("objA")
RemoveReference("objA") RemoveReference("objA")
DeleteObject("objA") DeleteObject("objA")
Creating bags
The easiest way to create a new bag is to list the elements in the constructor. The
order in which arguments appear doesn??™tmatter, and duplicates will be used as many
times as they appear:
Bag cities = new Bag("Athens", "Rome", "Athens",
"Paris", "New York", "Seattle");
Assert.
Pages:
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237