plug-obp.github.io/assets/docs/AliceBobPeterson.tuml at master · plug-obp/plug-obp.github.io · GitHub

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
model AliceBob1 with(public deployment) {

	primitiveType Integer;
	primitiveType Boolean;

	package deployment imports bsp_smt32, system {

		instance instSUS of SUS {

		}
	}

	package bsp_meta imports system {

	}

	package bsp_smt32 imports bsp_meta  {

	}

	package system imports bsp_meta {

		class SUS {
			public composite alice[1-1] : Alice;
			public composite bob[1-1] : Bob;
			public composite dataManager[1-1] : DataManager;

			connector "c1" : Alice_Bob between bob and alice;
			connector "c2" : DataManager_Alice between dataManager and alice;
			connector "c3" : DataManager_Bob between dataManager and bob;
		}

		association Alice_Bob {
			bob[1-1] : Bob in Alice_Bob;
			alice[1-1] : Alice in Alice_Bob;
		}

		association DataManager_Alice {
			alice[1-1] : Alice in DataManager_Alice;
			dataManager[1-1] : DataManager in DataManager_Alice;
		}

		association DataManager_Bob {
			bob[1-1] : Bob in DataManager_Bob;
			dataManager[1-1] : DataManager in DataManager_Bob;
		}


		class |Alice| behavesAs SM {

			stateMachine SM {
				region R {
					Initial -> I;
					I -> W : /
						opaqueBehavior = 'dataManager.flagAlice = 1; dataManager.turn = 1;' in C;;
					W -> CS: [constraint "" is opaqueExpression = 'dataManager.turn == 0 || dataManager.flagBob == 0' in C;] / ;
					CS -> I: /
						opaqueBehavior = 'dataManager.flagAlice = 0;' in C;;
					initial pseudoState Initial;
				}
			}
		}

		class |Bob| behavesAs SM {

			stateMachine SM {
				region R {
					Initial -> I;
					I -> W : /
						opaqueBehavior = 'dataManager.flagBob = 1; dataManager.turn = 0;' in C;;
					W -> CS: [constraint "" is opaqueExpression = 'dataManager.turn == 1 || dataManager.flagAlice == 0' in C;] / ;
					CS -> I: /
						opaqueBehavior = 'dataManager.flagBob = 0;' in C;;
					initial pseudoState Initial;
				}
			}
		}


		class DataManager {
			private flagAlice[1-1] : Boolean;
			private flagBob[1-1] : Boolean;
			private turn[1-1] : Integer;
		}


	}
}