|
|
|
CONTENT |
|
|
\ No newline at end of file |
|
|
|
> TODO
|
|
|
|
|
|
|
|
# Examples
|
|
|
|
|
|
|
|
> TODO (example description)
|
|
|
|
|
|
|
|
## EDP Prosumer Community
|
|
|
|
|
|
|
|
> TODO
|
|
|
|
|
|
|
|
```ruby
|
|
|
|
# roles
|
|
|
|
P(Number)
|
|
|
|
Z
|
|
|
|
;
|
|
|
|
# security lattice / information flow
|
|
|
|
Z flows Z
|
|
|
|
P flows P
|
|
|
|
;
|
|
|
|
|
|
|
|
# computation events
|
|
|
|
(pInfo_1:Info) (Z;Z) ['Electric Vehicle'] [P(0)]
|
|
|
|
(pInfo_2:Info) (Z;Z) ['House with Solar Panel'] [P(1)]
|
|
|
|
(pInfo_3:Info) (Z;Z) ['House with Battery'] [P(2)]
|
|
|
|
|
|
|
|
# interaction and input events
|
|
|
|
|
|
|
|
(consume:consume) (Z;Z) [? :{kw:Number, t:String}] [P(0) -> P(1), P(2)]
|
|
|
|
|
|
|
|
(reply_1: replyConsume) (Z;Z) [?: {kw:Number, t:String}] [P(1) -> P(0)]
|
|
|
|
(reply_2: replyConsume) (Z;Z) [?: {kw:Number, t:String}] [P(2) -> P(0)]
|
|
|
|
(accept_1: accept) (Z;Z) [?] [P(0) -> P(1)]
|
|
|
|
(reject_1: reject) (Z;Z) [?] [P(0) -> P(1)]
|
|
|
|
(accept_2: accept) (Z;Z) [?] [P(0) -> P(2)]
|
|
|
|
(reject_2: reject) (Z;Z) [?] [P(0) -> P(2)]
|
|
|
|
;
|
|
|
|
|
|
|
|
# producers can't reply until they receive a request
|
|
|
|
consume -->* reply_1
|
|
|
|
consume -->* reply_2
|
|
|
|
# consumer can't accept or reject until they receive a reply
|
|
|
|
reply_1 -->* reject_1
|
|
|
|
reply_2 -->* reject_2
|
|
|
|
reply_1 -->* accept_1
|
|
|
|
reply_2 -->* accept_2
|
|
|
|
|
|
|
|
# producers can't reply more than once
|
|
|
|
reply_1 -->% reply_1
|
|
|
|
reply_2 -->% reply_2
|
|
|
|
|
|
|
|
# if accept, then cannot reject, and vice-versa
|
|
|
|
accept_1 -->% reject_1
|
|
|
|
reject_1 -->% accept_1
|
|
|
|
accept_2 -->% reject_2
|
|
|
|
reject_2 -->% accept_2
|
|
|
|
|
|
|
|
# accept and reject can only happen once
|
|
|
|
accept_1 -->% accept_1
|
|
|
|
accept_2 -->% accept_2
|
|
|
|
reject_1 -->% reject_1
|
|
|
|
reject_2 -->% reject_2
|
|
|
|
``` |
|
|
\ No newline at end of file |
