BPMNOS-Maude/BPMNOS_RULES_AS_EQUATIONS_POOL_LEVEL.maude at master · PROSLab/BPMNOS-Maude · 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
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
*** SEMANTICS MODULE RESERVED TO RULES DEFINITION
load BPMNOS_RULES_AS_EQUATIONS_PROCESS_LEVEL

mod BPMNOS-SEMANTICS-POOL is
	including BPMNOS-SEMANTICS-PROCESS .

	including SETCommitment .

*** Variables definition
	---OrgName
	vars Org1Name Org2Name : OrgName .
	---Edges
	vars Edges0 Edges1 Edges2 : Edges .
  ---
	vars Status1 : Status .
	---TaskName
	var TName : TaskName .
  ---EdgeName, InputEdgeName and OutputEdgeName
	var EName IEName OEName BNIEName : EdgeName .
	---EdgeToken,  InputEdgeToken and OutputEdgeToken
	var EToken IEToken OEToken BNIEToken : EdgeToken .
	---Var for Messages
	vars Msgs1 inputMsgSet outputMsgSet inputMsgSet1 outputMsgSet1 inputMsgSet2 outputMsgSet2 : Msgs .
	vars MsgName1 MsgName2 : MsgName .
	vars MsgToken1 MsgToken1' MsgToken2 : MsgToken .
	---interRcv
	var interRcv : InterRcv .
	---Var for Collaboration
	vars Coll1 Coll2 Coll1' Coll3 : Collaboration .
	vars ProcElem1 ProcElem2 ProcElem1' : ProcElement .
	---var for Action
	var Action1 Action2 Action1' : Action .
	var ActProcElement1 : ActProcElement .
	var CollAction1 CollAction2 CollAction3 : CollaborationAction .

  var Pool1 Pool1' : Pool .

	var ProcElements1 ProcElements2 ProcElements1' : ProcElements .

	var SetCommitment1 : SetCommitment .

	op allPoolCommitments : Collaboration -> SetCommitment .
	op poolCommitment : ActCollaboration -> Commitment [ctor].
	op poolCommit : Collaboration -> Commitment .

	var poolCommitmentsCreati : SetCommitment .
	var nextState : Commitment .

	op computeAllInternalPoolCommitments(_,_) : Pool SetCommitment -> SetCommitment .


	---C-Receive
	ceq [C-Receive] :
	allPoolCommitments( pool(Org1Name,proc({Action1}ProcElements1 ),in: inputMsgSet andmsg MsgName1 .msg MsgToken1 , out: outputMsgSet))
	=
	poolCommitment( {collab(Org1Name , rcv(MsgName1))} pool(Org1Name,proc({rcv(MsgName1)}ProcElements1' ),in: inputMsgSet andmsg MsgName1 .msg decreaseMsgToken(MsgToken1),out: outputMsgSet))
	if
	(commitment({rcv(MsgName1)}ProcElements1'), SetCommitment1) := allCommitments(ProcElements1)
	/\
	MsgToken1 > 0
	.

		---G-ReceiveEvent acts on a eventSplit with one InterRcv with MsgToken > 0, and it changes the Status to msgReceived and disables all the other InterRcv .
		ceq [G-ReceiveEvent] :
		 allPoolCommitments(
		 pool(Org1Name,
			proc(
				{Action1} ProcElements1
				| eventSplit( IEName .  IEToken , eventRcvSplit( eventInterRcv( enabled , EName . EToken , MsgName1 .msg MsgToken1 )
				^ interRcv ))
			),in: inputMsgSet1 andmsg MsgName1 .msg MsgToken2 ,out: outputMsgSet1
		 )
		)
		=
		poolCommitment(
		 {collab(Org1Name , rcv(MsgName1))}
		 pool(Org1Name,
			proc(
				{rcv(MsgName1)}ProcElements1
				| eventSplit( IEName . IEToken , eventRcvSplit( eventInterRcv( msgReceived , EName . EToken , MsgName1 .msg increaseMsgToken( MsgToken1 ))
				^ setStatusDisabled( interRcv ) ))
				),in: inputMsgSet1 andmsg MsgName1 .msg decreaseMsgToken( MsgToken2 ) ,out: outputMsgSet1
		 )
		)
		if MsgToken2 > 0
		.


		---C-Internal
	 eq [C-Internal] :
	 allPoolCommitments( pool(Org1Name,proc({Action1}ProcElements1 ),in: inputMsgSet ,out: outputMsgSet ) )
	 =
	 computeAllInternalPoolCommitments( pool(Org1Name,proc({Action1}ProcElements1 ),in: inputMsgSet ,out: outputMsgSet ) , empty )
	 .

	ceq [C-Internal-ALL] :
	computeAllInternalPoolCommitments(
	 pool(Org1Name,proc({Action1}ProcElements1 ),in: inputMsgSet ,out: outputMsgSet),
	 poolCommitmentsCreati)
	=
	computeAllInternalPoolCommitments(
	 pool(Org1Name,proc({Action1}ProcElements1 ),in: inputMsgSet ,out: outputMsgSet),
	 (poolCommitmentsCreati, nextState))
	 , nextState
	--- if ProcElements1 => {Action1'}ProcElements1' /\ isInternal(Action1') .
	if (commitment({Action1'}ProcElements1'), SetCommitment1) := allCommitments(ProcElements1)
	/\ isInternal(Action1')
	/\ nextState := poolCommitment({collab(Org1Name , Action1')} pool(Org1Name,proc({Action1'}ProcElements1' ),in: inputMsgSet ,out: outputMsgSet))
	/\ ((nextState in poolCommitmentsCreati) == false ) .


	eq computeAllInternalPoolCommitments( pool(Org1Name,proc({Action1}ProcElements1 ),in: inputMsgSet ,out: outputMsgSet ),
	 poolCommitmentsCreati ) = empty [owise] .

endm