-
Notifications
You must be signed in to change notification settings - Fork 1
/
dotsource.dot
465 lines (463 loc) · 93.9 KB
/
dotsource.dot
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
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
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
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
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
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
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
digraph G {
node[shape=record,style=filled,fillcolor=gray95];
edge[concentrate=true];
graph[splines = ortho, ranksep = 1, ratio = fill, color=blue];
rankdir = TB;
n0 [label = <{HeaderSelect|<b><i>-ROTATION_MULTIPLIER : int</i></b><BR/><b><i>-HEADER_FONT : Font</i></b><BR/>-reference : InputHandler<BR/>-codeBase : int|+HeaderSelect(x : int, y : int, wid : int, hei : int, inCode : int) : HeaderSelect<BR/>+updateSizeLoc(x : int, y : int, wid : int, hei : int) : void<BR/>+update(header : ArrayList<String>, select : int) : void<BR/>+setInputHandler(in : InputHandler) : void<BR/>+getCodeBase() : int}>];
n1 [label = <{DecideSBCoobs|<i>-attributeObservableRef : String</i><BR/>-plants : ArrayList<TransitionSystem><BR/>-specs : ArrayList<TransitionSystem><BR/>-attributes : ArrayList<String><BR/>-agents : ArrayList<Agent><BR/>-events : HashSet<String><BR/>-sbStructure : StateBased<BR/>-pathKnowledge : boolean|+DecideSBCoobs(pathIn : boolean) : DecideSBCoobs<BR/>+DecideSBCoobs(eventsIn : ArrayList<String>, specStart : TransitionSystem, attr : ArrayList<String>, agentsIn : ArrayList<Agent>) : DecideSBCoobs<BR/>+DecideSBCoobs(inPlants : ArrayList<TransitionSystem>, inSpecs : ArrayList<TransitionSystem>, attrIn : ArrayList<String>, agentsIn : ArrayList<Agent>) : DecideSBCoobs<BR/><i>+assignAttributeReferences(obs : String) : void</i><BR/>-generateSigmaStarion(spec : TransitionSystem) : TransitionSystem<BR/>#assignPathKnowledge(in : boolean) : void<BR/>-getPathKnowledge() : boolean<BR/>-getSequences(index : int, aS : AgentStates, paths : ArrayList<ArrayList<StateSet>>, use : ArrayList<ArrayList<String>>, s : String, out : HashSet<IllegalConfig>) : void<BR/>-copy(in : ArrayList<ArrayList<String>>) : ArrayList<ArrayList<String>>}>];
n2 [label = <{UStructMemoryMeasure|-stateSize : int<BR/>-transSize : int<BR/>-numberAgentGroups : ArrayList<Integer><BR/>-sizeStateGroups : ArrayList<Integer>|+assignStateSize(in : int) : void<BR/>+assignTransitionSize(in : int) : void<BR/>+logAgentGroupSize(in : int) : void<BR/>+logStateGroupSize(in : int) : void<BR/>-getAverageAgents() : double<BR/>-getAverageStates() : double<BR/>-averageList(in : ArrayList<Integer>) : double<BR/>-getMaximumStates() : int}>];
n3 [label = <{FSMImage|<b><i>-DEFAULT_IMAGE_PATH : String</i></b><BR/><b><i>-EVENT_RECEIVER_NAME : String</i></b><BR/>-reference : String<BR/>-path : String<BR/>-zoom : double<BR/>-x : int<BR/>-y : int<BR/><i>-iD : ImageDisplay</i>|+FSMImage(inRef : String, inPath : String) : FSMImage<BR/><i>+attachPanel(p : HandlePanel) : void</i><BR/><i>+dettachPanel(p : HandlePanel) : void</i><BR/>+drawPage() : void<BR/>+setZoom(in : double) : void<BR/>+setX(in : int) : void<BR/>+setY(in : int) : void<BR/>+setReferenceName(in : String) : void<BR/>+setImage(in : String) : void<BR/>+getZoom() : double<BR/>+getX() : int<BR/>+getY() : int<BR/>+getReferenceName() : String<BR/>+getImage() : String}>];
n4 [label = <{<i>EntrySet</i>|<b><i>#DEFAULT_FONT : Font</i></b><BR/><b><i>-SUBSYSTEM_CODE_DEFAULT : int</i></b><BR/><b><i>+SIGNIFIER_TRUE : String</i></b><BR/><i>#subSystemCode : int</i><BR/>-contents : ArrayList<String><BR/>-codes : HashMap<Integer,String><BR/>-prefix : String<BR/>-label : String<BR/>-button : boolean<BR/>-code : int|+EntrySet(inPref : String, inName : String, submit : boolean, inCode : int) : EntrySet<BR/>+drawEntrySet(y : int, lineHei : int, p : HandlePanel) : int<BR/><u>#draw(y : int, lineHei : int, p : HandlePanel) : int</u><BR/>+handleInput(code : int, p : HandlePanel) : boolean<BR/>+resetContent() : String<BR/>+reset(p : HandlePanel) : void<BR/>#registerCode(in : int, ref : String) : void<BR/>#deregisterCode(in : int) : void<BR/>#deregisterCodes() : void<BR/>+setContents(in : ArrayList<String>) : void<BR/>+setContent(in : String, index : int) : void<BR/>+addContent(in : String) : void<BR/>+resetContentAt(i : int) : void<BR/>+deleteContentAt(i : int) : void<BR/>#getCodeMapping(code : int) : String<BR/>#prefix() : String<BR/>+containsCode(in : int) : boolean<BR/>+getName() : String<BR/>+getCode() : int<BR/>+getContentAt(i : int) : String<BR/>+getContents() : ArrayList<String>}>];
n5 [label = <{DisplayPage|<b><i>-TITLE_FONT : Font</i></b><BR/><b><i>-TEXT_FONT : Font</i></b><BR/><b><i>-ATTRIBUTE_FONT : Font</i></b><BR/><b><i>-STAND_IN_CODE : int</i></b><BR/><b><i>-DEFAULT_ENTRY_SIZE : int</i></b><BR/><b><i>-TITLE_STATES : String</i></b><BR/><b><i>-TITLE_EVENTS : String</i></b><BR/><b><i>-TITLE_TRANS : String</i></b><BR/><b><i>-VERT_PROP : double</i></b><BR/>-info : FSMInfo<BR/>-imageDisplay : FSMImage<BR/>-displayImageMode : boolean<BR/>-reference : InputHandler<BR/>-p : HandlePanel|+DisplayPage(give : InputHandler, panel : HandlePanel) : DisplayPage<BR/>+draw() : void<BR/>+updateFSMInfo(in : FSMInfo) : void<BR/>+drawInfo() : void<BR/>-drawDisplayThing(x : int, y : int, wid : int, hei : int, title : String, attributes : ArrayList<String>, entries : ArrayList<String>, factors : HashMap<String,ArrayList<Boolean>>) : void<BR/>+drawImage() : void<BR/>-drawCycleImageButton() : void<BR/>+drawDefault() : void<BR/>-addFraming() : void<BR/>+toggleDisplayMode() : void<BR/>+updateImage() : void<BR/>+adjustOffsets() : void<BR/>-getVertBuffer(p : HandlePanel) : int<BR/>-getSideBuffer(p : HandlePanel) : int<BR/>+hasDisplay() : boolean}>];
n6 [label = <{CrushMap|-crushMapping : HashMap<String,HashSet<Integer>>|+CrushMap() : CrushMap<BR/>+assignStateGroup(state : String, group : int) : void<BR/>+getOutput(importantStates : ArrayList<String>) : String<BR/>+getStateMemberships(stateName : String) : ArrayList<Integer><BR/>+hasStateMembership(stateName : String, group : int) : boolean}>];
n7 [label = <{Category|<b><i>-CATEGORY_FONT : Font</i></b><BR/>-name : String<BR/>-sets : ArrayList<EntrySet><BR/>-open : boolean<BR/>-catCode : int|+Category(nom : String) : Category<BR/>+draw(y : int, heiLine : int, p : HandlePanel) : int<BR/>+drawCategoryHeader(y : int, lineHei : int, p : HandlePanel) : int<BR/>+handleInput(code : int, p : HandlePanel) : boolean<BR/>+toggleOpen() : void<BR/>+hideContents() : void<BR/>+setCode(in : int) : void<BR/>+addEntrySet(in : EntrySet) : void<BR/>+setEntrySetContents(code : int, ref : ArrayList<String>) : void<BR/>+setEntrySetContent(code : int, index : int, ref : String) : void<BR/>+resetEntrySetContent(code : int, index : int) : void<BR/>+deleteEntrySetContent(code : int, index : int) : void<BR/>+resetEntrySetContents(code : int) : String<BR/>+prefix() : String<BR/>+getTitle() : String<BR/>+isOpen() : boolean<BR/>+getCode() : int<BR/>#getEntrySet(code : int) : EntrySet<BR/>+getContents(code : int) : ArrayList<String><BR/>+getContent(code : int, posit : int) : String<BR/>+contains(code : int) : boolean}>];
n8 [label = <{ProcessDES||<i>+buildObserver(in : TransitionSystem) : TransitionSystem</i><BR/><i>+product(fsms : ArrayList<TransitionSystem>) : TransitionSystem</i><BR/><i>+parallelComposition(fsms : ArrayList<TransitionSystem>) : TransitionSystem</i><BR/><i>+permissiveUnion(fsms : ArrayList<TransitionSystem>) : TransitionSystem</i><BR/><i>+convertSoloPlantSpec(in : TransitionSystem) : TransitionSystem</i><BR/><i>+trim(in : TransitionSystem) : TransitionSystem</i><BR/><i>+makeAccessible(in : TransitionSystem) : TransitionSystem</i><BR/><i>+makeCoAccessible(in : TransitionSystem) : TransitionSystem</i><BR/><i>+isBlocking(in : TransitionSystem) : Boolean</i><BR/><i>+isAccessible(in : TransitionSystem) : Boolean</i><BR/><i>+findPrivateStates(in : TransitionSystem) : ArrayList<String></i><BR/><i>+testOpacity(in : TransitionSystem) : Boolean</i><BR/><i>+isCoobservableUStruct(plant : TransitionSystem, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean</i><BR/><i>+isInferenceCoobservableUStruct(plant : TransitionSystem, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean</i><BR/><i>+isCoobservableUStruct(plant : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean</i><BR/><i>+isInferenceCoobservableUStruct(plant : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean</i><BR/><i>+isSBCoobservableUrvashi(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean</i><BR/><i>+isIncrementalCoobservable(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean</i><BR/><i>+isIncrementalInferenceCoobservable(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean</i><BR/><i>+isIncrementalSBCoobservable(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean</i><BR/><i>+buildUStructure(plant : TransitionSystem, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : TransitionSystem</i><BR/><i>+buildUStructure(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : TransitionSystem</i><BR/><i>+buildUStructureCrush(plant : TransitionSystem, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : ArrayList<TransitionSystem></i><BR/><i>+buildUStructureCrush(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : ArrayList<TransitionSystem></i><BR/><i>+assignReferences(rmm : ReceiveMemoryMeasure, init : String, mark : String, priv : String, obs : String, cont : String, bad : String, good : String) : void</i>}>];
n9 [label = <{EntryTextDisplay||+EntryTextDisplay(pref : String, name : String, button : boolean, code : int) : EntryTextDisplay<BR/>#formTextButtonName(index : int) : String}>];
n10 [label = <{OptionPageManager|<b><i>-ROTATION_MULTIPLIER : int</i></b><BR/><b><i>-CODE_BASE_OPTIONS_HEADER : int</i></b><BR/>-optionPages : OptionPage[]<BR/><i>-currentOptionPageIndex : int</i><BR/>-bodyPanel : HandlePanel<BR/>-loading : boolean<BR/>-lastX : int<BR/>-lastY : int<BR/>-optionHeader : HeaderSelect|+OptionPageManager(reference : InputHandler, xIn : int, yIn : int, wid : int, hei : int, vertProp : double) : OptionPageManager<BR/>+updateSizeLoc(x : int, y : int, wid : int, hei : int, vertProp : double) : void<BR/>-generateHandlePanel(x : int, y : int, width : int, height : int) : void<BR/>+drawPage() : void<BR/>+startLoading() : void<BR/>+endLoading() : void<BR/>+clearTextContents(code : int) : void<BR/>+setCurrentOptionPageIndex(in : int) : void<BR/>+setEntrySetContent(code : int, posit : int, ref : String) : void<BR/>+getCodeReferenceBase() : int<BR/>+getSizePageList() : int<BR/>+getHeaderPanel() : HandlePanel<BR/>+getTextContent(code : int, posit : int) : String<BR/>+getCheckboxContent(code : int) : Boolean<BR/>+getContent(code : int) : ArrayList<String><BR/>+getOptionPageNames() : ArrayList<String><BR/>-getCurrentPage() : OptionPage<BR/>+getBodyPanel() : HandlePanel<BR/>+getCurrentOptionPageIndex() : int<BR/>+getOptionPageList() : OptionPage[]}>];
n11 [label = <{Main||<i>+main(args : String[]) : void</i>}>];
n12 [label = <{UMLConfigValidation|<b><i>+CODE_FAILURE_DOT_ADDRESS : int</i></b><BR/><b><i>+CODE_FAILURE_FILE_MISSING : int</i></b>|-verifyDotAddress(path : String) : int}>];
n13 [label = <{EntryCheckbox||+EntryCheckbox(pref : String, name : String, butt : boolean, code : int) : EntryCheckbox}>];
n14 [label = <{EntryList|<b><i>-ADD_FONT : Font</i></b><BR/>-addCode : int|+EntryList(pref : String, name : String, butt : boolean, code : int, inCode : int) : EntryList}>];
n15 [label = <{TransitionFunction|-transitions : HashMap<String,ArrayList<Transition>><BR/>-attributes : ArrayList<String>|+TransitionFunction(defAttrib : ArrayList<String>) : TransitionFunction<BR/>+mergeTransitionFunctions(in : TransitionFunction) : void<BR/>+mergeTransitions(in : TransitionFunction) : void<BR/>+renameEvent(old : String, newNom : String) : void<BR/>+addTransition(inState : String, event : String, outState : String) : void<BR/>+addTransitions(state : String, inTransitions : ArrayList<Transition>) : void<BR/>+addTransition(state : String, event : String, target : String, context : TransitionFunction) : void<BR/>+removeStateTransitions(state : String) : void<BR/>+removeEventTransitions(event : String) : void<BR/>+removeTransition(stateFrom : String, event : String, stateTo : String) : void<BR/>+removeTransition(stateFrom : String, event : String) : void<BR/>+setAttributes(attrib : ArrayList<String>) : void<BR/>+setTransitionAttribute(state : String, event : String, ref : String, val : boolean) : void<BR/>+getTransitionsWithAttribute(attrib : String) : ArrayList<String><BR/>+getAttributes() : ArrayList<String><BR/>+getTransitionAttribute(state : String, event : String, ref : String) : Boolean<BR/>+getStateNames() : ArrayList<String><BR/>+getStateEvents(state : String) : ArrayList<String><BR/>+getTransitionStates(state : String, event : String) : ArrayList<String><BR/>+eventExists(state : String, event : String) : boolean<BR/>#getTransitions() : HashMap<String,ArrayList<Transition>><BR/>#getTransitions(state : String) : ArrayList<Transition><BR/>#getTransition(state : String, event : String) : Transition<BR/>+contains(reference : String, transition : Transition) : boolean}>];
n16 [label = <{StateMap|-states : HashMap<String,Entity><BR/>-composition : HashMap<String,ArrayList<String>><BR/>-attributes : ArrayList<String>|+StateMap(defAttrib : ArrayList<String>) : StateMap<BR/>+mergeStateMaps(in : StateMap) : void<BR/>+mergeStateCompositions(in : StateMap) : void<BR/>+mergeStates(in : StateMap) : void<BR/>+renameState(oldName : String, newName : String) : boolean<BR/>+renameStates() : void<BR/>+addState(stateName : String) : void<BR/>+addState(stateName : String, context : StateMap) : void<BR/>+addStateComposition(keyState : String, composedStates : ArrayList<String>) : void<BR/>+addAttributeToState(stateName : String, attribute : String, set : boolean) : void<BR/>+removeState(stateName : String) : void<BR/>+setAttributes(attrib : ArrayList<String>) : void<BR/>+setStateAttribute(nom : String, ref : String, val : boolean) : void<BR/>+setStates(in : StateMap) : void<BR/>+setStateComposition(state : String, comp : ArrayList<String>) : void<BR/>+setStateCompositions(in : StateMap) : void<BR/>#getState(stateName : String) : Entity<BR/>+getStatesWithAttribute(attrib : String) : ArrayList<String><BR/>+getAttributes() : ArrayList<String><BR/>+getNames() : ArrayList<String><BR/>+getStateComposition(provided : String) : ArrayList<String><BR/>+stateExists(stateName : String) : boolean<BR/>+getStateAttribute(nom : String, ref : String) : Boolean<BR/>#getStates() : HashMap<String,Entity><BR/>#getStateCompositions() : HashMap<String,ArrayList<String>>}>];
n17 [label = <{Transition|-states : ArrayList<String>|+Transition(inEvent : String, state : String) : Transition<BR/>+Transition(inString : String, inStates : ArrayList<String>) : Transition<BR/>#Transition(base : Entity) : Transition<BR/>+setTransitionStates(in : ArrayList<String>) : void<BR/>+setTransitionEvent(in : String) : void<BR/>+getEvent() : String<BR/>+getStates() : ArrayList<String><BR/>+hasState(stateName : String) : boolean<BR/>+isEmpty() : boolean<BR/>+addTransitionState(in : String) : void<BR/>+removeTransitionState(stateName : String) : void<BR/>+removeTargetStates() : void}>];
n18 [label = <{ReadWrite|<i>-SEPARATOR : String</i><BR/><i>-REGION_SEPARATOR : String</i><BR/><i>-TRUE_SYMBOL : String</i><BR/><i>-FALSE_SYMBOL : String</i>|<i>+assignConstants(separator : String, regionSeparator : String, trueSymbol : String, falseSymbol : String) : void</i><BR/><i>+generateFile(in : TransitionSystem) : String</i><BR/><i>+readFile(in : String) : TransitionSystem</i><BR/><i>+readDESpotFile(in : String) : TransitionSystem</i><BR/><i>+generateAgentFile(nom : String, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>, attributes : ArrayList<String>) : String</i><BR/><i>+readAgentFile(in : String) : ArrayList<HashMap<String,ArrayList<Boolean>>></i><BR/><i>-attribute(use : ArrayList<String>, out : StringBuilder) : StringBuilder</i>}>];
n19 [label = <{StateSetPath|-parent : StateSetPath<BR/>-eventPath : ArrayList<String><BR/>-problemEvent : String|+StateSetPath(in : String[], inParent : StateSetPath) : StateSetPath<BR/>+setProblemEvent(in : String) : void<BR/>#search(check : StateSet) : boolean<BR/>+isNew() : boolean<BR/>+StateSetPath(in : String[]) : StateSetPath<BR/>+addEvent(s : String) : void<BR/>+getEventPath() : ArrayList<String>}>];
n20 [label = <{AgentRep|-nom : String<BR/>-events : ArrayList<EventRep><BR/><i>-SEPARATOR : String</i><BR/><i>-SYMBOL_TRUE : String</i><BR/><i>-SYMBOL_FALSE : String</i>|+AgentRep(inNom : String, eves : ArrayList<String>, attr : int) : AgentRep<BR/>+AgentRep(readIn : String) : AgentRep<BR/><i>+assignSymbols(sep : String, tr : String, fa : String) : void</i><BR/>+setName(in : String) : void<BR/>+getName() : String<BR/>+getEvent(i : int) : EventRep<BR/>+getEvents() : ArrayList<EventRep><BR/>+toString() : String}>];
n21 [label = <{GenerateFSM|<b><i>-ALPHABET_STATE : String</i></b><BR/><b><i>-ALPHABET_EVENT : String</i></b><BR/><b><i>-MAX_PERCENTAGE_VALUE : int</i></b><BR/><i>-SEPARATOR : String</i><BR/><i>-REGION_SEPARATOR : String</i><BR/><i>-TRUE_SYMBOL : String</i><BR/><i>-FALSE_SYMBOL : String</i><BR/><i>-stateAttributes : ArrayList<String></i><BR/><i>-stateNumbers : ArrayList<Integer></i><BR/><i>-eventAttributes : ArrayList<String></i><BR/><i>-eventNumbers : ArrayList<Integer></i><BR/><i>-transitionAttributes : ArrayList<String></i><BR/><i>-transitionNumbers : ArrayList<Integer></i><BR/><i>-defaultStateSet : ArrayList<String></i><BR/><i>-defaultEventSet : ArrayList<String></i>|<i>+assignStateAttributes(in : ArrayList<String>, amounts : ArrayList<Integer>) : void</i><BR/><i>+assignEventAttributes(in : ArrayList<String>, amounts : ArrayList<Integer>) : void</i><BR/><i>+assignTransitionAttributes(in : ArrayList<String>, amounts : ArrayList<Integer>) : void</i><BR/><i>+assignDefaultStateSet(in : ArrayList<String>) : void</i><BR/><i>+wipeDefaultStateSet() : void</i><BR/><i>+assignDefaultEventSet(in : ArrayList<String>) : void</i><BR/><i>+wipeDefaultEventSet() : void</i><BR/><i>+createNewFSM(name : String, sizeStates : int, sizeEvents : int, sizeTrans : int, det : boolean) : String</i><BR/><i>-writeComponentGenerative(out : StringBuilder, rand : Random, sizeComponent : int, attributes : ArrayList<String>, numbers : ArrayList<Integer>, stateNames : boolean) : HashMap<Integer,String></i><BR/><i>-writeComponentDefaultSet(out : StringBuilder, rand : Random, components : ArrayList<String>, attributes : ArrayList<String>, numbers : ArrayList<Integer>) : HashMap<Integer,String></i><BR/><i>-writeTransitions(out : StringBuilder, rand : Random, stateNames : HashMap<Integer,String>, eventNames : HashMap<Integer,String>, sizeTrans : int, isDet : boolean) : StringBuilder</i><BR/><i>+assignConstants(separator : String, regionSeparator : String, trueSymbol : String, falseSymbol : String) : void</i><BR/><i>-generateName(i : int, character : boolean) : String</i><BR/><i>-getRandomValue(rand : Random) : int</i><BR/><i>-writeAttributes(rand : int, size : int, index : int, attri : ArrayList<String>, numbers : ArrayList<Integer>, track : ArrayList<Integer>) : String</i><BR/><i>-writeAttribute(out : StringBuilder, attri : ArrayList<String>) : void</i>}>];
n22 [label = <{ProcessAnalysis|<i>-attributePrivateRef : String</i><BR/><i>-attributeInitialRef : String</i>|<i>+assignAttributeReferences(priv : String, init : String) : void</i><BR/><i>+isBlocking(in : TransitionSystem) : Boolean</i><BR/><i>+isAccessible(in : TransitionSystem) : Boolean</i><BR/><i>+findPrivateStates(in : TransitionSystem) : ArrayList<String></i><BR/><i>+testOpacity(in : TransitionSystem) : Boolean</i>}>];
n23 [label = <{EntryText|-size : int<BR/>-expand : boolean|+EntryText(pref : String, ref : String, button : boolean, buttCode : int, len : int, fill : boolean) : EntryText<BR/>+handleInput(code : int, p : HandlePanel) : boolean<BR/>-formTextEntryName(index : int) : String}>];
n24 [label = <{IllegalConfig|-stateSet : AgentStates<BR/>-observedPaths : ArrayList<ArrayList<String>><BR/>-event : String|+IllegalConfig(inStates : AgentStates, inPaths : ArrayList<ArrayList<String>>, inEvent : String) : IllegalConfig<BR/>+getStateSet() : AgentStates<BR/>+getEventPath() : ArrayList<String><BR/>+getObservedPaths() : ArrayList<ArrayList<String>><BR/>+getEventPathLength() : int<BR/>+getNumberDistinctEvents() : int<BR/>+getEvent() : String<BR/>-copy(in : ArrayList<String>) : ArrayList<String>}>];
n25 [label = <{SVGtoTikZ||<i>+convertSVGToTikZ(f : File, path : String) : File</i><BR/><i>-drawCircleNode(x : double, y : double, rad : double, mark : boolean, name : String, color : String) : String</i><BR/><i>-drawEdges(path : ArrayList<Double>, color : String, dotted : boolean) : String</i><BR/><i>-drawPolygon(path : ArrayList<Double>, color : String) : String</i><BR/><i>-drawLabel(x : double, y : double, name : String) : String</i>}>];
n26 [label = <{AgentStates|-currentStates : String[]<BR/>-eventPath : ArrayList<ArrayList<String>>|+AgentStates(states : String[], inPath : ArrayList<String>) : AgentStates<BR/>+AgentStates(states : String[]) : AgentStates<BR/>+addGuess(index : int, s : String) : void<BR/>+deriveChild(newStates : String[], canAct : boolean[], s : String) : AgentStates<BR/>+deriveChild(newStates : String[], index : int, s : String) : AgentStates<BR/>+getStates() : String[]<BR/>+getEventPath() : ArrayList<String><BR/>+getObservedPath(index : int) : ArrayList<String><BR/>+getCompositeName() : String<BR/>#setObservedPath(index : int, inPath : ArrayList<String>) : void}>];
n27 [label = <{PopoutAgentSelection|<b><i>-WIDTH : int</i></b><BR/><b><i>-HEIGHT : int</i></b><BR/><b><i>-CODE_ADD_AGENT : int</i></b><BR/><b><i>-CODE_SUBMIT : int</i></b><BR/><b><i>-CODE_TOGGLE_EVENT : int</i></b><BR/><b><i>-CODE_REMOVE_RANGE : int</i></b><BR/><b><i>-BLOCK_SIZE_RATIO : double</i></b><BR/>-DEFAULT_FONT : Font<BR/>-SMALLER_FONT : Font<BR/>-agents : ArrayList<AgentRep><BR/>-refEvents : ArrayList<String><BR/>-attributes : ArrayList<String><BR/>-ready : boolean|+PopoutAgentSelection(inAge : ArrayList<String>, inEven : ArrayList<String>, inAttrib : ArrayList<String>) : PopoutAgentSelection<BR/>+drawPage() : void<BR/><i>+assignSymbols(separator : String, tr : String, fa : String) : void</i><BR/>+getResult() : ArrayList<String>}>];
n28 [label = <{Attribute|-id : String<BR/>-value : boolean<BR/>-wrap : Attribute|+Attribute(inId : String) : Attribute<BR/>+addWrapper(ref : String) : void<BR/>+setAttributes(in : LinkedList<String>) : void<BR/>+setValue(ref : String, in : boolean) : void<BR/>+getValue(ref : String) : Boolean<BR/>+getAttributes() : LinkedList<String>}>];
n29 [label = <{ColorPack|<b><i>-COLOR_ADJUST : double</i></b><BR/>-r : int<BR/>-g : int<BR/>-b : int|+ColorPack(a : int, d : int, c : int) : ColorPack<BR/>+ColorPack(a : String, d : String, c : String) : ColorPack<BR/>+getGraphvizColor() : String<BR/>-hex(in : int) : String<BR/>+cycleColor(in : int) : ColorPack<BR/>+cycleColor() : ColorPack<BR/>-affixColor(in : int) : int}>];
n30 [label = <{UStructurePage|<b><i>-HEADER : String</i></b><BR/><b><i>-CATEGORY_USTRUC : String</i></b><BR/><b><i>-HELP : String</i></b>|+UStructurePage() : UStructurePage}>];
n31 [label = <{FSMInfo|-fsmName : String<BR/>-image : String<BR/>-fsmStateAttributes : ArrayList<String><BR/>-fsmStateDetails : HashMap<String,ArrayList<Boolean>><BR/>-fsmEventAttributes : ArrayList<String><BR/>-fsmEventDetails : HashMap<String,ArrayList<Boolean>><BR/>-fsmTransitionAttributes : ArrayList<String><BR/>-fsmTransitionDetails : HashMap<String,ArrayList<Boolean>>|+FSMInfo(name : String) : FSMInfo<BR/>+updateStateAttributes(statAttr : ArrayList<String>) : void<BR/>+updateStateDetails(statDeta : HashMap<String,ArrayList<Boolean>>) : void<BR/>+updateEventAttributes(evenAttr : ArrayList<String>) : void<BR/>+updateEventDetails(evenDeta : HashMap<String,ArrayList<Boolean>>) : void<BR/>+updateTransitionAttributes(transAttr : ArrayList<String>) : void<BR/>+updateTransitionDetails(transDeta : HashMap<String,ArrayList<Boolean>>) : void<BR/>+updateImage(img : String) : void<BR/>+getStates() : ArrayList<String><BR/>+getEvents() : ArrayList<String><BR/>+getTransitions() : ArrayList<String><BR/>+getStateAttributes() : ArrayList<String><BR/>+getEventAttributes() : ArrayList<String><BR/>+getTransitionAttributes() : ArrayList<String><BR/>+getStateDetails() : HashMap<String,ArrayList<Boolean>><BR/>+getEventDetails() : HashMap<String,ArrayList<Boolean>><BR/>+getTransitionDetails() : HashMap<String,ArrayList<Boolean>><BR/>+getName() : String<BR/>+getImage() : String}>];
n32 [label = <{ProcessOperation|<i>+attributeObservableRef : String</i><BR/><i>+attributeInitialRef : String</i>|<i>+assignAttributeReferences(init : String, obs : String) : void</i><BR/><i>+buildObserver(in : TransitionSystem) : TransitionSystem</i><BR/><i>+product(fsms : ArrayList<TransitionSystem>) : TransitionSystem</i><BR/><i>+parallelComposition(fsms : ArrayList<TransitionSystem>) : TransitionSystem</i><BR/><i>+permissiveUnion(fsms : ArrayList<TransitionSystem>) : TransitionSystem</i><BR/><i>-collapseStates(in : TransitionSystem) : HashMap<String,ArrayList<String>></i><BR/><i>-collapseStatesRecurs(curr : String, in : TransitionSystem, map : HashMap<String,ArrayList<String>>, visited : HashSet<String>) : ArrayList<String></i><BR/><i>-productHelper(in : TransitionSystem, other : TransitionSystem) : TransitionSystem</i><BR/><i>-parallelCompositionHelper(in : TransitionSystem, other : TransitionSystem) : TransitionSystem</i><BR/><i>-permissiveUnionHelper(in : TransitionSystem, other : TransitionSystem) : TransitionSystem</i><BR/><i>-compileDestination(stateA : String, stateB : String, compA : ArrayList<String>, compB : ArrayList<String>, source : String, event : String, out : TransitionSystem, use : ArrayList<TransitionSystem>) : void</i>}>];
n33 [label = <{AgentChicanery||<i>+generateAgentsA() : ArrayList<HashMap<String,ArrayList<Boolean>>></i><BR/><i>+generateAgentsB() : ArrayList<HashMap<String,ArrayList<Boolean>>></i><BR/><i>+generateAgentsB2() : ArrayList<HashMap<String,ArrayList<Boolean>>></i><BR/><i>+generateAgentsC() : ArrayList<HashMap<String,ArrayList<Boolean>>></i><BR/><i>+generateAgentsD() : ArrayList<HashMap<String,ArrayList<Boolean>>></i><BR/><i>+generateAgentsE() : ArrayList<HashMap<String,ArrayList<Boolean>>></i><BR/><i>+generateAgentsFinn5() : ArrayList<HashMap<String,ArrayList<Boolean>>></i><BR/><i>+generateAgentsLiuOne() : ArrayList<HashMap<String,ArrayList<Boolean>>></i><BR/><i>+generateAgentsUrvashi() : ArrayList<HashMap<String,ArrayList<Boolean>>></i><BR/><i>#generateAgentSet(agentInfo : boolean[][][], eventList : String[]) : ArrayList<HashMap<String,ArrayList<Boolean>>></i>}>];
n34 [label = <{DecideCoobs|<b><i>+DECISION_MODE_ENABLE : int</i></b><BR/><b><i>+DECISION_MODE_DISABLE : int</i></b><BR/><i>-initialRef : String</i><BR/><i>-controllableRef : String</i><BR/><i>-badTransRef : String</i><BR/><i>-observableRef : String</i><BR/>-plants : ArrayList<TransitionSystem><BR/>-specs : ArrayList<TransitionSystem><BR/>-attr : ArrayList<String><BR/>-agents : ArrayList<Agent><BR/>-events : HashSet<String><BR/>#ustruct : UStructure<BR/>-enableDisableMode : int|+DecideCoobs() : DecideCoobs<BR/>+DecideCoobs(inPlan : ArrayList<TransitionSystem>, inSpe : ArrayList<TransitionSystem>, attrIn : ArrayList<String>, agentsIn : ArrayList<Agent>) : DecideCoobs<BR/>+DecideCoobs(eventsIn : ArrayList<String>, specStart : TransitionSystem, attrIn : ArrayList<String>, agentsIn : ArrayList<Agent>) : DecideCoobs<BR/>+DecideCoobs(root : TransitionSystem, attrIn : ArrayList<String>, agentsIn : ArrayList<Agent>) : DecideCoobs<BR/><i>+assignAttributeReferences(init : String, cont : String, obs : String, bad : String) : void</i><BR/>-decideResult() : boolean<BR/>-getEnableDisableModeCounterExamples() : HashSet<IllegalConfig><BR/>+getUStructure() : UStructure<BR/>-generatePlantSigmaStarion(template : TransitionSystem) : TransitionSystem<BR/>-generateSigmaStarion(spec : TransitionSystem) : TransitionSystem<BR/>-deriveTruePlant() : TransitionSystem<BR/>-cantPerform(ultSpec : TransitionSystem, specState : String, e : String) : boolean<BR/>-getRelevantEvents() : HashSet<String><BR/>-isSpecEventNoPlant() : boolean<BR/>-parallelCompSpecs() : TransitionSystem<BR/>-parallelCompPlants() : TransitionSystem<BR/>-performPermissiveUnion(pl : TransitionSystem, sp : TransitionSystem) : TransitionSystem}>];
n35 [label = <{GenerateDot|<b><i>-INITIAL_STATE_MARKER : String</i></b><BR/><b><i>-backgroundColorCycle : ColorPack[]</i></b><BR/><b><i>-SUB_START : String</i></b><BR/><b><i>-SUP_START : String</i></b><BR/><b><i>-SCRIPT_END : String</i></b><BR/><b><i>-SUB_CONVERT_START : String</i></b><BR/><b><i>-SUB_CONVERT_END : String</i></b><BR/><b><i>-SUP_CONVERT_START : String</i></b><BR/><b><i>-SUP_CONVERT_END : String</i></b>|<i>+generateDot(in : TransitionSystem) : String</i><BR/><i>-generateStateDot(in : TransitionSystem, ref : String) : String</i><BR/><i>-generateTransitionDot(in : TransitionSystem, state : String, event : String) : String</i><BR/><i>-processObjectNameScripts(in : String) : String</i>}>];
n36 [label = <{UStructure|<b><i>-UNOBSERVED_EVENT : String</i></b><BR/><i>#attributeInitialRef : String</i><BR/><i>#attributeObservableRef : String</i><BR/><i>#attributeControllableRef : String</i><BR/><i>#attributeBadRef : String</i><BR/><i>#attributeGoodRef : String</i><BR/>-uStructure : TransitionSystem<BR/>-goodBadStates : HashSet<IllegalConfig><BR/>-badGoodStates : HashSet<IllegalConfig><BR/>-objectMap : HashMap<String,AgentStates><BR/>-eventNameMap : HashMap<String,String[]><BR/>-crushMap : CrushMap[]<BR/>-agents : Agent[]|+UStructure(thePlant : TransitionSystem, attr : ArrayList<String>, theAgents : ArrayList<Agent>) : UStructure<BR/>-initializeBadTransitions(thePlant : TransitionSystem) : HashMap<String,HashSet<String>><BR/>-initializeAgents(thePlant : TransitionSystem, attr : ArrayList<String>, theAgents : ArrayList<Agent>) : Agent[]<BR/><i>+assignAttributeReferences(init : String, obs : String, cont : String, bad : String, good : String) : void</i><BR/>+createUStructure(plant : TransitionSystem, badTransitions : HashMap<String,HashSet<String>>, agents : Agent[]) : void<BR/>-initializeUStructure(plant : TransitionSystem) : TransitionSystem<BR/>-calculateCrush(display : boolean) : void<BR/>+printOutCrushMaps(pointOut : boolean) : String<BR/>+getFilteredIllegalConfigStates() : HashSet<IllegalConfig><BR/>+getUStructure() : TransitionSystem<BR/>+getCrushUStructures() : ArrayList<TransitionSystem><BR/>+getIllegalConfigOneStates() : HashSet<IllegalConfig><BR/>+getIllegalConfigTwoStates() : HashSet<IllegalConfig><BR/>+getCrushMappings() : CrushMap[]<BR/>-getNextState(plant : TransitionSystem, currState : String, event : String) : String<BR/>-getState(plant : TransitionSystem, eventPath : ArrayList<String>) : String<BR/>-getTargetStates(states : HashSet<String>, event : String, age : Agent, index : int) : HashSet<String><BR/>-getPossibleVisibleEvents(states : HashSet<String>, age : Agent, index : int) : HashSet<String><BR/>-getReachableStates(start : String, age : Agent, index : int) : HashSet<String><BR/>-copy(in : ArrayList<String>) : ArrayList<String><BR/>-isMeaninglessTransition(events : String[]) : boolean<BR/>-filterEventPath(events : ArrayList<String>, contr : String, age : Agent) : ArrayList<String><BR/>-handleNewTransition(next : AgentStates, eventName : String[], currState : String) : void<BR/>-constructEventName(es : String[]) : String<BR/>-filterGroups(typeOne : HashSet<IllegalConfig>, typeTwo : HashSet<IllegalConfig>) : void}>];
n37 [label = <{SkiptheUI|<b><i>-PLANT_NAME : String</i></b><BR/><b><i>-EVENT_LIST : String[]</i></b><BR/><i>-model : Manager</i><BR/><i>-agents : ArrayList<HashMap<String,ArrayList<Boolean>>></i><BR/><i>-eventAtt : ArrayList<String></i>|<i>+main(args : String[]) : void</i><BR/><i>-setupStates() : void</i><BR/><i>-setupEvents() : void</i><BR/><i>-setupTransitions() : void</i><BR/><i>-setupAgents() : void</i><BR/><i>-makeImageDisplay(in : String) : void</i>}>];
n38 [label = <{<i>OptionPage</i>|<b><i>-HELP_FONT : Font</i></b><BR/><b><i>#OPTIONS_FONT : Font</i></b><BR/>-header : String<BR/>-help : String<BR/>-categories : ArrayList<Category><BR/><i>-p : HandlePanel</i><BR/>-showHelp : boolean<BR/>-helpKey : int<BR/>-showSettings : boolean<BR/>-settingsKey : int<BR/><i>-inputRef : InputHandler</i><BR/><i>-lineHeightFraction : int</i>|+OptionPage(head : String, inHelp : String) : OptionPage<BR/>+drawPage() : void<BR/>-drawNormalPage() : void<BR/>-drawHelpPage() : void<BR/>+handleMouseInput(code : int, x : int, y : int, mouseType : int) : void<BR/>+handleInput(code : int) : boolean<BR/>-addFraming() : void<BR/><i>+assignInputHandler(iR : InputHandler) : void</i><BR/><i>+assignHandlePanel(inP : HandlePanel) : void</i><BR/>+toggleCategory(code : int) : boolean<BR/>+addCategory(title : String) : void<BR/>+resetCodeEntries(code : int) : void<BR/>+setEntrySetContent(code : int, index : int, reference : String) : void<BR/>+removeContentsFromCode(code : int, index : int) : void<BR/>+deleteContentsFromCode(code : int, index : int) : void<BR/>+resetContents(code : int) : void<BR/>+addEntryText(category : String, label : String, button : boolean, code : int, size : int, flex : boolean) : void<BR/>+addEntryTextDisplay(category : String, label : String, button : boolean, code : int) : void<BR/>+addEntryList(category : String, label : String, button : boolean, code : int, newCode : int) : void<BR/>+addEntryCheckbox(category : String, label : String, button : boolean, code : int) : void<BR/>+addEntryEmpty(category : String, label : String, button : boolean, code : int) : void<BR/>+getHeader() : String<BR/><i>+getHandlePanel() : HandlePanel</i><BR/>+getCategory(title : String) : Category<BR/>+getCategoryFromCode(code : int) : Category<BR/>+getTextFromCode(code : int, posit : int) : String<BR/>+getIntegerFromCode(code : int, posit : int) : Integer<BR/>+getCheckboxContentsFromCode(code : int) : Boolean<BR/>+getContentFromCode(code : int) : ArrayList<String>}>];
n39 [label = <{FormatConversion|<b><i>-TYPE_SVG : String</i></b><BR/><b><i>-TYPE_JPG : String</i></b><BR/><b><i>-TYPE_PNG : String</i></b><BR/><b><i>-DPI_INCREASE : int</i></b><BR/><i>-CONFIG_PATH : String</i><BR/><i>-WORKING_PATH : String</i><BR/><i>-initialized : boolean</i>|<i>+assignPaths(workingPath : String, configPath : String) : void</i><BR/><i>+createImgFromFSM(fsm : String, name : String) : String</i><BR/><i>+createSVGFromFSM(fsm : String, name : String) : String</i><BR/><i>+createTikZFromSVG(fsm : String, name : String) : String</i><BR/><i>+createTikZFromFSM(fsm : String, name : String) : String</i><BR/><i>+generateDotFile(fsm : String, name : String, type : String) : File</i><BR/><i>-initializeCheck() : boolean</i>}>];
n40 [label = <{ConcreteMemoryMeasure|-startingMemory : long<BR/>-spaceUsage : ArrayList<Long><BR/>-hold : TransitionSystem|+ConcreteMemoryMeasure() : ConcreteMemoryMeasure<BR/>+logMemoryUsage() : void<BR/><i>+produceBlank() : ConcreteMemoryMeasure</i><BR/>-getMemoryUsage() : long<BR/>+getAverageMemoryUsage() : double<BR/>+getMaximumMemoryUsage() : double<BR/><i>-inMB(in : long) : double</i><BR/><i>#threeSig(in : double) : Double</i>}>];
n41 [label = <{ProcessCoobservability|<i>-badTransRef : String</i><BR/><i>-memoryRecipient : ReceiveMemoryMeasure</i>|<i>+assignReferences(rmm : ReceiveMemoryMeasure, cont : String, obs : String, init : String, badTrans : String, goodThing : String) : void</i><BR/><i>+assignIncrementalOptions(a : int, b : int, c : int) : void</i><BR/><i>+isCoobservableUStruct(plant : TransitionSystem, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : boolean</i><BR/><i>+isCoobservableUStruct(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : boolean</i><BR/><i>+isInferenceCoobservableUStruct(plant : TransitionSystem, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : boolean</i><BR/><i>+isInferenceCoobservableUStruct(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : boolean</i><BR/><i>+isSBCoobservable(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : boolean</i><BR/><i>+isIncrementalCoobservable(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : boolean</i><BR/><i>+isIncrementalInferenceCoobservable(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : boolean</i><BR/><i>+isIncrementalSBCoobservable(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : boolean</i><BR/><i>+convertSoloPlantSpec(plant : TransitionSystem) : TransitionSystem</i><BR/><i>+constructUStruct(plant : TransitionSystem, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : UStructure</i><BR/><i>+constructUStruct(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : UStructure</i><BR/><i>+constructUStructRaw(plant : TransitionSystem, attr : ArrayList<String>, agents : ArrayList<Agent>) : UStructure</i><BR/><i>-getAllEvents(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>) : ArrayList<String></i><BR/><i>-constructAgents(event : ArrayList<String>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : ArrayList<Agent></i>}>];
n42 [label = <{Agent|-events : EventMap|+Agent(attr : ArrayList<String>, inEvents : ArrayList<String>) : Agent<BR/>+Agent(in : EventMap) : Agent<BR/>+addUnknownEvent(in : String) : void<BR/>+addUnknownEvents(in : Collection<String>) : void<BR/>+setAttributeTrue(attrib : String, names : ArrayList<String>) : void<BR/>+setAttribute(attrib : String, name : String, set : boolean) : void<BR/>+getEventAttribute(event : String, attrib : String) : Boolean<BR/>+getEvents() : ArrayList<String><BR/>+getEventsAttributeSet(attrib : String, val : boolean) : ArrayList<String><BR/>+contains(eventName : String) : boolean}>];
n43 [label = <{StateBased|<i>-attributeInitialRef : String</i><BR/><i>-attributeObservableRef : String</i><BR/><i>-attributeControllableRef : String</i><BR/>-disable : HashMap<String,HashSet<StateSet>><BR/>-enable : HashMap<String,HashSet<StateSet>><BR/>-pathTracing : HashMap<StateSet,ArrayList<ArrayList<StateSet>>>|+StateBased(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<Agent>, pathTrack : boolean) : StateBased<BR/><i>+assignAttributeReference(init : String, obs : String, cont : String) : void</i><BR/>+isSBCoobservable() : boolean<BR/>-operate(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agen : ArrayList<Agent>) : void<BR/>-initializeEnableDisable(disable : HashMap<String,HashSet<StateSet>>, enable : HashMap<String,HashSet<StateSet>>, plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, controllable : HashSet<String>) : void<BR/>-observerConstructHiding(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, enable : HashMap<String,HashSet<StateSet>>, disable : HashMap<String,HashSet<StateSet>>, agentObs : ArrayList<String>, agentCont : ArrayList<String>, controllable : HashSet<String>) : HashMap<String,HashSet<StateSet>><BR/>+getEquivalentPaths(in : StateSet) : ArrayList<ArrayList<StateSet>><BR/>-getInitialState(t : TransitionSystem) : String<BR/>-getAllEvents(plants : ArrayList<TransitionSystem>) : ArrayList<String><BR/>+getRemainingDisableStates() : ArrayList<StateSet><BR/>+getRemainingEnableStates() : ArrayList<StateSet><BR/>-initialStateSetPath(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>) : StateSet<BR/>-stateSetStep(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, curr : StateSet, event : String) : StateSet<BR/>-reachableStateSetPaths(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, initial : HashSet<StateSet>, agentObs : ArrayList<String>) : HashSet<StateSet><BR/>-knowsEvent(system : TransitionSystem, event : String) : boolean<BR/>-canPerformEvent(system : TransitionSystem, state : String, event : String) : boolean<BR/>-canProceed(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, curr : StateSet, event : String) : boolean<BR/>-printEnableDisableSets() : void<BR/>-intersection(conglom : HashSet<StateSet>, check : HashSet<StateSet>) : HashSet<StateSet>}>];
n44 [label = <{StateSet|<i>-sizePlants : int</i><BR/><i>-sizeSpecs : int</i><BR/>-plant : String[]<BR/>-spec : String[]|+StateSet(in : String[]) : StateSet<BR/><i>+assignSizes(sizePl : int, sizeSp : int) : void</i><BR/>+getStates() : String[]<BR/>+getPlantStates() : String[]<BR/>+getPlantState(index : int) : String<BR/>+getSpecStates() : String[]<BR/>+getSpecState(index : int) : String<BR/>+getState(index : int) : String<BR/>+getPairName() : String}>];
n45 [label = <{IncrementalMemoryMeasure|-endStates : ArrayList<MemoryMeasure><BR/>-endNumComponents : ArrayList<Integer><BR/>-componentNames : ArrayList<ArrayList<String>>|+logFinishedProcess(in : MemoryMeasure) : void<BR/>+logFinishedComponents(in : int) : void<BR/>+logComponentNames(in : ArrayList<String>) : void}>];
n46 [label = <{EventMap|-events : HashMap<String,Entity><BR/>-attributes : ArrayList<String>|+EventMap(defAttrib : ArrayList<String>) : EventMap<BR/>+renameEvent(oldName : String, newName : String) : void<BR/>+mergeEventMaps(in : EventMap) : void<BR/>+mergeEvents(in : EventMap) : void<BR/>+addEvent(eventName : String) : void<BR/>+addEvent(eventName : String, context : EventMap) : void<BR/>+removeEvent(eventName : String) : void<BR/>+addAttributes(attrib : ArrayList<String>) : void<BR/>+overwriteAttributes(attrib : ArrayList<String>) : void<BR/>+setEventAttribute(nom : String, ref : String, val : boolean) : void<BR/>#getEvent(eventName : String) : Entity<BR/>+getAttributes() : ArrayList<String><BR/>+getEventNames() : ArrayList<String><BR/>+getEventsWithAttribute(attrib : String) : ArrayList<String><BR/>+getEventAttribute(nom : String, ref : String) : Boolean<BR/>+eventExists(eventName : String) : boolean<BR/>#getEvents() : HashMap<String,Entity><BR/>+contains(in : String) : boolean}>];
n47 [label = <{TransitionSystem|-states : StateMap<BR/>-events : EventMap<BR/>-transitions : TransitionFunction<BR/>-id : String|+TransitionSystem(inId : String, attribState : ArrayList<String>, attribEvent : ArrayList<String>, attribTransition : ArrayList<String>) : TransitionSystem<BR/>+TransitionSystem(inId : String) : TransitionSystem<BR/>+renameStates() : void<BR/>+renameState(old : String, newName : String) : void<BR/>+renameEvent(old : String, newName : String) : void<BR/>+compileStateName(in : ArrayList<String>) : String<BR/>+compileStateAttributes(in : ArrayList<String>, context : TransitionSystem) : void<BR/>+compileStateAttributes(source : String, in : ArrayList<String>, context : ArrayList<TransitionSystem>) : void<BR/>+compileEventAttributes(eventName : String, context : ArrayList<TransitionSystem>) : void<BR/>+copyAttributes(ot : TransitionSystem) : void<BR/>+mergeStates(other : TransitionSystem) : void<BR/>+mergeEvents(other : TransitionSystem) : void<BR/>+mergeTransitions(other : TransitionSystem) : void<BR/>+toTextFile(filePath : String, name : String) : void<BR/>+addState(stateName : String) : void<BR/>+addState(stateName : String, context : TransitionSystem) : void<BR/>+addAttributeToState(stateName : String, attribute : String, ref : boolean) : void<BR/>+addStateComposition(main : String, pieces : ArrayList<String>) : void<BR/>+addEvent(eventName : String) : void<BR/>+addEvent(eventName : String, context : TransitionSystem) : void<BR/>+addTransition(state : String, event : String, state2 : String) : void<BR/>+addTransition(state : String, event : String, state2 : String, context : TransitionSystem) : void<BR/>+removeState(stateName : String) : void<BR/>+removeEvent(event : String) : void<BR/>+removeTransition(state1 : String, eventName : String, state2 : String) : void<BR/>+setId(inId : String) : void<BR/>+setFSMStateMap(inState : StateMap) : void<BR/>+setFSMEventMap(inEvent : EventMap) : void<BR/>+setFSMTransitionFunction(inTrans : TransitionFunction) : void<BR/>+setStateAttributes(attrib : ArrayList<String>) : void<BR/>+setStateAttribute(nom : String, ref : String, val : boolean) : void<BR/>+setStateComposition(aggregate : String, pieces : ArrayList<String>) : void<BR/>+setStateCompositions(in : StateMap) : void<BR/>+addEventAttributes(attrib : ArrayList<String>) : void<BR/>+overwriteEventAttributes(attrib : ArrayList<String>) : void<BR/>+setEventAttribute(nom : String, ref : String, val : boolean) : void<BR/>+setTransitionAttributes(attrib : ArrayList<String>) : void<BR/>+setTransitionAttribute(nom : String, event : String, ref : String, val : boolean) : void<BR/>+getId() : String<BR/>+getStateMap() : StateMap<BR/>+getEventMap() : EventMap<BR/>+getTransitionFunction() : TransitionFunction<BR/>+hasStateAttribute(ref : String) : boolean<BR/>+getStateAttributeMap() : HashMap<String,ArrayList<Boolean>><BR/>+getStatesWithAttribute(attrib : String) : ArrayList<String><BR/>+getStateAttributes() : ArrayList<String><BR/>+getStateNames() : ArrayList<String><BR/>+getStateComposition(state : String) : ArrayList<String><BR/>+stateExists(stateName : String) : boolean<BR/>+getStateAttribute(nom : String, ref : String) : Boolean<BR/>+hasEventAttribute(ref : String) : boolean<BR/>+getEventAttributeMap() : HashMap<String,ArrayList<Boolean>><BR/>+getEventsWithAttribute(attrib : String) : ArrayList<String><BR/>+getEventAttributes() : ArrayList<String><BR/>+getEventNames() : ArrayList<String><BR/>+eventExists(eventName : String) : boolean<BR/>+getEventAttribute(nom : String, ref : String) : Boolean<BR/>+hasTransitionAttribute(ref : String) : boolean<BR/>+getTransitionsWithAttribute(attrib : String) : ArrayList<String><BR/>+getTransitionAttributes() : ArrayList<String><BR/>+getStateTransitionEvents(state : String) : ArrayList<String><BR/>+getNumberTransitions() : int<BR/>+getStateEventTransitionStates(state : String, event : String) : ArrayList<String><BR/>+getTransitionLabels() : ArrayList<String><BR/>+getTransitionLabelAttributeMap() : HashMap<String,ArrayList<Boolean>><BR/>+getTransitionAttribute(nom : String, event : String, ref : String) : Boolean<BR/>-formTransitionLabel(start : String, end : String, event : String) : String<BR/>-copy(in : ArrayList<String>) : ArrayList<String><BR/>+copy() : TransitionSystem}>];
n48 [label = <{EventSets|<b><i>+EVENT_ATTR_LIST : String[]</i></b><BR/><b><i>+EVENT_LIST_A : String[]</i></b><BR/><b><i>+EVENT_LIST_B : String[]</i></b><BR/><b><i>+EVENT_LIST_C : String[]</i></b><BR/><b><i>+EVENT_LIST_D : String[]</i></b><BR/><b><i>+EVENT_LIST_E : String[]</i></b><BR/><b><i>+EVENT_LIST_FINN5 : String[]</i></b><BR/><b><i>+EVENT_LIST_LIU_ONE : String[]</i></b>|}>];
n49 [label = <{AdjustFSM|<b><i>-HEADER : String</i></b><BR/><b><i>-CATEGORY_GENERATE : String</i></b><BR/><b><i>-CATEGORY_EDIT_FSM : String</i></b><BR/><b><i>-CATEGORY_EDIT_STATES : String</i></b><BR/><b><i>-CATEGORY_EDIT_EVENTS : String</i></b><BR/><b><i>-CATEGORY_EDIT_TRANSITIONS : String</i></b><BR/><b><i>-CATEGORY_ADMIN : String</i></b><BR/><b><i>-CATEGORIES : String[]</i></b><BR/><b><i>-HELP : String</i></b>|+AdjustFSM() : AdjustFSM}>];
n50 [label = <{EntryEmpty||+EntryEmpty(prefix : String, label : String, button : boolean, code : int) : EntryEmpty}>];
n51 [label = <{PopoutInputRequest|<b><i>-POPUP_WIDTH : int</i></b><BR/><b><i>-POPUP_HEIGHT : int</i></b><BR/><b><i>-CODE_SUBMIT : int</i></b><BR/><b><i>-ELEMENT_NAME_ENTRY : String</i></b><BR/>-entryNum : int<BR/>-ready : boolean<BR/>-out : ArrayList<String>|+PopoutInputRequest(text : String, num : int) : PopoutInputRequest<BR/>+getSubmitted() : ArrayList<String><BR/>-compileEntryName(in : int) : String}>];
n52 [label = <{DisplayPageManager|<b><i>-CODE_BASE_DISPLAY_HEADER : int</i></b><BR/>-imageHeader : HeaderSelect<BR/>-display : DisplayPage<BR/>-p : HandlePanel<BR/>-fsms : ArrayList<FSMInfo><BR/>-index : int<BR/>-reference : InputHandler|+DisplayPageManager(ref : InputHandler, xIn : int, yIn : int, wid : int, hei : int, vertProp : double) : DisplayPageManager<BR/>+generateElementPanel(x : int, y : int, width : int, height : int) : void<BR/>+updateSizeLoc(x : int, y : int, wid : int, hei : int, vertProp : double) : void<BR/>+drawPage() : void<BR/>+toggleDisplayImageMode() : void<BR/>+removeFSM(ref : String) : void<BR/>+updateFSMInfo(ref : String, stateAttrib : ArrayList<String>, eventAttrib : ArrayList<String>, tranAttrib : ArrayList<String>, stateMap : HashMap<String,ArrayList<Boolean>>, eventMap : HashMap<String,ArrayList<Boolean>>, transMap : HashMap<String,ArrayList<Boolean>>) : void<BR/>+updateFSMImage(ref : String, img : String) : void<BR/>+setCurrentDisplayIndex(ind : int) : void<BR/>+getCurrentFSM() : String<BR/>-getCurrentFSMInfo() : FSMInfo<BR/>-getFSMInfo(ref : String) : FSMInfo<BR/>-getDisplayNames() : ArrayList<String><BR/>+getCodeReferenceBase() : int<BR/>+getSizeDisplayList() : int<BR/>+getBodyPanel() : HandlePanel<BR/>+getHeaderPanel() : HeaderSelect}>];
n53 [label = <{CrushIdentityGroup|-parentGroup : CrushIdentityGroup<BR/>-event : String<BR/>-thisGroup : HashSet<String>|+CrushIdentityGroup(parent : CrushIdentityGroup, ev : String, group : HashSet<String>) : CrushIdentityGroup<BR/>+getGroup() : HashSet<String><BR/>+getSize() : int<BR/>-search(check : HashSet<String>) : boolean}>];
n54 [label = <{DecideInfCoobs||+DecideInfCoobs(inPlan : ArrayList<TransitionSystem>, inSpe : ArrayList<TransitionSystem>, attrIn : ArrayList<String>, agentsIn : ArrayList<Agent>) : DecideInfCoobs<BR/>+DecideInfCoobs(events : ArrayList<String>, specStart : TransitionSystem, attrIn : ArrayList<String>, agentsIn : ArrayList<Agent>) : DecideInfCoobs<BR/>+DecideInfCoobs(root : TransitionSystem, attr : ArrayList<String>, in : ArrayList<Agent>) : DecideInfCoobs<BR/>+DecideInfCoobs() : DecideInfCoobs}>];
n55 [label = <{TestFunctionality|<b><i>-RESULTS_FILE : String</i></b><BR/><b><i>-ANALYSIS_FILE : String</i></b><BR/><i>-model : Manager</i><BR/><i>-eventAtt : ArrayList<String></i><BR/><i>-defaultWritePath : String</i><BR/><i>-writePath : String</i><BR/><i>-terminalPrint : boolean</i>|<i>+main(args : String[]) : void</i><BR/><i>-runAllTests() : void</i><BR/><i>-runAllCoobsTests() : void</i><BR/><i>-runAllInfCoobsTests() : void</i><BR/><i>-runAllSBTests() : void</i><BR/><i>-runAllIncrementalCoobsTests() : void</i><BR/><i>-generateSystems() : void</i><BR/><i>-basicUStructCheck() : void</i><BR/><i>-crushUStructCheck() : void</i><BR/><i>-crushUStructCheck2() : void</i><BR/><i>-crushUStructCheck3() : void</i><BR/><i>-crushUStructCheckFinn() : void</i><BR/><i>-autoTestNewRandomSystem(numPlants : int, numSpecs : int, numStates : int, numStateVar : int, numEve : int, numEveVar : int, shareRate : double, numAgents : int, numAgentVar : int, obsRate : double, ctrRate : double) : void</i><BR/><i>-autoTestOldSystem(prefixNom : String) : void</i><BR/><i>-pullReserveDisplay() : void</i><BR/><i>-autoTestSystemFull(prefixNom : String, plantNames : ArrayList<String>, specNames : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>, displays : boolean) : void</i><BR/><i>-autoTestHeuristicsIncremental(numPlants : int, numSpecs : int, numStates : int, numStateVar : int, numEve : int, numEveVar : int, shareRate : double, numAgents : int, numAgentVar : int, obsRate : double, ctrRate : double) : void</i><BR/><i>-checkCoobservable(name : String, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>, inf : boolean) : boolean</i><BR/><i>-checkCoobservable(plants : ArrayList<String>, specs : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>, inf : boolean) : boolean</i><BR/><i>-printCoobsLabel(system : String, type : boolean) : void</i><BR/><i>-checkSystemACoobservable(inf : boolean) : void</i><BR/><i>-checkSystemBCoobservable(inf : boolean) : void</i><BR/><i>-checkSystemBAltCoobservable(inf : boolean) : void</i><BR/><i>-checkSystemCCoobservable(inf : boolean) : void</i><BR/><i>-checkSystemDCoobservable(inf : boolean) : void</i><BR/><i>-checkSystemECoobservable(inf : boolean) : void</i><BR/><i>-checkSystemFinnCoobservable(inf : boolean) : void</i><BR/><i>-checkSystemLiuOneCoobservable(inf : boolean) : void</i><BR/><i>-checkSystemLiuTwoCoobservable(inf : boolean) : void</i><BR/><i>-checkSBCoobservable(name : String, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : boolean</i><BR/><i>-checkSBCoobservable(plants : ArrayList<String>, specs : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : boolean</i><BR/><i>-prepSoloSpecRunSB(name : String, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : boolean</i><BR/><i>-printSBCoobsLabel(system : String) : void</i><BR/><i>-checkSystemASBCoobservable() : void</i><BR/><i>-checkSystemBSBCoobservable() : void</i><BR/><i>-checkSystemCSBCoobservable() : void</i><BR/><i>-checkSystemDSBCoobservable() : void</i><BR/><i>-checkSystemESBCoobservable() : void</i><BR/><i>-checkSystemUrvashiSBCoobservable() : void</i><BR/><i>-checkSystemLiuOneSBCoobservable() : void</i><BR/><i>-checkSystemLiuTwoSBCoobservable() : void</i><BR/><i>-checkIncrementalCoobservable(plants : ArrayList<String>, specs : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>, inf : boolean) : boolean</i><BR/><i>-checkIncrementalSBCoobservable(plants : ArrayList<String>, specs : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : boolean</i><BR/><i>-printIncrementalLabel(system : String, inf : boolean) : void</i><BR/><i>-printIncrementalSBLabel(system : String) : void</i><BR/><i>-checkSystemLiuOneIncrementalCoobservable() : void</i><BR/><i>-checkSystemLiuTwoIncrementalCoobservable() : void</i><BR/><i>-pullSourceData(path : String) : String</i><BR/><i>-makeImage(path : String, name : String) : void</i><BR/><i>-handleOutData(t : long, hold : long) : void</i><BR/><i>-printOut(text : String) : void</i><BR/><i>-printEquivalentResults(guide : ArrayList<String>, time : long, overallMem : double, vals : ArrayList<Double>) : void</i><BR/><i>-garbageCollect() : void</i><BR/><i>-resetModel() : void</i><BR/><i>-printTimeTook(t : long) : void</i><BR/><i>-printMemoryUsage(reduction : double) : void</i><BR/><i>-getCurrentMemoryUsage() : long</i><BR/><i>-inMB(in : long) : double</i><BR/><i>-threeSig(in : double) : Double</i><BR/><i>-generateSoloSpecPlant(plant : String, spec : String) : void</i><BR/><i>-makeImageDisplay(in : String, nom : String) : void</i><BR/><i>-makeSVGImage(in : String, nom : String) : void</i>}>];
n56 [label = <{SystemGeneration|<i>-model : Manager</i>|<i>+assignManager(man : Manager) : void</i><BR/><i>+generateSystemExample1(name : String) : void</i><BR/><i>+generateSystemExample2(name : String) : void</i><BR/><i>+generateSystemExample3(name : String) : void</i><BR/><i>+generateSystemExample4(name : String) : void</i><BR/><i>+generateSystemA(name : String) : void</i><BR/><i>+generateSystemB(name : String) : void</i><BR/><i>+generateSystemBAlt(name : String) : void</i><BR/><i>+generateSystemC(name : String) : void</i><BR/><i>+generateSystemD(name : String) : void</i><BR/><i>+generateSystemE(name : String) : void</i><BR/><i>+generateSystemFinn(name : String) : void</i><BR/><i>+generateSystemSigmaStarion(name : String, events : ArrayList<String>) : void</i><BR/><i>+generateSystemSetA(name : ArrayList<String>) : void</i><BR/><i>+generateSystemSetB(name : ArrayList<String>) : void</i><BR/><i>-generateLiuG1(name : String) : void</i><BR/><i>-generateLiuG2(name : String) : void</i><BR/><i>-generateLiuH1(name : String) : void</i><BR/><i>-generateLiuG3(name : String) : void</i><BR/><i>-generateLiuG4(name : String) : void</i><BR/><i>-generateLiuH2(name : String) : void</i><BR/><i>+generateSystemSetUrvashi(plant : String, spec : String) : void</i><BR/><i>-generateUrvashiPlant(name : String) : void</i><BR/><i>-generateUrvashiSpec(name : String) : void</i><BR/><i>-generateSystemDefault(name : String) : void</i><BR/><i>-initiateEvents(name : String, eventList : String[], controllables : String...) : void</i><BR/><i>-setBadTransitions(name : String, pairTrans : String...) : void</i><BR/><i>-addTransitions(name : String, event : String, statePairs : String...) : void</i><BR/><i>-initialState(name : String, state : String) : void</i>}>];
n57 [label = <{Entity|-id : String<BR/>-wrap : Attribute|+Entity(name : String) : Entity<BR/>+copy() : Entity<BR/>+wipeAttributes() : void<BR/>+copyAttributes(ot : Entity) : void<BR/>+addAttribute(attr : String, set : boolean) : void<BR/>+addAttributes(refs : LinkedList<String>) : void<BR/>+setName(in : String) : void<BR/>+setAttributeValue(ref : String, val : boolean) : void<BR/>+setAttributes(refs : LinkedList<String>) : void<BR/>+getName() : String<BR/>+getAttributeValue(ref : String) : Boolean<BR/>+getAttributes() : LinkedList<String><BR/>+equals(other : Object) : boolean}>];
n58 [label = <{Incremental|<b><i>+INCREMENTAL_A_BOTH : int</i></b><BR/><b><i>+INCREMENTAL_A_PLANTS : int</i></b><BR/><b><i>+INCREMENTAL_A_SPECS : int</i></b><BR/><b><i>+INCREMENTAL_B_RANDOM : int</i></b><BR/><b><i>+INCREMENTAL_B_SOONEST : int</i></b><BR/><b><i>+INCREMENTAL_B_LATEST : int</i></b><BR/><b><i>+INCREMENTAL_B_LOW_STATE : int</i></b><BR/><b><i>+INCREMENTAL_B_HIGH_STATE : int</i></b><BR/><b><i>+INCREMENTAL_B_LOW_EVENTS : int</i></b><BR/><b><i>+INCREMENTAL_B_HIGH_EVENTS : int</i></b><BR/><b><i>+INCREMENTAL_B_LOW_TRANS : int</i></b><BR/><b><i>+INCREMENTAL_B_HIGH_TRANS : int</i></b><BR/><b><i>+INCREMENTAL_B_SHARE_EVENTS : int</i></b><BR/><b><i>+INCREMENTAL_B_DIFF_EVENTS : int</i></b><BR/><b><i>+COUNTEREXAMPLE_RANDOM : int</i></b><BR/><b><i>+COUNTEREXAMPLE_SHORT : int</i></b><BR/><b><i>+COUNTEREXAMPLE_LONG : int</i></b><BR/><b><i>+COUNTEREXAMPLE_FEWEST_EVENTS : int</i></b><BR/><b><i>+COUNTEREXAMPLE_MOST_EVENTS : int</i></b><BR/><b><i>+NUM_A_HEURISTICS : int</i></b><BR/><b><i>+NUM_B_HEURISTICS : int</i></b><BR/><b><i>+NUM_C_HEURISTICS : int</i></b><BR/><i>-incrementalOptionA : int</i><BR/><i>-incrementalOptionB : int</i><BR/><i>-counterexampleChoice : int</i><BR/><i>-observableRef : String</i><BR/><i>-initialRef : String</i><BR/><i>-badRef : String</i><BR/>-decider : DecideCondition|<i>+assignIncrementalOptions(a : int, b : int, c : int) : void</i><BR/><i>+assignAttributeReference(obs : String, init : String, bad : String) : void</i><BR/>+Incremental(dC : DecideCondition) : Incremental<BR/>+decideIncrementalCondition(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, attr : ArrayList<String>, agents : ArrayList<Agent>) : boolean<BR/>-logData(dec : DecideCondition, hold : ArrayList<TransitionSystem>) : void<BR/>-pickCounterExample(counters : HashSet<IllegalConfig>) : IllegalConfig<BR/>-pickComponent(plants : ArrayList<TransitionSystem>, specs : ArrayList<TransitionSystem>, counterexample : IllegalConfig) : TransitionSystem<BR/>-pickComponentHeuristicNoReject(in : int) : int<BR/>-getIncrementalSettings() : int[]<BR/>-getComponentNames(components : ArrayList<TransitionSystem>) : ArrayList<String><BR/>-getAllEvents(plants : ArrayList<TransitionSystem>) : ArrayList<String><BR/>-countTransitions(plant : TransitionSystem) : int<BR/>-sharedEvents(plant : TransitionSystem, eventPath : ArrayList<String>) : int<BR/>-canReject(plant : TransitionSystem, spec : boolean, ic : IllegalConfig) : boolean<BR/>-navigateTransitionSystem(plant : TransitionSystem, eventPath : ArrayList<String>) : String<BR/>-observablePath(plant : TransitionSystem, eventPath : ArrayList<String>) : ArrayList<String>}>];
n59 [label = <{RandomGeneration|<b><i>-TRANSITION_NUMBER_DEFAULT : int</i></b><BR/><b><i>-ALPHABET : String</i></b>|<i>+setupRandomFSMConditions(model : Manager, numObsEve : int, numContrEve : int, badTran : int) : void</i><BR/><i>+setupRandomFSMDefaultEvents(model : Manager, defaultEvents : ArrayList<String>) : void</i><BR/><i>+generateRandomFSM(nom : String, model : Manager, numStates : int, numEvents : int, numTransition : int, accessible : boolean) : String</i><BR/><i>+generateRandomSystemSet(prefixNom : String, model : Manager, numPlants : int, numSpecs : int, stateSizeAverage : int, stateVariance : int, eventSizeAverage : int, eventVariance : int, eventShareRate : double) : ArrayList<String></i><BR/><i>+generateRandomAgents(events : ArrayList<String>, agentSizeAverage : int, agentSizeVariance : int, obsRate : double, ctrRate : double) : ArrayList<HashMap<String,ArrayList<Boolean>>></i><BR/><i>+getComponentNames(prefixNom : String, numPlants : int, numSpecs : int) : ArrayList<String></i><BR/><i>+getPlantNames(prefixNom : String, numPlants : int) : ArrayList<String></i><BR/><i>+getSpecNames(prefixNom : String, numSpecs : int) : ArrayList<String></i><BR/><i>-copyArrayList(in : ArrayList<String>) : ArrayList<String></i><BR/><i>-getPlantEvents(numEvents : int, eventChar : String, plantName : String) : ArrayList<String></i><BR/><i>-configureName(prefix : String, num : int, plant : boolean) : String</i>}>];
n60 [label = <{AttributeList|<b><i>+STATE_ATTRIBUTES : String[]</i></b><BR/><b><i>+ATTRIBUTE_INITIAL : String</i></b><BR/><b><i>+ATTRIBUTE_AON_INITIAL : boolean</i></b><BR/><b><i>+ATTRIBUTE_MARKED : String</i></b><BR/><b><i>+ATTRIBUTE_AON_MARKED : boolean</i></b><BR/><b><i>+ATTRIBUTE_PRIVATE : String</i></b><BR/><b><i>+ATTRIBUTE_AON_PRIVATE : boolean</i></b><BR/><b><i>+ATTRIBUTE_BAD : String</i></b><BR/><b><i>+ATTRIBUTE_AON_BAD : boolean</i></b><BR/><b><i>+ATTRIBUTE_GOOD : String</i></b><BR/><b><i>+ATTRIBUTE_AON_GOOD : boolean</i></b><BR/><b><i>+EVENT_ATTRIBUTES : String[]</i></b><BR/><b><i>+ATTRIBUTE_OBSERVABLE : String</i></b><BR/><b><i>+ATTRIBUTE_AON_OBSERVABLE : boolean</i></b><BR/><b><i>+ATTRIBUTE_CONTROLLABLE : String</i></b><BR/><b><i>+ATTRIBUTE_AON_CONTROLLABLE : boolean</i></b><BR/><b><i>+ATTRIBUTE_ATTACKER_OBSERVABLE : String</i></b><BR/><b><i>+ATTRIBUTE_AON_ATTACKER_OBSERVABLE : boolean</i></b><BR/><b><i>+TRANSITION_ATTRIBUTES : String[]</i></b><BR/><i>-map : HashMap<String,Boolean></i>|<i>+getAON(ref : String) : boolean</i><BR/><i>-setupMap() : void</i>}>];
n61 [label = <{EntrySetFactory|<b><i>+SIGNIFIER_TRUE : String</i></b>|<i>+generateEntryText(pref : String, label : String, button : boolean, code : int, size : int, flex : boolean) : EntrySet</i><BR/><i>+generateEntryTextDisplay(pref : String, label : String, button : boolean, code : int) : EntrySet</i><BR/><i>+generateEntryList(pref : String, label : String, button : boolean, code : int, newCode : int) : EntrySet</i><BR/><i>+generateEntryCheckbox(pref : String, label : String, button : boolean, code : int) : EntrySet</i><BR/><i>+generateEntryEmpty(pref : String, label : String, button : boolean, code : int) : EntrySet</i>}>];
n62 [label = <{Manager|<b><i>-SEPARATOR : String</i></b><BR/><b><i>-REGION_SEPARATOR : String</i></b><BR/><b><i>-TRUE_SYMBOL : String</i></b><BR/><b><i>-FALSE_SYMBOL : String</i></b><BR/>-fsms : HashMap<String,TransitionSystem><BR/>-lastProcessData : MemoryMeasure|+Manager() : Manager<BR/>-assignAttributeReferences() : void<BR/>+generateFSMDot(ref : String) : String<BR/>+readInFSM(fileContents : String) : String<BR/>+exportFSM(ref : String) : String<BR/>+readInAgents(fileContents : String) : ArrayList<HashMap<String,ArrayList<Boolean>>><BR/>+exportAgents(nom : String, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>, attributes : ArrayList<String>) : String<BR/>+hasFSM(ref : String) : boolean<BR/>+duplicate(fsm : String) : String<BR/>+flushFSMs() : void<BR/>+generateEmptyFSM(nom : String) : String<BR/>+assignRandomFSMStateConfiguration(stateAttr : ArrayList<String>, stateNumb : ArrayList<Integer>) : void<BR/>+assignRandomFSMDefaultStateSet(defaultState : ArrayList<String>) : void<BR/>+assignRandomFSMEventConfiguration(eventAttr : ArrayList<String>, eventNumb : ArrayList<Integer>) : void<BR/>+assignRandomFSMDefaultEventSet(defaultEvent : ArrayList<String>) : void<BR/>+assignRandomFSMTransitionConfiguration(transAttr : ArrayList<String>, transNumb : ArrayList<Integer>) : void<BR/>+generateRandomFSM(nom : String, numStates : int, numEvents : int, numTrans : int, det : boolean) : String<BR/>+storeProcessHoldSystem() : String<BR/>+performProduct(ref : ArrayList<String>) : String<BR/>+performParallelComposition(ref : ArrayList<String>) : String<BR/>+buildObserver(ref : String) : String<BR/>+trim(ref : String) : String<BR/>+makeAccessible(ref : String) : String<BR/>+makeCoAccessible(ref : String) : String<BR/>+stateExists(ref : String, nom : String) : Boolean<BR/>+eventExists(ref : String, nom : String) : Boolean<BR/>+isBlocking(ref : String) : Boolean<BR/>+isAccessible(ref : String) : Boolean<BR/>+testOpacity(ref : String) : Boolean<BR/>+findPrivateStates(ref : String) : ArrayList<String><BR/>+buildUStructure(ref : String, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : String<BR/>+buildUStructure(plants : ArrayList<String>, specs : ArrayList<String>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : String<BR/>+buildUStructureCrush(ref : String, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : ArrayList<String><BR/>+isCoobservableUStruct(ref : String, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean<BR/>+isCoobservableUStruct(plants : ArrayList<String>, specs : ArrayList<String>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean<BR/>+isInferenceCoobservableUStruct(ref : String, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean<BR/>+isInferenceCoobservableUStruct(plants : ArrayList<String>, specs : ArrayList<String>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean<BR/>+isSBCoobservableUrvashi(refPlants : ArrayList<String>, refSpecs : ArrayList<String>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean<BR/>+isIncrementalCoobservable(refPlants : ArrayList<String>, refSpecs : ArrayList<String>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean<BR/>+isIncrementalInferenceCoobservable(refPlants : ArrayList<String>, refSpecs : ArrayList<String>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean<BR/>+isIncrementalSBCoobservable(refPlants : ArrayList<String>, refSpecs : ArrayList<String>, attr : ArrayList<String>, agents : ArrayList<HashMap<String,ArrayList<Boolean>>>) : Boolean<BR/>+convertSoloPlantSpec(ref : String, newName : String) : String<BR/>+addFSM(id : String, stateAttr : ArrayList<String>, eventAttr : ArrayList<String>, tranAttr : ArrayList<String>) : void<BR/>+removeFSM(id : String) : void<BR/>+renameFSM(old : String, newFSM : String) : void<BR/>+assignStateAttributes(ref : String, stateAttr : ArrayList<String>) : void<BR/>+assignEventAttributes(ref : String, eventAttr : ArrayList<String>) : void<BR/>+assignTransitionAttributes(ref : String, tranAttr : ArrayList<String>) : void<BR/>+addState(ref : String, stateName : String) : void<BR/>+addStates(ref : String, num : int) : void<BR/>+removeState(ref : String, stateName : String) : void<BR/>+renameState(ref : String, old : String, newNom : String) : void<BR/>+setStateAttribute(ref : String, stateName : String, attrib : String, inValue : boolean) : void<BR/>+addEvent(ref : String, eventName : String) : void<BR/>+addEvents(ref : String, num : int) : void<BR/>+removeEvent(ref : String, eventName : String) : void<BR/>+renameEvent(ref : String, old : String, newNom : String) : void<BR/>+setEventAttribute(ref : String, eventName : String, attrib : String, inValue : boolean) : void<BR/>+addTransition(ref : String, star : String, even : String, targ : String) : void<BR/>+removeTransition(ref : String, star : String, even : String, targ : String) : void<BR/>+setTransitionAttribute(ref : String, star : String, even : String, attrib : String, inValue : boolean) : void<BR/>+setFSMStateAttributes(ref : String, attri : ArrayList<String>) : void<BR/>+setFSMEventAttributes(ref : String, attri : ArrayList<String>) : void<BR/>+setFSMTransitionAttributes(ref : String, attri : ArrayList<String>) : void<BR/>+assignMemoryMeasure(m : MemoryMeasure) : void<BR/>+getLastProcessData() : MemoryMeasure<BR/>+getFSMStateList(ref : String) : ArrayList<String><BR/>+getFSMStateAttributes(ref : String) : ArrayList<String><BR/>+getFSMStateAttributeMap(ref : String) : HashMap<String,ArrayList<Boolean>><BR/>+getFSMEventList(ref : String) : ArrayList<String><BR/>+getFSMEventAttributes(ref : String) : ArrayList<String><BR/>+getFSMEventAttributeMap(ref : String) : HashMap<String,ArrayList<Boolean>><BR/>+getFSMTransitionList(ref : String) : ArrayList<String><BR/>+getFSMTransitionAttributes(ref : String) : ArrayList<String><BR/>+getFSMTransitionAttributeMap(ref : String) : HashMap<String,ArrayList<Boolean>><BR/>+getStateAttributeList() : String[]<BR/>+getEventAttributeList() : String[]<BR/>+getTransitionAttributeList() : String[]<BR/>+getReferences() : ArrayList<String><BR/>-appendFSM(nom : String, fsm : TransitionSystem, overwrite : boolean) : String<BR/>-bail(ref : String) : boolean<BR/>-bail(ref : ArrayList<String>) : boolean<BR/>-bailMulti(ref : ArrayList<String>) : boolean}>];
n63 [label = <{FiniteStateMachine|<b><i>+DOT_ADDRESS_VAR : String</i></b><BR/><b><i>+ADDRESS_SETTINGS : String</i></b><BR/><b><i>+ADDRESS_IMAGES : String</i></b><BR/><b><i>+ADDRESS_SOURCES : String</i></b><BR/><b><i>+ADDRESS_CONFIG : String</i></b><BR/><b><i>-DEFAULT_CONFIG_COMMENT : String</i></b><BR/><b><i>-SEPARATOR : String</i></b><BR/><b><i>-SYMBOL_FALSE : String</i></b><BR/><b><i>-SYMBOL_TRUE : String</i></b><BR/><b><i>-REGEX_NEWLINE_REPLACE : String</i></b><BR/>-view : FSMUI<BR/>-model : Manager|+FiniteStateMachine() : FiniteStateMachine<BR/>+receiveCode(code : int, mouseType : int) : void<BR/>+receiveKeyInput(code : char, keyType : int) : void<BR/>+updateViewFSM(ref : String) : void<BR/>-codeHandlingAdjustFSM(code : int, mouseType : int) : void<BR/>-codeHandlingOperations(code : int, mouseType : int) : void<BR/>-codeHandlingUStructure(code : int, mouseType : int) : void<BR/>-codeHandlingDisplay(code : int, mouseType : int) : void<BR/>-loadSource() : void<BR/>-saveFSM(currFSM : String) : void<BR/>-generateRandomFSM(code : int) : void<BR/>-addTransition(currFSM : String, code : int) : void<BR/>-removeTransition(currFSM : String, code : int) : void<BR/>-addAttributeLists(newStuff : ArrayList<String>, oldStuff : ArrayList<String>) : ArrayList<String><BR/>-subtractAttributeLists(remv : ArrayList<String>, oldStuff : ArrayList<String>) : ArrayList<String><BR/>-appendSingleChosenAttribute(in : String[], code : int) : void<BR/>-appendSingleChosenAttribute(in : ArrayList<String>, code : int) : void<BR/>-requestAttributeChoice(code : int, attributes : String[], phrase : String) : void<BR/>-requestFSMChoice(code : int) : void<BR/><i>+fileConfiguration() : void</i><BR/>-generateDotImage(ref : String) : String<BR/>-allotFSMToView(fsm : String) : void}>];
n64 [label = <{FSMUI|<b><i>-PANEL_RATIO_VERTICAL : double</i></b><BR/><b><i>-WINDOW_NAME : String</i></b><BR/><b><i>-DEFAULT_POPUP_WIDTH : int</i></b><BR/><b><i>-DEFAULT_POPUP_HEIGHT : int</i></b><BR/>-frame : WindowFrame<BR/>-displayPageManager : DisplayPageManager<BR/>-optionPageManager : OptionPageManager<BR/>-reference : InputReceiver|+FSMUI(wid : int, hei : int, ref : InputReceiver) : FSMUI<BR/>-createPages() : void<BR/>+receiveCode(code : int, mouseType : int) : void<BR/>+receiveKeyInput(code : char, keyType : int) : void<BR/>+displayAlert(text : String) : void<BR/>+requestFolderPath(defDir : String, display : String) : String<BR/>+requestFilePath(defDir : String, display : String) : String<BR/>+requestUserInputList(refs : String[], search : boolean) : String<BR/>+requestUserInputList(refs : ArrayList<String>, search : boolean) : String<BR/>+requestUserInput(phrase : String) : String<BR/>+requestUserInput(phrase : String, size : int) : ArrayList<String><BR/>+requestUserIntegerInput(phrase : String) : Integer<BR/>+requestAgentInput(inAgents : ArrayList<String>, events : ArrayList<String>, attrib : ArrayList<String>) : ArrayList<String><BR/>+removeFSM(ref : String) : void<BR/>+updateFSMInfo(ref : String, stateAttrib : ArrayList<String>, eventAttrib : ArrayList<String>, tranAttrib : ArrayList<String>, stateMap : HashMap<String,ArrayList<Boolean>>, eventMap : HashMap<String,ArrayList<Boolean>>, transMap : HashMap<String,ArrayList<Boolean>>) : void<BR/>+updateFSMImage(ref : String, img : String) : void<BR/>+clearTextContents(code : int) : void<BR/>+startLoading() : void<BR/>+endLoading() : void<BR/>+updateDisplay() : void<BR/>+updateActiveOptionPage() : void<BR/>+updateDisplayPanel() : void<BR/>+setTextContent(code : int, posit : int, ref : String) : void<BR/>+assignSymbols(separator : String, tr : String, fal : String) : void<BR/>+getCurrentFSM() : String<BR/>+getTextContent(code : int) : String<BR/>+getTextContent(code : int, posit : int) : String<BR/>+getIntegerContent(code : int) : Integer<BR/>+getIntegerContent(code : int, posit : int) : Integer<BR/>+getCheckboxContent(code : int) : Boolean<BR/>+getContent(code : int) : ArrayList<String><BR/>+retrieveFileReader(pathIn : String) : BufferedReader<BR/><i>+stripPath(in : String) : String</i>}>];
n65 [label = <{EventRep|-event : String<BR/>-setVals : ArrayList<Boolean>|+EventRep(inEve : String, i : int) : EventRep<BR/>+toggle(i : int) : void<BR/>+getValues() : ArrayList<Boolean><BR/>+getValue(i : int) : boolean<BR/>+getName() : String}>];
n66 [label = <{ProcessClean|<i>-BAD_STATE_ATTRIBUTES : Exception</i><BR/><i>+attributeInitialRef : String</i><BR/><i>+attributeMarkedRef : String</i>|<i>+assignAttributeReferences(init : String, mark : String) : void</i><BR/><i>+trim(in : TransitionSystem) : TransitionSystem</i><BR/><i>+makeAccessible(in : TransitionSystem) : TransitionSystem</i><BR/><i>+makeCoAccessible(in : TransitionSystem) : TransitionSystem</i><BR/><i>-getCoAccessibleMap(in : TransitionSystem) : ArrayList<String></i><BR/><i>-recursivelyFindMarked(curr : String, positive : HashSet<String>, negative : HashSet<String>, visited : HashSet<String>, in : TransitionSystem) : boolean</i>}>];
n67 [label = <{GraphViz|-configFile : Properties<BR/>-osName : String<BR/>-cfgProp : String<BR/>-tempDir : String<BR/>-DOT : String<BR/>-graph : StringBuilder<BR/>-dpiSizes : int[]<BR/>-currentDpiPos : int<BR/><b><i>-serialVersionUID : long</i></b>|+GraphViz(workingPath : String, configPath : String) : GraphViz<BR/><i>+verifyDotPath(path : String) : boolean</i><BR/>+increaseDpi() : void<BR/>+decreaseDpi() : void<BR/>+writeGraphToFile(img : byte[], file : String) : int<BR/>+writeGraphToFile(img : byte[], to : File) : int<BR/>-writeDotSourceToFile(str : String) : File<BR/>+readSource(input : String) : void<BR/>+getImageDpi() : int<BR/>+getDotSource() : String<BR/>+getGraph(dot_source : String, type : String) : byte[]<BR/>-get_img_stream(dot : File, type : String) : byte[]<BR/>+start_subgraph(clusterid : int) : String<BR/>+end_subgraph() : String<BR/>+start_graph() : String<BR/>+end_graph() : String<BR/>+clearGraph() : void<BR/>+add(line : String) : void<BR/>+addln(line : String) : void<BR/>+addln() : void}>];
n68 [label = <{CodeReference|<b><i>+CODE_GENERATE_IMAGE : int</i></b><BR/><b><i>+CODE_DISPLAY_CYCLE_VIEW : int</i></b><BR/><b><i>+CODE_ACCESS_NUM_STATES : int</i></b><BR/><b><i>+CODE_ACCESS_NUM_EVENTS : int</i></b><BR/><b><i>+CODE_ACCESS_NUM_TRANS : int</i></b><BR/><b><i>+CODE_ACCESS_FSM_NAME : int</i></b><BR/><b><i>+CODE_ACCESS_NON_DETERMINISTIC : int</i></b><BR/><b><i>+CODE_ACCESS_STATE_ATTRIBUTES : int</i></b><BR/><b><i>+CODE_ACCESS_EVENT_ATTRIBUTES : int</i></b><BR/><b><i>+CODE_ACCESS_TRANS_ATTRIBUTES : int</i></b><BR/><b><i>+CODE_ADD_STATE_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_ADD_EVENT_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_ADD_TRANS_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_GENERATE_FSM : int</i></b><BR/><b><i>+CODE_RENAME_FSM : int</i></b><BR/><b><i>+CODE_FSM_ADD_STATE_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_FSM_ACCESS_ADD_STATE_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_FSM_REMOVE_STATE_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_FSM_ACCESS_REMOVE_STATE_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_FSM_ADD_EVENT_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_FSM_ACCESS_ADD_EVENT_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_FSM_REMOVE_EVENT_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_FSM_ACCESS_REMOVE_EVENT_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_FSM_ADD_TRANS_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_FSM_ACCESS_ADD_TRANS_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_FSM_REMOVE_TRANS_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_FSM_ACCESS_REMOVE_TRANS_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_ADD_STATE : int</i></b><BR/><b><i>+CODE_REMOVE_STATE : int</i></b><BR/><b><i>+CODE_RENAME_STATE : int</i></b><BR/><b><i>+CODE_ADD_STATES : int</i></b><BR/><b><i>+CODE_EDIT_STATE_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_ADD_EDIT_STATE_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_ACCESS_EDIT_STATE : int</i></b><BR/><b><i>+CODE_ADD_EVENT : int</i></b><BR/><b><i>+CODE_REMOVE_EVENT : int</i></b><BR/><b><i>+CODE_RENAME_EVENT : int</i></b><BR/><b><i>+CODE_ADD_EVENTS : int</i></b><BR/><b><i>+CODE_EDIT_EVENT_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_ADD_EDIT_EVENT_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_ACCESS_EDIT_EVENT : int</i></b><BR/><b><i>+CODE_ADD_TRANSITION : int</i></b><BR/><b><i>+CODE_REMOVE_TRANSITION : int</i></b><BR/><b><i>+CODE_EDIT_TRANS_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_ADD_EDIT_TRANS_ATTRIBUTE : int</i></b><BR/><b><i>+CODE_ACCESS_EDIT_TRANS : int</i></b><BR/><b><i>+CODE_SAVE_FSM : int</i></b><BR/><b><i>+CODE_SAVE_IMG : int</i></b><BR/><b><i>+CODE_SAVE_TKZ : int</i></b><BR/><b><i>+CODE_SAVE_SVG : int</i></b><BR/><b><i>+CODE_LOAD_SOURCE : int</i></b><BR/><b><i>+CODE_DELETE_SOURCE : int</i></b><BR/><b><i>+CODE_DUPLICATE_FSM : int</i></b><BR/><b><i>+CODE_CLOSE_FSM : int</i></b><BR/><b><i>+CODE_TRIM : int</i></b><BR/><b><i>+CODE_ACCESSIBLE : int</i></b><BR/><b><i>+CODE_CO_ACCESSIBLE : int</i></b><BR/><b><i>+CODE_OBSERVER : int</i></b><BR/><b><i>+CODE_PRODUCT_SELECT : int</i></b><BR/><b><i>+CODE_PRODUCT : int</i></b><BR/><b><i>+CODE_PARALLEL_COMPOSITION_SELECT : int</i></b><BR/><b><i>+CODE_PARALLEL_COMPOSITION : int</i></b><BR/><b><i>+CODE_SUP_CNT_SBL_SELECT : int</i></b><BR/><b><i>+CODE_SUP_CNT_SBL : int</i></b><BR/><b><i>+CODE_UNDER_FSM : int</i></b><BR/><b><i>+CODE_OPT_OPQ_CONTROLLER : int</i></b><BR/><b><i>+CODE_OPT_SPVR_SELECT : int</i></b><BR/><b><i>+CODE_OPT_SPVR : int</i></b><BR/><b><i>+CODE_GRT_LWR_BND_SELECT : int</i></b><BR/><b><i>+CODE_GRT_LWR_BND : int</i></b><BR/><b><i>+CODE_PRUNE : int</i></b><BR/><b><i>+CODE_BLOCKING : int</i></b><BR/><b><i>+CODE_STATE_EXISTS : int</i></b><BR/><b><i>+CODE_SELECT_PLANT : int</i></b><BR/><b><i>+CODE_ADD_BAD_TRANS : int</i></b><BR/><b><i>+CODE_BUILD_AGENTS : int</i></b><BR/><b><i>+CODE_BUILD_USTRUCT : int</i></b><BR/><b><i>+CODE_TOGGLE_USTRUCT : int</i></b><BR/><b><i>+CODE_DISPLAY_BAD_TRANS_START : int</i></b>|}>];
n69 [label = <{Operations|<b><i>-HEADER : String</i></b><BR/><b><i>-CATEGORY_TRANS_SYSTEMS : String</i></b><BR/><b><i>-CATEGORY_FSM : String</i></b><BR/><b><i>-CATEGORY_QUERIES : String</i></b><BR/><b><i>-CATEGORIES : String[]</i></b><BR/><b><i>-HELP : String</i></b>|+Operations() : Operations}>];
n70 [label = <{<<interface>><BR/>InputHandler||<u>+receiveCode(code : int, mouseType : int) : void</u><BR/><u>+receiveKeyInput(code : char, keyType : int) : void</u>}>];
n71 [label = <{<<interface>><BR/>ReceiveMemoryMeasure||<u>+assignMemoryMeasure(m : MemoryMeasure) : void</u>}>];
n72 [label = <{<<interface>><BR/>MemoryMeasure||<u>+getAverageMemoryUsage() : double</u><BR/><u>+getMaximumMemoryUsage() : double</u><BR/><u>+produceOutputLog() : String</u><BR/><u>+getOutputGuide() : ArrayList<String></u><BR/><u>+getStoredData() : ArrayList<Double></u><BR/><u>+getReserveSystem() : TransitionSystem</u><BR/><u>+reserveTransitionSystem(in : TransitionSystem) : void</u>}>];
n73 [label = <{<<interface>><BR/>InputReceiver||<u>+receiveCode(code : int, mouseType : int) : void</u><BR/><u>+receiveKeyInput(code : char, keyType : int) : void</u>}>];
n74 [label = <{<<interface>><BR/>DecideCondition||<u>+decideCondition() : boolean</u><BR/><u>+constructDeciderCoobs(events : ArrayList<String>, specStart : TransitionSystem, attr : ArrayList<String>, agents : ArrayList<Agent>) : DecideCondition</u><BR/><u>+getCounterExamples() : HashSet<IllegalConfig></u><BR/><u>+addComponent(next : TransitionSystem, plant : boolean) : void</u><BR/><u>+produceMemoryMeasure() : MemoryMeasure</u>}>];
subgraph cluster_{
label = "";
fontsize = 30;
penwidth = 1;
subgraph cluster_controller{
label = "controller";
fontsize = 26;
penwidth = 2;
n63;
n11;
n68;
n12;
n73;
subgraph cluster_controller_convert{
label = "controller.convert";
fontsize = 22;
penwidth = 3;
n39;
n67;
n25;
}
}
subgraph cluster_model{
label = "model";
fontsize = 26;
penwidth = 2;
n62;
n60;
subgraph cluster_model_convert{
label = "model.convert";
fontsize = 22;
penwidth = 3;
n29;
n18;
n21;
n35;
}
subgraph cluster_model_fsm{
label = "model.fsm";
fontsize = 22;
penwidth = 3;
n47;
subgraph cluster_model_fsm_component{
label = "model.fsm.component";
fontsize = 18;
penwidth = 4;
n16;
n46;
n57;
n28;
subgraph cluster_model_fsm_component_transition{
label = "model.fsm.component.transition";
fontsize = 14;
penwidth = 5;
n17;
n15;
}
}
}
subgraph cluster_model_process{
label = "model.process";
fontsize = 22;
penwidth = 3;
n8;
n32;
n66;
n41;
n22;
subgraph cluster_model_process_coobservability{
label = "model.process.coobservability";
fontsize = 18;
penwidth = 4;
n43;
n58;
n36;
subgraph cluster_model_process_coobservability_deciding{
label = "model.process.coobservability.deciding";
fontsize = 14;
penwidth = 5;
n54;
n1;
n34;
n74;
}
subgraph cluster_model_process_coobservability_support{
label = "model.process.coobservability.support";
fontsize = 14;
penwidth = 5;
n53;
n44;
n19;
n6;
n24;
n26;
n42;
}
}
subgraph cluster_model_process_memory{
label = "model.process.memory";
fontsize = 18;
penwidth = 4;
n45;
n2;
n71;
n40;
n72;
}
}
}
subgraph cluster_test{
label = "test";
fontsize = 26;
penwidth = 2;
n37;
n55;
subgraph cluster_test_help{
label = "test.help";
fontsize = 22;
penwidth = 3;
n33;
n48;
n56;
n59;
}
}
subgraph cluster_ui{
label = "ui";
fontsize = 26;
penwidth = 2;
n64;
n70;
subgraph cluster_ui_headers{
label = "ui.headers";
fontsize = 22;
penwidth = 3;
n0;
}
subgraph cluster_ui_page{
label = "ui.page";
fontsize = 22;
penwidth = 3;
subgraph cluster_ui_page_displaypage{
label = "ui.page.displaypage";
fontsize = 18;
penwidth = 4;
n52;
n31;
n3;
n5;
}
subgraph cluster_ui_page_optionpage{
label = "ui.page.optionpage";
fontsize = 18;
penwidth = 4;
n38;
n10;
n7;
subgraph cluster_ui_page_optionpage_entryset{
label = "ui.page.optionpage.entryset";
fontsize = 14;
penwidth = 5;
n9;
n4;
n23;
n13;
n14;
n50;
n61;
}
subgraph cluster_ui_page_optionpage_implementation{
label = "ui.page.optionpage.implementation";
fontsize = 14;
penwidth = 5;
n30;
n49;
n69;
}
}
}
subgraph cluster_ui_popups{
label = "ui.popups";
fontsize = 22;
penwidth = 3;
n20;
n65;
n27;
n51;
}
}
}
n0 -> n70[arrowhead=normal];
n1 -> n47[arrowhead=normal];
n1 -> n8[arrowhead=normal];
n1 -> n43[arrowhead=normal];
n1 -> n42[arrowhead=normal];
n1 -> n26[arrowhead=normal];
n1 -> n24[arrowhead=normal];
n1 -> n44[arrowhead=normal];
n1 -> n19[arrowhead=normal];
n1 -> n72[arrowhead=normal];
n1 -> n1[arrowhead=none];
n1 -> n74[arrowhead=onormal, style=dashed];
n2 -> n40[arrowhead=onormal];
n5 -> n68[arrowhead=normal];
n5 -> n70[arrowhead=normal];
n5 -> n31[arrowhead=normal];
n5 -> n3[arrowhead=normal];
n7 -> n4[arrowhead=normal];
n7 -> n38[arrowhead=none];
n8 -> n47[arrowhead=normal];
n8 -> n71[arrowhead=normal];
n8 -> n32[arrowhead=normal];
n8 -> n41[arrowhead=normal];
n8 -> n66[arrowhead=normal];
n8 -> n22[arrowhead=normal];
n9 -> n4[arrowhead=onormal];
n10 -> n70[arrowhead=normal];
n10 -> n0[arrowhead=normal];
n10 -> n49[arrowhead=normal];
n10 -> n69[arrowhead=normal];
n10 -> n30[arrowhead=normal];
n10 -> n38[arrowhead=normal];
n11 -> n63[arrowhead=normal];
n12 -> n67[arrowhead=normal];
n12 -> n63[arrowhead=none];
n13 -> n4[arrowhead=onormal];
n14 -> n9[arrowhead=onormal];
n15 -> n17[arrowhead=normal];
n15 -> n15[arrowhead=none];
n16 -> n57[arrowhead=normal];
n16 -> n16[arrowhead=none];
n17 -> n57[arrowhead=onormal];
n17 -> n17[arrowhead=onormal, style=dashed];
n18 -> n47[arrowhead=normal];
n19 -> n44[arrowhead=onormal];
n19 -> n19[arrowhead=onormal, style=dashed];
n20 -> n65[arrowhead=normal];
n22 -> n47[arrowhead=normal];
n22 -> n66[arrowhead=normal];
n23 -> n4[arrowhead=onormal];
n24 -> n26[arrowhead=normal];
n26 -> n26[arrowhead=onormal, style=dashed];
n27 -> n20[arrowhead=normal];
n27 -> n65[arrowhead=normal];
n28 -> n28[arrowhead=none];
n29 -> n29[arrowhead=none];
n30 -> n38[arrowhead=onormal];
n30 -> n68[arrowhead=normal];
n32 -> n47[arrowhead=normal];
n33 -> n48[arrowhead=normal];
n34 -> n47[arrowhead=normal];
n34 -> n8[arrowhead=normal];
n34 -> n36[arrowhead=normal];
n34 -> n42[arrowhead=normal];
n34 -> n24[arrowhead=normal];
n34 -> n44[arrowhead=normal];
n34 -> n72[arrowhead=normal];
n34 -> n34[arrowhead=none];
n34 -> n74[arrowhead=onormal, style=dashed];
n35 -> n60[arrowhead=normal];
n35 -> n47[arrowhead=normal];
n35 -> n29[arrowhead=normal];
n36 -> n2[arrowhead=onormal];
n36 -> n47[arrowhead=normal];
n36 -> n42[arrowhead=normal];
n36 -> n26[arrowhead=normal];
n36 -> n53[arrowhead=normal];
n36 -> n6[arrowhead=normal];
n36 -> n24[arrowhead=normal];
n37 -> n63[arrowhead=normal];
n37 -> n39[arrowhead=normal];
n37 -> n60[arrowhead=normal];
n37 -> n62[arrowhead=normal];
n38 -> n70[arrowhead=normal];
n38 -> n61[arrowhead=normal];
n39 -> n25[arrowhead=normal];
n39 -> n67[arrowhead=normal];
n40 -> n47[arrowhead=normal];
n40 -> n40[arrowhead=none];
n40 -> n72[arrowhead=onormal, style=dashed];
n41 -> n47[arrowhead=normal];
n41 -> n58[arrowhead=normal];
n41 -> n43[arrowhead=normal];
n41 -> n36[arrowhead=normal];
n41 -> n34[arrowhead=normal];
n41 -> n54[arrowhead=normal];
n41 -> n1[arrowhead=normal];
n41 -> n42[arrowhead=normal];
n41 -> n71[arrowhead=normal];
n42 -> n46[arrowhead=normal];
n43 -> n40[arrowhead=onormal];
n43 -> n47[arrowhead=normal];
n43 -> n42[arrowhead=normal];
n43 -> n44[arrowhead=normal];
n44 -> n44[arrowhead=none];
n45 -> n40[arrowhead=onormal];
n45 -> n72[arrowhead=normal];
n46 -> n57[arrowhead=normal];
n46 -> n46[arrowhead=none];
n47 -> n60[arrowhead=normal];
n47 -> n46[arrowhead=normal];
n47 -> n16[arrowhead=normal];
n47 -> n15[arrowhead=normal];
n47 -> n47[arrowhead=none];
n48 -> n60[arrowhead=normal];
n49 -> n38[arrowhead=onormal];
n49 -> n68[arrowhead=normal];
n50 -> n4[arrowhead=onormal];
n52 -> n68[arrowhead=normal];
n52 -> n0[arrowhead=normal];
n52 -> n5[arrowhead=normal];
n52 -> n31[arrowhead=normal];
n52 -> n70[arrowhead=onormal, style=dashed];
n53 -> n53[arrowhead=onormal, style=dashed];
n54 -> n34[arrowhead=onormal];
n54 -> n47[arrowhead=normal];
n54 -> n42[arrowhead=normal];
n54 -> n74[arrowhead=normal];
n54 -> n54[arrowhead=none];
n55 -> n63[arrowhead=normal];
n55 -> n39[arrowhead=normal];
n55 -> n60[arrowhead=normal];
n55 -> n62[arrowhead=normal];
n55 -> n47[arrowhead=normal];
n55 -> n58[arrowhead=normal];
n55 -> n33[arrowhead=normal];
n55 -> n48[arrowhead=normal];
n55 -> n59[arrowhead=normal];
n55 -> n56[arrowhead=normal];
n56 -> n60[arrowhead=normal];
n56 -> n62[arrowhead=normal];
n56 -> n47[arrowhead=normal];
n56 -> n48[arrowhead=normal];
n57 -> n28[arrowhead=normal];
n57 -> n57[arrowhead=none];
n58 -> n45[arrowhead=onormal];
n58 -> n47[arrowhead=normal];
n58 -> n74[arrowhead=normal];
n58 -> n42[arrowhead=normal];
n58 -> n24[arrowhead=normal];
n59 -> n60[arrowhead=normal];
n59 -> n62[arrowhead=normal];
n59 -> n48[arrowhead=normal];
n59 -> n33[arrowhead=normal];
n60 -> n60[arrowhead=none];
n61 -> n4[arrowhead=normal];
n61 -> n23[arrowhead=normal];
n61 -> n9[arrowhead=normal];
n61 -> n14[arrowhead=normal];
n61 -> n13[arrowhead=normal];
n61 -> n50[arrowhead=normal];
n62 -> n35[arrowhead=normal];
n62 -> n21[arrowhead=normal];
n62 -> n18[arrowhead=normal];
n62 -> n47[arrowhead=normal];
n62 -> n8[arrowhead=normal];
n62 -> n72[arrowhead=normal];
n62 -> n60[arrowhead=normal];
n62 -> n71[arrowhead=onormal, style=dashed];
n63 -> n39[arrowhead=normal];
n63 -> n60[arrowhead=normal];
n63 -> n62[arrowhead=normal];
n63 -> n64[arrowhead=normal];
n63 -> n68[arrowhead=normal];
n63 -> n73[arrowhead=onormal, style=dashed];
n64 -> n73[arrowhead=normal];
n64 -> n52[arrowhead=normal];
n64 -> n10[arrowhead=normal];
n64 -> n27[arrowhead=normal];
n64 -> n51[arrowhead=normal];
n64 -> n64[arrowhead=none];
n64 -> n70[arrowhead=onormal, style=dashed];
n66 -> n47[arrowhead=normal];
n69 -> n38[arrowhead=onormal];
n69 -> n68[arrowhead=normal];
n71 -> n72[arrowhead=normal];
n72 -> n47[arrowhead=normal];
n74 -> n47[arrowhead=normal];
n74 -> n42[arrowhead=normal];
n74 -> n24[arrowhead=normal];
n74 -> n72[arrowhead=normal];
n74 -> n74[arrowhead=none];
}