DCR-Choreographies/EDP-Use-Case.md

 # Overview
-An Energy Community is a network of local consumers and producers that efficiently share energy resources. In these communities, "prosumers" both produce and consume energy. For instance, homes equipped with solar panels generate energy, while electric vehicles or batteries act as consumers. Using automated systems, prosumers can send energy requests and make offers, optimizing local energy exchange in a decentralized manner. Below, we present an extension of the ReGraDa language to model this use case:
+
+An Energy Community is a network of local consumers and producers that efficiently share energy resources. In these communities, "prosumers" both produce and consume energy. For instance, homes equipped with solar panels generate energy, while electric vehicles or batteries act as consumers. Using automated systems, prosumers can send energy requests and make offers, optimizing local energy exchange in a decentralized manner.
+
+Below, we present an extension of the ReGraDa language to model this use case:
 
 ```ruby
 # roles
@@ -28,6 +31,57 @@ P flows P
 (reject_2: reject) (Z;Z) [?] [P(0) -> P(2)]
 ;
 
+consume -->* reply_1
+consume -->* reply_2
+
+reply_1 -->*  reject_1
+reply_2 -->*  reject_2
+reply_1 -->*  accept_1
+reply_2 -->*  accept_2
+
+reply_1 -->% reply_1
+reply_2 -->% reply_2
+
+accept_1 -->% reject_1
+reject_1 -->% accept_1
+accept_2 -->% reject_2
+reject_2 -->% accept_2
+
+accept_1 -->% accept_1
+accept_2 -->% accept_2
+reject_1 -->% reject_1
+reject_2 -->% reject_2
+```
+
+There is only one role, Prosumer represented as P, and to identify each prosumer, we parameterize the role with an id, _e.g:_ `P(1)`.
+
+> **NOTE**: The roles are defined in the first lines of the process and are used to identify the prosumers in the process. The role `Z` is a dummy role that is used to define the security lattice and information flow of all the events in the process.
+
+---
+
+The process is composed of the following events which represent the information of each prosumer (computation events).
+
+```ruby
+(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)]
+```
+
+To emulate the intended behavior, we execute the `consume` event of `P(0)` which will request energy from `P(1)` and `P(2)`. To respond to the request, we use the events `reply_1` and `reply_2`, sending a message between `P(1)`and`P(2)`to`P(0)`(interaction events).
+
+```ruby
+(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)]
+```
+
+To define the process flow, we use arrows representing relations between events ([doc](DCR%20Choreographies)). These arrows indicate the requirement for either acceptance or rejection of each request.
+
+```ruby
+
 # producers can't reply until they receive a request
 consume -->* reply_1
 consume -->* reply_2