| ... | ... | @@ -8,123 +8,3 @@ |
|
|
|
- [References](#references)
|
|
|
|
|
|
|
|
[Prototype](Prototype) |
|
|
|
\ No newline at end of file |
|
|
|
|
|
|
|
# Introduction
|
|
|
|
|
|
|
|
> TODO
|
|
|
|
|
|
|
|
# Examples
|
|
|
|
|
|
|
|
> TODO
|
|
|
|
|
|
|
|
## 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
|
|
|
|
```
|
|
|
|
|
|
|
|
## Watering Plant Robot Management
|
|
|
|
|
|
|
|
> TODO
|
|
|
|
|
|
|
|
```ruby
|
|
|
|
# roles
|
|
|
|
Plant(Number)
|
|
|
|
Robot(Number)
|
|
|
|
Z
|
|
|
|
;
|
|
|
|
# security lattice / information flow
|
|
|
|
Z flows Z
|
|
|
|
Plant flows Plant
|
|
|
|
Robot flows Robot
|
|
|
|
;
|
|
|
|
|
|
|
|
# computation events
|
|
|
|
(pInfo_1:prossumerInfo) (Z;Z) ['Plant 1'] [Plant(1)]
|
|
|
|
(rInfo_1:robotInfo) (Z;Z) ['Robot 1'] [Robot(1)]
|
|
|
|
(rInfo_2:robotInfo) (Z;Z) ['Robot 2'] [Robot(2)]
|
|
|
|
(rInfo_3:robotInfo) (Z;Z) ['Robot 3'] [Robot(3)]
|
|
|
|
|
|
|
|
(request_1:waterRequest) (Z;Z) [?] [Plant(1) -> Robot(1),Robot(2),Robot(3)]
|
|
|
|
(assign_1:waterAssignment) (Z;Z) [?] [Robot(1) -> Plant(1)]
|
|
|
|
(assign_2:waterAssignment) (Z;Z) [?] [Robot(2) -> Plant(1)]
|
|
|
|
(assign_3:waterAssignment) (Z;Z) [?] [Robot(3) -> Plant(1)]
|
|
|
|
|
|
|
|
(accept_1:waterAccept) (Z;Z) [?] [Plant(1) -> Robot(1)]
|
|
|
|
(accept_2:waterAccept) (Z;Z) [?] [Plant(1) -> Robot(2)]
|
|
|
|
(accept_3:waterAccept) (Z;Z) [?] [Plant(1) -> Robot(3)]
|
|
|
|
|
|
|
|
(water_1:water) (Z;Z) [?] [Robot(1) -> Plant(1)]
|
|
|
|
(water_2:water) (Z;Z) [?] [Robot(2) -> Plant(1)]
|
|
|
|
(water_3:water) (Z;Z) [?] [Robot(3) -> Plant(1)]
|
|
|
|
|
|
|
|
;
|
|
|
|
|
|
|
|
request_1 -->* assign_1
|
|
|
|
request_1 -->* assign_2
|
|
|
|
request_1 -->* assign_3
|
|
|
|
|
|
|
|
assign_1 -->* accept_1
|
|
|
|
assign_2 -->* accept_2
|
|
|
|
assign_3 -->* accept_3
|
|
|
|
|
|
|
|
accept_1 -->* water_1
|
|
|
|
accept_2 -->* water_2
|
|
|
|
accept_3 -->* water_3
|
|
|
|
```
|
|
|
|
|
|
|
|
# References
|
|
|
|
|
|
|
|
- [Repository](https://codelab.fct.unl.pt/di/research/tardis/wp3/TaRDIS-DCR/-/tree/demo)
|
|
|
|
- [Video Demo](https://www.youtube.com/watch?v=u8JrlQ1yNbI) |
|
|
\ No newline at end of file |
