1use super::{
2 Action, Channel, ChannelSystem, Clock, CsError, Location, Message, PgError, PgExpression, PgId,
3 ProgramGraphBuilder, TimeConstraint, Var,
4};
5use crate::grammar::{BooleanExpr, Type};
6use crate::program_graph::ProgramGraph;
7use crate::{Expression, Val};
8use log::info;
9use std::collections::BTreeMap;
10
11pub type CsExpression = Expression<Var>;
13
14pub type CsGuard = BooleanExpr<Var>;
16
17impl From<(PgId, CsExpression)> for PgExpression {
20 fn from((pg_id, expr): (PgId, CsExpression)) -> Self {
21 expr.map(&|cs_var: Var| {
22 assert_eq!(cs_var.0, pg_id);
23 cs_var.1
24 })
25 }
26}
27
28pub struct ChannelSystemBuilder {
30 program_graphs: Vec<ProgramGraphBuilder>,
31 channels: Vec<(Vec<Type>, Option<usize>)>,
32 communications: BTreeMap<Action, Option<(Channel, Message)>>,
33}
34
35impl Default for ChannelSystemBuilder {
36 fn default() -> Self {
37 Self::new()
38 }
39}
40
41impl ChannelSystemBuilder {
42 pub fn new() -> Self {
45 Self {
46 program_graphs: Vec::new(),
47 channels: Vec::new(),
48 communications: BTreeMap::new(),
49 }
50 }
51
52 pub fn new_program_graph(&mut self) -> PgId {
54 let pg_id = PgId(self.program_graphs.len() as u16);
55 let pg = ProgramGraphBuilder::new();
56 self.program_graphs.push(pg);
57 pg_id
58 }
59
60 pub fn new_var(&mut self, pg_id: PgId, val: Val) -> Result<Var, CsError> {
66 let pg = self
67 .program_graphs
68 .get_mut(pg_id.0 as usize)
69 .ok_or(CsError::MissingPg(pg_id))?;
70 let var = pg
71 .new_var(val)
72 .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
73 Ok(Var(pg_id, var))
74 }
75
76 pub fn new_clock(&mut self, pg_id: PgId) -> Result<Clock, CsError> {
82 self.program_graphs
83 .get_mut(pg_id.0 as usize)
84 .ok_or(CsError::MissingPg(pg_id))
85 .map(|pg| Clock(pg_id, pg.new_clock()))
86 }
87
88 pub fn new_action(&mut self, pg_id: PgId) -> Result<Action, CsError> {
94 self.program_graphs
95 .get_mut(pg_id.0 as usize)
96 .ok_or(CsError::MissingPg(pg_id))
97 .map(|pg| Action(pg_id, pg.new_action()))
98 .inspect(|&action| {
99 self.communications.insert(action, None);
100 })
101 }
102
103 pub fn add_reset(&mut self, pg_id: PgId, action: Action, clock: Clock) -> Result<(), CsError> {
110 if action.0 != pg_id {
111 return Err(CsError::ActionNotInPg(action, pg_id));
112 }
113 if clock.0 != pg_id {
114 return Err(CsError::ClockNotInPg(clock, pg_id));
115 }
116 self.program_graphs
117 .get_mut(pg_id.0 as usize)
118 .ok_or(CsError::MissingPg(pg_id))
119 .and_then(|pg| {
120 pg.add_reset(action.1, clock.1)
121 .map_err(|err| CsError::ProgramGraph(pg_id, err))
122 })
123 }
124
125 pub fn add_effect(
162 &mut self,
163 pg_id: PgId,
164 action: Action,
165 var: Var,
166 effect: CsExpression,
167 ) -> Result<(), CsError> {
168 if action.0 != pg_id {
169 Err(CsError::ActionNotInPg(action, pg_id))
170 } else if var.0 != pg_id {
171 Err(CsError::VarNotInPg(var, pg_id))
172 } else if self
173 .communications
174 .get(&action)
175 .ok_or(CsError::ProgramGraph(
176 action.0,
177 PgError::MissingAction(action.1),
178 ))?
179 .is_some()
180 {
181 Err(CsError::ActionIsCommunication(action))
183 } else {
184 let effect = PgExpression::from((pg_id, effect));
185 self.program_graphs
186 .get_mut(pg_id.0 as usize)
187 .ok_or(CsError::MissingPg(pg_id))
188 .and_then(|pg| {
189 pg.add_effect(action.1, var.1, effect)
190 .map_err(|err| CsError::ProgramGraph(pg_id, err))
191 })
192 }
193 }
194
195 pub fn new_location(&mut self, pg_id: PgId) -> Result<Location, CsError> {
201 self.program_graphs
202 .get_mut(pg_id.0 as usize)
203 .ok_or(CsError::MissingPg(pg_id))
204 .map(|pg| Location(pg_id, pg.new_location()))
205 }
206
207 pub fn new_timed_location(
214 &mut self,
215 pg_id: PgId,
216 invariants: &[TimeConstraint],
217 ) -> Result<Location, CsError> {
218 let invariants = invariants
219 .iter()
220 .map(|(c, l, u)| {
221 if c.0 == pg_id {
222 Ok((c.1, *l, *u))
223 } else {
224 Err(CsError::DifferentPgs(pg_id, c.0))
225 }
226 })
227 .collect::<Result<Vec<_>, CsError>>()?;
228 self.program_graphs
229 .get_mut(pg_id.0 as usize)
230 .ok_or(CsError::MissingPg(pg_id))
231 .and_then(|pg| {
232 pg.new_timed_location(invariants)
233 .map(|loc| Location(pg_id, loc))
234 .map_err(|err| CsError::ProgramGraph(pg_id, err))
235 })
236 }
237
238 pub fn new_process(&mut self, pg_id: PgId, location: Location) -> Result<(), CsError> {
244 if location.0 != pg_id {
245 Err(CsError::LocationNotInPg(location, pg_id))
246 } else {
247 self.program_graphs
248 .get_mut(pg_id.0 as usize)
249 .ok_or(CsError::MissingPg(pg_id))
250 .and_then(|pg| {
251 pg.new_process(location.1)
252 .map_err(|err| CsError::ProgramGraph(pg_id, err))
253 })
254 }
255 }
256
257 pub fn new_initial_location(&mut self, pg_id: PgId) -> Result<Location, CsError> {
263 self.new_initial_timed_location(pg_id, &[])
264 }
265
266 pub fn new_initial_timed_location(
273 &mut self,
274 pg_id: PgId,
275 invariants: &[TimeConstraint],
276 ) -> Result<Location, CsError> {
277 let invariants = invariants
278 .iter()
279 .map(|(c, l, u)| {
280 if c.0 == pg_id {
281 Ok((c.1, *l, *u))
282 } else {
283 Err(CsError::DifferentPgs(pg_id, c.0))
284 }
285 })
286 .collect::<Result<Vec<_>, CsError>>()?;
287 self.program_graphs
288 .get_mut(pg_id.0 as usize)
289 .ok_or(CsError::MissingPg(pg_id))
290 .and_then(|pg| {
291 pg.new_initial_timed_location(invariants)
292 .map(|loc| Location(pg_id, loc))
293 .map_err(|err| CsError::ProgramGraph(pg_id, err))
294 })
295 }
296
297 pub fn add_transition(
303 &mut self,
304 pg_id: PgId,
305 pre: Location,
306 action: Action,
307 post: Location,
308 guard: Option<CsGuard>,
309 ) -> Result<(), CsError> {
310 if action.0 != pg_id {
311 Err(CsError::ActionNotInPg(action, pg_id))
312 } else if pre.0 != pg_id {
313 Err(CsError::LocationNotInPg(pre, pg_id))
314 } else if post.0 != pg_id {
315 Err(CsError::LocationNotInPg(post, pg_id))
316 } else {
317 let guard = guard.map(|guard| {
319 guard.map(&|cs_var: Var| {
320 assert_eq!(cs_var.0, pg_id);
321 cs_var.1
322 })
323 });
324 self.program_graphs
325 .get_mut(pg_id.0 as usize)
326 .ok_or(CsError::MissingPg(pg_id))
327 .and_then(|pg| {
328 pg.add_transition(pre.1, action.1, post.1, guard)
329 .map_err(|err| CsError::ProgramGraph(pg_id, err))
330 })
331 }
332 }
333
334 pub fn add_timed_transition(
340 &mut self,
341 pg_id: PgId,
342 pre: Location,
343 action: Action,
344 post: Location,
345 guard: Option<CsGuard>,
346 constraints: &[TimeConstraint],
347 ) -> Result<(), CsError> {
348 if action.0 != pg_id {
349 Err(CsError::ActionNotInPg(action, pg_id))
350 } else if pre.0 != pg_id {
351 Err(CsError::LocationNotInPg(pre, pg_id))
352 } else if post.0 != pg_id {
353 Err(CsError::LocationNotInPg(post, pg_id))
354 } else {
355 let guard = guard.map(|guard| {
357 guard.map(&|cs_var: Var| {
358 assert_eq!(cs_var.0, pg_id);
359 cs_var.1
360 })
361 });
362 let constraints = constraints
363 .iter()
364 .map(|(c, l, u)| {
365 if c.0 == pg_id {
366 Ok((c.1, *l, *u))
367 } else {
368 Err(CsError::DifferentPgs(pg_id, c.0))
369 }
370 })
371 .collect::<Result<Vec<_>, CsError>>()?;
372 self.program_graphs
373 .get_mut(pg_id.0 as usize)
374 .ok_or(CsError::MissingPg(pg_id))
375 .and_then(|pg| {
376 pg.add_timed_transition(pre.1, action.1, post.1, guard, constraints)
377 .map_err(|err| CsError::ProgramGraph(pg_id, err))
378 })
379 }
380 }
381
382 pub fn add_autonomous_transition(
388 &mut self,
389 pg_id: PgId,
390 pre: Location,
391 post: Location,
392 guard: Option<CsGuard>,
393 ) -> Result<(), CsError> {
394 if pre.0 != pg_id {
395 Err(CsError::LocationNotInPg(pre, pg_id))
396 } else if post.0 != pg_id {
397 Err(CsError::LocationNotInPg(post, pg_id))
398 } else {
399 let guard = guard.map(|guard| {
401 guard.map(&|cs_var: Var| {
402 assert_eq!(cs_var.0, pg_id);
403 cs_var.1
404 })
405 });
406 self.program_graphs
407 .get_mut(pg_id.0 as usize)
408 .ok_or(CsError::MissingPg(pg_id))
409 .and_then(|pg| {
410 pg.add_autonomous_transition(pre.1, post.1, guard)
411 .map_err(|err| CsError::ProgramGraph(pg_id, err))
412 })
413 }
414 }
415
416 pub fn add_autonomous_timed_transition(
422 &mut self,
423 pg_id: PgId,
424 pre: Location,
425 post: Location,
426 guard: Option<CsGuard>,
427 constraints: &[TimeConstraint],
428 ) -> Result<(), CsError> {
429 if pre.0 != pg_id {
430 Err(CsError::LocationNotInPg(pre, pg_id))
431 } else if post.0 != pg_id {
432 Err(CsError::LocationNotInPg(post, pg_id))
433 } else {
434 let guard = guard.map(|guard| {
436 guard.map(&|cs_var: Var| {
437 assert_eq!(cs_var.0, pg_id);
438 cs_var.1
439 })
440 });
441 let constraints = constraints
442 .iter()
443 .map(|(c, l, u)| {
444 if c.0 == pg_id {
445 Ok((c.1, *l, *u))
446 } else {
447 Err(CsError::DifferentPgs(pg_id, c.0))
448 }
449 })
450 .collect::<Result<Vec<_>, CsError>>()?;
451 self.program_graphs
452 .get_mut(pg_id.0 as usize)
453 .ok_or(CsError::MissingPg(pg_id))
454 .and_then(|pg| {
455 pg.add_autonomous_timed_transition(pre.1, post.1, guard, constraints)
456 .map_err(|err| CsError::ProgramGraph(pg_id, err))
457 })
458 }
459 }
460
461 pub fn new_channel(&mut self, var_types: Vec<Type>, capacity: Option<usize>) -> Channel {
466 let channel = Channel(self.channels.len() as u16);
467 self.channels.push((var_types, capacity));
468 channel
469 }
470
471 pub fn new_send(
475 &mut self,
476 pg_id: PgId,
477 channel: Channel,
478 msgs: Vec<CsExpression>,
479 ) -> Result<Action, CsError> {
480 let channel_type = self
481 .channels
482 .get(channel.0 as usize)
483 .ok_or(CsError::MissingChannel(channel))?
484 .0
485 .to_owned();
486 let message_type = msgs.iter().map(|msg| msg.r#type()).collect::<Vec<_>>();
487 let msg = msgs
488 .into_iter()
489 .map(|msg| PgExpression::from((pg_id, msg)))
490 .collect::<Vec<_>>();
491 if channel_type != message_type {
492 Err(CsError::ProgramGraph(pg_id, PgError::TypeMismatch))
493 } else {
494 let action = self.program_graphs[pg_id.0 as usize]
495 .new_send(msg)
496 .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
497 let action = Action(pg_id, action);
498 self.communications
499 .insert(action, Some((channel, Message::Send)));
500 Ok(action)
501 }
502 }
503
504 pub fn new_receive(
508 &mut self,
509 pg_id: PgId,
510 channel: Channel,
511 vars: Vec<Var>,
512 ) -> Result<Action, CsError> {
513 if let Some(var) = vars.iter().find(|var| pg_id != var.0) {
514 Err(CsError::VarNotInPg(*var, pg_id))
515 } else {
516 let channel_type = self
517 .channels
518 .get(channel.0 as usize)
519 .ok_or(CsError::MissingChannel(channel))?
520 .0
521 .to_owned();
522 let pg = self
523 .program_graphs
524 .get(pg_id.0 as usize)
525 .ok_or(CsError::MissingPg(pg_id))?;
526 let message_type = vars
527 .iter()
528 .map(|var| pg.var_type(var.1))
529 .collect::<Result<Vec<_>, _>>()
530 .map_err(|err| CsError::ProgramGraph(pg_id, err))?
531 .to_owned();
532 if channel_type != message_type {
533 Err(CsError::ProgramGraph(pg_id, PgError::TypeMismatch))
534 } else {
535 let action = self.program_graphs[pg_id.0 as usize]
536 .new_receive(vars.iter().map(|var| var.1).collect())
537 .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
538 let action = Action(pg_id, action);
539 self.communications
540 .insert(action, Some((channel, Message::Receive)));
541 Ok(action)
542 }
543 }
544 }
545
546 pub fn new_probe_empty_queue(
550 &mut self,
551 pg_id: PgId,
552 channel: Channel,
553 ) -> Result<Action, CsError> {
554 let (_, cap) = self
555 .channels
556 .get(channel.0 as usize)
557 .ok_or(CsError::MissingChannel(channel))?;
558 if matches!(cap, Some(0)) {
559 Err(CsError::ProbingHandshakeChannel(channel))
561 } else {
562 let action = self
563 .program_graphs
564 .get_mut(pg_id.0 as usize)
565 .ok_or(CsError::MissingPg(pg_id))?
566 .new_send(Vec::new())
568 .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
569 let action = Action(pg_id, action);
570 self.communications
571 .insert(action, Some((channel, Message::ProbeEmptyQueue)));
572 Ok(action)
573 }
574 }
575
576 pub fn new_probe_full_queue(
580 &mut self,
581 pg_id: PgId,
582 channel: Channel,
583 ) -> Result<Action, CsError> {
584 let (_, cap) = self
585 .channels
586 .get(channel.0 as usize)
587 .ok_or(CsError::MissingChannel(channel))?;
588 if matches!(cap, Some(0)) {
589 Err(CsError::ProbingHandshakeChannel(channel))
591 } else if cap.is_none() {
592 Err(CsError::ProbingInfiniteQueue(channel))
594 } else {
595 let action = self
596 .program_graphs
597 .get_mut(pg_id.0 as usize)
598 .ok_or(CsError::MissingPg(pg_id))?
599 .new_send(Vec::new())
601 .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
602 let action = Action(pg_id, action);
603 self.communications
604 .insert(action, Some((channel, Message::ProbeFullQueue)));
605 Ok(action)
606 }
607 }
608
609 pub fn build(mut self) -> ChannelSystem {
611 info!(
612 "create Channel System with:\n{} Program Graphs\n{} channels",
613 self.program_graphs.len(),
614 self.channels.len(),
615 );
616 let mut program_graphs: Vec<ProgramGraph> = self
617 .program_graphs
618 .into_iter()
619 .map(|builder| builder.build())
620 .collect();
621
622 program_graphs.shrink_to_fit();
623 self.channels.shrink_to_fit();
624 let communications_map = Vec::from_iter(self.communications);
625 let communications = Vec::from_iter(communications_map.iter().map(|&(_, comm)| comm));
626 let mut index = 0;
627 let mut communications_pg_idxs = Vec::<usize>::with_capacity(program_graphs.len() + 1);
628 communications_pg_idxs.push(index);
629 for pg_id in (0..program_graphs.len() as u16).map(PgId) {
630 index = communications_map[index..]
631 .iter()
632 .position(|(a, ..)| a.0.0 > pg_id.0)
633 .map_or(communications_map.len(), |pos| pos + index);
634 communications_pg_idxs.push(index);
635 }
636
637 assert_eq!(communications_pg_idxs.len(), program_graphs.len() + 1);
638
639 ChannelSystem {
640 channels: self.channels,
641 communications,
642 communications_pg_idxs,
643 program_graphs,
644 }
645 }
646}